ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
utilTruth.h
Go to the documentation of this file.
1
20
21#ifndef ABC__misc__util__utilTruth_h
22#define ABC__misc__util__utilTruth_h
23
27
28#ifdef _MSC_VER
29# include <intrin.h>
30# define __builtin_popcount __popcnt
31#endif
32
36
37ABC_NAMESPACE_HEADER_START
38
42
43static unsigned s_Truths5[6] = {
44 0xAAAAAAAA,
45 0xCCCCCCCC,
46 0xF0F0F0F0,
47 0xFF00FF00,
48 0xFFFF0000
49};
50
51static unsigned s_Truths5Neg[6] = {
52 0x55555555,
53 0x33333333,
54 0x0F0F0F0F,
55 0x00FF00FF,
56 0x0000FFFF
57};
58
59static word s_Truths6[6] = {
60 ABC_CONST(0xAAAAAAAAAAAAAAAA),
61 ABC_CONST(0xCCCCCCCCCCCCCCCC),
62 ABC_CONST(0xF0F0F0F0F0F0F0F0),
63 ABC_CONST(0xFF00FF00FF00FF00),
64 ABC_CONST(0xFFFF0000FFFF0000),
65 ABC_CONST(0xFFFFFFFF00000000)
66};
67
68static word s_Truths6Neg[6] = {
69 ABC_CONST(0x5555555555555555),
70 ABC_CONST(0x3333333333333333),
71 ABC_CONST(0x0F0F0F0F0F0F0F0F),
72 ABC_CONST(0x00FF00FF00FF00FF),
73 ABC_CONST(0x0000FFFF0000FFFF),
74 ABC_CONST(0x00000000FFFFFFFF)
75};
76
77static word s_Truth26[2][6] = {
78 {
79 ABC_CONST(0xAAAAAAAAAAAAAAAA),
80 ABC_CONST(0xCCCCCCCCCCCCCCCC),
81 ABC_CONST(0xF0F0F0F0F0F0F0F0),
82 ABC_CONST(0xFF00FF00FF00FF00),
83 ABC_CONST(0xFFFF0000FFFF0000),
84 ABC_CONST(0xFFFFFFFF00000000)
85 },
86 {
87 ABC_CONST(0x5555555555555555),
88 ABC_CONST(0x3333333333333333),
89 ABC_CONST(0x0F0F0F0F0F0F0F0F),
90 ABC_CONST(0x00FF00FF00FF00FF),
91 ABC_CONST(0x0000FFFF0000FFFF),
92 ABC_CONST(0x00000000FFFFFFFF)
93 }
94};
95
96static word s_TruthXors[6] = {
97 ABC_CONST(0x0000000000000000),
98 ABC_CONST(0x6666666666666666),
99 ABC_CONST(0x6969696969696969),
100 ABC_CONST(0x6996699669966996),
101 ABC_CONST(0x6996966969969669),
102 ABC_CONST(0x6996966996696996)
103};
104
105static word s_PMasks[5][3] = {
106 { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
107 { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
108 { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
109 { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
110 { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
111};
112
113static word s_PPMasks[5][6][3] = {
114 {
115 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 0 0
116 { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) }, // 0 1
117 { ABC_CONST(0xA5A5A5A5A5A5A5A5), ABC_CONST(0x0A0A0A0A0A0A0A0A), ABC_CONST(0x5050505050505050) }, // 0 2
118 { ABC_CONST(0xAA55AA55AA55AA55), ABC_CONST(0x00AA00AA00AA00AA), ABC_CONST(0x5500550055005500) }, // 0 3
119 { ABC_CONST(0xAAAA5555AAAA5555), ABC_CONST(0x0000AAAA0000AAAA), ABC_CONST(0x5555000055550000) }, // 0 4
120 { ABC_CONST(0xAAAAAAAA55555555), ABC_CONST(0x00000000AAAAAAAA), ABC_CONST(0x5555555500000000) } // 0 5
121 },
122 {
123 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 1 0
124 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 1 1
125 { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) }, // 1 2
126 { ABC_CONST(0xCC33CC33CC33CC33), ABC_CONST(0x00CC00CC00CC00CC), ABC_CONST(0x3300330033003300) }, // 1 3
127 { ABC_CONST(0xCCCC3333CCCC3333), ABC_CONST(0x0000CCCC0000CCCC), ABC_CONST(0x3333000033330000) }, // 1 4
128 { ABC_CONST(0xCCCCCCCC33333333), ABC_CONST(0x00000000CCCCCCCC), ABC_CONST(0x3333333300000000) } // 1 5
129 },
130 {
131 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 2 0
132 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 2 1
133 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 2 2
134 { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) }, // 2 3
135 { ABC_CONST(0xF0F00F0FF0F00F0F), ABC_CONST(0x0000F0F00000F0F0), ABC_CONST(0x0F0F00000F0F0000) }, // 2 4
136 { ABC_CONST(0xF0F0F0F00F0F0F0F), ABC_CONST(0x00000000F0F0F0F0), ABC_CONST(0x0F0F0F0F00000000) } // 2 5
137 },
138 {
139 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 0
140 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 1
141 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 2
142 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 3
143 { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) }, // 3 4
144 { ABC_CONST(0xFF00FF0000FF00FF), ABC_CONST(0x00000000FF00FF00), ABC_CONST(0x00FF00FF00000000) } // 3 5
145 },
146 {
147 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 0
148 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 1
149 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 2
150 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 3
151 { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 4
152 { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) } // 4 5
153 }
154};
155
156static inline int Abc_TtBitCount16( int i ) { return __builtin_popcount( i & 0xffff ); }
157
161
165
177// read/write/flip i-th bit of a bit string table:
178static inline int Abc_TtGetBit( word * p, int k ) { return (int)(p[k>>6] >> (k & 63)) & 1; }
179static inline void Abc_TtSetBit( word * p, int k ) { p[k>>6] |= (((word)1)<<(k & 63)); }
180static inline void Abc_TtXorBit( word * p, int k ) { p[k>>6] ^= (((word)1)<<(k & 63)); }
181
182// read/write k-th digit d of a quaternary number:
183static inline int Abc_TtGetQua( word * p, int k ) { return (int)(p[k>>5] >> ((k<<1) & 63)) & 3; }
184static inline void Abc_TtSetQua( word * p, int k, int d ) { p[k>>5] |= (((word)d)<<((k<<1) & 63)); }
185static inline void Abc_TtXorQua( word * p, int k, int d ) { p[k>>5] ^= (((word)d)<<((k<<1) & 63)); }
186
187// read/write k-th digit d of a hexadecimal number:
188static inline int Abc_TtGetHex( word * p, int k ) { return (int)(p[k>>4] >> ((k<<2) & 63)) & 15; }
189static inline void Abc_TtSetHex( word * p, int k, int d ) { p[k>>4] |= (((word)d)<<((k<<2) & 63)); }
190static inline void Abc_TtXorHex( word * p, int k, int d ) { p[k>>4] ^= (((word)d)<<((k<<2) & 63)); }
191
192// read/write k-th digit d of a 256-base number:
193static inline int Abc_TtGet256( word * p, int k ) { return (int)(p[k>>3] >> ((k<<3) & 63)) & 255; }
194static inline void Abc_TtSet256( word * p, int k, int d ) { p[k>>3] |= (((word)d)<<((k<<3) & 63)); }
195static inline void Abc_TtXor256( word * p, int k, int d ) { p[k>>3] ^= (((word)d)<<((k<<3) & 63)); }
196
197// read/write k-th digit d of a 2^16-base number:
198static inline int Abc_TtGet65536( word * p, int k ) { return (int)(p[k>>2] >> ((k<<4) & 63))&0xFFFF; }
199static inline void Abc_TtSet65536( word * p, int k, int d ) { p[k>>2] |= (((word)d)<<((k<<4) & 63)); }
200static inline void Abc_TtXor65536( word * p, int k, int d ) { p[k>>2] ^= (((word)d)<<((k<<4) & 63)); }
201
202// read/write k-th digit d of a 2^2^v-base number:
203static inline int Abc_TtGetV( word * p, int v, int k ) { return (int)((p[k>>(6-v)] << (64-(1<<v)-((k<<v) & 63))) >> (64-(1<<v)));}
204static inline void Abc_TtSetV( word * p, int v, int k, int d ) { p[k>>(6-v)] |= (((word)d)<<((k<<v) & 63)); }
205static inline void Abc_TtXorV( word * p, int v, int k, int d ) { p[k>>(6-v)] ^= (((word)d)<<((k<<v) & 63)); }
206
218static inline int Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); }
219static inline int Abc_TtByteNum( int nVars ) { return nVars <= 3 ? 1 : 1 << (nVars-3); }
220static inline int Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 << (nVars-2); }
221
233static inline word Abc_Tt6Mask( int nBits ) { assert( nBits >= 0 && nBits <= 64 ); return (~(word)0) >> (64-nBits); }
234static inline void Abc_TtMask( word * pTruth, int nWords, int nBits )
235{
236 int w;
237 assert( nBits >= 0 && nBits <= nWords * 64 );
238 for ( w = 0; w < nWords; w++ )
239 if ( nBits >= (w + 1) * 64 )
240 pTruth[w] = ~(word)0;
241 else if ( nBits > w * 64 )
242 pTruth[w] = Abc_Tt6Mask( nBits - w * 64 );
243 else
244 pTruth[w] = 0;
245}
246
258static inline word Abc_TtWordReverseBits( word w )
259{
260 int Rev[16] = {0, 8, 4, 12, 2, 10, 6, 14, 1, 9, 5, 13, 3, 11, 7, 15};
261 word r = 0; int i;
262 for ( i = 0; i < 16; i++ )
263 r |= (word)Rev[(w >> (i<<2))&15] << ((15-i)<<2);
264 return r;
265}
266static inline word Abc_TtWordReverseHexDigits( word w )
267{
268 word r = 0; int i;
269 for ( i = 0; i < 16; i++ )
270 r |= ((w >> (i<<2))&15) << ((15-i)<<2);
271 return r;
272}
273
285static inline void Abc_TtVec( word * pOut, int nWords, word Entry )
286{
287 int w;
288 for ( w = 0; w < nWords; w++ )
289 pOut[w] = Entry;
290}
291static inline void Abc_TtConst( word * pOut, int nWords, int fConst1 )
292{
293 int w;
294 for ( w = 0; w < nWords; w++ )
295 pOut[w] = fConst1 ? ~(word)0 : 0;
296}
297static inline void Abc_TtClear( word * pOut, int nWords )
298{
299 int w;
300 for ( w = 0; w < nWords; w++ )
301 pOut[w] = 0;
302}
303static inline void Abc_TtFill( word * pOut, int nWords )
304{
305 int w;
306 for ( w = 0; w < nWords; w++ )
307 pOut[w] = ~(word)0;
308}
309static inline void Abc_TtUnit( word * pOut, int nWords, int fCompl )
310{
311 int w;
312 for ( w = 0; w < nWords; w++ )
313 pOut[w] = fCompl ? ~s_Truths6[0] : s_Truths6[0];
314}
315static inline void Abc_TtNot( word * pOut, int nWords )
316{
317 int w;
318 for ( w = 0; w < nWords; w++ )
319 pOut[w] = ~pOut[w];
320}
321static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
322{
323 int w;
324 if ( fCompl )
325 for ( w = 0; w < nWords; w++ )
326 pOut[w] = ~pIn[w];
327 else
328 for ( w = 0; w < nWords; w++ )
329 pOut[w] = pIn[w];
330}
331static inline word * Abc_TtDup( word * pIn, int nWords, int fCompl )
332{
333 word * pOut = ABC_ALLOC( word, nWords );
334 Abc_TtCopy( pOut, pIn, nWords, fCompl );
335 return pOut;
336}
337static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
338{
339 int w;
340 if ( fCompl )
341 for ( w = 0; w < nWords; w++ )
342 pOut[w] = ~(pIn1[w] & pIn2[w]);
343 else
344 for ( w = 0; w < nWords; w++ )
345 pOut[w] = pIn1[w] & pIn2[w];
346}
347static inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords )
348{
349 int w;
350 if ( fCompl1 )
351 {
352 if ( fCompl2 )
353 for ( w = 0; w < nWords; w++ )
354 pOut[w] = ~pIn1[w] & ~pIn2[w];
355 else
356 for ( w = 0; w < nWords; w++ )
357 pOut[w] = ~pIn1[w] & pIn2[w];
358 }
359 else
360 {
361 if ( fCompl2 )
362 for ( w = 0; w < nWords; w++ )
363 pOut[w] = pIn1[w] & ~pIn2[w];
364 else
365 for ( w = 0; w < nWords; w++ )
366 pOut[w] = pIn1[w] & pIn2[w];
367 }
368}
369static inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
370{
371 int w;
372 if ( fCompl )
373 for ( w = 0; w < nWords; w++ )
374 pOut[w] = pIn1[w] & ~pIn2[w];
375 else
376 for ( w = 0; w < nWords; w++ )
377 pOut[w] = pIn1[w] & pIn2[w];
378}
379static inline void Abc_TtSharp( word * pOut, word * pIn1, word * pIn2, int nWords )
380{
381 int w;
382 for ( w = 0; w < nWords; w++ )
383 pOut[w] = pIn1[w] & ~pIn2[w];
384}
385static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
386{
387 int w;
388 for ( w = 0; w < nWords; w++ )
389 pOut[w] = pIn1[w] | pIn2[w];
390}
391static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWords )
392{
393 int w;
394 for ( w = 0; w < nWords; w++ )
395 pOut[w] |= pIn1[w] ^ pIn2[w];
396}
397static inline void Abc_TtAndXor( word * pOut, word * pIn1, word * pIn2, int nWords )
398{
399 int w;
400 for ( w = 0; w < nWords; w++ )
401 pOut[w] &= pIn1[w] ^ pIn2[w];
402}
403static inline void Abc_TtOrAnd( word * pOut, word * pIn1, word * pIn2, int nWords )
404{
405 int w;
406 for ( w = 0; w < nWords; w++ )
407 pOut[w] |= pIn1[w] & pIn2[w];
408}
409static inline void Abc_TtSharpOr( word * pOut, word * pIn1, word * pIn2, int nWords )
410{
411 int w;
412 for ( w = 0; w < nWords; w++ )
413 pOut[w] = (pOut[w] & ~pIn1[w]) | pIn2[w];
414}
415static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
416{
417 int w;
418 if ( fCompl )
419 for ( w = 0; w < nWords; w++ )
420 pOut[w] = pIn1[w] ^ ~pIn2[w];
421 else
422 for ( w = 0; w < nWords; w++ )
423 pOut[w] = pIn1[w] ^ pIn2[w];
424}
425static inline void Abc_TtXorMask( word * pOut, word * pIn1, word * pIn2, word * pMask, int nWords, int fCompl )
426{
427 int w;
428 if ( fCompl )
429 for ( w = 0; w < nWords; w++ )
430 pOut[w] = (pIn1[w] ^ pIn2[w]) & ~pMask[w];
431 else
432 for ( w = 0; w < nWords; w++ )
433 pOut[w] = (pIn1[w] ^ pIn2[w]) & pMask[w];
434}
435static inline void Abc_TtMux( word * pOut, word * pCtrl, word * pIn1, word * pIn0, int nWords )
436{
437 int w;
438 for ( w = 0; w < nWords; w++ )
439 pOut[w] = (pCtrl[w] & pIn1[w]) | (~pCtrl[w] & pIn0[w]);
440}
441static inline void Abc_TtMaj( word * pOut, word * pIn0, word * pIn1, word * pIn2, int nWords )
442{
443 int w;
444 for ( w = 0; w < nWords; w++ )
445 pOut[w] = (pIn0[w] & pIn1[w]) | (pIn0[w] & pIn2[w]) | (pIn1[w] & pIn2[w]);
446}
447static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords, int fCompl )
448{
449 int w;
450 if ( fCompl )
451 {
452 for ( w = 0; w < nWords; w++ )
453 if ( ~pIn1[w] & pIn2[w] )
454 return 1;
455 }
456 else
457 {
458 for ( w = 0; w < nWords; w++ )
459 if ( pIn1[w] & pIn2[w] )
460 return 1;
461 }
462 return 0;
463}
464static inline int Abc_TtIntersectCare( word * pIn1, word * pIn2, word * pCare, int nWords, int fCompl )
465{
466 int w;
467 if ( fCompl )
468 {
469 for ( w = 0; w < nWords; w++ )
470 if ( ~pIn1[w] & pIn2[w] & pCare[w] )
471 return 1;
472 }
473 else
474 {
475 for ( w = 0; w < nWords; w++ )
476 if ( pIn1[w] & pIn2[w] & pCare[w] )
477 return 1;
478 }
479 return 0;
480}static inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords )
481{
482 int w;
483 if ( fComp0 )
484 {
485 if ( fComp )
486 {
487 for ( w = 0; w < nWords; w++ )
488 if ( ~pIn[w] & ~pOut[w] )
489 return 1;
490 }
491 else
492 {
493 for ( w = 0; w < nWords; w++ )
494 if ( ~pIn[w] & pOut[w] )
495 return 1;
496 }
497 }
498 else
499 {
500 if ( fComp )
501 {
502 for ( w = 0; w < nWords; w++ )
503 if ( pIn[w] & ~pOut[w] )
504 return 1;
505 }
506 else
507 {
508 for ( w = 0; w < nWords; w++ )
509 if ( pIn[w] & pOut[w] )
510 return 1;
511 }
512 }
513 return 0;
514}
515static inline int Abc_TtIntersectTwo( word * pOut, int fComp, word * pIn0, int fComp0, word * pIn1, int fComp1, int nWords )
516{
517 int w;
518 if ( fComp0 && fComp1 )
519 {
520 if ( fComp )
521 {
522 for ( w = 0; w < nWords; w++ )
523 if ( ~pIn0[w] & ~pIn1[w] & ~pOut[w] )
524 return 1;
525 }
526 else
527 {
528 for ( w = 0; w < nWords; w++ )
529 if ( ~pIn0[w] & ~pIn1[w] & pOut[w] )
530 return 1;
531 }
532 }
533 else if ( fComp0 )
534 {
535 if ( fComp )
536 {
537 for ( w = 0; w < nWords; w++ )
538 if ( ~pIn0[w] & pIn1[w] & ~pOut[w] )
539 return 1;
540 }
541 else
542 {
543 for ( w = 0; w < nWords; w++ )
544 if ( ~pIn0[w] & pIn1[w] & pOut[w] )
545 return 1;
546 }
547 }
548 else if ( fComp1 )
549 {
550 if ( fComp )
551 {
552 for ( w = 0; w < nWords; w++ )
553 if ( pIn0[w] & ~pIn1[w] & ~pOut[w] )
554 return 1;
555 }
556 else
557 {
558 for ( w = 0; w < nWords; w++ )
559 if ( pIn0[w] & ~pIn1[w] & pOut[w] )
560 return 1;
561 }
562 }
563 else
564 {
565 if ( fComp )
566 {
567 for ( w = 0; w < nWords; w++ )
568 if ( pIn0[w] & pIn1[w] & ~pOut[w] )
569 return 1;
570 }
571 else
572 {
573 for ( w = 0; w < nWords; w++ )
574 if ( pIn0[w] & pIn1[w] & pOut[w] )
575 return 1;
576 }
577 }
578 return 0;
579}
580static inline int Abc_TtIntersectXor( word * pOut, int fComp, word * pIn0, word * pIn1, int fComp01, int nWords )
581{
582 int w;
583 if ( fComp01 )
584 {
585 if ( fComp )
586 {
587 for ( w = 0; w < nWords; w++ )
588 if ( ~(pIn0[w] ^ pIn1[w]) & ~pOut[w] )
589 return 1;
590 }
591 else
592 {
593 for ( w = 0; w < nWords; w++ )
594 if ( ~(pIn0[w] ^ pIn1[w]) & pOut[w] )
595 return 1;
596 }
597 }
598 else
599 {
600 if ( fComp )
601 {
602 for ( w = 0; w < nWords; w++ )
603 if ( (pIn0[w] ^ pIn1[w]) & ~pOut[w] )
604 return 1;
605 }
606 else
607 {
608 for ( w = 0; w < nWords; w++ )
609 if ( (pIn0[w] ^ pIn1[w]) & pOut[w] )
610 return 1;
611 }
612 }
613 return 0;
614}
615static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
616{
617 int w;
618 for ( w = 0; w < nWords; w++ )
619 if ( pIn1[w] != pIn2[w] )
620 return 0;
621 return 1;
622}
623static inline int Abc_TtEqualCare( word * pIn1, word * pIn2, word * pCare, int fComp, int nWords )
624{
625 int w;
626 if ( fComp )
627 {
628 for ( w = 0; w < nWords; w++ )
629 if ( (~pIn1[w] ^ pIn2[w]) & pCare[w] )
630 return 0;
631 }
632 else
633 {
634 for ( w = 0; w < nWords; w++ )
635 if ( (pIn1[w] ^ pIn2[w]) & pCare[w] )
636 return 0;
637 }
638 return 1;
639}
640static inline int Abc_TtOpposite( word * pIn1, word * pIn2, int nWords )
641{
642 int w;
643 for ( w = 0; w < nWords; w++ )
644 if ( pIn1[w] != ~pIn2[w] )
645 return 0;
646 return 1;
647}
648static inline int Abc_TtImply( word * pIn1, word * pIn2, int nWords )
649{
650 int w;
651 for ( w = 0; w < nWords; w++ )
652 if ( (pIn1[w] & pIn2[w]) != pIn1[w] )
653 return 0;
654 return 1;
655}
656static inline int Abc_TtCompare( word * pIn1, word * pIn2, int nWords )
657{
658 int w;
659 for ( w = 0; w < nWords; w++ )
660 if ( pIn1[w] != pIn2[w] )
661 return (pIn1[w] < pIn2[w]) ? -1 : 1;
662 return 0;
663}
664static inline int Abc_TtCompareRev( word * pIn1, word * pIn2, int nWords )
665{
666 int w;
667 for ( w = nWords - 1; w >= 0; w-- )
668 if ( pIn1[w] != pIn2[w] )
669 return (pIn1[w] < pIn2[w]) ? -1 : 1;
670 return 0;
671}
672static inline int Abc_TtIsConst0( word * pIn1, int nWords )
673{
674 int w;
675 for ( w = 0; w < nWords; w++ )
676 if ( pIn1[w] )
677 return 0;
678 return 1;
679}
680static inline int Abc_TtIsConst1( word * pIn1, int nWords )
681{
682 int w;
683 for ( w = 0; w < nWords; w++ )
684 if ( ~pIn1[w] )
685 return 0;
686 return 1;
687}
688static inline void Abc_TtConst0( word * pIn1, int nWords )
689{
690 int w;
691 for ( w = 0; w < nWords; w++ )
692 pIn1[w] = 0;
693}
694static inline void Abc_TtConst1( word * pIn1, int nWords )
695{
696 int w;
697 for ( w = 0; w < nWords; w++ )
698 pIn1[w] = ~(word)0;
699}
700static inline void Abc_TtIthVar( word * pOut, int iVar, int nVars )
701{
702 int k, nWords = Abc_TtWordNum( nVars );
703 if ( iVar < 6 )
704 {
705 for ( k = 0; k < nWords; k++ )
706 pOut[k] = s_Truths6[iVar];
707 }
708 else
709 {
710 for ( k = 0; k < nWords; k++ )
711 if ( k & (1 << (iVar-6)) )
712 pOut[k] = ~(word)0;
713 else
714 pOut[k] = 0;
715 }
716}
717static inline void Abc_TtTruth2( word * pOut, word * pIn0, word * pIn1, int Truth, int nWords )
718{
719 int w;
720 assert( Truth >= 0 && Truth <= 0xF );
721 switch ( Truth )
722 {
723 case 0x0 : for ( w = 0; w < nWords; w++ ) pOut[w] = 0; break; // 0000
724 case 0x1 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] & ~pIn0[w]; break; // 0001
725 case 0x2 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] & pIn0[w]; break; // 0010
726 case 0x3 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] ; break; // 0011
727 case 0x4 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & ~pIn0[w]; break; // 0100
728 case 0x5 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn0[w]; break; // 0101
729 case 0x6 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ^ pIn0[w]; break; // 0110
730 case 0x7 : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] | ~pIn0[w]; break; // 0111
731 case 0x8 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & pIn0[w]; break; // 1000
732 case 0x9 : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ^ ~pIn0[w]; break; // 1001
733 case 0xA : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn0[w]; break; // 1010
734 case 0xB : for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn1[w] | pIn0[w]; break; // 1011
735 case 0xC : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] ; break; // 1100
736 case 0xD : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] | ~pIn0[w]; break; // 1101
737 case 0xE : for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] | pIn0[w]; break; // 1110
738 case 0xF : for ( w = 0; w < nWords; w++ ) pOut[w] = ~(word)0; break; // 1111
739 default : assert( 0 );
740 }
741}
742static inline void Abc_TtTruth4( word Entry, word ** pNodes, word * pOut, int nWords, int fCompl )
743{
744 unsigned First = (unsigned)Entry;
745 unsigned Second = (unsigned)(Entry >> 32);
746 int i, k = 5;
747 for ( i = 0; i < 4; i++ )
748 {
749 int Lit0, Lit1, Pair = (First >> (i*8)) & 0xFF;
750 if ( Pair == 0 )
751 break;
752 Lit0 = Pair & 0xF;
753 Lit1 = Pair >> 4;
754 assert( Lit0 != Lit1 );
755 if ( Lit0 < Lit1 )
756 Abc_TtAndCompl( pNodes[k++], pNodes[Lit0 >> 1], Lit0 & 1, pNodes[Lit1 >> 1], Lit1 & 1, nWords );
757 else
758 Abc_TtXor( pNodes[k++], pNodes[Lit0 >> 1], pNodes[Lit1 >> 1], nWords, (Lit0 & 1) ^ (Lit1 & 1) );
759 }
760 for ( i = 0; i < 3; i++ )
761 {
762 int Lit0, Lit1, Pair = (Second >> (i*10)) & 0x3FF;
763 if ( Pair == 0 )
764 break;
765 Lit0 = Pair & 0x1F;
766 Lit1 = Pair >> 5;
767 assert( Lit0 != Lit1 );
768 if ( Lit0 < Lit1 )
769 Abc_TtAndCompl( pNodes[k++], pNodes[Lit0 >> 1], Lit0 & 1, pNodes[Lit1 >> 1], Lit1 & 1, nWords );
770 else
771 Abc_TtXor( pNodes[k++], pNodes[Lit0 >> 1], pNodes[Lit1 >> 1], nWords, (Lit0 & 1) ^ (Lit1 & 1) );
772 }
773 assert( k > 5 );
774 Abc_TtCopy( pOut, pNodes[k-1], nWords, (int)(Entry >> 62) ^ fCompl );
775}
776
788static inline int Abc_TtIsAndCompl( word * pOut, int fCompl, word * pIn1, int fCompl1, word * pIn2, int fCompl2, word * pCare, int nWords )
789{
790 int w;
791 if ( fCompl )
792 {
793 if ( fCompl1 )
794 {
795 if ( fCompl2 )
796 {
797 for ( w = 0; w < nWords; w++ )
798 if ( (~pOut[w] & pCare[w]) != (~pIn1[w] & ~pIn2[w] & pCare[w]) )
799 return 0;
800 }
801 else
802 {
803 for ( w = 0; w < nWords; w++ )
804 if ( (~pOut[w] & pCare[w]) != (~pIn1[w] & pIn2[w] & pCare[w]) )
805 return 0;
806 }
807 }
808 else
809 {
810 if ( fCompl2 )
811 {
812 for ( w = 0; w < nWords; w++ )
813 if ( (~pOut[w] & pCare[w]) != (pIn1[w] & ~pIn2[w] & pCare[w]) )
814 return 0;
815 }
816 else
817 {
818 for ( w = 0; w < nWords; w++ )
819 if ( (~pOut[w] & pCare[w]) != (pIn1[w] & pIn2[w] & pCare[w]) )
820 return 0;
821 }
822 }
823 }
824 else
825 {
826 if ( fCompl1 )
827 {
828 if ( fCompl2 )
829 {
830 for ( w = 0; w < nWords; w++ )
831 if ( (pOut[w] & pCare[w]) != (~pIn1[w] & ~pIn2[w] & pCare[w]) )
832 return 0;
833 }
834 else
835 {
836 for ( w = 0; w < nWords; w++ )
837 if ( (pOut[w] & pCare[w]) != (~pIn1[w] & pIn2[w] & pCare[w]) )
838 return 0;
839 }
840 }
841 else
842 {
843 if ( fCompl2 )
844 {
845 for ( w = 0; w < nWords; w++ )
846 if ( (pOut[w] & pCare[w]) != (pIn1[w] & ~pIn2[w] & pCare[w]) )
847 return 0;
848 }
849 else
850 {
851 for ( w = 0; w < nWords; w++ )
852 if ( (pOut[w] & pCare[w]) != (pIn1[w] & pIn2[w] & pCare[w]) )
853 return 0;
854 }
855 }
856 }
857 return 1;
858}
859
860static inline int Abc_TtIsXorCompl( word * pOut, int fCompl, word * pIn1, word * pIn2, word * pCare, int nWords )
861{
862 int w;
863 if ( fCompl )
864 {
865 for ( w = 0; w < nWords; w++ )
866 if ( (~pOut[w] & pCare[w]) != ((pIn1[w] ^ pIn2[w]) & pCare[w]) )
867 return 0;
868 }
869 else
870 {
871 for ( w = 0; w < nWords; w++ )
872 if ( ( pOut[w] & pCare[w]) != ((pIn1[w] ^ pIn2[w]) & pCare[w]) )
873 return 0;
874 }
875 return 1;
876}
877
878
890static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
891{
892 if ( nWords == 1 )
893 {
894 word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
895 word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
896 if ( Cof0 != Cof1 )
897 return Cof0 < Cof1 ? -1 : 1;
898 return 0;
899 }
900 if ( iVar <= 5 )
901 {
902 word Cof0, Cof1;
903 int w, shift = (1 << iVar);
904 for ( w = 0; w < nWords; w++ )
905 {
906 Cof0 = pTruth[w] & s_Truths6Neg[iVar];
907 Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
908 if ( Cof0 != Cof1 )
909 return Cof0 < Cof1 ? -1 : 1;
910 }
911 return 0;
912 }
913 // if ( iVar > 5 )
914 {
915 word * pLimit = pTruth + nWords;
916 int i, iStep = Abc_TtWordNum(iVar);
917 assert( nWords >= 2 );
918 for ( ; pTruth < pLimit; pTruth += 2*iStep )
919 for ( i = 0; i < iStep; i++ )
920 if ( pTruth[i] != pTruth[i + iStep] )
921 return pTruth[i] < pTruth[i + iStep] ? -1 : 1;
922 return 0;
923 }
924}
925static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar )
926{
927 if ( nWords == 1 )
928 {
929 word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
930 word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
931 if ( Cof0 != Cof1 )
932 return Cof0 < Cof1 ? -1 : 1;
933 return 0;
934 }
935 if ( iVar <= 5 )
936 {
937 word Cof0, Cof1;
938 int w, shift = (1 << iVar);
939 for ( w = nWords - 1; w >= 0; w-- )
940 {
941 Cof0 = pTruth[w] & s_Truths6Neg[iVar];
942 Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
943 if ( Cof0 != Cof1 )
944 return Cof0 < Cof1 ? -1 : 1;
945 }
946 return 0;
947 }
948 // if ( iVar > 5 )
949 {
950 word * pLimit = pTruth + nWords;
951 int i, iStep = Abc_TtWordNum(iVar);
952 assert( nWords >= 2 );
953 for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep )
954 for ( i = iStep - 1; i >= 0; i-- )
955 if ( pLimit[i] != pLimit[i + iStep] )
956 return pLimit[i] < pLimit[i + iStep] ? -1 : 1;
957 return 0;
958 }
959}
960
972static inline void Abc_TtElemInit( word ** pTtElems, int nVars )
973{
974 int i, k, nWords = Abc_TtWordNum( nVars );
975 for ( i = 0; i < nVars; i++ )
976 if ( i < 6 )
977 for ( k = 0; k < nWords; k++ )
978 pTtElems[i][k] = s_Truths6[i];
979 else
980 for ( k = 0; k < nWords; k++ )
981 pTtElems[i][k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
982}
983static inline void Abc_TtElemInit2( word * pTtElems, int nVars )
984{
985 int i, k, nWords = Abc_TtWordNum( nVars );
986 for ( i = 0; i < nVars; i++ )
987 {
988 word * pTruth = pTtElems + i * nWords;
989 if ( i < 6 )
990 for ( k = 0; k < nWords; k++ )
991 pTruth[k] = s_Truths6[i];
992 else
993 for ( k = 0; k < nWords; k++ )
994 pTruth[k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
995 }
996}
997
1009static inline int Abc_Tt5HasVar( unsigned t, int iVar )
1010{
1011 return ((t << (1<<iVar)) & s_Truths5[iVar]) != (t & s_Truths5[iVar]);
1012}
1013static inline unsigned Abc_Tt5Cofactor0( unsigned t, int iVar )
1014{
1015 assert( iVar >= 0 && iVar < 5 );
1016 return (t &s_Truths5Neg[iVar]) | ((t &s_Truths5Neg[iVar]) << (1<<iVar));
1017}
1018static inline unsigned Abc_Tt5Cofactor1( unsigned t, int iVar )
1019{
1020 assert( iVar >= 0 && iVar < 5 );
1021 return (t & s_Truths5[iVar]) | ((t & s_Truths5[iVar]) >> (1<<iVar));
1022}
1023
1024
1036static inline word Abc_Tt6Cofactor0( word t, int iVar )
1037{
1038 assert( iVar >= 0 && iVar < 6 );
1039 return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
1040}
1041static inline word Abc_Tt6Cofactor1( word t, int iVar )
1042{
1043 assert( iVar >= 0 && iVar < 6 );
1044 return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
1045}
1046
1047static inline void Abc_TtCofactor0p( word * pOut, word * pIn, int nWords, int iVar )
1048{
1049 if ( nWords == 1 )
1050 pOut[0] = ((pIn[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pIn[0] & s_Truths6Neg[iVar]);
1051 else if ( iVar <= 5 )
1052 {
1053 int w, shift = (1 << iVar);
1054 for ( w = 0; w < nWords; w++ )
1055 pOut[w] = ((pIn[w] & s_Truths6Neg[iVar]) << shift) | (pIn[w] & s_Truths6Neg[iVar]);
1056 }
1057 else // if ( iVar > 5 )
1058 {
1059 word * pLimit = pIn + nWords;
1060 int i, iStep = Abc_TtWordNum(iVar);
1061 for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
1062 for ( i = 0; i < iStep; i++ )
1063 {
1064 pOut[i] = pIn[i];
1065 pOut[i + iStep] = pIn[i];
1066 }
1067 }
1068}
1069static inline void Abc_TtCofactor1p( word * pOut, word * pIn, int nWords, int iVar )
1070{
1071 if ( nWords == 1 )
1072 pOut[0] = (pIn[0] & s_Truths6[iVar]) | ((pIn[0] & s_Truths6[iVar]) >> (1 << iVar));
1073 else if ( iVar <= 5 )
1074 {
1075 int w, shift = (1 << iVar);
1076 for ( w = 0; w < nWords; w++ )
1077 pOut[w] = (pIn[w] & s_Truths6[iVar]) | ((pIn[w] & s_Truths6[iVar]) >> shift);
1078 }
1079 else // if ( iVar > 5 )
1080 {
1081 word * pLimit = pIn + nWords;
1082 int i, iStep = Abc_TtWordNum(iVar);
1083 for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
1084 for ( i = 0; i < iStep; i++ )
1085 {
1086 pOut[i] = pIn[i + iStep];
1087 pOut[i + iStep] = pIn[i + iStep];
1088 }
1089 }
1090}
1091static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
1092{
1093 if ( nWords == 1 )
1094 pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]);
1095 else if ( iVar <= 5 )
1096 {
1097 int w, shift = (1 << iVar);
1098 for ( w = 0; w < nWords; w++ )
1099 pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
1100 }
1101 else // if ( iVar > 5 )
1102 {
1103 word * pLimit = pTruth + nWords;
1104 int i, iStep = Abc_TtWordNum(iVar);
1105 for ( ; pTruth < pLimit; pTruth += 2*iStep )
1106 for ( i = 0; i < iStep; i++ )
1107 pTruth[i + iStep] = pTruth[i];
1108 }
1109}
1110static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
1111{
1112 if ( nWords == 1 )
1113 pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
1114 else if ( iVar <= 5 )
1115 {
1116 int w, shift = (1 << iVar);
1117 for ( w = 0; w < nWords; w++ )
1118 pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
1119 }
1120 else // if ( iVar > 5 )
1121 {
1122 word * pLimit = pTruth + nWords;
1123 int i, iStep = Abc_TtWordNum(iVar);
1124 for ( ; pTruth < pLimit; pTruth += 2*iStep )
1125 for ( i = 0; i < iStep; i++ )
1126 pTruth[i] = pTruth[i + iStep];
1127 }
1128}
1129
1141static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int jVar, int Num1, int Num2 )
1142{
1143 assert( Num1 < Num2 && Num2 < 4 );
1144 assert( iVar < jVar );
1145 if ( nWords == 1 )
1146 {
1147 word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
1148 int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
1149 int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
1150 return ((pTruth[0] >> shift1) & Mask) == ((pTruth[0] >> shift2) & Mask);
1151 }
1152 if ( jVar <= 5 )
1153 {
1154 word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
1155 int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
1156 int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
1157 int w;
1158 for ( w = 0; w < nWords; w++ )
1159 if ( ((pTruth[w] >> shift1) & Mask) != ((pTruth[w] >> shift2) & Mask) )
1160 return 0;
1161 return 1;
1162 }
1163 if ( iVar <= 5 && jVar > 5 )
1164 {
1165 word * pLimit = pTruth + nWords;
1166 int j, jStep = Abc_TtWordNum(jVar);
1167 int shift1 = (Num1 & 1) * (1 << iVar);
1168 int shift2 = (Num2 & 1) * (1 << iVar);
1169 int Offset1 = (Num1 >> 1) * jStep;
1170 int Offset2 = (Num2 >> 1) * jStep;
1171 for ( ; pTruth < pLimit; pTruth += 2*jStep )
1172 for ( j = 0; j < jStep; j++ )
1173 if ( ((pTruth[j + Offset1] >> shift1) & s_Truths6Neg[iVar]) != ((pTruth[j + Offset2] >> shift2) & s_Truths6Neg[iVar]) )
1174 return 0;
1175 return 1;
1176 }
1177 {
1178 word * pLimit = pTruth + nWords;
1179 int j, jStep = Abc_TtWordNum(jVar);
1180 int i, iStep = Abc_TtWordNum(iVar);
1181 int Offset1 = (Num1 >> 1) * jStep + (Num1 & 1) * iStep;
1182 int Offset2 = (Num2 >> 1) * jStep + (Num2 & 1) * iStep;
1183 for ( ; pTruth < pLimit; pTruth += 2*jStep )
1184 for ( i = 0; i < jStep; i += 2*iStep )
1185 for ( j = 0; j < iStep; j++ )
1186 if ( pTruth[Offset1 + i + j] != pTruth[Offset2 + i + j] )
1187 return 0;
1188 return 1;
1189 }
1190}
1191
1192
1204static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == 0; }
1205static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar]; }
1206static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0; }
1207static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar]; }
1208static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return (~t & s_Truths6Neg[iVar]) == ((t >> (1 << iVar)) & s_Truths6Neg[iVar]); }
1209static inline int Abc_Tt6Cof0EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == ((t2 >> (1 << iVar)) & s_Truths6Neg[iVar]); }
1210static inline int Abc_Tt6Cof0EqualCof0( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == (t2 & s_Truths6Neg[iVar]); }
1211static inline int Abc_Tt6Cof1EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6[iVar]) == (t2 & s_Truths6[iVar]); }
1212
1224static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; }
1225static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
1226
1227static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar )
1228{
1229 if ( iVar < 6 )
1230 {
1231 int i;
1232 for ( i = 0; i < nWords; i++ )
1233 if ( t[i] & s_Truths6Neg[iVar] )
1234 return 0;
1235 return 1;
1236 }
1237 else
1238 {
1239 int i, Step = (1 << (iVar - 6));
1240 word * tLimit = t + nWords;
1241 for ( ; t < tLimit; t += 2*Step )
1242 for ( i = 0; i < Step; i++ )
1243 if ( t[i] )
1244 return 0;
1245 return 1;
1246 }
1247}
1248static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar )
1249{
1250 if ( iVar < 6 )
1251 {
1252 int i;
1253 for ( i = 0; i < nWords; i++ )
1254 if ( (t[i] & s_Truths6Neg[iVar]) != s_Truths6Neg[iVar] )
1255 return 0;
1256 return 1;
1257 }
1258 else
1259 {
1260 int i, Step = (1 << (iVar - 6));
1261 word * tLimit = t + nWords;
1262 for ( ; t < tLimit; t += 2*Step )
1263 for ( i = 0; i < Step; i++ )
1264 if ( ~t[i] )
1265 return 0;
1266 return 1;
1267 }
1268}
1269static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar )
1270{
1271 if ( iVar < 6 )
1272 {
1273 int i;
1274 for ( i = 0; i < nWords; i++ )
1275 if ( t[i] & s_Truths6[iVar] )
1276 return 0;
1277 return 1;
1278 }
1279 else
1280 {
1281 int i, Step = (1 << (iVar - 6));
1282 word * tLimit = t + nWords;
1283 for ( ; t < tLimit; t += 2*Step )
1284 for ( i = 0; i < Step; i++ )
1285 if ( t[i+Step] )
1286 return 0;
1287 return 1;
1288 }
1289}
1290static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar )
1291{
1292 if ( iVar < 6 )
1293 {
1294 int i;
1295 for ( i = 0; i < nWords; i++ )
1296 if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
1297 return 0;
1298 return 1;
1299 }
1300 else
1301 {
1302 int i, Step = (1 << (iVar - 6));
1303 word * tLimit = t + nWords;
1304 for ( ; t < tLimit; t += 2*Step )
1305 for ( i = 0; i < Step; i++ )
1306 if ( ~t[i+Step] )
1307 return 0;
1308 return 1;
1309 }
1310}
1311static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
1312{
1313 if ( iVar < 6 )
1314 {
1315 int i, Shift = (1 << iVar);
1316 for ( i = 0; i < nWords; i++ )
1317 if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
1318 return 0;
1319 return 1;
1320 }
1321 else
1322 {
1323 int i, Step = (1 << (iVar - 6));
1324 word * tLimit = t + nWords;
1325 for ( ; t < tLimit; t += 2*Step )
1326 for ( i = 0; i < Step; i++ )
1327 if ( t[i] != ~t[i+Step] )
1328 return 0;
1329 return 1;
1330 }
1331}
1332
1344static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
1345{
1346 int w, i, step, nWords;
1347 if ( nVarS == nVarB )
1348 return;
1349 assert( nVarS < nVarB );
1350 step = Abc_TruthWordNum(nVarS);
1351 nWords = Abc_TruthWordNum(nVarB);
1352 if ( step == nWords )
1353 return;
1354 assert( step < nWords );
1355 for ( w = 0; w < nWords; w += step )
1356 for ( i = 0; i < step; i++ )
1357 pInOut[w + i] = pInOut[i];
1358}
1359static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
1360{
1361 int w, i, step, nWords;
1362 if ( nVarS == nVarB )
1363 return;
1364 assert( nVarS < nVarB );
1365 step = Abc_Truth6WordNum(nVarS);
1366 nWords = Abc_Truth6WordNum(nVarB);
1367 if ( step == nWords )
1368 return;
1369 assert( step < nWords );
1370 for ( w = 0; w < nWords; w += step )
1371 for ( i = 0; i < step; i++ )
1372 pInOut[w + i] = pInOut[i];
1373}
1374static inline word Abc_Tt6Stretch( word t, int nVars )
1375{
1376 assert( nVars >= 0 );
1377 if ( nVars == 0 )
1378 nVars++, t = (t & 0x1) | ((t & 0x1) << 1);
1379 if ( nVars == 1 )
1380 nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
1381 if ( nVars == 2 )
1382 nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
1383 if ( nVars == 3 )
1384 nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
1385 if ( nVars == 4 )
1386 nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
1387 if ( nVars == 5 )
1388 nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
1389 assert( nVars == 6 );
1390 return t;
1391}
1392
1404static inline int Abc_TtIsHexDigit( char HexChar )
1405{
1406 return (HexChar >= '0' && HexChar <= '9') || (HexChar >= 'A' && HexChar <= 'F') || (HexChar >= 'a' && HexChar <= 'f');
1407}
1408static inline char Abc_TtPrintDigit( int Digit )
1409{
1410 assert( Digit >= 0 && Digit < 16 );
1411 if ( Digit < 10 )
1412 return '0' + Digit;
1413 return 'A' + Digit-10;
1414}
1415static inline char Abc_TtPrintDigitLower( int Digit )
1416{
1417 assert( Digit >= 0 && Digit < 16 );
1418 if ( Digit < 10 )
1419 return '0' + Digit;
1420 return 'a' + Digit-10;
1421}
1422static inline int Abc_TtReadHexDigit( char HexChar )
1423{
1424 if ( HexChar >= '0' && HexChar <= '9' )
1425 return HexChar - '0';
1426 if ( HexChar >= 'A' && HexChar <= 'F' )
1427 return HexChar - 'A' + 10;
1428 if ( HexChar >= 'a' && HexChar <= 'f' )
1429 return HexChar - 'a' + 10;
1430 assert( 0 ); // not a hexadecimal symbol
1431 return -1; // return value which makes no sense
1432}
1433
1445static inline void Abc_TtPrintHex( word * pTruth, int nVars )
1446{
1447 word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
1448 int k;
1449 if ( nVars < 2 )
1450 printf( "%c", Abc_TtPrintDigit((int)pTruth[0] & 15) );
1451 else
1452 {
1453 assert( nVars >= 2 );
1454 for ( pThis = pTruth; pThis < pLimit; pThis++ )
1455 for ( k = 0; k < 16; k++ )
1456 printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
1457 }
1458 printf( "\n" );
1459}
1460static inline void Abc_TtPrintHexRev( FILE * pFile, word * pTruth, int nVars )
1461{
1462 word * pThis;
1463 int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
1464 if ( nVars < 2 )
1465 fprintf( pFile, "%c", Abc_TtPrintDigit((int)pTruth[0] & 15) );
1466 else
1467 {
1468 assert( nVars >= 2 );
1469 for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
1470 for ( k = StartK - 1; k >= 0; k-- )
1471 fprintf( pFile, "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
1472 }
1473// printf( "\n" );
1474}
1475static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
1476{
1477 word * pThis;
1478 int k;
1479 if ( nVars < 2 )
1480 printf( "%c", Abc_TtPrintDigit((int)pTruth[0] & 15) );
1481 else
1482 {
1483 assert( nVars >= 2 );
1484 for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
1485 for ( k = 0; k < 16; k++ )
1486 printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
1487 }
1488 printf( "\n" );
1489}
1490static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
1491{
1492 word * pThis;
1493 char * pStrInit = pStr;
1494 int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
1495 if ( nVars < 2 )
1496 *pStr++ = Abc_TtPrintDigit((int)pTruth[0] & 15);
1497 else
1498 {
1499 assert( nVars >= 2 );
1500 for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
1501 for ( k = StartK - 1; k >= 0; k-- )
1502 *pStr++ = Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
1503 }
1504 return pStr - pStrInit;
1505}
1506static inline void Abc_TtPrintHexArrayRev( FILE * pFile, word * pTruth, int nDigits )
1507{
1508 int k;
1509 for ( k = nDigits - 1; k >= 0; k-- )
1510 fprintf( pFile, "%c", Abc_TtPrintDigitLower( Abc_TtGetHex(pTruth, k) ) );
1511}
1512
1524static inline int Abc_TtReadHex( word * pTruth, char * pString )
1525{
1526 int k, nVars, Digit, nDigits;
1527 // skip the first 2 symbols if they are "0x"
1528 if ( pString[0] == '0' && pString[1] == 'x' )
1529 pString += 2;
1530 // count the number of hex digits
1531 nDigits = 0;
1532 for ( k = 0; Abc_TtIsHexDigit(pString[k]); k++ )
1533 nDigits++;
1534 if ( nDigits == 1 )
1535 {
1536 if ( pString[0] == '0' || pString[0] == 'F' )
1537 {
1538 pTruth[0] = (pString[0] == '0') ? 0 : ~(word)0;
1539 return 0;
1540 }
1541 if ( pString[0] == '5' || pString[0] == 'A' )
1542 {
1543 pTruth[0] = (pString[0] == '5') ? s_Truths6Neg[0] : s_Truths6[0];
1544 return 1;
1545 }
1546 }
1547 // determine the number of variables
1548 nVars = 2 + (nDigits == 1 ? 0 : Abc_Base2Log(nDigits));
1549 // clean storage
1550 for ( k = Abc_TtWordNum(nVars) - 1; k >= 0; k-- )
1551 pTruth[k] = 0;
1552 // read hexadecimal digits in the reverse order
1553 // (the last symbol in the string is the least significant digit)
1554 for ( k = 0; k < nDigits; k++ )
1555 {
1556 Digit = Abc_TtReadHexDigit( pString[nDigits - 1 - k] );
1557 assert( Digit >= 0 && Digit < 16 );
1558 Abc_TtSetHex( pTruth, k, Digit );
1559 }
1560 if ( nVars < 6 )
1561 pTruth[0] = Abc_Tt6Stretch( pTruth[0], nVars );
1562 return nVars;
1563}
1564static inline int Abc_TtReadHexNumber( word * pTruth, char * pString )
1565{
1566 // count the number of hex digits
1567 int k, Digit, nDigits = 0;
1568 for ( k = 0; Abc_TtIsHexDigit(pString[k]); k++ )
1569 nDigits++;
1570 // read hexadecimal digits in the reverse order
1571 // (the last symbol in the string is the least significant digit)
1572 for ( k = 0; k < nDigits; k++ )
1573 {
1574 Digit = Abc_TtReadHexDigit( pString[nDigits - 1 - k] );
1575 assert( Digit >= 0 && Digit < 16 );
1576 Abc_TtSetHex( pTruth, k, Digit );
1577 }
1578 return nDigits;
1579}
1580
1581
1593static inline void Abc_TtPrintBits( word * pTruth, int nBits )
1594{
1595 int k;
1596 for ( k = 0; k < nBits; k++ )
1597 printf( "%d", Abc_InfoHasBit( (unsigned *)pTruth, k ) );
1598 printf( "\n" );
1599}
1600static inline void Abc_TtPrintBits2( word * pTruth, int nBits )
1601{
1602 int k;
1603 for ( k = nBits-1; k >= 0; k-- )
1604 printf( "%d", Abc_InfoHasBit( (unsigned *)pTruth, k ) );
1605 printf( "\n" );
1606}
1607static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
1608{
1609 word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
1610 int k, Limit = Abc_MinInt( 64, (1 << nVars) );
1611 assert( nVars >= 2 );
1612 for ( pThis = pTruth; pThis < pLimit; pThis++ )
1613 for ( k = 0; k < Limit; k++ )
1614 printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
1615 printf( "\n" );
1616}
1617static inline void Abc_TtPrintBinary1( FILE * pFile, word * pTruth, int nVars )
1618{
1619 word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
1620 int k, Limit = Abc_MinInt( 64, (1 << nVars) );
1621 assert( nVars >= 2 );
1622 for ( pThis = pTruth; pThis < pLimit; pThis++ )
1623 for ( k = 0; k < Limit; k++ )
1624 fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
1625}
1626static inline void Abc_TtPrintBinary2( FILE * pFile, word * pTruth, int nVars )
1627{
1628 word * pThis;
1629 int k, Limit = Abc_MinInt( 64, (1 << nVars) );
1630 assert( nVars >= 2 );
1631 for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
1632 for ( k = Limit-1; k >= 0; k-- )
1633 fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
1634}
1635
1647static inline int Abc_TtSuppFindFirst( int Supp )
1648{
1649 int i;
1650 assert( Supp > 0 );
1651 for ( i = 0; i < 32; i++ )
1652 if ( Supp & (1 << i) )
1653 return i;
1654 return -1;
1655}
1656static inline int Abc_TtSuppOnlyOne( int Supp )
1657{
1658 if ( Supp == 0 )
1659 return 0;
1660 return (Supp & (Supp-1)) == 0;
1661}
1662static inline int Abc_TtSuppIsMinBase( int Supp )
1663{
1664 assert( Supp > 0 );
1665 return (Supp & (Supp+1)) == 0;
1666}
1667static inline int Abc_Tt6HasVar( word t, int iVar )
1668{
1669 return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) != (t & s_Truths6Neg[iVar]);
1670}
1671static inline int Abc_Tt6XorVar( word t, int iVar )
1672{
1673 return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) == ~(t & s_Truths6Neg[iVar]);
1674}
1675static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
1676{
1677 assert( iVar < nVars );
1678 if ( nVars <= 6 )
1679 return Abc_Tt6HasVar( t[0], iVar );
1680 if ( iVar < 6 )
1681 {
1682 int i, Shift = (1 << iVar);
1683 int nWords = Abc_TtWordNum( nVars );
1684 for ( i = 0; i < nWords; i++ )
1685 if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
1686 return 1;
1687 return 0;
1688 }
1689 else
1690 {
1691 int i, Step = (1 << (iVar - 6));
1692 word * tLimit = t + Abc_TtWordNum( nVars );
1693 for ( ; t < tLimit; t += 2*Step )
1694 for ( i = 0; i < Step; i++ )
1695 if ( t[i] != t[Step+i] )
1696 return 1;
1697 return 0;
1698 }
1699}
1700static inline int Abc_TtSupport( word * t, int nVars )
1701{
1702 int v, Supp = 0;
1703 for ( v = 0; v < nVars; v++ )
1704 if ( Abc_TtHasVar( t, nVars, v ) )
1705 Supp |= (1 << v);
1706 return Supp;
1707}
1708static inline int Abc_TtSupportSize( word * t, int nVars )
1709{
1710 int v, SuppSize = 0;
1711 for ( v = 0; v < nVars; v++ )
1712 if ( Abc_TtHasVar( t, nVars, v ) )
1713 SuppSize++;
1714 return SuppSize;
1715}
1716static inline int Abc_TtSupportAndSize( word * t, int nVars, int * pSuppSize )
1717{
1718 int v, Supp = 0;
1719 *pSuppSize = 0;
1720 for ( v = 0; v < nVars; v++ )
1721 if ( Abc_TtHasVar( t, nVars, v ) )
1722 Supp |= (1 << v), (*pSuppSize)++;
1723 return Supp;
1724}
1725static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
1726{
1727 int v, Supp = 0;
1728 *pSuppSize = 0;
1729 assert( nVars <= 6 );
1730 for ( v = 0; v < nVars; v++ )
1731 if ( Abc_Tt6HasVar( t, v ) )
1732 Supp |= (1 << v), (*pSuppSize)++;
1733 return Supp;
1734}
1735static inline int Abc_Tt6Check1( word t, int nVars )
1736{
1737 int n, v, u;
1738 for ( n = 0; n < 2; n++ )
1739 for ( v = 0; v < nVars; v++ )
1740 {
1741 word Cof = n ? Abc_Tt6Cofactor1(t, v) : Abc_Tt6Cofactor0(t, v);
1742 for ( u = 0; u < nVars; u++ )
1743 if ( v != u && !Abc_Tt6HasVar(Cof, u) )
1744 return 1;
1745 }
1746 return 0;
1747}
1748static inline int Abc_Tt6Check2( word t, int nVars )
1749{
1750 int n, v;
1751 for ( n = 0; n < 2; n++ )
1752 for ( v = 0; v < nVars; v++ )
1753 {
1754 word Cof = n ? Abc_Tt6Cofactor1(t, v) : Abc_Tt6Cofactor0(t, v);
1755 if ( Cof == 0 || ~Cof == 0 )
1756 return 1;
1757 }
1758 return 0;
1759}
1771static inline int Abc_TtCheckCondDep2( word * pTruth, int nVars, int nSuppLim )
1772{
1773 int v, d, nWords = Abc_TtWordNum(nVars);
1774 if ( nVars <= nSuppLim + 1 )
1775 return 0;
1776 for ( v = 0; v < nVars; v++ )
1777 {
1778 int nDep0 = 0, nDep1 = 0;
1779 for ( d = 0; d < nVars; d++ )
1780 {
1781 if ( v == d )
1782 continue;
1783 if ( v < d )
1784 {
1785 nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 0, 2 );
1786 nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 1, 3 );
1787 }
1788 else // if ( v > d )
1789 {
1790 nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 0, 1 );
1791 nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 2, 3 );
1792 }
1793 if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
1794 break;
1795 }
1796 if ( d == nVars )
1797 return v;
1798 }
1799 return nVars;
1800}
1801static inline int Abc_TtCheckCondDep( word * pTruth, int nVars, int nSuppLim )
1802{
1803 int nVarsMax = 13;
1804 word Cof0[128], Cof1[128]; // pow( 2, nVarsMax-6 )
1805 int v, d, nWords = Abc_TtWordNum(nVars);
1806 assert( nVars <= nVarsMax );
1807 if ( nVars <= nSuppLim + 1 )
1808 return 0;
1809 for ( v = 0; v < nVars; v++ )
1810 {
1811 int nDep0 = 0, nDep1 = 0;
1812 Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
1813 Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
1814 for ( d = 0; d < nVars; d++ )
1815 {
1816 if ( v == d )
1817 continue;
1818 nDep0 += Abc_TtHasVar( Cof0, nVars, d );
1819 nDep1 += Abc_TtHasVar( Cof1, nVars, d );
1820 if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
1821 break;
1822 }
1823 if ( d == nVars )
1824 return v;
1825 }
1826 return nVars;
1827}
1828
1829
1841static inline int Abc_TtOnlyOneOne( word t )
1842{
1843 if ( t == 0 )
1844 return 0;
1845 return (t & (t-1)) == 0;
1846}
1847static inline int Abc_Tt6IsAndType( word t, int nVars )
1848{
1849 return Abc_TtOnlyOneOne( t & Abc_Tt6Mask(1 << nVars) );
1850}
1851static inline int Abc_Tt6IsOrType( word t, int nVars )
1852{
1853 return Abc_TtOnlyOneOne( ~t & Abc_Tt6Mask(1 << nVars) );
1854}
1855static inline int Abc_Tt6IsXorType( word t, int nVars )
1856{
1857 return ((((t & 1) ? ~t : t) ^ s_TruthXors[nVars]) & Abc_Tt6Mask(1 << nVars)) == 0;
1858}
1859
1860
1872static inline word Abc_Tt6Flip( word Truth, int iVar )
1873{
1874 return Truth = ((Truth << (1 << iVar)) & s_Truths6[iVar]) | ((Truth & s_Truths6[iVar]) >> (1 << iVar));
1875}
1876static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
1877{
1878 if ( nWords == 1 )
1879 pTruth[0] = ((pTruth[0] << (1 << iVar)) & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
1880 else if ( iVar <= 5 )
1881 {
1882 int w, shift = (1 << iVar);
1883 for ( w = 0; w < nWords; w++ )
1884 pTruth[w] = ((pTruth[w] << shift) & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
1885 }
1886 else // if ( iVar > 5 )
1887 {
1888 word * pLimit = pTruth + nWords;
1889 int i, iStep = Abc_TtWordNum(iVar);
1890 for ( ; pTruth < pLimit; pTruth += 2*iStep )
1891 for ( i = 0; i < iStep; i++ )
1892 ABC_SWAP( word, pTruth[i], pTruth[i + iStep] );
1893 }
1894}
1895
1907static inline word Abc_Tt6SwapAdjacent( word Truth, int iVar )
1908{
1909 return (Truth & s_PMasks[iVar][0]) | ((Truth & s_PMasks[iVar][1]) << (1 << iVar)) | ((Truth & s_PMasks[iVar][2]) >> (1 << iVar));
1910}
1911static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
1912{
1913 if ( iVar < 5 )
1914 {
1915 int i, Shift = (1 << iVar);
1916 for ( i = 0; i < nWords; i++ )
1917 pTruth[i] = (pTruth[i] & s_PMasks[iVar][0]) | ((pTruth[i] & s_PMasks[iVar][1]) << Shift) | ((pTruth[i] & s_PMasks[iVar][2]) >> Shift);
1918 }
1919 else if ( iVar == 5 )
1920 {
1921 unsigned * pTruthU = (unsigned *)pTruth;
1922 unsigned * pLimitU = (unsigned *)(pTruth + nWords);
1923 for ( ; pTruthU < pLimitU; pTruthU += 4 )
1924 ABC_SWAP( unsigned, pTruthU[1], pTruthU[2] );
1925 }
1926 else // if ( iVar > 5 )
1927 {
1928 word * pLimit = pTruth + nWords;
1929 int i, iStep = Abc_TtWordNum(iVar);
1930 for ( ; pTruth < pLimit; pTruth += 4*iStep )
1931 for ( i = 0; i < iStep; i++ )
1932 ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] );
1933 }
1934}
1935static inline word Abc_Tt6SwapVars( word t, int iVar, int jVar )
1936{
1937 word * s_PMasks = s_PPMasks[iVar][jVar];
1938 int shift = (1 << jVar) - (1 << iVar);
1939 assert( iVar < jVar );
1940 return (t & s_PMasks[0]) | ((t & s_PMasks[1]) << shift) | ((t & s_PMasks[2]) >> shift);
1941}
1942static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
1943{
1944 if ( iVar == jVar )
1945 return;
1946 if ( jVar < iVar )
1947 ABC_SWAP( int, iVar, jVar );
1948 assert( iVar < jVar && jVar < nVars );
1949 if ( nVars <= 6 )
1950 {
1951 pTruth[0] = Abc_Tt6SwapVars( pTruth[0], iVar, jVar );
1952 return;
1953 }
1954 if ( jVar <= 5 )
1955 {
1956 word * s_PMasks = s_PPMasks[iVar][jVar];
1957 int nWords = Abc_TtWordNum(nVars);
1958 int w, shift = (1 << jVar) - (1 << iVar);
1959 for ( w = 0; w < nWords; w++ )
1960 pTruth[w] = (pTruth[w] & s_PMasks[0]) | ((pTruth[w] & s_PMasks[1]) << shift) | ((pTruth[w] & s_PMasks[2]) >> shift);
1961 return;
1962 }
1963 if ( iVar <= 5 && jVar > 5 )
1964 {
1965 word low2High, high2Low;
1966 word * pLimit = pTruth + Abc_TtWordNum(nVars);
1967 int j, jStep = Abc_TtWordNum(jVar);
1968 int shift = 1 << iVar;
1969 for ( ; pTruth < pLimit; pTruth += 2*jStep )
1970 for ( j = 0; j < jStep; j++ )
1971 {
1972 low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
1973 high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
1974 pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
1975 pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
1976 }
1977 return;
1978 }
1979 {
1980 word * pLimit = pTruth + Abc_TtWordNum(nVars);
1981 int i, iStep = Abc_TtWordNum(iVar);
1982 int j, jStep = Abc_TtWordNum(jVar);
1983 for ( ; pTruth < pLimit; pTruth += 2*jStep )
1984 for ( i = 0; i < jStep; i += 2*iStep )
1985 for ( j = 0; j < iStep; j++ )
1986 ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] );
1987 return;
1988 }
1989}
1990// moves one var (v) to the given position (p)
1991static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, int v, int p )
1992{
1993 int iVar = V2P[v], jVar = p;
1994 if ( iVar == jVar )
1995 return;
1996 Abc_TtSwapVars( pF, nVars, iVar, jVar );
1997 V2P[P2V[iVar]] = jVar;
1998 V2P[P2V[jVar]] = iVar;
1999 P2V[iVar] ^= P2V[jVar];
2000 P2V[jVar] ^= P2V[iVar];
2001 P2V[iVar] ^= P2V[jVar];
2002}
2003static inline word Abc_Tt6RemoveVar( word t, int iVar )
2004{
2005 assert( !Abc_Tt6HasVar(t, iVar) );
2006 while ( iVar < 5 )
2007 t = Abc_Tt6SwapAdjacent( t, iVar++ );
2008 return t;
2009}
2010// permutes two variables while keeping track of their places
2011static inline void Abc_TtPermuteTwo( word * p, int nTTVars, int * Var2Pla, int * Pla2Var, int Var0, int Var1 )
2012{
2013 int iPlace0 = Var2Pla[Var0];
2014 int iPlace1 = Var2Pla[Var1];
2015 if ( iPlace0 == iPlace1 )
2016 return;
2017 Abc_TtSwapVars( p, nTTVars, iPlace0, iPlace1 );
2018 Var2Pla[Pla2Var[iPlace0]] = iPlace1;
2019 Var2Pla[Pla2Var[iPlace1]] = iPlace0;
2020 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
2021 Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
2022 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
2023}
2024// restores natural variable order
2025static inline void Abc_TtRestoreOrder( word * p, int nTTVars, int * Var2Pla, int * Pla2Var, int nPermVars )
2026{
2027 int i;
2028 for ( i = 0; i < nPermVars; i++ )
2029 Abc_TtPermuteTwo( p, nTTVars, Var2Pla, Pla2Var, i, Var2Pla[i] );
2030}
2031
2043static inline word Abc_Tt6Permute_rec( word t, int * pPerm, int nVars )
2044{
2045 word uRes0, uRes1; int Var;
2046 if ( t == 0 ) return 0;
2047 if ( ~t == 0 ) return ~(word)0;
2048 for ( Var = nVars-1; Var >= 0; Var-- )
2049 if ( Abc_Tt6HasVar( t, Var ) )
2050 break;
2051 assert( Var >= 0 );
2052 uRes0 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor0(t, Var), pPerm, Var );
2053 uRes1 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor1(t, Var), pPerm, Var );
2054 return (uRes0 & s_Truths6Neg[pPerm[Var]]) | (uRes1 & s_Truths6[pPerm[Var]]);
2055}
2056static inline void Abc_TtPermute( word * p, int * pPerm, int nVars )
2057{
2058 int v, UnPerm[16], Perm[16];
2059 assert( nVars <= 16 );
2060 for ( v = 0; v < nVars; v++ )
2061 UnPerm[v] = Perm[v] = v;
2062 for ( v = nVars-1; v >= 0; v-- )
2063 {
2064 int Lev = UnPerm[pPerm[v]];
2065 if ( v == Lev )
2066 continue;
2067 Abc_TtSwapVars( p, nVars, v, Lev );
2068 ABC_SWAP( int, Perm[v], Perm[Lev] );
2069 UnPerm[Perm[Lev]] = Lev;
2070 UnPerm[Perm[v]] = v;
2071 }
2072 for ( v = 0; v < nVars; v++ )
2073 assert( Perm[v] == pPerm[v] );
2074}
2075static inline void Abc_TtUnpermute( word * p, int * pPerm, int nVars )
2076{
2077 int v, Perm[16];
2078 assert( nVars <= 16 );
2079 for ( v = 0; v < nVars; v++ )
2080 Perm[v] = pPerm[v];
2081 for ( v = nVars-1; v >= 0; v-- )
2082 {
2083 while ( v != Perm[v] )
2084 {
2085 int vCur = Perm[v];
2086 Abc_TtSwapVars( p, nVars, v, vCur );
2087 Perm[v] = Perm[vCur];
2088 Perm[vCur]= vCur;
2089 }
2090 }
2091 for ( v = 0; v < nVars; v++ )
2092 assert( Perm[v] == v );
2093}
2094
2106static inline void Abc_TtShrink( word * pF, int nVars, int nVarsAll, unsigned Phase )
2107{
2108 int i, k, Var = 0;
2109 assert( nVarsAll <= 16 );
2110 for ( i = 0; i < nVarsAll; i++ )
2111 if ( Phase & (1 << i) )
2112 {
2113 for ( k = i-1; k >= Var; k-- )
2114 Abc_TtSwapAdjacent( pF, Abc_TtWordNum(nVarsAll), k );
2115 Var++;
2116 }
2117 assert( Var == nVars );
2118}
2119static inline int Abc_TtMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars )
2120{
2121 int v, iVar = 0, uSupp = 0;
2122 assert( nVarsAll <= 16 );
2123 for ( v = 0; v < nVarsAll; v++ )
2124 if ( Abc_TtHasVar( t, nVarsAll, v ) )
2125 {
2126 uSupp |= (1 << v);
2127 if ( pSupp )
2128 pSupp[iVar] = pSupp[v];
2129 iVar++;
2130 }
2131 if ( pnVars )
2132 *pnVars = iVar;
2133 if ( uSupp == 0 || Abc_TtSuppIsMinBase( uSupp ) )
2134 return 0;
2135 Abc_TtShrink( t, iVar, nVarsAll, uSupp );
2136 return 1;
2137}
2138static inline int Abc_TtSimplify( word * t, int * pLits, int nVarsAll, int * pnVars )
2139{
2140 int v, u;
2141 for ( v = 0; v < nVarsAll; v++ )
2142 {
2143 if ( pLits[v] == 0 )
2144 Abc_TtCofactor0( t, Abc_TtWordNum(nVarsAll), v );
2145 else if ( pLits[v] == 1 )
2146 Abc_TtCofactor1( t, Abc_TtWordNum(nVarsAll), v );
2147 }
2148 for ( v = 0; v < nVarsAll; v++ )
2149 for ( u = v+1; u < nVarsAll; u++ )
2150 if ( Abc_Lit2Var(pLits[v]) == Abc_Lit2Var(pLits[u]) )
2151 {
2152 assert( nVarsAll <= 6 );
2153 if ( pLits[v] == pLits[u] )
2154 {
2155 word t0 = Abc_Tt6Cofactor0(Abc_Tt6Cofactor0(*t, v), u);
2156 word t1 = Abc_Tt6Cofactor1(Abc_Tt6Cofactor1(*t, v), u);
2157 *t = (t0 & s_Truths6Neg[v]) | (t1 & s_Truths6[v]);
2158 }
2159 else // if ( pLits[v] == Abc_LitNot(pLits[u]) )
2160 {
2161 word t0 = Abc_Tt6Cofactor1(Abc_Tt6Cofactor0(*t, v), u);
2162 word t1 = Abc_Tt6Cofactor0(Abc_Tt6Cofactor1(*t, v), u);
2163 *t = (t0 & s_Truths6Neg[v]) | (t1 & s_Truths6[v]);
2164 }
2165 }
2166 return Abc_TtMinimumBase( t, pLits, nVarsAll, pnVars );
2167}
2168
2180static inline word Abc_Tt6Expand( word t, int * pCut0, int nCutSize0, int * pCut, int nCutSize )
2181{
2182 int i, k;
2183 for ( i = nCutSize - 1, k = nCutSize0 - 1; i >= 0 && k >= 0; i-- )
2184 {
2185 if ( pCut[i] > pCut0[k] )
2186 continue;
2187 assert( pCut[i] == pCut0[k] );
2188 if ( k < i )
2189 t = Abc_Tt6SwapVars( t, k, i );
2190 k--;
2191 }
2192 assert( k == -1 );
2193 return t;
2194}
2195static inline void Abc_TtExpand( word * pTruth0, int nVars, int * pCut0, int nCutSize0, int * pCut, int nCutSize )
2196{
2197 int i, k;
2198 for ( i = nCutSize - 1, k = nCutSize0 - 1; i >= 0 && k >= 0; i-- )
2199 {
2200 if ( pCut[i] > pCut0[k] )
2201 continue;
2202 assert( pCut[i] == pCut0[k] );
2203 if ( k < i )
2204 Abc_TtSwapVars( pTruth0, nVars, k, i );
2205 k--;
2206 }
2207 assert( k == -1 );
2208}
2209static inline int Abc_Tt6MinBase( word * pTruth, int * pVars, int nVars )
2210{
2211 word t = *pTruth;
2212 int i, k;
2213 for ( i = k = 0; i < nVars; i++ )
2214 {
2215 if ( !Abc_Tt6HasVar( t, i ) )
2216 continue;
2217 if ( k < i )
2218 {
2219 if ( pVars ) pVars[k] = pVars[i];
2220 t = Abc_Tt6SwapVars( t, k, i );
2221 }
2222 k++;
2223 }
2224 if ( k == nVars )
2225 return k;
2226 assert( k < nVars );
2227 *pTruth = t;
2228 return k;
2229}
2230static inline int Abc_TtMinBase( word * pTruth, int * pVars, int nVars, int nVarsAll )
2231{
2232 int i, k;
2233 assert( nVars <= nVarsAll );
2234 for ( i = k = 0; i < nVars; i++ )
2235 {
2236 if ( !Abc_TtHasVar( pTruth, nVarsAll, i ) )
2237 continue;
2238 if ( k < i )
2239 {
2240 if ( pVars ) pVars[k] = pVars[i];
2241 Abc_TtSwapVars( pTruth, nVarsAll, k, i );
2242 }
2243 k++;
2244 }
2245 if ( k == nVars )
2246 return k;
2247 assert( k < nVars );
2248// assert( k == Abc_TtSupportSize(pTruth, nVars) );
2249 return k;
2250}
2251
2263static inline void Abc_TtImplementNpnConfig( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
2264{
2265 int i, k, nWords = Abc_TtWordNum( nVars );
2266 if ( (uCanonPhase >> nVars) & 1 )
2267 Abc_TtNot( pTruth, nWords );
2268 for ( i = 0; i < nVars; i++ )
2269 if ( (uCanonPhase >> i) & 1 )
2270 Abc_TtFlip( pTruth, nWords, i );
2271 if ( pCanonPerm )
2272 for ( i = 0; i < nVars; i++ )
2273 {
2274 for ( k = i; k < nVars; k++ )
2275 if ( pCanonPerm[k] == i )
2276 break;
2277 assert( k < nVars );
2278 if ( i == k )
2279 continue;
2280 Abc_TtSwapVars( pTruth, nVars, i, k );
2281 ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] );
2282 }
2283}
2284
2296static inline int Abc_TtCountOnesSlow( word t )
2297{
2298 t = (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
2299 t = (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
2300 t = (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
2301 t = (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
2302 t = (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
2303 return (t & ABC_CONST(0x00000000FFFFFFFF)) + (t>>32);
2304}
2305static inline int Abc_TtCountOnes( word x )
2306{
2307 x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
2308 x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
2309 x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
2310 x = x + (x >> 8);
2311 x = x + (x >> 16);
2312 x = x + (x >> 32);
2313 return (int)(x & 0xFF);
2314}
2315static inline int Abc_TtCountOnes2( word x )
2316{
2317 return x ? Abc_TtCountOnes(x) : 0;
2318}
2319static inline int Abc_TtCountOnesVec( word * x, int nWords )
2320{
2321 int w, Count = 0;
2322 for ( w = 0; w < nWords; w++ )
2323 Count += Abc_TtCountOnes2( x[w] );
2324 return Count;
2325}
2326static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, int fCompl )
2327{
2328 int w, Count = 0;
2329 if ( fCompl )
2330 {
2331 for ( w = 0; w < nWords; w++ )
2332 Count += Abc_TtCountOnes2( pMask[w] & ~x[w] );
2333 }
2334 else
2335 {
2336 for ( w = 0; w < nWords; w++ )
2337 Count += Abc_TtCountOnes2( pMask[w] & x[w] );
2338 }
2339 return Count;
2340}
2341static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords )
2342{
2343 int w, Count = 0;
2344 if ( !fComp0 && !fComp1 )
2345 for ( w = 0; w < nWords; w++ )
2346 Count += Abc_TtCountOnes2( pMask[w] & x0[w] & x1[w] );
2347 else if ( fComp0 && !fComp1 )
2348 for ( w = 0; w < nWords; w++ )
2349 Count += Abc_TtCountOnes2( pMask[w] & ~x0[w] & x1[w] );
2350 else if ( !fComp0 && fComp1 )
2351 for ( w = 0; w < nWords; w++ )
2352 Count += Abc_TtCountOnes2( pMask[w] & x0[w] & ~x1[w] );
2353 else
2354 for ( w = 0; w < nWords; w++ )
2355 Count += Abc_TtCountOnes2( pMask[w] & ~x0[w] & ~x1[w] );
2356 return Count;
2357}
2358static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords )
2359{
2360 int w, Count = 0;
2361 for ( w = 0; w < nWords; w++ )
2362 Count += Abc_TtCountOnes2( x[w] ^ y[w] );
2363 return Count;
2364}
2365static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords )
2366{
2367 int w, Count = 0;
2368 if ( fCompl )
2369 for ( w = 0; w < nWords; w++ )
2370 Count += Abc_TtCountOnes2( pMask[w] & (x[w] ^ ~y[w]) );
2371 else
2372 for ( w = 0; w < nWords; w++ )
2373 Count += Abc_TtCountOnes2( pMask[w] & (x[w] ^ y[w]) );
2374 return Count;
2375}
2376static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nWords )
2377{
2378 int w, Count = 0;
2379 for ( w = 0; w < nWords; w++ )
2380 {
2381 pOut[w] &= pIn1[w] ^ pIn2[w];
2382 Count += Abc_TtCountOnes2( pOut[w] );
2383 }
2384 return Count;
2385}
2386static inline void Abc_TtIsfPrint( word * pOff, word * pOn, int nWords )
2387{
2388 int nTotal = 64*nWords;
2389 int nOffset = Abc_TtCountOnesVec(pOff, nWords);
2390 int nOnset = Abc_TtCountOnesVec(pOn, nWords);
2391 int nDcset = nTotal - nOffset - nOnset;
2392 printf( "OFF =%6d (%6.2f %%) ", nOffset, 100.0*nOffset/nTotal );
2393 printf( "ON =%6d (%6.2f %%) ", nOnset, 100.0*nOnset/nTotal );
2394 printf( "DC =%6d (%6.2f %%)", nDcset, 100.0*nDcset/nTotal );
2395}
2396
2408static inline int Abc_Tt6FirstBit( word t )
2409{
2410 int n = 0;
2411 if ( t == 0 ) return -1;
2412 if ( (t & ABC_CONST(0x00000000FFFFFFFF)) == 0 ) { n += 32; t >>= 32; }
2413 if ( (t & ABC_CONST(0x000000000000FFFF)) == 0 ) { n += 16; t >>= 16; }
2414 if ( (t & ABC_CONST(0x00000000000000FF)) == 0 ) { n += 8; t >>= 8; }
2415 if ( (t & ABC_CONST(0x000000000000000F)) == 0 ) { n += 4; t >>= 4; }
2416 if ( (t & ABC_CONST(0x0000000000000003)) == 0 ) { n += 2; t >>= 2; }
2417 if ( (t & ABC_CONST(0x0000000000000001)) == 0 ) { n++; }
2418 return n;
2419}
2420static inline int Abc_Tt6LastBit( word t )
2421{
2422 int n = 0;
2423 if ( t == 0 ) return -1;
2424 if ( (t & ABC_CONST(0xFFFFFFFF00000000)) == 0 ) { n += 32; t <<= 32; }
2425 if ( (t & ABC_CONST(0xFFFF000000000000)) == 0 ) { n += 16; t <<= 16; }
2426 if ( (t & ABC_CONST(0xFF00000000000000)) == 0 ) { n += 8; t <<= 8; }
2427 if ( (t & ABC_CONST(0xF000000000000000)) == 0 ) { n += 4; t <<= 4; }
2428 if ( (t & ABC_CONST(0xC000000000000000)) == 0 ) { n += 2; t <<= 2; }
2429 if ( (t & ABC_CONST(0x8000000000000000)) == 0 ) { n++; }
2430 return 63-n;
2431}
2432static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
2433{
2434 int w, nWords = Abc_TtWordNum(nVars);
2435 for ( w = 0; w < nWords; w++ )
2436 if ( pIn[w] )
2437 return 64*w + Abc_Tt6FirstBit(pIn[w]);
2438 return -1;
2439}
2440static inline int Abc_TtFindFirstBit2( word * pIn, int nWords )
2441{
2442 int w;
2443 for ( w = 0; w < nWords; w++ )
2444 if ( pIn[w] )
2445 return 64*w + Abc_Tt6FirstBit(pIn[w]);
2446 return -1;
2447}
2448static inline int Abc_TtFindLastBit( word * pIn, int nVars )
2449{
2450 int w, nWords = Abc_TtWordNum(nVars);
2451 for ( w = nWords - 1; w >= 0; w-- )
2452 if ( pIn[w] )
2453 return 64*w + Abc_Tt6LastBit(pIn[w]);
2454 return -1;
2455}
2456static inline int Abc_TtFindLastBit2( word * pIn, int nWords )
2457{
2458 int w;
2459 for ( w = nWords - 1; w >= 0; w-- )
2460 if ( pIn[w] )
2461 return 64*w + Abc_Tt6LastBit(pIn[w]);
2462 return -1;
2463}
2464static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
2465{
2466 int w, nWords = Abc_TtWordNum(nVars);
2467 for ( w = 0; w < nWords; w++ )
2468 if ( pIn1[w] ^ pIn2[w] )
2469 return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
2470 return -1;
2471}
2472static inline int Abc_TtFindFirstDiffBit2( word * pIn1, word * pIn2, int nWords )
2473{
2474 int w;
2475 for ( w = 0; w < nWords; w++ )
2476 if ( pIn1[w] ^ pIn2[w] )
2477 return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
2478 return -1;
2479}
2480static inline int Abc_TtFindLastDiffBit( word * pIn1, word * pIn2, int nVars )
2481{
2482 int w, nWords = Abc_TtWordNum(nVars);
2483 for ( w = nWords - 1; w >= 0; w-- )
2484 if ( pIn1[w] ^ pIn2[w] )
2485 return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
2486 return -1;
2487}
2488static inline int Abc_TtFindLastDiffBit2( word * pIn1, word * pIn2, int nWords )
2489{
2490 int w;
2491 for ( w = nWords - 1; w >= 0; w-- )
2492 if ( pIn1[w] ^ pIn2[w] )
2493 return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
2494 return -1;
2495}
2496static inline int Abc_TtFindFirstAndBit2( word * pIn1, word * pIn2, int nWords )
2497{
2498 int w;
2499 for ( w = 0; w < nWords; w++ )
2500 if ( pIn1[w] & pIn2[w] )
2501 return 64*w + Abc_Tt6FirstBit(pIn1[w] & pIn2[w]);
2502 return -1;
2503}
2504static inline int Abc_TtFindLastAndBit2( word * pIn1, word * pIn2, int nWords )
2505{
2506 int w;
2507 for ( w = nWords - 1; w >= 0; w-- )
2508 if ( pIn1[w] & pIn2[w] )
2509 return 64*w + Abc_Tt6LastBit(pIn1[w] & pIn2[w]);
2510 return -1;
2511}
2512static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
2513{
2514 int w, nWords = Abc_TtWordNum(nVars);
2515 for ( w = 0; w < nWords; w++ )
2516 if ( ~pIn[w] )
2517 return 64*w + Abc_Tt6FirstBit(~pIn[w]);
2518 return -1;
2519}
2520static inline int Abc_TtFindLastZero( word * pIn, int nVars )
2521{
2522 int w, nWords = Abc_TtWordNum(nVars);
2523 for ( w = nWords - 1; w >= 0; w-- )
2524 if ( ~pIn[w] )
2525 return 64*w + Abc_Tt6LastBit(~pIn[w]);
2526 return -1;
2527}
2528
2529
2541static inline void Abc_TtReverseVars( word * pTruth, int nVars )
2542{
2543 int k;
2544 for ( k = 0; k < nVars/2 ; k++ )
2545 Abc_TtSwapVars( pTruth, nVars, k, nVars - 1 - k );
2546}
2547static inline void Abc_TtReverseBits( word * pTruth, int nVars )
2548{
2549 static unsigned char pMirror[256] = {
2550 0, 128, 64, 192, 32, 160, 96, 224, 16, 144, 80, 208, 48, 176, 112, 240,
2551 8, 136, 72, 200, 40, 168, 104, 232, 24, 152, 88, 216, 56, 184, 120, 248,
2552 4, 132, 68, 196, 36, 164, 100, 228, 20, 148, 84, 212, 52, 180, 116, 244,
2553 12, 140, 76, 204, 44, 172, 108, 236, 28, 156, 92, 220, 60, 188, 124, 252,
2554 2, 130, 66, 194, 34, 162, 98, 226, 18, 146, 82, 210, 50, 178, 114, 242,
2555 10, 138, 74, 202, 42, 170, 106, 234, 26, 154, 90, 218, 58, 186, 122, 250,
2556 6, 134, 70, 198, 38, 166, 102, 230, 22, 150, 86, 214, 54, 182, 118, 246,
2557 14, 142, 78, 206, 46, 174, 110, 238, 30, 158, 94, 222, 62, 190, 126, 254,
2558 1, 129, 65, 193, 33, 161, 97, 225, 17, 145, 81, 209, 49, 177, 113, 241,
2559 9, 137, 73, 201, 41, 169, 105, 233, 25, 153, 89, 217, 57, 185, 121, 249,
2560 5, 133, 69, 197, 37, 165, 101, 229, 21, 149, 85, 213, 53, 181, 117, 245,
2561 13, 141, 77, 205, 45, 173, 109, 237, 29, 157, 93, 221, 61, 189, 125, 253,
2562 3, 131, 67, 195, 35, 163, 99, 227, 19, 147, 83, 211, 51, 179, 115, 243,
2563 11, 139, 75, 203, 43, 171, 107, 235, 27, 155, 91, 219, 59, 187, 123, 251,
2564 7, 135, 71, 199, 39, 167, 103, 231, 23, 151, 87, 215, 55, 183, 119, 247,
2565 15, 143, 79, 207, 47, 175, 111, 239, 31, 159, 95, 223, 63, 191, 127, 255
2566 };
2567 unsigned char Temp, * pTruthC = (unsigned char *)pTruth;
2568 int i, nBytes = (nVars > 6) ? (1 << (nVars - 3)) : 8;
2569 for ( i = 0; i < nBytes/2; i++ )
2570 {
2571 Temp = pMirror[pTruthC[i]];
2572 pTruthC[i] = pMirror[pTruthC[nBytes-1-i]];
2573 pTruthC[nBytes-1-i] = Temp;
2574 }
2575}
2576
2577
2589static inline int Abc_Tt6PosVar( word t, int iVar )
2590{
2591 return ((t >> (1<<iVar)) & t & s_Truths6Neg[iVar]) == (t & s_Truths6Neg[iVar]);
2592}
2593static inline int Abc_Tt6NegVar( word t, int iVar )
2594{
2595 return ((t << (1<<iVar)) & t & s_Truths6[iVar]) == (t & s_Truths6[iVar]);
2596}
2597static inline int Abc_TtPosVar( word * t, int nVars, int iVar )
2598{
2599 assert( iVar < nVars );
2600 if ( nVars <= 6 )
2601 return Abc_Tt6PosVar( t[0], iVar );
2602 if ( iVar < 6 )
2603 {
2604 int i, Shift = (1 << iVar);
2605 int nWords = Abc_TtWordNum( nVars );
2606 for ( i = 0; i < nWords; i++ )
2607 if ( ((t[i] >> Shift) & t[i] & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
2608 return 0;
2609 return 1;
2610 }
2611 else
2612 {
2613 int i, Step = (1 << (iVar - 6));
2614 word * tLimit = t + Abc_TtWordNum( nVars );
2615 for ( ; t < tLimit; t += 2*Step )
2616 for ( i = 0; i < Step; i++ )
2617 if ( t[i] != (t[i] & t[Step+i]) )
2618 return 0;
2619 return 1;
2620 }
2621}
2622static inline int Abc_TtNegVar( word * t, int nVars, int iVar )
2623{
2624 assert( iVar < nVars );
2625 if ( nVars <= 6 )
2626 return Abc_Tt6NegVar( t[0], iVar );
2627 if ( iVar < 6 )
2628 {
2629 int i, Shift = (1 << iVar);
2630 int nWords = Abc_TtWordNum( nVars );
2631 for ( i = 0; i < nWords; i++ )
2632 if ( ((t[i] << Shift) & t[i] & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
2633 return 0;
2634 return 1;
2635 }
2636 else
2637 {
2638 int i, Step = (1 << (iVar - 6));
2639 word * tLimit = t + Abc_TtWordNum( nVars );
2640 for ( ; t < tLimit; t += 2*Step )
2641 for ( i = 0; i < Step; i++ )
2642 if ( (t[i] & t[Step+i]) != t[Step+i] )
2643 return 0;
2644 return 1;
2645 }
2646}
2647static inline int Abc_TtIsUnate( word * t, int nVars )
2648{
2649 int i;
2650 for ( i = 0; i < nVars; i++ )
2651 if ( !Abc_TtNegVar(t, nVars, i) && !Abc_TtPosVar(t, nVars, i) )
2652 return 0;
2653 return 1;
2654}
2655static inline int Abc_TtIsPosUnate( word * t, int nVars )
2656{
2657 int i;
2658 for ( i = 0; i < nVars; i++ )
2659 if ( !Abc_TtPosVar(t, nVars, i) )
2660 return 0;
2661 return 1;
2662}
2663static inline void Abc_TtMakePosUnate( word * t, int nVars )
2664{
2665 int i, nWords = Abc_TtWordNum(nVars);
2666 for ( i = 0; i < nVars; i++ )
2667 if ( Abc_TtNegVar(t, nVars, i) )
2668 Abc_TtFlip( t, nWords, i );
2669 else assert( Abc_TtPosVar(t, nVars, i) );
2670}
2671
2672
2684static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars, int * pnCubes )
2685{
2686 word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
2687 int Var;
2688 assert( nVars <= 6 );
2689 assert( (uOn & ~uOnDc) == 0 );
2690 if ( uOn == 0 )
2691 return 0;
2692 if ( uOnDc == ~(word)0 )
2693 {
2694 (*pnCubes)++;
2695 return ~(word)0;
2696 }
2697 assert( nVars > 0 );
2698 // find the topmost var
2699 for ( Var = nVars-1; Var >= 0; Var-- )
2700 if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
2701 break;
2702 assert( Var >= 0 );
2703 // cofactor
2704 uOn0 = Abc_Tt6Cofactor0( uOn, Var );
2705 uOn1 = Abc_Tt6Cofactor1( uOn , Var );
2706 uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
2707 uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
2708 // solve for cofactors
2709 uRes0 = Abc_Tt6Isop( uOn0 & ~uOnDc1, uOnDc0, Var, pnCubes );
2710 uRes1 = Abc_Tt6Isop( uOn1 & ~uOnDc0, uOnDc1, Var, pnCubes );
2711 uRes2 = Abc_Tt6Isop( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pnCubes );
2712 // derive the final truth table
2713 uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
2714 assert( (uOn & ~uRes2) == 0 );
2715 assert( (uRes2 & ~uOnDc) == 0 );
2716 return uRes2;
2717}
2718static inline int Abc_Tt7Isop( word uOn[2], word uOnDc[2], int nVars, word uRes[2] )
2719{
2720 int nCubes = 0;
2721 if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
2722 uRes[0] = uRes[1] = Abc_Tt6Isop( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), &nCubes );
2723 else
2724 {
2725 word uRes0, uRes1, uRes2;
2726 assert( nVars == 7 );
2727 // solve for cofactors
2728 uRes0 = Abc_Tt6Isop( uOn[0] & ~uOnDc[1], uOnDc[0], 6, &nCubes );
2729 uRes1 = Abc_Tt6Isop( uOn[1] & ~uOnDc[0], uOnDc[1], 6, &nCubes );
2730 uRes2 = Abc_Tt6Isop( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, &nCubes );
2731 // derive the final truth table
2732 uRes[0] = uRes2 | uRes0;
2733 uRes[1] = uRes2 | uRes1;
2734 assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
2735 assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
2736 }
2737 return nCubes;
2738}
2739static inline int Abc_Tt8Isop( word uOn[4], word uOnDc[4], int nVars, word uRes[4] )
2740{
2741 int nCubes = 0;
2742 if ( nVars <= 6 )
2743 uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6Isop( uOn[0], uOnDc[0], nVars, &nCubes );
2744 else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
2745 {
2746 nCubes = Abc_Tt7Isop( uOn, uOnDc, 7, uRes );
2747 uRes[2] = uRes[0];
2748 uRes[3] = uRes[1];
2749 }
2750 else
2751 {
2752 word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
2753 assert( nVars == 8 );
2754 // cofactor
2755 uOn0[0] = uOn[0] & ~uOnDc[2];
2756 uOn0[1] = uOn[1] & ~uOnDc[3];
2757 uOn1[0] = uOn[2] & ~uOnDc[0];
2758 uOn1[1] = uOn[3] & ~uOnDc[1];
2759 uOnDc2[0] = uOnDc[0] & uOnDc[2];
2760 uOnDc2[1] = uOnDc[1] & uOnDc[3];
2761 // solve for cofactors
2762 nCubes += Abc_Tt7Isop( uOn0, uOnDc+0, 7, uRes0 );
2763 nCubes += Abc_Tt7Isop( uOn1, uOnDc+2, 7, uRes1 );
2764 uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
2765 uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
2766 nCubes += Abc_Tt7Isop( uOn2, uOnDc2, 7, uRes2 );
2767 // derive the final truth table
2768 uRes[0] = uRes2[0] | uRes0[0];
2769 uRes[1] = uRes2[1] | uRes0[1];
2770 uRes[2] = uRes2[0] | uRes1[0];
2771 uRes[3] = uRes2[1] | uRes1[1];
2772 assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
2773 assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
2774 }
2775 return nCubes;
2776}
2777
2789static inline int Abc_Tt6CnfSize( word t, int nVars )
2790{
2791 int nCubes = 0;
2792 Abc_Tt6Isop( t, t, nVars, &nCubes );
2793 Abc_Tt6Isop( ~t, ~t, nVars, &nCubes );
2794 assert( nCubes <= 64 );
2795 return nCubes;
2796}
2797static inline int Abc_Tt8CnfSize( word t[4], int nVars )
2798{
2799 word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
2800 int nCubes = 0;
2801 nCubes += Abc_Tt8Isop( t, t, nVars, uRes );
2802 nCubes += Abc_Tt8Isop( tc, tc, nVars, uRes );
2803 assert( nCubes <= 256 );
2804 return nCubes;
2805}
2806
2818static inline word Abc_Tt6IsopCover( word uOn, word uOnDc, int nVars, int * pCover, int * pnCubes )
2819{
2820 word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
2821 int c, Var, nBeg0, nEnd0, nEnd1;
2822 assert( nVars <= 6 );
2823 assert( (uOn & ~uOnDc) == 0 );
2824 if ( uOn == 0 )
2825 return 0;
2826 if ( uOnDc == ~(word)0 )
2827 {
2828 pCover[(*pnCubes)++] = 0;
2829 return ~(word)0;
2830 }
2831 assert( nVars > 0 );
2832 // find the topmost var
2833 for ( Var = nVars-1; Var >= 0; Var-- )
2834 if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
2835 break;
2836 assert( Var >= 0 );
2837 // cofactor
2838 uOn0 = Abc_Tt6Cofactor0( uOn, Var );
2839 uOn1 = Abc_Tt6Cofactor1( uOn , Var );
2840 uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
2841 uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
2842 // solve for cofactors
2843 nBeg0 = *pnCubes;
2844 uRes0 = Abc_Tt6IsopCover( uOn0 & ~uOnDc1, uOnDc0, Var, pCover, pnCubes );
2845 nEnd0 = *pnCubes;
2846 uRes1 = Abc_Tt6IsopCover( uOn1 & ~uOnDc0, uOnDc1, Var, pCover, pnCubes );
2847 nEnd1 = *pnCubes;
2848 uRes2 = Abc_Tt6IsopCover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pCover, pnCubes );
2849 // derive the final truth table
2850 uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
2851 for ( c = nBeg0; c < nEnd0; c++ )
2852 pCover[c] |= (1 << (2*Var+0));
2853 for ( c = nEnd0; c < nEnd1; c++ )
2854 pCover[c] |= (1 << (2*Var+1));
2855 assert( (uOn & ~uRes2) == 0 );
2856 assert( (uRes2 & ~uOnDc) == 0 );
2857 return uRes2;
2858}
2859static inline void Abc_Tt7IsopCover( word uOn[2], word uOnDc[2], int nVars, word uRes[2], int * pCover, int * pnCubes )
2860{
2861 if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
2862 uRes[0] = uRes[1] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), pCover, pnCubes );
2863 else
2864 {
2865 word uRes0, uRes1, uRes2;
2866 int c, nBeg0, nEnd0, nEnd1;
2867 assert( nVars == 7 );
2868 // solve for cofactors
2869 nBeg0 = *pnCubes;
2870 uRes0 = Abc_Tt6IsopCover( uOn[0] & ~uOnDc[1], uOnDc[0], 6, pCover, pnCubes );
2871 nEnd0 = *pnCubes;
2872 uRes1 = Abc_Tt6IsopCover( uOn[1] & ~uOnDc[0], uOnDc[1], 6, pCover, pnCubes );
2873 nEnd1 = *pnCubes;
2874 uRes2 = Abc_Tt6IsopCover( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, pCover, pnCubes );
2875 // derive the final truth table
2876 uRes[0] = uRes2 | uRes0;
2877 uRes[1] = uRes2 | uRes1;
2878 for ( c = nBeg0; c < nEnd0; c++ )
2879 pCover[c] |= (1 << (2*6+0));
2880 for ( c = nEnd0; c < nEnd1; c++ )
2881 pCover[c] |= (1 << (2*6+1));
2882 assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
2883 assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
2884 }
2885}
2886static inline void Abc_Tt8IsopCover( word uOn[4], word uOnDc[4], int nVars, word uRes[4], int * pCover, int * pnCubes )
2887{
2888 if ( nVars <= 6 )
2889 uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], nVars, pCover, pnCubes );
2890 else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
2891 {
2892 Abc_Tt7IsopCover( uOn, uOnDc, 7, uRes, pCover, pnCubes );
2893 uRes[2] = uRes[0];
2894 uRes[3] = uRes[1];
2895 }
2896 else
2897 {
2898 word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
2899 int c, nBeg0, nEnd0, nEnd1;
2900 assert( nVars == 8 );
2901 // cofactor
2902 uOn0[0] = uOn[0] & ~uOnDc[2];
2903 uOn0[1] = uOn[1] & ~uOnDc[3];
2904 uOn1[0] = uOn[2] & ~uOnDc[0];
2905 uOn1[1] = uOn[3] & ~uOnDc[1];
2906 uOnDc2[0] = uOnDc[0] & uOnDc[2];
2907 uOnDc2[1] = uOnDc[1] & uOnDc[3];
2908 // solve for cofactors
2909 nBeg0 = *pnCubes;
2910 Abc_Tt7IsopCover( uOn0, uOnDc+0, 7, uRes0, pCover, pnCubes );
2911 nEnd0 = *pnCubes;
2912 Abc_Tt7IsopCover( uOn1, uOnDc+2, 7, uRes1, pCover, pnCubes );
2913 nEnd1 = *pnCubes;
2914 uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
2915 uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
2916 Abc_Tt7IsopCover( uOn2, uOnDc2, 7, uRes2, pCover, pnCubes );
2917 // derive the final truth table
2918 uRes[0] = uRes2[0] | uRes0[0];
2919 uRes[1] = uRes2[1] | uRes0[1];
2920 uRes[2] = uRes2[0] | uRes1[0];
2921 uRes[3] = uRes2[1] | uRes1[1];
2922 for ( c = nBeg0; c < nEnd0; c++ )
2923 pCover[c] |= (1 << (2*7+0));
2924 for ( c = nEnd0; c < nEnd1; c++ )
2925 pCover[c] |= (1 << (2*7+1));
2926 assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
2927 assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
2928 }
2929}
2930
2942static inline int Abc_Tt6Cnf( word t, int nVars, int * pCover )
2943{
2944 int c, nCubes = 0;
2945 Abc_Tt6IsopCover( t, t, nVars, pCover, &nCubes );
2946 for ( c = 0; c < nCubes; c++ )
2947 pCover[c] |= (1 << (2*nVars+0));
2948 Abc_Tt6IsopCover( ~t, ~t, nVars, pCover, &nCubes );
2949 for ( ; c < nCubes; c++ )
2950 pCover[c] |= (1 << (2*nVars+1));
2951 assert( nCubes <= 64 );
2952 return nCubes;
2953}
2954static inline int Abc_Tt8Cnf( word t[4], int nVars, int * pCover )
2955{
2956 word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
2957 int c, nCubes = 0;
2958 Abc_Tt8IsopCover( t, t, nVars, uRes, pCover, &nCubes );
2959 for ( c = 0; c < nCubes; c++ )
2960 pCover[c] |= (1 << (2*nVars+0));
2961 Abc_Tt8IsopCover( tc, tc, nVars, uRes, pCover, &nCubes );
2962 for ( ; c < nCubes; c++ )
2963 pCover[c] |= (1 << (2*nVars+1));
2964 assert( nCubes <= 256 );
2965 return nCubes;
2966}
2967
2968
2980static inline int Abc_Tt6Esop( word t, int nVars, int * pCover )
2981{
2982 word c0, c1;
2983 int Var, r0, r1, r2, Max, i;
2984 assert( nVars <= 6 );
2985 if ( t == 0 )
2986 return 0;
2987 if ( t == ~(word)0 )
2988 {
2989 if ( pCover ) *pCover = 0;
2990 return 1;
2991 }
2992 assert( nVars > 0 );
2993 // find the topmost var
2994 for ( Var = nVars-1; Var >= 0; Var-- )
2995 if ( Abc_Tt6HasVar( t, Var ) )
2996 break;
2997 assert( Var >= 0 );
2998 // cofactor
2999 c0 = Abc_Tt6Cofactor0( t, Var );
3000 c1 = Abc_Tt6Cofactor1( t, Var );
3001 // call recursively
3002 r0 = Abc_Tt6Esop( c0, Var, pCover ? pCover : NULL );
3003 r1 = Abc_Tt6Esop( c1, Var, pCover ? pCover + r0 : NULL );
3004 r2 = Abc_Tt6Esop( c0 ^ c1, Var, pCover ? pCover + r0 + r1 : NULL );
3005 Max = Abc_MaxInt( r0, Abc_MaxInt(r1, r2) );
3006 // add literals
3007 if ( pCover )
3008 {
3009 if ( Max == r0 )
3010 {
3011 for ( i = 0; i < r1; i++ )
3012 pCover[i] = pCover[r0+i];
3013 for ( i = 0; i < r2; i++ )
3014 pCover[r1+i] = pCover[r0+r1+i] | (1 << (2*Var+0));
3015 }
3016 else if ( Max == r1 )
3017 {
3018 for ( i = 0; i < r2; i++ )
3019 pCover[r0+i] = pCover[r0+r1+i] | (1 << (2*Var+1));
3020 }
3021 else
3022 {
3023 for ( i = 0; i < r0; i++ )
3024 pCover[i] |= (1 << (2*Var+0));
3025 for ( i = 0; i < r1; i++ )
3026 pCover[r0+i] |= (1 << (2*Var+1));
3027 }
3028 }
3029 return r0 + r1 + r2 - Max;
3030}
3031static inline word Abc_Tt6EsopBuild( int nVars, int * pCover, int nCubes )
3032{
3033 word p, t = 0; int c, v;
3034 for ( c = 0; c < nCubes; c++ )
3035 {
3036 p = ~(word)0;
3037 for ( v = 0; v < nVars; v++ )
3038 if ( ((pCover[c] >> (v << 1)) & 3) == 1 )
3039 p &= ~s_Truths6[v];
3040 else if ( ((pCover[c] >> (v << 1)) & 3) == 2 )
3041 p &= s_Truths6[v];
3042 t ^= p;
3043 }
3044 return t;
3045}
3046static inline int Abc_Tt6EsopVerify( word t, int nVars )
3047{
3048 int pCover[64];
3049 int nCubes = Abc_Tt6Esop( t, nVars, pCover );
3050 word t2 = Abc_Tt6EsopBuild( nVars, pCover, nCubes );
3051 if ( t != t2 )
3052 printf( "Verification failed.\n" );
3053 return nCubes;
3054}
3055
3067static inline int Abc_Tt6CheckOutDec( word t, int i, word * pOut )
3068{
3069 word c0 = Abc_Tt6Cofactor0( t, i );
3070 word c1 = Abc_Tt6Cofactor1( t, i );
3071 assert( c0 != c1 );
3072 if ( c0 == 0 ) // F = i * G
3073 {
3074 if ( pOut ) *pOut = c1;
3075 return 0;
3076 }
3077 if ( c1 == 0 ) // F = ~i * G
3078 {
3079 if ( pOut ) *pOut = c0;
3080 return 1;
3081 }
3082 if ( ~c0 == 0 ) // F = ~i + G
3083 {
3084 if ( pOut ) *pOut = c1;
3085 return 2;
3086 }
3087 if ( ~c1 == 0 ) // F = i + G
3088 {
3089 if ( pOut ) *pOut = c0;
3090 return 3;
3091 }
3092 if ( c0 == ~c1 ) // F = i # G
3093 {
3094 if ( pOut ) *pOut = c0;
3095 return 4;
3096 }
3097 return -1;
3098}
3099static inline int Abc_TtCheckOutDec( word * pTruth, int nVars, int v, word * pOut )
3100{
3101 word Cof0[4], Cof1[4];
3102 int nWords = Abc_TtWordNum(nVars);
3103 assert( nVars <= 8 );
3104 Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
3105 Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
3106 assert( !Abc_TtEqual(Cof0, Cof1, nWords) );
3107 if ( Abc_TtIsConst0(Cof0, nWords) ) //if ( c0 == 0 ) // F = i * G
3108 {
3109 if ( pOut ) Abc_TtCopy( pOut, Cof1, nWords, 0 ); //*pOut = c1;
3110 return 0;
3111 }
3112 if ( Abc_TtIsConst0(Cof1, nWords) ) //if ( c1 == 0 ) // F = ~i * G
3113 {
3114 if ( pOut ) Abc_TtCopy( pOut, Cof0, nWords, 0 ); //*pOut = c0;
3115 return 1;
3116 }
3117 if ( Abc_TtIsConst1(Cof0, nWords) ) //if ( ~c0 == 0 ) // F = ~i + G
3118 {
3119 if ( pOut ) Abc_TtCopy( pOut, Cof1, nWords, 0 ); //*pOut = c1;
3120 return 2;
3121 }
3122 if ( Abc_TtIsConst1(Cof1, nWords) ) //if ( ~c1 == 0 ) // F = i + G
3123 {
3124 if ( pOut ) Abc_TtCopy( pOut, Cof0, nWords, 0 ); //*pOut = c0;
3125 return 3;
3126 }
3127 if ( Abc_TtOpposite(Cof0, Cof1, nWords) ) //if ( c0 == ~c1 ) // F = i # G
3128 {
3129 if ( pOut ) Abc_TtCopy( pOut, Cof0, nWords, 0 ); //*pOut = c0;
3130 return 4;
3131 }
3132 return -1;
3133}
3134static inline word Abc_TtCheckDecOutOne7( word * t, int * piVar, int * pType )
3135{
3136 int v, Type, Type2; word Out[2];
3137 for ( v = 6; v >= 0; v-- )
3138 if ( (Type = Abc_TtCheckOutDec(t, 7, v, NULL)) != -1 )
3139 {
3140 Abc_TtSwapVars( t, 7, 6, v );
3141 Type2 = Abc_TtCheckOutDec( t, 7, 6, Out );
3142 assert( Type == Type2 );
3143 *piVar = v;
3144 *pType = Type;
3145 return Out[0];
3146 }
3147 return 0;
3148}
3149static inline word Abc_TtCheckDecOutOne8( word * t, int * piVar1, int * piVar2, int * pType1, int * pType2 )
3150{
3151 int v, Type1, Type12, Type2, Type22; word Out[4], Out2[2];
3152 for ( v = 7; v >= 0; v-- )
3153 if ( (Type1 = Abc_TtCheckOutDec(t, 8, v, NULL)) != -1 )
3154 {
3155 Abc_TtSwapVars( t, 8, 7, v );
3156 Type12 = Abc_TtCheckOutDec( t, 8, 7, Out );
3157 assert( Type1 == Type12 );
3158 *piVar1 = v;
3159 *pType1 = Type1;
3160 break;
3161 }
3162 if ( v == -1 )
3163 return 0;
3164 for ( v = 6; v >= 0; v-- )
3165 if ( (Type2 = Abc_TtCheckOutDec(Out, 7, v, NULL)) != -1 && Abc_Lit2Var(Type2) == Abc_Lit2Var(Type1) )
3166 {
3167 Abc_TtSwapVars( Out, 7, 6, v );
3168 Type22 = Abc_TtCheckOutDec(Out, 7, 6, Out2);
3169 assert( Type2 == Type22 );
3170 *piVar2 = v;
3171 *pType2 = Type2;
3172 assert( *piVar2 < *piVar1 );
3173 return Out2[0];
3174 }
3175 return 0;
3176}
3177
3189static inline int Abc_TtCheckDsdAnd( word t, int i, int j, word * pOut )
3190{
3191 word c0 = Abc_Tt6Cofactor0( t, i );
3192 word c1 = Abc_Tt6Cofactor1( t, i );
3193 word c00 = Abc_Tt6Cofactor0( c0, j );
3194 word c01 = Abc_Tt6Cofactor1( c0, j );
3195 word c10 = Abc_Tt6Cofactor0( c1, j );
3196 word c11 = Abc_Tt6Cofactor1( c1, j );
3197 if ( c00 == c01 && c00 == c10 ) // i * j
3198 {
3199 if ( pOut ) *pOut = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11);
3200 return 0;
3201 }
3202 if ( c11 == c00 && c11 == c10 ) // i * !j
3203 {
3204 if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c01);
3205 return 1;
3206 }
3207 if ( c11 == c00 && c11 == c01 ) // !i * j
3208 {
3209 if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
3210 return 2;
3211 }
3212 if ( c11 == c01 && c11 == c10 ) // !i * !j
3213 {
3214 if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c00);
3215 return 3;
3216 }
3217 if ( c00 == c11 && c01 == c10 )
3218 {
3219 if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
3220 return 4;
3221 }
3222 return -1;
3223}
3224static inline int Abc_TtCheckDsdMux( word t, int i, word * pOut )
3225{
3226 word c0 = Abc_Tt6Cofactor0( t, i );
3227 word c1 = Abc_Tt6Cofactor1( t, i );
3228 word c00, c01, c10, c11;
3229 int k, fPres0, fPres1, iVar0 = -1, iVar1 = -1;
3230 for ( k = 0; k < 6; k++ )
3231 {
3232 if ( k == i ) continue;
3233 fPres0 = Abc_Tt6HasVar( c0, k );
3234 fPres1 = Abc_Tt6HasVar( c1, k );
3235 if ( fPres0 && !fPres1 )
3236 {
3237 if ( iVar0 >= 0 )
3238 return -1;
3239 iVar0 = k;
3240 }
3241 if ( !fPres0 && fPres1 )
3242 {
3243 if ( iVar1 >= 0 )
3244 return -1;
3245 iVar1 = k;
3246 }
3247 }
3248 if ( iVar0 == -1 || iVar1 == -1 )
3249 return -1;
3250 c00 = Abc_Tt6Cofactor0( c0, iVar0 );
3251 c01 = Abc_Tt6Cofactor1( c0, iVar0 );
3252 c10 = Abc_Tt6Cofactor0( c1, iVar1 );
3253 c11 = Abc_Tt6Cofactor1( c1, iVar1 );
3254 if ( c00 == c10 && c01 == c11 ) // ITE(i, iVar1, iVar0)
3255 {
3256 if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
3257 return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 0);
3258 }
3259 if ( c00 == ~c10 && c01 == ~c11 ) // ITE(i, iVar1, !iVar0)
3260 {
3261 if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
3262 return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 1);
3263 }
3264 return -1;
3265}
3266static inline void Unm_ManCheckTest2()
3267{
3268 word t, t1, Out, Var0, Var1, Var0_, Var1_;
3269 int iVar0, iVar1, i, Res;
3270 for ( iVar0 = 0; iVar0 < 6; iVar0++ )
3271 for ( iVar1 = 0; iVar1 < 6; iVar1++ )
3272 {
3273 if ( iVar0 == iVar1 )
3274 continue;
3275 Var0 = s_Truths6[iVar0];
3276 Var1 = s_Truths6[iVar1];
3277 for ( i = 0; i < 5; i++ )
3278 {
3279 Var0_ = ((i >> 0) & 1) ? ~Var0 : Var0;
3280 Var1_ = ((i >> 1) & 1) ? ~Var1 : Var1;
3281
3282 t = Var0_ & Var1_;
3283 if ( i == 4 )
3284 t = ~(Var0_ ^ Var1_);
3285
3286// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
3287
3288 Res = Abc_TtCheckDsdAnd( t, iVar0, iVar1, &Out );
3289 if ( Res == -1 )
3290 {
3291 printf( "No decomposition\n" );
3292 continue;
3293 }
3294
3295 Var0_ = s_Truths6[iVar0];
3296 Var0_ = ((Res >> 0) & 1) ? ~Var0_ : Var0_;
3297
3298 Var1_ = s_Truths6[iVar1];
3299 Var1_ = ((Res >> 1) & 1) ? ~Var1_ : Var1_;
3300
3301 t1 = Var0_ & Var1_;
3302 if ( Res == 4 )
3303 t1 = Var0_ ^ Var1_;
3304
3305 t1 = (~t1 & Abc_Tt6Cofactor0(Out, iVar0)) | (t1 & Abc_Tt6Cofactor1(Out, iVar0));
3306
3307// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
3308
3309 if ( t1 != t )
3310 printf( "Verification failed.\n" );
3311 else
3312 printf( "Verification succeeded.\n" );
3313 }
3314 }
3315}
3316static inline void Unm_ManCheckTest()
3317{
3318 word t, t1, Out, Ctrl, Var0, Var1, Ctrl_, Var0_, Var1_;
3319 int iVar0, iVar1, iCtrl, i, Res;
3320 for ( iCtrl = 0; iCtrl < 6; iCtrl++ )
3321 for ( iVar0 = 0; iVar0 < 6; iVar0++ )
3322 for ( iVar1 = 0; iVar1 < 6; iVar1++ )
3323 {
3324 if ( iCtrl == iVar0 || iCtrl == iVar1 || iVar0 == iVar1 )
3325 continue;
3326 Ctrl = s_Truths6[iCtrl];
3327 Var0 = s_Truths6[iVar0];
3328 Var1 = s_Truths6[iVar1];
3329 for ( i = 0; i < 8; i++ )
3330 {
3331 Ctrl_ = ((i >> 0) & 1) ? ~Ctrl : Ctrl;
3332 Var0_ = ((i >> 1) & 1) ? ~Var0 : Var0;
3333 Var1_ = ((i >> 2) & 1) ? ~Var1 : Var1;
3334
3335 t = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
3336
3337// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
3338
3339 Res = Abc_TtCheckDsdMux( t, iCtrl, &Out );
3340 if ( Res == -1 )
3341 {
3342 printf( "No decomposition\n" );
3343 continue;
3344 }
3345
3346// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
3347
3348 Ctrl_ = s_Truths6[iCtrl];
3349 Var0_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
3350 Var0_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var0_ : Var0_;
3351
3352 Res >>= 16;
3353 Var1_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
3354 Var1_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var1_ : Var1_;
3355
3356 t1 = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
3357
3358// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
3359// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
3360
3361 t1 = (~t1 & Abc_Tt6Cofactor0(Out, iCtrl)) | (t1 & Abc_Tt6Cofactor1(Out, iCtrl));
3362
3363// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
3364
3365 if ( t1 != t )
3366 printf( "Verification failed.\n" );
3367 else
3368 printf( "Verification succeeded.\n" );
3369 }
3370 }
3371}
3372
3373
3385static inline word Abc_TtEvalLut6( word Ins[6], word Lut, int nVars )
3386{
3387 word Cube, Res = 0; int k, i;
3388 for ( k = 0; k < (1<<nVars); k++ )
3389 {
3390 if ( ((Lut >> k) & 1) == 0 )
3391 continue;
3392 Cube = ~(word)0;
3393 for ( i = 0; i < nVars; i++ )
3394 Cube &= ((k >> i) & 1) ? Ins[i] : ~Ins[i];
3395 Res |= Cube;
3396 }
3397 return Res;
3398}
3399static inline unsigned Abc_TtEvalLut5( unsigned Ins[5], int Lut, int nVars )
3400{
3401 unsigned Cube, Res = 0; int k, i;
3402 for ( k = 0; k < (1<<nVars); k++ )
3403 {
3404 if ( ((Lut >> k) & 1) == 0 )
3405 continue;
3406 Cube = ~(unsigned)0;
3407 for ( i = 0; i < nVars; i++ )
3408 Cube &= ((k >> i) & 1) ? Ins[i] : ~Ins[i];
3409 Res |= Cube;
3410 }
3411 return Res;
3412}
3413static inline int Abc_TtEvalLut4( int Ins[4], int Lut, int nVars )
3414{
3415 int Cube, Res = 0; int k, i;
3416 for ( k = 0; k < (1<<nVars); k++ )
3417 {
3418 if ( ((Lut >> k) & 1) == 0 )
3419 continue;
3420 Cube = ~(int)0;
3421 for ( i = 0; i < nVars; i++ )
3422 Cube &= ((k >> i) & 1) ? Ins[i] : ~Ins[i];
3423 Res |= Cube;
3424 }
3425 return Res & ~(~0 << (1<<nVars));
3426}
3427
3428
3440static inline void Abc_TtComputeGraph( word * pTruth, int v, int nVars, int * pGraph )
3441{
3442 word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 )
3443 word Cof00[64], Cof01[64], Cof10[64], Cof11[64];
3444 word CofXor, CofAndTest;
3445 int i, w, nWords = Abc_TtWordNum(nVars);
3446 pGraph[v] |= (1 << v);
3447 if ( v == nVars - 1 )
3448 return;
3449 assert( v < nVars - 1 );
3450 Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
3451 Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
3452 for ( i = v + 1; i < nVars; i++ )
3453 {
3454 Abc_TtCofactor0p( Cof00, Cof0, nWords, i );
3455 Abc_TtCofactor1p( Cof01, Cof0, nWords, i );
3456 Abc_TtCofactor0p( Cof10, Cof1, nWords, i );
3457 Abc_TtCofactor1p( Cof11, Cof1, nWords, i );
3458 for ( w = 0; w < nWords; w++ )
3459 {
3460 CofXor = Cof00[w] ^ Cof01[w] ^ Cof10[w] ^ Cof11[w];
3461 CofAndTest = (Cof00[w] & Cof01[w]) | (Cof10[w] & Cof11[w]);
3462 if ( CofXor & CofAndTest )
3463 {
3464 pGraph[v] |= (1 << i);
3465 pGraph[i] |= (1 << v);
3466 }
3467 else if ( CofXor & ~CofAndTest )
3468 {
3469 pGraph[v] |= (1 << (16+i));
3470 pGraph[i] |= (1 << (16+v));
3471 }
3472 }
3473 }
3474}
3475static inline void Abc_TtPrintVarSet( int Mask, int nVars )
3476{
3477 int i;
3478 for ( i = 0; i < nVars; i++ )
3479 if ( (Mask >> i) & 1 )
3480 printf( "1" );
3481 else
3482 printf( "." );
3483}
3484static inline void Abc_TtPrintBiDec( word * pTruth, int nVars )
3485{
3486 int v, pGraph[12] = {0};
3487 assert( nVars <= 12 );
3488 for ( v = 0; v < nVars; v++ )
3489 {
3490 Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
3491 Abc_TtPrintVarSet( pGraph[v], nVars );
3492 printf( " " );
3493 Abc_TtPrintVarSet( pGraph[v] >> 16, nVars );
3494 printf( "\n" );
3495 }
3496}
3497static inline int Abc_TtVerifyBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word wThis, word wThat )
3498{
3499 int pVarsThis[12], pVarsThat[12], pVarsAll[12];
3500 int nThis = Abc_TtBitCount16(This);
3501 int nThat = Abc_TtBitCount16(That);
3502 int i, k, nWords = Abc_TtWordNum(nVars);
3503 word pThis[64] = {wThis}, pThat[64] = {wThat};
3504 assert( nVars <= 12 );
3505 for ( i = 0; i < nVars; i++ )
3506 pVarsAll[i] = i;
3507 for ( i = k = 0; i < nVars; i++ )
3508 if ( (This >> i) & 1 )
3509 pVarsThis[k++] = i;
3510 assert( k == nThis );
3511 for ( i = k = 0; i < nVars; i++ )
3512 if ( (That >> i) & 1 )
3513 pVarsThat[k++] = i;
3514 assert( k == nThat );
3515 Abc_TtStretch6( pThis, nThis, nVars );
3516 Abc_TtStretch6( pThat, nThat, nVars );
3517 Abc_TtExpand( pThis, nVars, pVarsThis, nThis, pVarsAll, nVars );
3518 Abc_TtExpand( pThat, nVars, pVarsThat, nThat, pVarsAll, nVars );
3519 for ( k = 0; k < nWords; k++ )
3520 if ( pTruth[k] != (pThis[k] & pThat[k]) )
3521 return 0;
3522 return 1;
3523}
3524static inline void Abc_TtExist( word * pTruth, int iVar, int nWords )
3525{
3526 word Cof0[64], Cof1[64];
3527 Abc_TtCofactor0p( Cof0, pTruth, nWords, iVar );
3528 Abc_TtCofactor1p( Cof1, pTruth, nWords, iVar );
3529 Abc_TtOr( pTruth, Cof0, Cof1, nWords );
3530}
3531static inline int Abc_TtCheckBiDec( word * pTruth, int nVars, int This, int That )
3532{
3533 int VarMask[2] = {This & ~That, That & ~This};
3534 int v, c, nWords = Abc_TtWordNum(nVars);
3535 word pTempR[2][64];
3536 for ( c = 0; c < 2; c++ )
3537 {
3538 Abc_TtCopy( pTempR[c], pTruth, nWords, 0 );
3539 for ( v = 0; v < nVars; v++ )
3540 if ( ((VarMask[c] >> v) & 1) )
3541 Abc_TtExist( pTempR[c], v, nWords );
3542 }
3543 for ( v = 0; v < nWords; v++ )
3544 if ( ~pTruth[v] & pTempR[0][v] & pTempR[1][v] )
3545 return 0;
3546 return 1;
3547}
3548static inline word Abc_TtDeriveBiDecOne( word * pTruth, int nVars, int This )
3549{
3550 word pTemp[64];
3551 int nThis = Abc_TtBitCount16(This);
3552 int v, nWords = Abc_TtWordNum(nVars);
3553 Abc_TtCopy( pTemp, pTruth, nWords, 0 );
3554 for ( v = 0; v < nVars; v++ )
3555 if ( !((This >> v) & 1) )
3556 Abc_TtExist( pTemp, v, nWords );
3557 Abc_TtShrink( pTemp, nThis, nVars, This );
3558 return Abc_Tt6Stretch( pTemp[0], nThis );
3559}
3560static inline void Abc_TtDeriveBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word * pThis, word * pThat )
3561{
3562 assert( Abc_TtBitCount16(This) <= nSuppLim );
3563 assert( Abc_TtBitCount16(That) <= nSuppLim );
3564 pThis[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, This );
3565 pThat[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, That );
3566 if ( !Abc_TtVerifyBiDec(pTruth, nVars, This, That, nSuppLim, pThis[0], pThat[0] ) )
3567 printf( "Bi-decomposition verification failed.\n" );
3568}
3569// detect simple case of decomposition with topmost AND gate
3570static inline int Abc_TtCheckBiDecSimple( word * pTruth, int nVars, int nSuppLim )
3571{
3572 word Cof0[64], Cof1[64];
3573 int v, Res = 0, nDecVars = 0, nWords = Abc_TtWordNum(nVars);
3574 for ( v = 0; v < nVars; v++ )
3575 {
3576 Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
3577 Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
3578 if ( !Abc_TtIsConst0(Cof0, nWords) && !Abc_TtIsConst0(Cof1, nWords) )
3579 continue;
3580 nDecVars++;
3581 Res |= 1 << v;
3582 if ( nDecVars >= nVars - nSuppLim )
3583 return ((Res ^ (int)Abc_Tt6Mask(nVars)) << 16) | Res;
3584 }
3585 return 0;
3586}
3587static inline int Abc_TtProcessBiDecInt( word * pTruth, int nVars, int nSuppLim )
3588{
3589 int i, v, Res, nSupp, CountShared = 0, pGraph[12] = {0};
3590 assert( nSuppLim < nVars && nVars <= 2 * nSuppLim && nVars <= 12 );
3591 assert( 2 <= nSuppLim && nSuppLim <= 6 );
3592 Res = Abc_TtCheckBiDecSimple( pTruth, nVars, nSuppLim );
3593 if ( Res )
3594 return Res;
3595 for ( v = 0; v < nVars; v++ )
3596 {
3597 Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
3598 nSupp = Abc_TtBitCount16(pGraph[v] & 0xFFFF);
3599 if ( nSupp > nSuppLim )
3600 {
3601 // this variable is shared - check if the limit is exceeded
3602 if ( ++CountShared > 2*nSuppLim - nVars )
3603 return 0;
3604 }
3605 else if ( nVars - nSupp <= nSuppLim )
3606 {
3607 int This = pGraph[v] & 0xFFFF;
3608 int That = This ^ (int)Abc_Tt6Mask(nVars);
3609 // find the other component
3610 int Graph = That;
3611 for ( i = 0; i < nVars; i++ )
3612 if ( (That >> i) & 1 )
3613 Graph |= pGraph[i] & 0xFFFF;
3614 // check if this can be done
3615 if ( Abc_TtBitCount16(Graph) > nSuppLim )
3616 continue;
3617 // try decomposition
3618 if ( Abc_TtCheckBiDec(pTruth, nVars, This, Graph) )
3619 return (Graph << 16) | This;
3620 }
3621 }
3622 return 0;
3623}
3624static inline int Abc_TtProcessBiDec( word * pTruth, int nVars, int nSuppLim )
3625{
3626 word pFunc[64];
3627 int Res, nWords = Abc_TtWordNum(nVars);
3628 Abc_TtCopy( pFunc, pTruth, nWords, 0 );
3629 Res = Abc_TtProcessBiDecInt( pFunc, nVars, nSuppLim );
3630 if ( Res )
3631 return Res;
3632 Abc_TtCopy( pFunc, pTruth, nWords, 1 );
3633 Res = Abc_TtProcessBiDecInt( pFunc, nVars, nSuppLim );
3634 if ( Res )
3635 return Res | (1 << 30);
3636 return 0;
3637}
3638
3650static inline void Abc_TtProcessBiDecTest( word * pTruth, int nVars, int nSuppLim )
3651{
3652 word This, That, pTemp[64];
3653 int Res, resThis, resThat;//, nThis, nThat;
3654 int nWords = Abc_TtWordNum(nVars);
3655 Abc_TtCopy( pTemp, pTruth, nWords, 0 );
3656 Res = Abc_TtProcessBiDec( pTemp, nVars, nSuppLim );
3657 if ( Res == 0 )
3658 {
3659 //Dau_DsdPrintFromTruth( pTemp, nVars );
3660 //printf( "Non_dec\n\n" );
3661 return;
3662 }
3663
3664 resThis = Res & 0xFFFF;
3665 resThat = Res >> 16;
3666
3667 Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
3668 return;
3669
3670 //if ( !(resThis & resThat) )
3671 // return;
3672
3673// Dau_DsdPrintFromTruth( pTemp, nVars );
3674
3675 //nThis = Abc_TtBitCount16(resThis);
3676 //nThat = Abc_TtBitCount16(resThat);
3677
3678 printf( "Variable sets: " );
3679 Abc_TtPrintVarSet( resThis, nVars );
3680 printf( " " );
3681 Abc_TtPrintVarSet( resThat, nVars );
3682 printf( "\n" );
3683 Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
3684// Dau_DsdPrintFromTruth( &This, nThis );
3685// Dau_DsdPrintFromTruth( &That, nThat );
3686 printf( "\n" );
3687}
3688static inline void Abc_TtProcessBiDecExperiment()
3689{
3690 int nVars = 3;
3691 int nSuppLim = 2;
3692 int Res, resThis, resThat;
3693 word This, That;
3694// word t = ABC_CONST(0x8000000000000000);
3695// word t = (s_Truths6[0] | s_Truths6[1]) & (s_Truths6[2] | s_Truths6[3] | s_Truths6[4] | s_Truths6[5]);
3696// word t = ((s_Truths6[0] & s_Truths6[1]) | (~s_Truths6[1] & s_Truths6[2]));
3697 word t = ((s_Truths6[0] | s_Truths6[1]) & (s_Truths6[1] | s_Truths6[2]));
3698 Abc_TtPrintBiDec( &t, nVars );
3699 Res = Abc_TtProcessBiDec( &t, nVars, nSuppLim );
3700 resThis = Res & 0xFFFF;
3701 resThat = Res >> 16;
3702 Abc_TtDeriveBiDec( &t, nVars, resThis, resThat, nSuppLim, &This, &That );
3703// Dau_DsdPrintFromTruth( &This, Abc_TtBitCount16(resThis) );
3704// Dau_DsdPrintFromTruth( &That, Abc_TtBitCount16(resThat) );
3705 nVars = nSuppLim;
3706 This = s_Truth26[0][0];
3707}
3708
3720static inline int Abc_Tt4Equal3( int c0, int c1, int c2, int c3 )
3721{
3722 if ( c0 == c1 && c0 == c2 ) return 3;
3723 if ( c0 == c1 && c0 == c3 ) return 2;
3724 if ( c0 == c3 && c0 == c2 ) return 1;
3725 if ( c3 == c1 && c3 == c2 ) return 0;
3726 return -1;
3727}
3728static inline int Abc_Tt4Check2( int t, int i, int j, int * f, int * r )
3729{
3730 int c0 = t & r[j];
3731 int c1 = (t & f[j]) >> (1 << j);
3732 int c00 = c0 & r[i];
3733 int c01 = (c0 & f[i]) >> (1 << i);
3734 int c10 = c1 & r[i];
3735 int c11 = (c1 & f[i]) >> (1 << i);
3736 return Abc_Tt4Equal3( c00, c01, c10, c11 );
3737}
3738static inline int Abc_Tt4CheckTwoLevel( int t )
3739{
3740 int pair1, pair2;
3741 int f[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
3742 int r[4] = { 0x5555, 0x3333, 0x0F0F, 0x00FF };
3743 if ( (pair1 = Abc_Tt4Check2(t, 0, 1, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 2, 3, f, r)) >= 0 ) return (1 << 4) | (pair2 << 2) | pair1;
3744 if ( (pair1 = Abc_Tt4Check2(t, 0, 2, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 1, 3, f, r)) >= 0 ) return (2 << 4) | (pair2 << 2) | pair1;
3745 if ( (pair1 = Abc_Tt4Check2(t, 0, 3, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 1, 2, f, r)) >= 0 ) return (3 << 4) | (pair2 << 2) | pair1;
3746 return -1;
3747}
3748static inline int Abc_Tt4CountOnes( int t )
3749{
3750 t = (t & (0x5555)) + ((t >> 1) & (0x5555));
3751 t = (t & (0x3333)) + ((t >> 2) & (0x3333));
3752 t = (t & (0x0f0f)) + ((t >> 4) & (0x0f0f));
3753 t = (t & (0x00ff)) + ((t >> 8) & (0x00ff));
3754 return t;
3755}
3756static inline int Abc_Tt4FirstBit( int t )
3757{
3758 int n = 0;
3759 if ( t == 0 ) return -1;
3760 if ( (t & 0x00FF) == 0 ) { n += 8; t >>= 8; }
3761 if ( (t & 0x000F) == 0 ) { n += 4; t >>= 4; }
3762 if ( (t & 0x0003) == 0 ) { n += 2; t >>= 2; }
3763 if ( (t & 0x0001) == 0 ) { n++; }
3764 return n;
3765}
3766static inline int Abc_Tt4Check( int t )
3767{
3768 int Count, tn = 0xFFFF & ~t;
3769 if ( t == 0x6996 || tn == 0x6996 ) return 1;
3770 if ( (t & (t-1)) == 0 ) return 1;
3771 if ( (tn & (tn-1)) == 0 ) return 1;
3772 Count = Abc_Tt4CountOnes( t );
3773 if ( Count == 7 && Abc_Tt4CheckTwoLevel(t) > 0 ) return 1;
3774 if ( Count == 9 && Abc_Tt4CheckTwoLevel(tn) > 0 ) return 1;
3775 return 0;
3776}
3777
3778
3790static inline int Abc_Tt6VarsAreSymmetric( word t, int iVar, int jVar )
3791{
3792 word * s_PMasks = s_PPMasks[iVar][jVar];
3793 int shift = (1 << jVar) - (1 << iVar);
3794 assert( iVar < jVar );
3795 return ((t & s_PMasks[1]) << shift) == (t & s_PMasks[2]);
3796}
3797static inline int Abc_Tt6VarsAreAntiSymmetric( word t, int iVar, int jVar )
3798{
3799 word * s_PMasks = s_PPMasks[iVar][jVar];
3800 int shift = (1 << jVar) + (1 << iVar);
3801 assert( iVar < jVar );
3802 return ((t & (s_PMasks[1] >> (1 << iVar))) << shift) == (t & (s_PMasks[2] << (1 << iVar)));
3803}
3804static inline int Abc_TtVarsAreSymmetric( word * pTruth, int nVars, int i, int j, word * pCof0, word * pCof1 )
3805{
3806 int nWords = Abc_TtWordNum( nVars );
3807 assert( i < nVars && j < nVars );
3808 Abc_TtCofactor0p( pCof0, pTruth, nWords, i );
3809 Abc_TtCofactor1p( pCof1, pTruth, nWords, i );
3810 Abc_TtCofactor1( pCof0, nWords, j );
3811 Abc_TtCofactor0( pCof1, nWords, j );
3812 return Abc_TtEqual( pCof0, pCof1, nWords );
3813}
3814static inline int Abc_TtVarsAreAntiSymmetric( word * pTruth, int nVars, int i, int j, word * pCof0, word * pCof1 )
3815{
3816 int nWords = Abc_TtWordNum( nVars );
3817 assert( i < nVars && j < nVars );
3818 Abc_TtCofactor0p( pCof0, pTruth, nWords, i );
3819 Abc_TtCofactor1p( pCof1, pTruth, nWords, i );
3820 Abc_TtCofactor0( pCof0, nWords, j );
3821 Abc_TtCofactor1( pCof1, nWords, j );
3822 return Abc_TtEqual( pCof0, pCof1, nWords );
3823}
3824static inline int Abc_TtIsFullySymmetric( word * pTruth, int nVars )
3825{
3826 int m, v, Polar = 0, Seen = 0;
3827 for ( m = 0; m < (1<<nVars); m++ )
3828 {
3829 int Count = 0;
3830 int Value = Abc_TtGetBit( pTruth, m );
3831 for ( v = 0; v < nVars; v++ )
3832 Count += ((m >> v) & 1);
3833 if ( (Seen >> Count) & 1 ) // seen this count
3834 {
3835 if ( Value != ((Polar >> Count) & 1) )
3836 return -1;
3837 }
3838 else // new count
3839 {
3840 Seen |= 1 << Count;
3841 if ( Value )
3842 Polar |= 1 << Count;
3843 }
3844 }
3845 return Polar;
3846}
3847static inline void Abc_TtGenFullySymmetric( word * pTruth, int nVars, int Polar )
3848{
3849 int m, v, nWords = Abc_TtWordNum( nVars );
3850 Abc_TtClear( pTruth, nWords );
3851 for ( m = 0; m < (1<<nVars); m++ )
3852 {
3853 int Count = 0;
3854 for ( v = 0; v < nVars; v++ )
3855 Count += ((m >> v) & 1);
3856 if ( (Polar >> Count) & 1 )
3857 Abc_TtSetBit( pTruth, m );
3858 }
3859}
3860static inline void Abc_TtTestFullySymmetric()
3861{
3862 word pTruth[4]; // 8-var function
3863 int PolarOut, PolarIn = 271;
3864 Abc_TtGenFullySymmetric( pTruth, 8, PolarIn );
3865 //Abc_TtXorBit( pTruth, 171 );
3866 PolarOut = Abc_TtIsFullySymmetric( pTruth, 8 );
3867 assert( PolarIn == PolarOut );
3868}
3869
3870
3882static inline word * Abc_TtSymFunGenerate( char * pOnes, int nVars )
3883{
3884 int m, k, Count;
3885 word * pTruth = ABC_CALLOC( word, Abc_TtWordNum(nVars) );
3886 assert( (int)strlen(pOnes) == nVars + 1 );
3887 for ( m = 0; m < (1 << nVars); m++ )
3888 {
3889 Count = 0;
3890 for ( k = 0; k < nVars; k++ )
3891 Count += (m >> k) & 1;
3892 if ( pOnes[Count] == '1' )
3893 Abc_TtXorBit( pTruth, m );
3894 }
3895 return pTruth;
3896}
3897
3909static inline void Abc_TtFlipVar5( word * p, int nVars )
3910{
3911 int Test = 1;
3912 if ( *((char *)&Test) == 0 && nVars > 5 )
3913 Abc_TtFlip( p, Abc_TtWordNum(nVars), 5 );
3914}
3915
3916ABC_NAMESPACE_HEADER_END
3917
3918#endif
3919
nWords
int nWords
Definition abcNpn.c:127
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition abc_namespaces.h:51
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition abc_namespaces.h:50
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
Cube
struct cube Cube
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213
strlen
int strlen()
Var1
@ Var1
Definition xsatSolver.h:56
Var0
@ Var0
Definition xsatSolver.h:55