ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
kitTruth.c
Go to the documentation of this file.
1
20
21#include "kit.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
33
46void Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
47{
48 static unsigned PMasks[4][3] = {
49 { 0x99999999, 0x22222222, 0x44444444 },
50 { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
51 { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
52 { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
53 };
54 int nWords = Kit_TruthWordNum( nVars );
55 int i, k, Step, Shift;
56
57 assert( iVar < nVars - 1 );
58 if ( iVar < 4 )
59 {
60 Shift = (1 << iVar);
61 for ( i = 0; i < nWords; i++ )
62 pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
63 }
64 else if ( iVar > 4 )
65 {
66 Step = (1 << (iVar - 5));
67 for ( k = 0; k < nWords; k += 4*Step )
68 {
69 for ( i = 0; i < Step; i++ )
70 pOut[i] = pIn[i];
71 for ( i = 0; i < Step; i++ )
72 pOut[Step+i] = pIn[2*Step+i];
73 for ( i = 0; i < Step; i++ )
74 pOut[2*Step+i] = pIn[Step+i];
75 for ( i = 0; i < Step; i++ )
76 pOut[3*Step+i] = pIn[3*Step+i];
77 pIn += 4*Step;
78 pOut += 4*Step;
79 }
80 }
81 else // if ( iVar == 4 )
82 {
83 for ( i = 0; i < nWords; i += 2 )
84 {
85 pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
86 pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
87 }
88 }
89}
90
103void Kit_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int Start )
104{
105 int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
106 int i, k, Step;
107
108 assert( Start < nVars - 1 );
109 switch ( Start )
110 {
111 case 0:
112 for ( i = 0; i < nWords; i++ )
113 pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
114 return;
115 case 1:
116 for ( i = 0; i < nWords; i++ )
117 pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
118 return;
119 case 2:
120 for ( i = 0; i < nWords; i++ )
121 pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
122 return;
123 case 3:
124 for ( i = 0; i < nWords; i++ )
125 pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
126 return;
127 case 4:
128 for ( i = 0; i < nWords; i += 2 )
129 {
130 pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
131 pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
132 }
133 return;
134 default:
135 Step = (1 << (Start - 5));
136 for ( k = 0; k < nWords; k += 4*Step )
137 {
138 for ( i = 0; i < Step; i++ )
139 pOut[i] = pIn[i];
140 for ( i = 0; i < Step; i++ )
141 pOut[Step+i] = pIn[2*Step+i];
142 for ( i = 0; i < Step; i++ )
143 pOut[2*Step+i] = pIn[Step+i];
144 for ( i = 0; i < Step; i++ )
145 pOut[3*Step+i] = pIn[3*Step+i];
146 pIn += 4*Step;
147 pOut += 4*Step;
148 }
149 return;
150 }
151}
152
166void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
167{
168 unsigned * pTemp;
169 int i, k, Var = nVars - 1, Counter = 0;
170 for ( i = nVarsAll - 1; i >= 0; i-- )
171 if ( Phase & (1 << i) )
172 {
173 for ( k = Var; k < i; k++ )
174 {
175 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
176 pTemp = pIn; pIn = pOut; pOut = pTemp;
177 Counter++;
178 }
179 Var--;
180 }
181 assert( Var == -1 );
182 // swap if it was moved an even number of times
183 if ( fReturnIn ^ !(Counter & 1) )
184 Kit_TruthCopy( pOut, pIn, nVarsAll );
185}
186
200void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
201{
202 unsigned * pTemp;
203 int i, k, Var = 0, Counter = 0;
204 for ( i = 0; i < nVarsAll; i++ )
205 if ( Phase & (1 << i) )
206 {
207 for ( k = i-1; k >= Var; k-- )
208 {
209 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
210 pTemp = pIn; pIn = pOut; pOut = pTemp;
211 Counter++;
212 }
213 Var++;
214 }
215 assert( Var == nVars );
216 // swap if it was moved an even number of times
217 if ( fReturnIn ^ !(Counter & 1) )
218 Kit_TruthCopy( pOut, pIn, nVarsAll );
219}
220
233void Kit_TruthPermute( unsigned * pOut, unsigned * pIn, int nVars, char * pPerm, int fReturnIn )
234{
235 unsigned * pTemp;
236 int i, Temp, fChange, Counter = 0;
237 do {
238 fChange = 0;
239 for ( i = 0; i < nVars-1; i++ )
240 {
241 assert( pPerm[i] != pPerm[i+1] );
242 if ( pPerm[i] <= pPerm[i+1] )
243 continue;
244 Counter++;
245 fChange = 1;
246
247 Temp = pPerm[i];
248 pPerm[i] = pPerm[i+1];
249 pPerm[i+1] = Temp;
250
251 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
252 pTemp = pIn; pIn = pOut; pOut = pTemp;
253 }
254 } while ( fChange );
255 if ( fReturnIn ^ !(Counter & 1) )
256 Kit_TruthCopy( pOut, pIn, nVars );
257}
258
270int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
271{
272 int nWords = Kit_TruthWordNum( nVars );
273 int i, k, Step;
274
275 assert( iVar < nVars );
276 switch ( iVar )
277 {
278 case 0:
279 for ( i = 0; i < nWords; i++ )
280 if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
281 return 1;
282 return 0;
283 case 1:
284 for ( i = 0; i < nWords; i++ )
285 if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
286 return 1;
287 return 0;
288 case 2:
289 for ( i = 0; i < nWords; i++ )
290 if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
291 return 1;
292 return 0;
293 case 3:
294 for ( i = 0; i < nWords; i++ )
295 if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
296 return 1;
297 return 0;
298 case 4:
299 for ( i = 0; i < nWords; i++ )
300 if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
301 return 1;
302 return 0;
303 default:
304 Step = (1 << (iVar - 5));
305 for ( k = 0; k < nWords; k += 2*Step )
306 {
307 for ( i = 0; i < Step; i++ )
308 if ( pTruth[i] != pTruth[Step+i] )
309 return 1;
310 pTruth += 2*Step;
311 }
312 return 0;
313 }
314}
315
327int Kit_TruthSupportSize( unsigned * pTruth, int nVars )
328{
329 int i, Counter = 0;
330 for ( i = 0; i < nVars; i++ )
331 Counter += Kit_TruthVarInSupport( pTruth, nVars, i );
332 return Counter;
333}
334
346unsigned Kit_TruthSupport( unsigned * pTruth, int nVars )
347{
348 int i, Support = 0;
349 for ( i = 0; i < nVars; i++ )
350 if ( Kit_TruthVarInSupport( pTruth, nVars, i ) )
351 Support |= (1 << i);
352 return Support;
353}
354
355
356
368void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
369{
370 int nWords = Kit_TruthWordNum( nVars );
371 int i, k, Step;
372
373 assert( iVar < nVars );
374 switch ( iVar )
375 {
376 case 0:
377 for ( i = 0; i < nWords; i++ )
378 pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
379 return;
380 case 1:
381 for ( i = 0; i < nWords; i++ )
382 pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
383 return;
384 case 2:
385 for ( i = 0; i < nWords; i++ )
386 pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
387 return;
388 case 3:
389 for ( i = 0; i < nWords; i++ )
390 pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
391 return;
392 case 4:
393 for ( i = 0; i < nWords; i++ )
394 pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
395 return;
396 default:
397 Step = (1 << (iVar - 5));
398 for ( k = 0; k < nWords; k += 2*Step )
399 {
400 for ( i = 0; i < Step; i++ )
401 pTruth[Step+i] = pTruth[i];
402 pTruth += 2*Step;
403 }
404 return;
405 }
406}
407
419int Kit_TruthCofactor0Count( unsigned * pTruth, int nVars, int iVar )
420{
421 int nWords = Kit_TruthWordNum( nVars );
422 int i, k, Step, Counter = 0;
423
424 assert( iVar < nVars );
425 switch ( iVar )
426 {
427 case 0:
428 for ( i = 0; i < nWords; i++ )
429 Counter += Kit_WordCountOnes(pTruth[i] & 0x55555555);
430 return Counter;
431 case 1:
432 for ( i = 0; i < nWords; i++ )
433 Counter += Kit_WordCountOnes(pTruth[i] & 0x33333333);
434 return Counter;
435 case 2:
436 for ( i = 0; i < nWords; i++ )
437 Counter += Kit_WordCountOnes(pTruth[i] & 0x0F0F0F0F);
438 return Counter;
439 case 3:
440 for ( i = 0; i < nWords; i++ )
441 Counter += Kit_WordCountOnes(pTruth[i] & 0x00FF00FF);
442 return Counter;
443 case 4:
444 for ( i = 0; i < nWords; i++ )
445 Counter += Kit_WordCountOnes(pTruth[i] & 0x0000FFFF);
446 return Counter;
447 default:
448 Step = (1 << (iVar - 5));
449 for ( k = 0; k < nWords; k += 2*Step )
450 {
451 for ( i = 0; i < Step; i++ )
452 Counter += Kit_WordCountOnes(pTruth[i]);
453 pTruth += 2*Step;
454 }
455 return Counter;
456 }
457}
458
470void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
471{
472 int nWords = Kit_TruthWordNum( nVars );
473 int i, k, Step;
474
475 assert( iVar < nVars );
476 switch ( iVar )
477 {
478 case 0:
479 for ( i = 0; i < nWords; i++ )
480 pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
481 return;
482 case 1:
483 for ( i = 0; i < nWords; i++ )
484 pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
485 return;
486 case 2:
487 for ( i = 0; i < nWords; i++ )
488 pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
489 return;
490 case 3:
491 for ( i = 0; i < nWords; i++ )
492 pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
493 return;
494 case 4:
495 for ( i = 0; i < nWords; i++ )
496 pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
497 return;
498 default:
499 Step = (1 << (iVar - 5));
500 for ( k = 0; k < nWords; k += 2*Step )
501 {
502 for ( i = 0; i < Step; i++ )
503 pTruth[i] = pTruth[Step+i];
504 pTruth += 2*Step;
505 }
506 return;
507 }
508}
509
521void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
522{
523 int nWords = Kit_TruthWordNum( nVars );
524 int i, k, Step;
525
526 assert( iVar < nVars );
527 switch ( iVar )
528 {
529 case 0:
530 for ( i = 0; i < nWords; i++ )
531 pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
532 return;
533 case 1:
534 for ( i = 0; i < nWords; i++ )
535 pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
536 return;
537 case 2:
538 for ( i = 0; i < nWords; i++ )
539 pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
540 return;
541 case 3:
542 for ( i = 0; i < nWords; i++ )
543 pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
544 return;
545 case 4:
546 for ( i = 0; i < nWords; i++ )
547 pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
548 return;
549 default:
550 Step = (1 << (iVar - 5));
551 for ( k = 0; k < nWords; k += 2*Step )
552 {
553 for ( i = 0; i < Step; i++ )
554 pOut[i] = pOut[Step+i] = pIn[i];
555 pIn += 2*Step;
556 pOut += 2*Step;
557 }
558 return;
559 }
560}
561
573void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
574{
575 int nWords = Kit_TruthWordNum( nVars );
576 int i, k, Step;
577
578 assert( iVar < nVars );
579 switch ( iVar )
580 {
581 case 0:
582 for ( i = 0; i < nWords; i++ )
583 pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
584 return;
585 case 1:
586 for ( i = 0; i < nWords; i++ )
587 pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
588 return;
589 case 2:
590 for ( i = 0; i < nWords; i++ )
591 pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
592 return;
593 case 3:
594 for ( i = 0; i < nWords; i++ )
595 pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
596 return;
597 case 4:
598 for ( i = 0; i < nWords; i++ )
599 pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
600 return;
601 default:
602 Step = (1 << (iVar - 5));
603 for ( k = 0; k < nWords; k += 2*Step )
604 {
605 for ( i = 0; i < Step; i++ )
606 pOut[i] = pOut[Step+i] = pIn[Step+i];
607 pIn += 2*Step;
608 pOut += 2*Step;
609 }
610 return;
611 }
612}
613
625int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar )
626{
627 int nWords = Kit_TruthWordNum( nVars );
628 int i, k, Step;
629
630 assert( iVar < nVars );
631 switch ( iVar )
632 {
633 case 0:
634 for ( i = 0; i < nWords; i++ )
635 if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
636 return 0;
637 return 1;
638 case 1:
639 for ( i = 0; i < nWords; i++ )
640 if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
641 return 0;
642 return 1;
643 case 2:
644 for ( i = 0; i < nWords; i++ )
645 if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
646 return 0;
647 return 1;
648 case 3:
649 for ( i = 0; i < nWords; i++ )
650 if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
651 return 0;
652 return 1;
653 case 4:
654 for ( i = 0; i < nWords; i++ )
655 if ( ((pOnset[i] & (pOffset[i] >> 16)) | (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
656 return 0;
657 return 1;
658 default:
659 Step = (1 << (iVar - 5));
660 for ( k = 0; k < nWords; k += 2*Step )
661 {
662 for ( i = 0; i < Step; i++ )
663 if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
664 return 0;
665 pOnset += 2*Step;
666 pOffset += 2*Step;
667 }
668 return 1;
669 }
670}
671
672
684void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar )
685{
686 int nWords = Kit_TruthWordNum( nVars );
687 int i, k, Step;
688
689 assert( iVar < nVars );
690 switch ( iVar )
691 {
692 case 0:
693 for ( i = 0; i < nWords; i++ )
694 pTruth[i] |= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
695 return;
696 case 1:
697 for ( i = 0; i < nWords; i++ )
698 pTruth[i] |= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
699 return;
700 case 2:
701 for ( i = 0; i < nWords; i++ )
702 pTruth[i] |= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
703 return;
704 case 3:
705 for ( i = 0; i < nWords; i++ )
706 pTruth[i] |= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
707 return;
708 case 4:
709 for ( i = 0; i < nWords; i++ )
710 pTruth[i] |= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
711 return;
712 default:
713 Step = (1 << (iVar - 5));
714 for ( k = 0; k < nWords; k += 2*Step )
715 {
716 for ( i = 0; i < Step; i++ )
717 {
718 pTruth[i] |= pTruth[Step+i];
719 pTruth[Step+i] = pTruth[i];
720 }
721 pTruth += 2*Step;
722 }
723 return;
724 }
725}
726
738void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
739{
740 int nWords = Kit_TruthWordNum( nVars );
741 int i, k, Step;
742
743 assert( iVar < nVars );
744 switch ( iVar )
745 {
746 case 0:
747 for ( i = 0; i < nWords; i++ )
748 pRes[i] = pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
749 return;
750 case 1:
751 for ( i = 0; i < nWords; i++ )
752 pRes[i] = pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
753 return;
754 case 2:
755 for ( i = 0; i < nWords; i++ )
756 pRes[i] = pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
757 return;
758 case 3:
759 for ( i = 0; i < nWords; i++ )
760 pRes[i] = pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
761 return;
762 case 4:
763 for ( i = 0; i < nWords; i++ )
764 pRes[i] = pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
765 return;
766 default:
767 Step = (1 << (iVar - 5));
768 for ( k = 0; k < nWords; k += 2*Step )
769 {
770 for ( i = 0; i < Step; i++ )
771 {
772 pRes[i] = pTruth[i] | pTruth[Step+i];
773 pRes[Step+i] = pRes[i];
774 }
775 pRes += 2*Step;
776 pTruth += 2*Step;
777 }
778 return;
779 }
780}
781
793void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
794{
795 int v;
796 Kit_TruthCopy( pRes, pTruth, nVars );
797 for ( v = 0; v < nVars; v++ )
798 if ( uMask & (1 << v) )
799 Kit_TruthExist( pRes, nVars, v );
800}
801
813void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
814{
815 int nWords = Kit_TruthWordNum( nVars );
816 int i, k, Step;
817
818 assert( iVar < nVars );
819 switch ( iVar )
820 {
821 case 0:
822 for ( i = 0; i < nWords; i++ )
823 pTruth[i] &= ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
824 return;
825 case 1:
826 for ( i = 0; i < nWords; i++ )
827 pTruth[i] &= ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
828 return;
829 case 2:
830 for ( i = 0; i < nWords; i++ )
831 pTruth[i] &= ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
832 return;
833 case 3:
834 for ( i = 0; i < nWords; i++ )
835 pTruth[i] &= ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
836 return;
837 case 4:
838 for ( i = 0; i < nWords; i++ )
839 pTruth[i] &= ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
840 return;
841 default:
842 Step = (1 << (iVar - 5));
843 for ( k = 0; k < nWords; k += 2*Step )
844 {
845 for ( i = 0; i < Step; i++ )
846 {
847 pTruth[i] &= pTruth[Step+i];
848 pTruth[Step+i] = pTruth[i];
849 }
850 pTruth += 2*Step;
851 }
852 return;
853 }
854}
855
867void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
868{
869 int nWords = Kit_TruthWordNum( nVars );
870 int i, k, Step;
871
872 assert( iVar < nVars );
873 switch ( iVar )
874 {
875 case 0:
876 for ( i = 0; i < nWords; i++ )
877 pRes[i] = pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
878 return;
879 case 1:
880 for ( i = 0; i < nWords; i++ )
881 pRes[i] = pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
882 return;
883 case 2:
884 for ( i = 0; i < nWords; i++ )
885 pRes[i] = pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
886 return;
887 case 3:
888 for ( i = 0; i < nWords; i++ )
889 pRes[i] = pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
890 return;
891 case 4:
892 for ( i = 0; i < nWords; i++ )
893 pRes[i] = pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
894 return;
895 default:
896 Step = (1 << (iVar - 5));
897 for ( k = 0; k < nWords; k += 2*Step )
898 {
899 for ( i = 0; i < Step; i++ )
900 {
901 pRes[i] = pTruth[i] & pTruth[Step+i];
902 pRes[Step+i] = pRes[i];
903 }
904 pRes += 2*Step;
905 pTruth += 2*Step;
906 }
907 return;
908 }
909}
910
922void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
923{
924 int nWords = Kit_TruthWordNum( nVars );
925 int i, k, Step;
926
927 assert( iVar < nVars );
928 switch ( iVar )
929 {
930 case 0:
931 for ( i = 0; i < nWords; i++ )
932 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
933 return;
934 case 1:
935 for ( i = 0; i < nWords; i++ )
936 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
937 return;
938 case 2:
939 for ( i = 0; i < nWords; i++ )
940 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
941 return;
942 case 3:
943 for ( i = 0; i < nWords; i++ )
944 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
945 return;
946 case 4:
947 for ( i = 0; i < nWords; i++ )
948 pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
949 return;
950 default:
951 Step = (1 << (iVar - 5));
952 for ( k = 0; k < nWords; k += 2*Step )
953 {
954 for ( i = 0; i < Step; i++ )
955 {
956 pRes[i] = pTruth[i] ^ pTruth[Step+i];
957 pRes[Step+i] = pRes[i];
958 }
959 pRes += 2*Step;
960 pTruth += 2*Step;
961 }
962 return;
963 }
964}
965
977int Kit_TruthBooleanDiffCount( unsigned * pTruth, int nVars, int iVar )
978{
979 int nWords = Kit_TruthWordNum( nVars );
980 int i, k, Step, Counter = 0;
981
982 assert( iVar < nVars );
983 switch ( iVar )
984 {
985 case 0:
986 for ( i = 0; i < nWords; i++ )
987 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 1)) & 0x55555555 );
988 return Counter;
989 case 1:
990 for ( i = 0; i < nWords; i++ )
991 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 2)) & 0x33333333 );
992 return Counter;
993 case 2:
994 for ( i = 0; i < nWords; i++ )
995 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 4)) & 0x0F0F0F0F );
996 return Counter;
997 case 3:
998 for ( i = 0; i < nWords; i++ )
999 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 8)) & 0x00FF00FF );
1000 return Counter;
1001 case 4:
1002 for ( i = 0; i < nWords; i++ )
1003 Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >>16)) & 0x0000FFFF );
1004 return Counter;
1005 default:
1006 Step = (1 << (iVar - 5));
1007 for ( k = 0; k < nWords; k += 2*Step )
1008 {
1009 for ( i = 0; i < Step; i++ )
1010 Counter += Kit_WordCountOnes( pTruth[i] ^ pTruth[Step+i] );
1011 pTruth += 2*Step;
1012 }
1013 return Counter;
1014 }
1015}
1016
1028int Kit_TruthXorCount( unsigned * pTruth0, unsigned * pTruth1, int nVars )
1029{
1030 int nWords = Kit_TruthWordNum( nVars );
1031 int i, Counter = 0;
1032 for ( i = 0; i < nWords; i++ )
1033 Counter += Kit_WordCountOnes( pTruth0[i] ^ pTruth1[i] );
1034 return Counter;
1035}
1036
1048void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
1049{
1050 int v;
1051 Kit_TruthCopy( pRes, pTruth, nVars );
1052 for ( v = 0; v < nVars; v++ )
1053 if ( uMask & (1 << v) )
1054 Kit_TruthForall( pRes, nVars, v );
1055}
1056
1057
1069void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
1070{
1071 int nWords = Kit_TruthWordNum( nVars );
1072 int i, k, Step;
1073
1074 assert( iVar < nVars );
1075 switch ( iVar )
1076 {
1077 case 0:
1078 for ( i = 0; i < nWords; i++ )
1079 pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
1080 return;
1081 case 1:
1082 for ( i = 0; i < nWords; i++ )
1083 pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
1084 return;
1085 case 2:
1086 for ( i = 0; i < nWords; i++ )
1087 pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
1088 return;
1089 case 3:
1090 for ( i = 0; i < nWords; i++ )
1091 pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
1092 return;
1093 case 4:
1094 for ( i = 0; i < nWords; i++ )
1095 pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
1096 return;
1097 default:
1098 Step = (1 << (iVar - 5));
1099 for ( k = 0; k < nWords; k += 2*Step )
1100 {
1101 for ( i = 0; i < Step; i++ )
1102 {
1103 pOut[i] = pCof0[i];
1104 pOut[Step+i] = pCof1[Step+i];
1105 }
1106 pOut += 2*Step;
1107 pCof0 += 2*Step;
1108 pCof1 += 2*Step;
1109 }
1110 return;
1111 }
1112}
1113
1125void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 )
1126{
1127 int nWords = Kit_TruthWordNum( nVars );
1128 int i, k, Step;
1129
1130 if ( fCompl0 == 0 )
1131 {
1132 Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
1133 return;
1134 }
1135
1136 assert( iVar < nVars );
1137 switch ( iVar )
1138 {
1139 case 0:
1140 for ( i = 0; i < nWords; i++ )
1141 pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
1142 return;
1143 case 1:
1144 for ( i = 0; i < nWords; i++ )
1145 pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
1146 return;
1147 case 2:
1148 for ( i = 0; i < nWords; i++ )
1149 pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
1150 return;
1151 case 3:
1152 for ( i = 0; i < nWords; i++ )
1153 pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
1154 return;
1155 case 4:
1156 for ( i = 0; i < nWords; i++ )
1157 pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
1158 return;
1159 default:
1160 Step = (1 << (iVar - 5));
1161 for ( k = 0; k < nWords; k += 2*Step )
1162 {
1163 for ( i = 0; i < Step; i++ )
1164 {
1165 pOut[i] = ~pCof0[i];
1166 pOut[Step+i] = pCof1[Step+i];
1167 }
1168 pOut += 2*Step;
1169 pCof0 += 2*Step;
1170 pCof1 += 2*Step;
1171 }
1172 return;
1173 }
1174}
1175
1187int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
1188{
1189 static unsigned uTemp0[32], uTemp1[32];
1190 if ( pCof0 == NULL )
1191 {
1192 assert( nVars <= 10 );
1193 pCof0 = uTemp0;
1194 }
1195 if ( pCof1 == NULL )
1196 {
1197 assert( nVars <= 10 );
1198 pCof1 = uTemp1;
1199 }
1200 // compute Cof01
1201 Kit_TruthCopy( pCof0, pTruth, nVars );
1202 Kit_TruthCofactor0( pCof0, nVars, iVar0 );
1203 Kit_TruthCofactor1( pCof0, nVars, iVar1 );
1204 // compute Cof10
1205 Kit_TruthCopy( pCof1, pTruth, nVars );
1206 Kit_TruthCofactor1( pCof1, nVars, iVar0 );
1207 Kit_TruthCofactor0( pCof1, nVars, iVar1 );
1208 // compare
1209 return Kit_TruthIsEqual( pCof0, pCof1, nVars );
1210}
1211
1223int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
1224{
1225 static unsigned uTemp0[32], uTemp1[32];
1226 if ( pCof0 == NULL )
1227 {
1228 assert( nVars <= 10 );
1229 pCof0 = uTemp0;
1230 }
1231 if ( pCof1 == NULL )
1232 {
1233 assert( nVars <= 10 );
1234 pCof1 = uTemp1;
1235 }
1236 // compute Cof00
1237 Kit_TruthCopy( pCof0, pTruth, nVars );
1238 Kit_TruthCofactor0( pCof0, nVars, iVar0 );
1239 Kit_TruthCofactor0( pCof0, nVars, iVar1 );
1240 // compute Cof11
1241 Kit_TruthCopy( pCof1, pTruth, nVars );
1242 Kit_TruthCofactor1( pCof1, nVars, iVar0 );
1243 Kit_TruthCofactor1( pCof1, nVars, iVar1 );
1244 // compare
1245 return Kit_TruthIsEqual( pCof0, pCof1, nVars );
1246}
1247
1259void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar )
1260{
1261 int nWords = Kit_TruthWordNum( nVars );
1262 int i, k, Step;
1263 unsigned Temp;
1264
1265 assert( iVar < nVars );
1266 switch ( iVar )
1267 {
1268 case 0:
1269 for ( i = 0; i < nWords; i++ )
1270 pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
1271 return;
1272 case 1:
1273 for ( i = 0; i < nWords; i++ )
1274 pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
1275 return;
1276 case 2:
1277 for ( i = 0; i < nWords; i++ )
1278 pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
1279 return;
1280 case 3:
1281 for ( i = 0; i < nWords; i++ )
1282 pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
1283 return;
1284 case 4:
1285 for ( i = 0; i < nWords; i++ )
1286 pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
1287 return;
1288 default:
1289 Step = (1 << (iVar - 5));
1290 for ( k = 0; k < nWords; k += 2*Step )
1291 {
1292 for ( i = 0; i < Step; i++ )
1293 {
1294 Temp = pTruth[i];
1295 pTruth[i] = pTruth[Step+i];
1296 pTruth[Step+i] = Temp;
1297 }
1298 pTruth += 2*Step;
1299 }
1300 return;
1301 }
1302}
1303
1315int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin )
1316{
1317 static unsigned uCofactor[16];
1318 int i, ValueCur, ValueMin, VarMin;
1319 unsigned uSupp0, uSupp1;
1320 int nVars0, nVars1;
1321 assert( nVars <= 9 );
1322 ValueMin = 32;
1323 VarMin = -1;
1324 for ( i = 0; i < nVars; i++ )
1325 {
1326 // get negative cofactor
1327 Kit_TruthCopy( uCofactor, pTruth, nVars );
1328 Kit_TruthCofactor0( uCofactor, nVars, i );
1329 uSupp0 = Kit_TruthSupport( uCofactor, nVars );
1330 nVars0 = Kit_WordCountOnes( uSupp0 );
1331//Kit_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
1332 // get positive cofactor
1333 Kit_TruthCopy( uCofactor, pTruth, nVars );
1334 Kit_TruthCofactor1( uCofactor, nVars, i );
1335 uSupp1 = Kit_TruthSupport( uCofactor, nVars );
1336 nVars1 = Kit_WordCountOnes( uSupp1 );
1337//Kit_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
1338 // get the number of common vars
1339 ValueCur = Kit_WordCountOnes( uSupp0 & uSupp1 );
1340 if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
1341 {
1342 ValueMin = ValueCur;
1343 VarMin = i;
1344 }
1345 if ( ValueMin == 0 )
1346 break;
1347 }
1348 if ( pVarMin )
1349 *pVarMin = VarMin;
1350 return ValueMin;
1351}
1352
1353
1365int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
1366{
1367 int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
1368 if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
1369 return -1;
1370 // iterate through variables
1371 iBestVar = -1;
1372 nSuppSizeMin = KIT_INFINITY;
1373 for ( i = 0; i < nVars; i++ )
1374 {
1375 // cofactor the functiona and get support sizes
1376 Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
1377 Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
1378 nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
1379 nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
1380 nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
1381 // compare this variable with other variables
1382 if ( nSuppSizeMin > nSuppSizeCur )
1383 {
1384 nSuppSizeMin = nSuppSizeCur;
1385 iBestVar = i;
1386 }
1387 }
1388 assert( iBestVar != -1 );
1389 // cofactor w.r.t. this variable
1390 Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
1391 Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
1392 return iBestVar;
1393}
1394
1395
1410void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, int * pStore )
1411{
1412 int nWords = Kit_TruthWordNum( nVars );
1413 int i, k, Counter;
1414 memset( pStore, 0, sizeof(int) * 2 * nVars );
1415 if ( nVars <= 5 )
1416 {
1417 if ( nVars > 0 )
1418 {
1419 pStore[2*0+0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
1420 pStore[2*0+1] = Kit_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
1421 }
1422 if ( nVars > 1 )
1423 {
1424 pStore[2*1+0] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
1425 pStore[2*1+1] = Kit_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
1426 }
1427 if ( nVars > 2 )
1428 {
1429 pStore[2*2+0] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
1430 pStore[2*2+1] = Kit_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
1431 }
1432 if ( nVars > 3 )
1433 {
1434 pStore[2*3+0] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
1435 pStore[2*3+1] = Kit_WordCountOnes( pTruth[0] & 0xFF00FF00 );
1436 }
1437 if ( nVars > 4 )
1438 {
1439 pStore[2*4+0] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
1440 pStore[2*4+1] = Kit_WordCountOnes( pTruth[0] & 0xFFFF0000 );
1441 }
1442 return;
1443 }
1444 // nVars >= 6
1445 // count 1's for all other variables
1446 for ( k = 0; k < nWords; k++ )
1447 {
1448 Counter = Kit_WordCountOnes( pTruth[k] );
1449 for ( i = 5; i < nVars; i++ )
1450 if ( k & (1 << (i-5)) )
1451 pStore[2*i+1] += Counter;
1452 else
1453 pStore[2*i+0] += Counter;
1454 }
1455 // count 1's for the first five variables
1456 for ( k = 0; k < nWords/2; k++ )
1457 {
1458 pStore[2*0+0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
1459 pStore[2*0+1] += Kit_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >> 1) );
1460 pStore[2*1+0] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
1461 pStore[2*1+1] += Kit_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >> 2) );
1462 pStore[2*2+0] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
1463 pStore[2*2+1] += Kit_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >> 4) );
1464 pStore[2*3+0] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
1465 pStore[2*3+1] += Kit_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >> 8) );
1466 pStore[2*4+0] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
1467 pStore[2*4+1] += Kit_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
1468 pTruth += 2;
1469 }
1470}
1471
1486void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, int * pStore )
1487{
1488 int nWords = Kit_TruthWordNum( nVars );
1489 int i, k, Counter;
1490 memset( pStore, 0, sizeof(int) * nVars );
1491 if ( nVars <= 5 )
1492 {
1493 if ( nVars > 0 )
1494 pStore[0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
1495 if ( nVars > 1 )
1496 pStore[1] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
1497 if ( nVars > 2 )
1498 pStore[2] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
1499 if ( nVars > 3 )
1500 pStore[3] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
1501 if ( nVars > 4 )
1502 pStore[4] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
1503 return;
1504 }
1505 // nVars >= 6
1506 // count 1's for all other variables
1507 for ( k = 0; k < nWords; k++ )
1508 {
1509 Counter = Kit_WordCountOnes( pTruth[k] );
1510 for ( i = 5; i < nVars; i++ )
1511 if ( (k & (1 << (i-5))) == 0 )
1512 pStore[i] += Counter;
1513 }
1514 // count 1's for the first five variables
1515 for ( k = 0; k < nWords/2; k++ )
1516 {
1517 pStore[0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) << 1) );
1518 pStore[1] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) << 2) );
1519 pStore[2] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) << 4) );
1520 pStore[3] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) << 8) );
1521 pStore[4] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
1522 pTruth += 2;
1523 }
1524}
1525
1537void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, int * pStore, unsigned * pAux )
1538{
1539 int i;
1540 for ( i = 0; i < nVars; i++ )
1541 {
1542 Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
1543 pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
1544 Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
1545 pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
1546 }
1547}
1548
1560unsigned Kit_TruthHash( unsigned * pIn, int nWords )
1561{
1562 // The 1,024 smallest prime numbers used to compute the hash value
1563 // http://www.math.utah.edu/~alfeld/math/primelist.html
1564 static int HashPrimes[1024] = { 2, 3, 5,
1565 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97,
1566 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191,
1567 193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283,
1568 293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401,
1569 409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509,
1570 521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631,
1571 641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751,
1572 757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877,
1573 881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997,
1574 1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091,
1575 1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193,
1576 1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291,
1577 1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423,
1578 1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493,
1579 1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601,
1580 1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699,
1581 1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811,
1582 1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931,
1583 1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029,
1584 2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137,
1585 2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267,
1586 2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357,
1587 2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459,
1588 2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593,
1589 2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693,
1590 2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791,
1591 2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903,
1592 2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023,
1593 3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167,
1594 3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271,
1595 3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373,
1596 3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511,
1597 3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607,
1598 3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709,
1599 3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833,
1600 3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931,
1601 3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057,
1602 4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177,
1603 4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283,
1604 4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423,
1605 4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547,
1606 4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657,
1607 4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789,
1608 4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931,
1609 4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011,
1610 5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147,
1611 5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279,
1612 5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413,
1613 5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507,
1614 5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647,
1615 5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743,
1616 5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857,
1617 5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007,
1618 6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121,
1619 6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247,
1620 6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343,
1621 6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473,
1622 6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607,
1623 6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733,
1624 6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857,
1625 6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971,
1626 6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103,
1627 7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229,
1628 7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369,
1629 7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517,
1630 7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603,
1631 7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723,
1632 7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873,
1633 7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009,
1634 8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123,
1635 8147, 8161 };
1636 int i;
1637 unsigned uHashKey;
1638 assert( nWords <= 1024 );
1639 uHashKey = 0;
1640 for ( i = 0; i < nWords; i++ )
1641 uHashKey ^= HashPrimes[i] * pIn[i];
1642 return uHashKey;
1643}
1644
1645
1657unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm )
1658{
1659 int pStore[32];
1660 unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
1661 int nWords = Kit_TruthWordNum( nVars );
1662 int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
1663 unsigned uCanonPhase;
1664
1665 // canonicize output
1666 uCanonPhase = 0;
1667 for ( i = 0; i < nVars; i++ )
1668 pCanonPerm[i] = i;
1669
1670 nOnes = Kit_TruthCountOnes(pIn, nVars);
1671 //if(pIn[0] & 1)
1672 if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
1673 {
1674 uCanonPhase |= (1 << nVars);
1675 Kit_TruthNot( pIn, pIn, nVars );
1676 }
1677
1678 // collect the minterm counts
1679 Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
1680/*
1681 Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
1682 for ( i = 0; i < 2*nVars; i++ )
1683 {
1684 assert( pStore[i] == pStore2[i] );
1685 }
1686*/
1687 // canonicize phase
1688 for ( i = 0; i < nVars; i++ )
1689 {
1690 if ( pStore[2*i+0] >= pStore[2*i+1] )
1691 continue;
1692 uCanonPhase |= (1 << i);
1693 Temp = pStore[2*i+0];
1694 pStore[2*i+0] = pStore[2*i+1];
1695 pStore[2*i+1] = Temp;
1696 Kit_TruthChangePhase( pIn, nVars, i );
1697 }
1698
1699// Kit_PrintHexadecimal( stdout, pIn, nVars );
1700// printf( "\n" );
1701
1702 // permute
1703 Counter = 0;
1704 do {
1705 fChange = 0;
1706 for ( i = 0; i < nVars-1; i++ )
1707 {
1708 if ( pStore[2*i] >= pStore[2*(i+1)] )
1709 continue;
1710 Counter++;
1711 fChange = 1;
1712
1713 Temp = pCanonPerm[i];
1714 pCanonPerm[i] = pCanonPerm[i+1];
1715 pCanonPerm[i+1] = Temp;
1716
1717 Temp = pStore[2*i];
1718 pStore[2*i] = pStore[2*(i+1)];
1719 pStore[2*(i+1)] = Temp;
1720
1721 Temp = pStore[2*i+1];
1722 pStore[2*i+1] = pStore[2*(i+1)+1];
1723 pStore[2*(i+1)+1] = Temp;
1724
1725 // if the polarity of variables is different, swap them
1726 if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
1727 {
1728 uCanonPhase ^= (1 << i);
1729 uCanonPhase ^= (1 << (i+1));
1730 }
1731
1732 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
1733 pTemp = pIn; pIn = pOut; pOut = pTemp;
1734 }
1735 } while ( fChange );
1736
1737
1738/*
1739 Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
1740 for ( i = 0; i < nVars; i++ )
1741 printf( "%d=%d/%d ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
1742 printf( " C = %d\n", Counter );
1743 Extra_PrintHexadecimal( stdout, pIn, nVars );
1744 printf( "\n" );
1745*/
1746
1747/*
1748 // process symmetric variable groups
1749 uSymms = 0;
1750 for ( i = 0; i < nVars-1; i++ )
1751 {
1752 if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1753 continue;
1754 if ( pStore[2*i] != pStore[2*i+1] )
1755 continue;
1756 if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
1757 continue;
1758 if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
1759 Kit_TruthChangePhase( pIn, nVars, i+1 );
1760 }
1761*/
1762
1763/*
1764 // process symmetric variable groups
1765 uSymms = 0;
1766 for ( i = 0; i < nVars-1; i++ )
1767 {
1768 if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
1769 continue;
1770 // i and i+1 can be symmetric
1771 // find the end of this group
1772 for ( k = i+1; k < nVars; k++ )
1773 if ( pStore[2*i] != pStore[2*k] )
1774 break;
1775 Limit = k;
1776 assert( i < Limit-1 );
1777 // go through the variables in this group
1778 for ( j = i + 1; j < Limit; j++ )
1779 {
1780 // check symmetry
1781 if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
1782 {
1783 uSymms |= (1 << j);
1784 continue;
1785 }
1786 // they are phase-unknown
1787 if ( pStore[2*i] == pStore[2*i+1] )
1788 {
1789 if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
1790 {
1791 Kit_TruthChangePhase( pIn, nVars, j );
1792 uCanonPhase ^= (1 << j);
1793 uSymms |= (1 << j);
1794 continue;
1795 }
1796 }
1797
1798 // they are not symmetric - move j as far as it goes in the group
1799 for ( k = j; k < Limit-1; k++ )
1800 {
1801 Counter++;
1802
1803 Temp = pCanonPerm[k];
1804 pCanonPerm[k] = pCanonPerm[k+1];
1805 pCanonPerm[k+1] = Temp;
1806
1807 assert( pStore[2*k] == pStore[2*(k+1)] );
1808 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
1809 pTemp = pIn; pIn = pOut; pOut = pTemp;
1810 }
1811 Limit--;
1812 j--;
1813 }
1814 i = Limit - 1;
1815 }
1816*/
1817
1818 // swap if it was moved an even number of times
1819 if ( Counter & 1 )
1820 Kit_TruthCopy( pOut, pIn, nVars );
1821 return uCanonPhase;
1822}
1823
1824
1839int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytesInit )
1840{
1841 // the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
1842 static unsigned Table[256] = {
1843 0x00000000, 0x01010101, 0x01010001, 0x02020102, 0x01000101, 0x02010202, 0x02010102, 0x03020203,
1844 0x01000001, 0x02010102, 0x02010002, 0x03020103, 0x02000102, 0x03010203, 0x03010103, 0x04020204,
1845 0x00010101, 0x01020202, 0x01020102, 0x02030203, 0x01010202, 0x02020303, 0x02020203, 0x03030304,
1846 0x01010102, 0x02020203, 0x02020103, 0x03030204, 0x02010203, 0x03020304, 0x03020204, 0x04030305,
1847 0x00010001, 0x01020102, 0x01020002, 0x02030103, 0x01010102, 0x02020203, 0x02020103, 0x03030204,
1848 0x01010002, 0x02020103, 0x02020003, 0x03030104, 0x02010103, 0x03020204, 0x03020104, 0x04030205,
1849 0x00020102, 0x01030203, 0x01030103, 0x02040204, 0x01020203, 0x02030304, 0x02030204, 0x03040305,
1850 0x01020103, 0x02030204, 0x02030104, 0x03040205, 0x02020204, 0x03030305, 0x03030205, 0x04040306,
1851 0x00000101, 0x01010202, 0x01010102, 0x02020203, 0x01000202, 0x02010303, 0x02010203, 0x03020304,
1852 0x01000102, 0x02010203, 0x02010103, 0x03020204, 0x02000203, 0x03010304, 0x03010204, 0x04020305,
1853 0x00010202, 0x01020303, 0x01020203, 0x02030304, 0x01010303, 0x02020404, 0x02020304, 0x03030405,
1854 0x01010203, 0x02020304, 0x02020204, 0x03030305, 0x02010304, 0x03020405, 0x03020305, 0x04030406,
1855 0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
1856 0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
1857 0x00020203, 0x01030304, 0x01030204, 0x02040305, 0x01020304, 0x02030405, 0x02030305, 0x03040406,
1858 0x01020204, 0x02030305, 0x02030205, 0x03040306, 0x02020305, 0x03030406, 0x03030306, 0x04040407,
1859 0x00000001, 0x01010102, 0x01010002, 0x02020103, 0x01000102, 0x02010203, 0x02010103, 0x03020204,
1860 0x01000002, 0x02010103, 0x02010003, 0x03020104, 0x02000103, 0x03010204, 0x03010104, 0x04020205,
1861 0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
1862 0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
1863 0x00010002, 0x01020103, 0x01020003, 0x02030104, 0x01010103, 0x02020204, 0x02020104, 0x03030205,
1864 0x01010003, 0x02020104, 0x02020004, 0x03030105, 0x02010104, 0x03020205, 0x03020105, 0x04030206,
1865 0x00020103, 0x01030204, 0x01030104, 0x02040205, 0x01020204, 0x02030305, 0x02030205, 0x03040306,
1866 0x01020104, 0x02030205, 0x02030105, 0x03040206, 0x02020205, 0x03030306, 0x03030206, 0x04040307,
1867 0x00000102, 0x01010203, 0x01010103, 0x02020204, 0x01000203, 0x02010304, 0x02010204, 0x03020305,
1868 0x01000103, 0x02010204, 0x02010104, 0x03020205, 0x02000204, 0x03010305, 0x03010205, 0x04020306,
1869 0x00010203, 0x01020304, 0x01020204, 0x02030305, 0x01010304, 0x02020405, 0x02020305, 0x03030406,
1870 0x01010204, 0x02020305, 0x02020205, 0x03030306, 0x02010305, 0x03020406, 0x03020306, 0x04030407,
1871 0x00010103, 0x01020204, 0x01020104, 0x02030205, 0x01010204, 0x02020305, 0x02020205, 0x03030306,
1872 0x01010104, 0x02020205, 0x02020105, 0x03030206, 0x02010205, 0x03020306, 0x03020206, 0x04030307,
1873 0x00020204, 0x01030305, 0x01030205, 0x02040306, 0x01020305, 0x02030406, 0x02030306, 0x03040407,
1874 0x01020205, 0x02030306, 0x02030206, 0x03040307, 0x02020306, 0x03030407, 0x03030307, 0x04040408
1875 };
1876 unsigned uSum;
1877 unsigned char * pTruthC, * pLimit;
1878 int * pBytes = pBytesInit;
1879 int i, iVar, Step, nWords, nBytes, nTotal;
1880
1881 assert( nVars <= 20 );
1882
1883 // clear storage
1884 memset( pRes, 0, sizeof(int) * nVars );
1885
1886 // count the number of one's in 0-cofactors of the first three variables
1887 nTotal = uSum = 0;
1888 nWords = Kit_TruthWordNum( nVars );
1889 nBytes = nWords * 4;
1890 pTruthC = (unsigned char *)pTruth;
1891 pLimit = pTruthC + nBytes;
1892 for ( ; pTruthC < pLimit; pTruthC++ )
1893 {
1894 uSum += Table[*pTruthC];
1895 *pBytes++ = (Table[*pTruthC] & 0xff);
1896 if ( (uSum & 0xff) > 246 )
1897 {
1898 nTotal += (uSum & 0xff);
1899 pRes[0] += ((uSum >> 8) & 0xff);
1900 pRes[2] += ((uSum >> 16) & 0xff);
1901 pRes[3] += ((uSum >> 24) & 0xff);
1902 uSum = 0;
1903 }
1904 }
1905 if ( uSum )
1906 {
1907 nTotal += (uSum & 0xff);
1908 pRes[0] += ((uSum >> 8) & 0xff);
1909 pRes[1] += ((uSum >> 16) & 0xff);
1910 pRes[2] += ((uSum >> 24) & 0xff);
1911 }
1912
1913 // count all other variables
1914 for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
1915 for ( i = 0; i < nBytes; i += Step + Step )
1916 {
1917 pRes[iVar] += pBytesInit[i];
1918 pBytesInit[i] += pBytesInit[i+Step];
1919 }
1920 assert( pBytesInit[0] == nTotal );
1921 assert( iVar == nVars );
1922
1923 for ( i = 0; i < nVars; i++ )
1924 assert( pRes[i] == Kit_TruthCofactor0Count(pTruth, nVars, i) );
1925 return nTotal;
1926}
1927
1939void Kit_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars )
1940{
1941 int nDigits, Digit, k;
1942 // write the number into the file
1943 nDigits = (1 << nVars) / 4;
1944 for ( k = nDigits - 1; k >= 0; k-- )
1945 {
1946 Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
1947 if ( Digit < 10 )
1948 fprintf( pFile, "%d", Digit );
1949 else
1950 fprintf( pFile, "%c", 'a' + Digit-10 );
1951 }
1952// fprintf( pFile, "\n" );
1953}
1954
1966void Kit_TruthCountMintermsPrecomp()
1967{
1968 int bit_count[256] = {
1969 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
1970 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
1971 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
1972 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
1973 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
1974 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
1975 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
1976 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
1977 };
1978 unsigned i, uWord;
1979 for ( i = 0; i < 256; i++ )
1980 {
1981 if ( i % 8 == 0 )
1982 printf( "\n" );
1983 uWord = bit_count[i];
1984 uWord |= (bit_count[i & 0x55] << 8);
1985 uWord |= (bit_count[i & 0x33] << 16);
1986 uWord |= (bit_count[i & 0x0f] << 24);
1987 printf( "0x" );
1988 Kit_PrintHexadecimal( stdout, &uWord, 5 );
1989 printf( ", " );
1990 }
1991}
1992
2004char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
2005{
2006 static char pFileName[100];
2007 FILE * pFile;
2008 sprintf( pFileName, "tt\\s%04d", nFile );
2009 pFile = fopen( pFileName, "w" );
2010 fprintf( pFile, "rt " );
2011 Kit_PrintHexadecimal( pFile, pTruth, nVars );
2012 fprintf( pFile, "; bdd; sop; ps\n" );
2013 fclose( pFile );
2014 return pFileName;
2015}
2016
2017
2029void Kit_TruthPrintProfile_int( unsigned * pTruth, int nVars )
2030{
2031 int Mints[20];
2032 int Mints0[20];
2033 int Mints1[20];
2034 int Unique1[20];
2035 int Total2[20][20];
2036 int Unique2[20][20];
2037 int Common2[20][20];
2038 int nWords = Kit_TruthWordNum( nVars );
2039 int * pBytes = ABC_ALLOC( int, nWords * 4 );
2040 unsigned * pIn = ABC_ALLOC( unsigned, nWords );
2041 unsigned * pOut = ABC_ALLOC( unsigned, nWords );
2042 unsigned * pCof00 = ABC_ALLOC( unsigned, nWords );
2043 unsigned * pCof01 = ABC_ALLOC( unsigned, nWords );
2044 unsigned * pCof10 = ABC_ALLOC( unsigned, nWords );
2045 unsigned * pCof11 = ABC_ALLOC( unsigned, nWords );
2046 unsigned * pTemp;
2047 int nTotalMints, nTotalMints0, nTotalMints1;
2048 int v, u, i, iVar, nMints1;
2049 int Cof00, Cof01, Cof10, Cof11;
2050 int Coz00, Coz01, Coz10, Coz11;
2051 assert( nVars <= 20 );
2052 assert( nVars >= 6 );
2053
2054 nTotalMints = Kit_TruthCountMinterms( pTruth, nVars, Mints, pBytes );
2055 for ( v = 0; v < nVars; v++ )
2056 Unique1[v] = Kit_TruthBooleanDiffCount( pTruth, nVars, v );
2057
2058 for ( v = 0; v < nVars; v++ )
2059 for ( u = 0; u < nVars; u++ )
2060 Total2[v][u] = Unique2[v][u] = Common2[v][u] = -1;
2061
2062 nMints1 = (1<<(nVars-2));
2063 for ( v = 0; v < nVars; v++ )
2064 {
2065 // move this var to be the first
2066 Kit_TruthCopy( pIn, pTruth, nVars );
2067// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
2068 for ( i = v; i < nVars - 1; i++ )
2069 {
2070 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
2071 pTemp = pIn; pIn = pOut; pOut = pTemp;
2072 }
2073// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
2074// printf( "\n" );
2075
2076
2077 // count minterms in both cofactor
2078 nTotalMints0 = Kit_TruthCountMinterms( pIn, nVars-1, Mints0, pBytes );
2079 nTotalMints1 = Kit_TruthCountMinterms( pIn+nWords/2, nVars-1, Mints1, pBytes );
2080 assert( nTotalMints == nTotalMints0 + nTotalMints1 );
2081/*
2082 for ( u = 0; u < nVars-1; u++ )
2083 printf( "%2d ", Mints0[u] );
2084 printf( "\n" );
2085
2086 for ( u = 0; u < nVars-1; u++ )
2087 printf( "%2d ", Mints1[u] );
2088 printf( "\n" );
2089*/
2090 for ( u = 0; u < nVars-1; u++ )
2091 {
2092 if ( u < v )
2093 iVar = u;
2094 else
2095 iVar = u + 1;
2096 assert( v != iVar );
2097 // get minter counts in the cofactors
2098 Cof00 = Mints0[u]; Coz00 = nMints1 - Cof00;
2099 Cof01 = nTotalMints0-Mints0[u]; Coz01 = nMints1 - Cof01;
2100 Cof10 = Mints1[u]; Coz10 = nMints1 - Cof10;
2101 Cof11 = nTotalMints1-Mints1[u]; Coz11 = nMints1 - Cof11;
2102
2103 assert( Cof00 >= 0 && Cof00 <= nMints1 );
2104 assert( Cof01 >= 0 && Cof01 <= nMints1 );
2105 assert( Cof10 >= 0 && Cof10 <= nMints1 );
2106 assert( Cof11 >= 0 && Cof11 <= nMints1 );
2107
2108 assert( Coz00 >= 0 && Coz00 <= nMints1 );
2109 assert( Coz01 >= 0 && Coz01 <= nMints1 );
2110 assert( Coz10 >= 0 && Coz10 <= nMints1 );
2111 assert( Coz11 >= 0 && Coz11 <= nMints1 );
2112
2113 Common2[v][iVar] = Common2[iVar][v] = Cof00 * Coz11 + Coz00 * Cof11 + Cof01 * Coz10 + Coz01 * Cof10;
2114
2115 Total2[v][iVar] = Total2[iVar][v] =
2116 Cof00 * Coz01 + Coz00 * Cof01 +
2117 Cof00 * Coz10 + Coz00 * Cof10 +
2118 Cof00 * Coz11 + Coz00 * Cof11 +
2119 Cof01 * Coz10 + Coz01 * Cof10 +
2120 Cof01 * Coz11 + Coz01 * Cof11 +
2121 Cof10 * Coz11 + Coz10 * Cof11 ;
2122
2123
2124 Kit_TruthCofactor0New( pCof00, pIn, nVars-1, u );
2125 Kit_TruthCofactor1New( pCof01, pIn, nVars-1, u );
2126 Kit_TruthCofactor0New( pCof10, pIn+nWords/2, nVars-1, u );
2127 Kit_TruthCofactor1New( pCof11, pIn+nWords/2, nVars-1, u );
2128
2129 Unique2[v][iVar] = Unique2[iVar][v] =
2130 Kit_TruthXorCount( pCof00, pCof01, nVars-1 ) +
2131 Kit_TruthXorCount( pCof00, pCof10, nVars-1 ) +
2132 Kit_TruthXorCount( pCof00, pCof11, nVars-1 ) +
2133 Kit_TruthXorCount( pCof01, pCof10, nVars-1 ) +
2134 Kit_TruthXorCount( pCof01, pCof11, nVars-1 ) +
2135 Kit_TruthXorCount( pCof10, pCof11, nVars-1 );
2136 }
2137 }
2138
2139 printf( "\n" );
2140 printf( " V: " );
2141 for ( v = 0; v < nVars; v++ )
2142 printf( "%8c ", v+'a' );
2143 printf( "\n" );
2144
2145 printf( " M: " );
2146 for ( v = 0; v < nVars; v++ )
2147 printf( "%8d ", Mints[v] );
2148 printf( "\n" );
2149
2150 printf( " U: " );
2151 for ( v = 0; v < nVars; v++ )
2152 printf( "%8d ", Unique1[v] );
2153 printf( "\n" );
2154 printf( "\n" );
2155
2156 printf( "Unique:\n" );
2157 for ( i = 0; i < nVars; i++ )
2158 {
2159 printf( " %2d ", i );
2160 for ( v = 0; v < nVars; v++ )
2161 printf( "%8d ", Unique2[i][v] );
2162 printf( "\n" );
2163 }
2164
2165 printf( "Common:\n" );
2166 for ( i = 0; i < nVars; i++ )
2167 {
2168 printf( " %2d ", i );
2169 for ( v = 0; v < nVars; v++ )
2170 printf( "%8d ", Common2[i][v] );
2171 printf( "\n" );
2172 }
2173
2174 printf( "Total:\n" );
2175 for ( i = 0; i < nVars; i++ )
2176 {
2177 printf( " %2d ", i );
2178 for ( v = 0; v < nVars; v++ )
2179 printf( "%8d ", Total2[i][v] );
2180 printf( "\n" );
2181 }
2182
2183 ABC_FREE( pIn );
2184 ABC_FREE( pOut );
2185 ABC_FREE( pCof00 );
2186 ABC_FREE( pCof01 );
2187 ABC_FREE( pCof10 );
2188 ABC_FREE( pCof11 );
2189 ABC_FREE( pBytes );
2190}
2191
2203void Kit_TruthPrintProfile( unsigned * pTruth, int nVars )
2204{
2205 unsigned uTruth[2];
2206 if ( nVars >= 6 )
2207 {
2208 Kit_TruthPrintProfile_int( pTruth, nVars );
2209 return;
2210 }
2211 assert( nVars >= 2 );
2212 uTruth[0] = pTruth[0];
2213 uTruth[1] = pTruth[0];
2214 Kit_TruthPrintProfile( uTruth, 6 );
2215}
2216
2217
2221
2222
2223ABC_NAMESPACE_IMPL_END
2224
nWords
int nWords
Definition abcNpn.c:127
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Var
int Var
Definition exorList.c:228
Kit_TruthCofactor0
void Kit_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:368
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition kitTruth.c:346
Kit_TruthMuxVar
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition kitTruth.c:1069
Kit_TruthHash
unsigned Kit_TruthHash(unsigned *pIn, int nWords)
Definition kitTruth.c:1560
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:573
Kit_TruthDumpToFile
char * Kit_TruthDumpToFile(unsigned *pTruth, int nVars, int nFile)
Definition kitTruth.c:2004
Kit_TruthBestCofVar
int Kit_TruthBestCofVar(unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
Definition kitTruth.c:1365
Kit_TruthSemiCanonicize
unsigned Kit_TruthSemiCanonicize(unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
Definition kitTruth.c:1657
Kit_TruthUniqueNew
void Kit_TruthUniqueNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:922
Kit_TruthCountOnesInCofs
void Kit_TruthCountOnesInCofs(unsigned *pTruth, int nVars, int *pStore)
Definition kitTruth.c:1410
Kit_TruthChangePhase
void Kit_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:1259
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:521
Kit_TruthSwapAdjacentVars2
void Kit_TruthSwapAdjacentVars2(unsigned *pIn, unsigned *pOut, int nVars, int Start)
Definition kitTruth.c:103
Kit_TruthForallNew
void Kit_TruthForallNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:867
Kit_TruthBooleanDiffCount
int Kit_TruthBooleanDiffCount(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:977
Kit_TruthSupportSize
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition kitTruth.c:327
Kit_TruthCofactor1
void Kit_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:470
Kit_PrintHexadecimal
void Kit_PrintHexadecimal(FILE *pFile, unsigned Sign[], int nVars)
Definition kitTruth.c:1939
Kit_TruthVarIsVacuous
int Kit_TruthVarIsVacuous(unsigned *pOnset, unsigned *pOffset, int nVars, int iVar)
Definition kitTruth.c:625
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:270
Kit_TruthExistSet
void Kit_TruthExistSet(unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
Definition kitTruth.c:793
Kit_TruthPrintProfile
void Kit_TruthPrintProfile(unsigned *pTruth, int nVars)
Definition kitTruth.c:2203
Kit_TruthExist
void Kit_TruthExist(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:684
Kit_TruthCofactor0Count
int Kit_TruthCofactor0Count(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:419
Kit_TruthCountMintermsPrecomp
void Kit_TruthCountMintermsPrecomp()
Definition kitTruth.c:1966
Kit_TruthShrink
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:200
Kit_TruthCountMinterms
int Kit_TruthCountMinterms(unsigned *pTruth, int nVars, int *pRes, int *pBytesInit)
Definition kitTruth.c:1839
Kit_TruthExistNew
void Kit_TruthExistNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:738
Kit_TruthCountOnesInCofsSlow
void Kit_TruthCountOnesInCofsSlow(unsigned *pTruth, int nVars, int *pStore, unsigned *pAux)
Definition kitTruth.c:1537
Kit_TruthCountOnesInCofs0
void Kit_TruthCountOnesInCofs0(unsigned *pTruth, int nVars, int *pStore)
Definition kitTruth.c:1486
Kit_TruthPrintProfile_int
void Kit_TruthPrintProfile_int(unsigned *pTruth, int nVars)
Definition kitTruth.c:2029
Kit_TruthPermute
void Kit_TruthPermute(unsigned *pOut, unsigned *pIn, int nVars, char *pPerm, int fReturnIn)
Definition kitTruth.c:233
Kit_TruthXorCount
int Kit_TruthXorCount(unsigned *pTruth0, unsigned *pTruth1, int nVars)
Definition kitTruth.c:1028
Kit_TruthSwapAdjacentVars
ABC_NAMESPACE_IMPL_START void Kit_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
DECLARATIONS ///.
Definition kitTruth.c:46
Kit_TruthForall
void Kit_TruthForall(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:813
Kit_TruthForallSet
void Kit_TruthForallSet(unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
Definition kitTruth.c:1048
Kit_TruthVarsAntiSymm
int Kit_TruthVarsAntiSymm(unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
Definition kitTruth.c:1223
Kit_TruthStretch
void Kit_TruthStretch(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:166
Kit_TruthMinCofSuppOverlap
int Kit_TruthMinCofSuppOverlap(unsigned *pTruth, int nVars, int *pVarMin)
Definition kitTruth.c:1315
Kit_TruthMuxVarPhase
void Kit_TruthMuxVarPhase(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
Definition kitTruth.c:1125
Kit_TruthVarsSymm
int Kit_TruthVarsSymm(unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
Definition kitTruth.c:1187
KIT_INFINITY
#define KIT_INFINITY
Definition kit.h:176
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
sprintf
char * sprintf()