ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fxuPair.c
Go to the documentation of this file.
1
18
19#include "fxuInt.h"
20
21ABC_NAMESPACE_IMPL_START
22
23
27
28#define MAX_PRIMES 304
29
30static int s_Primes[MAX_PRIMES] =
31{
32 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37,
33 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89,
34 97, 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151,
35 157, 163, 167, 173, 179, 181, 191, 193, 197, 199, 211, 223,
36 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281,
37 283, 293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359,
38 367, 373, 379, 383, 389, 397, 401, 409, 419, 421, 431, 433,
39 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503,
40 509, 521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593,
41 599, 601, 607, 613, 617, 619, 631, 641, 643, 647, 653, 659,
42 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743,
43 751, 757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827,
44 829, 839, 853, 857, 859, 863, 877, 881, 883, 887, 907, 911,
45 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997,
46 1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069,
47 1087, 1091, 1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163,
48 1171, 1181, 1187, 1193, 1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249,
49 1259, 1277, 1279, 1283, 1289, 1291, 1297, 1301, 1303, 1307, 1319, 1321,
50 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, 1427, 1429, 1433, 1439,
51 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, 1499, 1511,
52 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601,
53 1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693,
54 1697, 1699, 1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783,
55 1787, 1789, 1801, 1811, 1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877,
56 1879, 1889, 1901, 1907, 1913, 1931, 1933, 1949, 1951, 1973, 1979, 1987,
57 1993, 1997, 1999, 2003
58};
59
63
75void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
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}
102
114void Fxu_PairCanonicize2( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
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}
125
137unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 )
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}
149
164unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2,
165 int * pnBase, int * pnLits1, int * pnLits2 )
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}
223
236int Fxu_PairCompare( Fxu_Pair * pPair1, Fxu_Pair * pPair2 )
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}
439
440
452void Fxu_PairAllocStorage( Fxu_Var * pVar, int nCubes )
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}
464
476void Fxu_PairClearStorage( Fxu_Cube * pCube )
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}
487
499void Fxu_PairFreeStorage( Fxu_Var * pVar )
500{
501 if ( pVar->ppPairs )
502 {
503 ABC_FREE( pVar->ppPairs[0] );
504 ABC_FREE( pVar->ppPairs );
505 }
506}
507
519Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 )
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}
531
543void Fxu_PairAdd( Fxu_Pair * pPair )
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}
553
557
558
559ABC_NAMESPACE_IMPL_END
560
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Code
#define Code
Definition deflate.h:76
p
Cube * p
Definition exorList.c:222
MEM_ALLOC_FXU
#define MEM_ALLOC_FXU(Manager, Type, Size)
Definition fxuInt.h:429
Fxu_Var
struct FxuVar Fxu_Var
Definition fxuInt.h:67
Fxu_Matrix
typedefABC_NAMESPACE_HEADER_START struct FxuMatrix Fxu_Matrix
INCLUDES ///.
Definition fxuInt.h:63
Fxu_Min
#define Fxu_Min(a, b)
MACRO DEFINITIONS ///.
Definition fxuInt.h:283
Fxu_Pair
struct FxuPair Fxu_Pair
Definition fxuInt.h:71
Fxu_Cube
struct FxuCube Fxu_Cube
Definition fxuInt.h:66
Fxu_Lit
struct FxuLit Fxu_Lit
Definition fxuInt.h:68
Fxu_PairCanonicize2
void Fxu_PairCanonicize2(Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
Definition fxuPair.c:114
Fxu_PairHashKeyArray
unsigned Fxu_PairHashKeyArray(Fxu_Matrix *p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2)
Definition fxuPair.c:137
Fxu_PairClearStorage
void Fxu_PairClearStorage(Fxu_Cube *pCube)
Definition fxuPair.c:476
Fxu_PairFreeStorage
void Fxu_PairFreeStorage(Fxu_Var *pVar)
Definition fxuPair.c:499
Fxu_PairAlloc
Fxu_Pair * Fxu_PairAlloc(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
Definition fxuPair.c:519
Fxu_PairCompare
int Fxu_PairCompare(Fxu_Pair *pPair1, Fxu_Pair *pPair2)
Definition fxuPair.c:236
Fxu_PairHashKey
unsigned Fxu_PairHashKey(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2, int *pnBase, int *pnLits1, int *pnLits2)
Definition fxuPair.c:164
Fxu_PairAllocStorage
void Fxu_PairAllocStorage(Fxu_Var *pVar, int nCubes)
Definition fxuPair.c:452
Fxu_PairAdd
void Fxu_PairAdd(Fxu_Pair *pPair)
Definition fxuPair.c:543
MAX_PRIMES
#define MAX_PRIMES
DECLARATIONS ///.
Definition fxuPair.c:28
Fxu_PairCanonicize
void Fxu_PairCanonicize(Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
FUNCTION DEFINITIONS ///.
Definition fxuPair.c:75
FxuCube::iCube
int iCube
Definition fxuInt.h:203
FxuCube::lLits
Fxu_ListLit lLits
Definition fxuInt.h:206
FxuCube::pVar
Fxu_Var * pVar
Definition fxuInt.h:205
FxuListLit::pHead
Fxu_Lit * pHead
Definition fxuInt.h:109
FxuLit::pHNext
Fxu_Lit * pHNext
Definition fxuInt.h:233
FxuLit::iVar
int iVar
Definition fxuInt.h:228
FxuPair::iCube1
int iCube1
Definition fxuInt.h:247
FxuPair::nLits2
int nLits2
Definition fxuInt.h:242
FxuPair::pCube1
Fxu_Cube * pCube1
Definition fxuInt.h:245
FxuPair::nLits1
int nLits1
Definition fxuInt.h:241
FxuPair::iCube2
int iCube2
Definition fxuInt.h:248
FxuPair::pCube2
Fxu_Cube * pCube2
Definition fxuInt.h:246
FxuVar::nCubes
int nCubes
Definition fxuInt.h:216
FxuVar::ppPairs
Fxu_Pair *** ppPairs
Definition fxuInt.h:218
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()