abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fxuPair.c File Reference
#include "fxuInt.h"

Go to the source code of this file.

Macros

#define MAX_PRIMES   304
 DECLARATIONS ///. More...
 

Functions

void Fxu_PairCanonicize (Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
 FUNCTION DEFINITIONS ///. More...
 
void Fxu_PairCanonicize2 (Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
 
unsigned Fxu_PairHashKeyArray (Fxu_Matrix *p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2)
 
unsigned Fxu_PairHashKey (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2, int *pnBase, int *pnLits1, int *pnLits2)
 
int Fxu_PairCompare (Fxu_Pair *pPair1, Fxu_Pair *pPair2)
 
void Fxu_PairAllocStorage (Fxu_Var *pVar, int nCubes)
 
void Fxu_PairClearStorage (Fxu_Cube *pCube)
 
void Fxu_PairFreeStorage (Fxu_Var *pVar)
 
Fxu_PairFxu_PairAlloc (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
 
void Fxu_PairAdd (Fxu_Pair *pPair)
 

Variables

static int s_Primes [MAX_PRIMES]
 

Macro Definition Documentation

#define MAX_PRIMES   304

DECLARATIONS ///.

CFile****************************************************************

FileName [fxuPair.c]

PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

Synopsis [Operations on cube pairs.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - February 1, 2003.]

Revision [

Id:
fxuPair.c,v 1.0 2003/02/01 00:00:00 alanmi Exp

]

Definition at line 28 of file fxuPair.c.

Function Documentation

void Fxu_PairAdd ( Fxu_Pair pPair)

Function*************************************************************

Synopsis [Adds the pair to storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 543 of file fxuPair.c.

544 {
545  Fxu_Var * pVar;
546 
547  pVar = pPair->pCube1->pVar;
548  assert( pVar == pPair->pCube2->pVar );
549 
550  pVar->ppPairs[pPair->iCube1][pPair->iCube2] = pPair;
551  pVar->ppPairs[pPair->iCube2][pPair->iCube1] = pPair;
552 }
Definition: fxuInt.h:213
int iCube1
Definition: fxuInt.h:247
Fxu_Cube * pCube1
Definition: fxuInt.h:245
Fxu_Var * pVar
Definition: fxuInt.h:205
Fxu_Cube * pCube2
Definition: fxuInt.h:246
Fxu_Pair *** ppPairs
Definition: fxuInt.h:218
#define assert(ex)
Definition: util_old.h:213
int iCube2
Definition: fxuInt.h:248
Fxu_Pair* Fxu_PairAlloc ( Fxu_Matrix p,
Fxu_Cube pCube1,
Fxu_Cube pCube2 
)

Function*************************************************************

Synopsis [Adds the pair to storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 519 of file fxuPair.c.

520 {
521  Fxu_Pair * pPair;
522  assert( pCube1->pVar == pCube2->pVar );
523  pPair = MEM_ALLOC_FXU( p, Fxu_Pair, 1 );
524  memset( pPair, 0, sizeof(Fxu_Pair) );
525  pPair->pCube1 = pCube1;
526  pPair->pCube2 = pCube2;
527  pPair->iCube1 = pCube1->iCube;
528  pPair->iCube2 = pCube2->iCube;
529  return pPair;
530 }
char * memset()
int iCube
Definition: fxuInt.h:203
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int iCube1
Definition: fxuInt.h:247
#define MEM_ALLOC_FXU(Manager, Type, Size)
Definition: fxuInt.h:429
Fxu_Cube * pCube1
Definition: fxuInt.h:245
Fxu_Var * pVar
Definition: fxuInt.h:205
Fxu_Cube * pCube2
Definition: fxuInt.h:246
#define assert(ex)
Definition: util_old.h:213
int iCube2
Definition: fxuInt.h:248
void Fxu_PairAllocStorage ( Fxu_Var pVar,
int  nCubes 
)

Function*************************************************************

Synopsis [Allocates the storage for cubes pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file fxuPair.c.

453 {
454  int k;
455 // assert( pVar->nCubes == 0 );
456  pVar->nCubes = nCubes;
457  // allocate memory for all the pairs
458  pVar->ppPairs = ABC_ALLOC( Fxu_Pair **, nCubes );
459  pVar->ppPairs[0] = ABC_ALLOC( Fxu_Pair *, nCubes * nCubes );
460  memset( pVar->ppPairs[0], 0, sizeof(Fxu_Pair *) * nCubes * nCubes );
461  for ( k = 1; k < nCubes; k++ )
462  pVar->ppPairs[k] = pVar->ppPairs[k-1] + nCubes;
463 }
char * memset()
int nCubes
Definition: fxuInt.h:216
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Fxu_Pair *** ppPairs
Definition: fxuInt.h:218
void Fxu_PairCanonicize ( Fxu_Cube **  ppCube1,
Fxu_Cube **  ppCube2 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Find the canonical permutation of two cubes in the pair.]

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file fxuPair.c.

76 {
77  Fxu_Lit * pLit1, * pLit2;
78  Fxu_Cube * pCubeTemp;
79 
80  // walk through the cubes to determine
81  // the one that has higher first variable
82  pLit1 = (*ppCube1)->lLits.pHead;
83  pLit2 = (*ppCube2)->lLits.pHead;
84  while ( 1 )
85  {
86  if ( pLit1->iVar == pLit2->iVar )
87  {
88  pLit1 = pLit1->pHNext;
89  pLit2 = pLit2->pHNext;
90  continue;
91  }
92  assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free
93  if ( pLit1->iVar > pLit2->iVar )
94  { // swap the cubes
95  pCubeTemp = *ppCube1;
96  *ppCube1 = *ppCube2;
97  *ppCube2 = pCubeTemp;
98  }
99  break;
100  }
101 }
Fxu_Lit * pHNext
Definition: fxuInt.h:233
int iVar
Definition: fxuInt.h:228
#define assert(ex)
Definition: util_old.h:213
Definition: fxuInt.h:226
void Fxu_PairCanonicize2 ( Fxu_Cube **  ppCube1,
Fxu_Cube **  ppCube2 
)

Function*************************************************************

Synopsis [Find the canonical permutation of two cubes in the pair.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file fxuPair.c.

115 {
116  Fxu_Cube * pCubeTemp;
117  // canonicize the pair by ordering the cubes
118  if ( (*ppCube1)->iCube > (*ppCube2)->iCube )
119  { // swap the cubes
120  pCubeTemp = *ppCube1;
121  *ppCube1 = *ppCube2;
122  *ppCube2 = pCubeTemp;
123  }
124 }
void Fxu_PairClearStorage ( Fxu_Cube pCube)

Function*************************************************************

Synopsis [Clears all pairs associated with this cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 476 of file fxuPair.c.

477 {
478  Fxu_Var * pVar;
479  int i;
480  pVar = pCube->pVar;
481  for ( i = 0; i < pVar->nCubes; i++ )
482  {
483  pVar->ppPairs[pCube->iCube][i] = NULL;
484  pVar->ppPairs[i][pCube->iCube] = NULL;
485  }
486 }
int nCubes
Definition: fxuInt.h:216
Definition: fxuInt.h:213
int iCube
Definition: fxuInt.h:203
Fxu_Var * pVar
Definition: fxuInt.h:205
Fxu_Pair *** ppPairs
Definition: fxuInt.h:218
int Fxu_PairCompare ( Fxu_Pair pPair1,
Fxu_Pair pPair2 
)

Function*************************************************************

Synopsis [Compares the two pairs.]

Description [Returns 1 if the divisors represented by these pairs are equal.]

SideEffects []

SeeAlso []

Definition at line 236 of file fxuPair.c.

237 {
238  Fxu_Lit * pD1C1, * pD1C2;
239  Fxu_Lit * pD2C1, * pD2C2;
240  int TopVar1, TopVar2;
241  int Code;
242 
243  if ( pPair1->nLits1 != pPair2->nLits1 )
244  return 0;
245  if ( pPair1->nLits2 != pPair2->nLits2 )
246  return 0;
247 
248  pD1C1 = pPair1->pCube1->lLits.pHead;
249  pD1C2 = pPair1->pCube2->lLits.pHead;
250 
251  pD2C1 = pPair2->pCube1->lLits.pHead;
252  pD2C2 = pPair2->pCube2->lLits.pHead;
253 
254  Code = pD1C1? 8: 0;
255  Code |= pD1C2? 4: 0;
256  Code |= pD2C1? 2: 0;
257  Code |= pD2C2? 1: 0;
258  assert( Code == 15 );
259 
260  while ( 1 )
261  {
262  switch ( Code )
263  {
264  case 0: // -- -- NULL NULL NULL NULL
265  return 1;
266  case 1: // -- -1 NULL NULL NULL pD2C2
267  return 0;
268  case 2: // -- 1- NULL NULL pD2C1 NULL
269  return 0;
270  case 3: // -- 11 NULL NULL pD2C1 pD2C2
271  if ( pD2C1->iVar != pD2C2->iVar )
272  return 0;
273  pD2C1 = pD2C1->pHNext;
274  pD2C2 = pD2C2->pHNext;
275  break;
276  case 4: // -1 -- NULL pD1C2 NULL NULL
277  return 0;
278  case 5: // -1 -1 NULL pD1C2 NULL pD2C2
279  if ( pD1C2->iVar != pD2C2->iVar )
280  return 0;
281  pD1C2 = pD1C2->pHNext;
282  pD2C2 = pD2C2->pHNext;
283  break;
284  case 6: // -1 1- NULL pD1C2 pD2C1 NULL
285  return 0;
286  case 7: // -1 11 NULL pD1C2 pD2C1 pD2C2
287  TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
288  if ( TopVar2 == pD1C2->iVar )
289  {
290  if ( pD2C1->iVar <= pD2C2->iVar )
291  return 0;
292  pD1C2 = pD1C2->pHNext;
293  pD2C2 = pD2C2->pHNext;
294  }
295  else if ( TopVar2 < pD1C2->iVar )
296  {
297  if ( pD2C1->iVar != pD2C2->iVar )
298  return 0;
299  pD2C1 = pD2C1->pHNext;
300  pD2C2 = pD2C2->pHNext;
301  }
302  else
303  return 0;
304  break;
305  case 8: // 1- -- pD1C1 NULL NULL NULL
306  return 0;
307  case 9: // 1- -1 pD1C1 NULL NULL pD2C2
308  return 0;
309  case 10: // 1- 1- pD1C1 NULL pD2C1 NULL
310  if ( pD1C1->iVar != pD2C1->iVar )
311  return 0;
312  pD1C1 = pD1C1->pHNext;
313  pD2C1 = pD2C1->pHNext;
314  break;
315  case 11: // 1- 11 pD1C1 NULL pD2C1 pD2C2
316  TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
317  if ( TopVar2 == pD1C1->iVar )
318  {
319  if ( pD2C1->iVar >= pD2C2->iVar )
320  return 0;
321  pD1C1 = pD1C1->pHNext;
322  pD2C1 = pD2C1->pHNext;
323  }
324  else if ( TopVar2 < pD1C1->iVar )
325  {
326  if ( pD2C1->iVar != pD2C2->iVar )
327  return 0;
328  pD2C1 = pD2C1->pHNext;
329  pD2C2 = pD2C2->pHNext;
330  }
331  else
332  return 0;
333  break;
334  case 12: // 11 -- pD1C1 pD1C2 NULL NULL
335  if ( pD1C1->iVar != pD1C2->iVar )
336  return 0;
337  pD1C1 = pD1C1->pHNext;
338  pD1C2 = pD1C2->pHNext;
339  break;
340  case 13: // 11 -1 pD1C1 pD1C2 NULL pD2C2
341  TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
342  if ( TopVar1 == pD2C2->iVar )
343  {
344  if ( pD1C1->iVar <= pD1C2->iVar )
345  return 0;
346  pD1C2 = pD1C2->pHNext;
347  pD2C2 = pD2C2->pHNext;
348  }
349  else if ( TopVar1 < pD2C2->iVar )
350  {
351  if ( pD1C1->iVar != pD1C2->iVar )
352  return 0;
353  pD1C1 = pD1C1->pHNext;
354  pD1C2 = pD1C2->pHNext;
355  }
356  else
357  return 0;
358  break;
359  case 14: // 11 1- pD1C1 pD1C2 pD2C1 NULL
360  TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
361  if ( TopVar1 == pD2C1->iVar )
362  {
363  if ( pD1C1->iVar >= pD1C2->iVar )
364  return 0;
365  pD1C1 = pD1C1->pHNext;
366  pD2C1 = pD2C1->pHNext;
367  }
368  else if ( TopVar1 < pD2C1->iVar )
369  {
370  if ( pD1C1->iVar != pD1C2->iVar )
371  return 0;
372  pD1C1 = pD1C1->pHNext;
373  pD1C2 = pD1C2->pHNext;
374  }
375  else
376  return 0;
377  break;
378  case 15: // 11 11 pD1C1 pD1C2 pD2C1 pD2C2
379  TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
380  TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
381  if ( TopVar1 == TopVar2 )
382  {
383  if ( pD1C1->iVar == pD1C2->iVar )
384  {
385  if ( pD2C1->iVar != pD2C2->iVar )
386  return 0;
387  pD1C1 = pD1C1->pHNext;
388  pD1C2 = pD1C2->pHNext;
389  pD2C1 = pD2C1->pHNext;
390  pD2C2 = pD2C2->pHNext;
391  }
392  else
393  {
394  if ( pD2C1->iVar == pD2C2->iVar )
395  return 0;
396  if ( pD1C1->iVar < pD1C2->iVar )
397  {
398  if ( pD2C1->iVar > pD2C2->iVar )
399  return 0;
400  pD1C1 = pD1C1->pHNext;
401  pD2C1 = pD2C1->pHNext;
402  }
403  else
404  {
405  if ( pD2C1->iVar < pD2C2->iVar )
406  return 0;
407  pD1C2 = pD1C2->pHNext;
408  pD2C2 = pD2C2->pHNext;
409  }
410  }
411  }
412  else if ( TopVar1 < TopVar2 )
413  {
414  if ( pD1C1->iVar != pD1C2->iVar )
415  return 0;
416  pD1C1 = pD1C1->pHNext;
417  pD1C2 = pD1C2->pHNext;
418  }
419  else
420  {
421  if ( pD2C1->iVar != pD2C2->iVar )
422  return 0;
423  pD2C1 = pD2C1->pHNext;
424  pD2C2 = pD2C2->pHNext;
425  }
426  break;
427  default:
428  assert( 0 );
429  break;
430  }
431 
432  Code = pD1C1? 8: 0;
433  Code |= pD1C2? 4: 0;
434  Code |= pD2C1? 2: 0;
435  Code |= pD2C2? 1: 0;
436  }
437  return 1;
438 }
Fxu_Lit * pHead
Definition: fxuInt.h:109
Fxu_Lit * pHNext
Definition: fxuInt.h:233
Fxu_Cube * pCube1
Definition: fxuInt.h:245
#define Code
Definition: deflate.h:76
Fxu_ListLit lLits
Definition: fxuInt.h:206
int nLits2
Definition: fxuInt.h:242
int iVar
Definition: fxuInt.h:228
Fxu_Cube * pCube2
Definition: fxuInt.h:246
#define Fxu_Min(a, b)
MACRO DEFINITIONS ///.
Definition: fxuInt.h:283
#define assert(ex)
Definition: util_old.h:213
int nLits1
Definition: fxuInt.h:241
Definition: fxuInt.h:226
void Fxu_PairFreeStorage ( Fxu_Var pVar)

Function*************************************************************

Synopsis [Clears all pairs associated with this cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file fxuPair.c.

500 {
501  if ( pVar->ppPairs )
502  {
503  ABC_FREE( pVar->ppPairs[0] );
504  ABC_FREE( pVar->ppPairs );
505  }
506 }
#define ABC_FREE(obj)
Definition: abc_global.h:232
Fxu_Pair *** ppPairs
Definition: fxuInt.h:218
unsigned Fxu_PairHashKey ( Fxu_Matrix p,
Fxu_Cube pCube1,
Fxu_Cube pCube2,
int *  pnBase,
int *  pnLits1,
int *  pnLits2 
)

Function*************************************************************

Synopsis [Computes the hash key of the divisor represented by the pair of cubes.]

Description [Goes through the variables in both cubes. Skips the identical ones (this corresponds to making the cubes cube-free). Computes the hash value of the cubes. Assigns the number of literals in the base and in the cubes without base.]

SideEffects []

SeeAlso []

Definition at line 164 of file fxuPair.c.

166 {
167  int Offset1 = 100, Offset2 = 200;
168  int nBase, nLits1, nLits2;
169  Fxu_Lit * pLit1, * pLit2;
170  unsigned Key;
171 
172  // compute the hash key
173  Key = 0;
174  nLits1 = 0;
175  nLits2 = 0;
176  nBase = 0;
177  pLit1 = pCube1->lLits.pHead;
178  pLit2 = pCube2->lLits.pHead;
179  while ( 1 )
180  {
181  if ( pLit1 && pLit2 )
182  {
183  if ( pLit1->iVar == pLit2->iVar )
184  { // ensure cube-free
185  pLit1 = pLit1->pHNext;
186  pLit2 = pLit2->pHNext;
187  // add this literal to the base
188  nBase++;
189  }
190  else if ( pLit1->iVar < pLit2->iVar )
191  {
192  Key ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
193  pLit1 = pLit1->pHNext;
194  nLits1++;
195  }
196  else
197  {
198  Key ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
199  pLit2 = pLit2->pHNext;
200  nLits2++;
201  }
202  }
203  else if ( pLit1 && !pLit2 )
204  {
205  Key ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
206  pLit1 = pLit1->pHNext;
207  nLits1++;
208  }
209  else if ( !pLit1 && pLit2 )
210  {
211  Key ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
212  pLit2 = pLit2->pHNext;
213  nLits2++;
214  }
215  else
216  break;
217  }
218  *pnBase = nBase;
219  *pnLits1 = nLits1;
220  *pnLits2 = nLits2;
221  return Key;
222 }
Fxu_Lit * pHead
Definition: fxuInt.h:109
Fxu_Lit * pHNext
Definition: fxuInt.h:233
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Fxu_ListLit lLits
Definition: fxuInt.h:206
int iVar
Definition: fxuInt.h:228
Definition: fxuInt.h:226
unsigned Fxu_PairHashKeyArray ( Fxu_Matrix p,
int  piVarsC1[],
int  piVarsC2[],
int  nVarsC1,
int  nVarsC2 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file fxuPair.c.

138 {
139  int Offset1 = 100, Offset2 = 200, i;
140  unsigned Key;
141  // compute the hash key
142  Key = 0;
143  for ( i = 0; i < nVarsC1; i++ )
144  Key ^= s_Primes[Offset1+i] * piVarsC1[i];
145  for ( i = 0; i < nVarsC2; i++ )
146  Key ^= s_Primes[Offset2+i] * piVarsC2[i];
147  return Key;
148 }
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30

Variable Documentation

int s_Primes[MAX_PRIMES]
static
Initial value:
=
{
2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37,
41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89,
97, 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151,
157, 163, 167, 173, 179, 181, 191, 193, 197, 199, 211, 223,
227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281,
283, 293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359,
367, 373, 379, 383, 389, 397, 401, 409, 419, 421, 431, 433,
439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503,
509, 521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593,
599, 601, 607, 613, 617, 619, 631, 641, 643, 647, 653, 659,
661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743,
751, 757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827,
829, 839, 853, 857, 859, 863, 877, 881, 883, 887, 907, 911,
919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997,
1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069,
1087, 1091, 1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163,
1171, 1181, 1187, 1193, 1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249,
1259, 1277, 1279, 1283, 1289, 1291, 1297, 1301, 1303, 1307, 1319, 1321,
1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, 1427, 1429, 1433, 1439,
1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, 1499, 1511,
1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601,
1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693,
1697, 1699, 1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783,
1787, 1789, 1801, 1811, 1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877,
1879, 1889, 1901, 1907, 1913, 1931, 1933, 1949, 1951, 1973, 1979, 1987,
1993, 1997, 1999, 2003
}

Definition at line 30 of file fxuPair.c.