ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Functions
fxuPair.c File Reference
#include "fxuInt.h"
Include dependency graph for fxuPair.c:

Go to the source code of this file.

Macros

#define MAX_PRIMES   304
 DECLARATIONS ///.
 

Functions

void Fxu_PairCanonicize (Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
 FUNCTION DEFINITIONS ///.
 
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_Pair * Fxu_PairAlloc (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
 
void Fxu_PairAdd (Fxu_Pair *pPair)
 

Macro Definition Documentation

◆ MAX_PRIMES

#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

◆ Fxu_PairAdd()

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}
Fxu_Var
struct FxuVar Fxu_Var
Definition fxuInt.h:67
FxuCube::pVar
Fxu_Var * pVar
Definition fxuInt.h:205
FxuPair::iCube1
int iCube1
Definition fxuInt.h:247
FxuPair::pCube1
Fxu_Cube * pCube1
Definition fxuInt.h:245
FxuPair::iCube2
int iCube2
Definition fxuInt.h:248
FxuPair::pCube2
Fxu_Cube * pCube2
Definition fxuInt.h:246
FxuVar::ppPairs
Fxu_Pair *** ppPairs
Definition fxuInt.h:218
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Fxu_PairAlloc()

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}
p
Cube * p
Definition exorList.c:222
MEM_ALLOC_FXU
#define MEM_ALLOC_FXU(Manager, Type, Size)
Definition fxuInt.h:429
Fxu_Pair
struct FxuPair Fxu_Pair
Definition fxuInt.h:71
FxuCube::iCube
int iCube
Definition fxuInt.h:203
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_PairAllocStorage()

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}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
FxuVar::nCubes
int nCubes
Definition fxuInt.h:216
Here is the call graph for this function:

◆ Fxu_PairCanonicize()

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_Cube
struct FxuCube Fxu_Cube
Definition fxuInt.h:66
Fxu_Lit
struct FxuLit Fxu_Lit
Definition fxuInt.h:68
FxuLit::pHNext
Fxu_Lit * pHNext
Definition fxuInt.h:233
FxuLit::iVar
int iVar
Definition fxuInt.h:228
Here is the caller graph for this function:

◆ Fxu_PairCanonicize2()

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}

◆ Fxu_PairClearStorage()

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}

◆ Fxu_PairCompare()

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}
Code
#define Code
Definition deflate.h:76
Fxu_Min
#define Fxu_Min(a, b)
MACRO DEFINITIONS ///.
Definition fxuInt.h:283
FxuCube::lLits
Fxu_ListLit lLits
Definition fxuInt.h:206
FxuListLit::pHead
Fxu_Lit * pHead
Definition fxuInt.h:109
FxuPair::nLits2
int nLits2
Definition fxuInt.h:242
FxuPair::nLits1
int nLits1
Definition fxuInt.h:241
Here is the caller graph for this function:

◆ Fxu_PairFreeStorage()

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}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267

◆ Fxu_PairHashKey()

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}
Here is the caller graph for this function:

◆ Fxu_PairHashKeyArray()

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}
Here is the caller graph for this function: