ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
kitDsd.c
Go to the documentation of this file.
1
20
21#include "kit.h"
22#include "misc/extra/extra.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
34
46Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
47{
48 Kit_DsdMan_t * p;
49 p = ABC_ALLOC( Kit_DsdMan_t, 1 );
50 memset( p, 0, sizeof(Kit_DsdMan_t) );
51 p->nVars = nVars;
52 p->nWords = Kit_TruthWordNum( p->nVars );
53 p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
54 p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
55 p->dd = Cloud_Init( 16, 14 );
56 p->vTtBdds = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
57 p->vNodes = Vec_IntAlloc( 512 );
58 return p;
59}
60
72void Kit_DsdManFree( Kit_DsdMan_t * p )
73{
74 Cloud_Quit( p->dd );
75 Vec_IntFree( p->vNodes );
76 Vec_PtrFree( p->vTtBdds );
77 Vec_PtrFree( p->vTtElems );
78 Vec_PtrFree( p->vTtNodes );
79 ABC_FREE( p );
80}
81
93Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans )
94{
95 Kit_DsdObj_t * pObj;
96 int nSize = sizeof(Kit_DsdObj_t) + sizeof(unsigned) * (Kit_DsdObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
97 pObj = (Kit_DsdObj_t *)ABC_ALLOC( char, nSize );
98 memset( pObj, 0, (size_t)nSize );
99 pObj->Id = pNtk->nVars + pNtk->nNodes;
100 pObj->Type = Type;
101 pObj->nFans = nFans;
102 pObj->Offset = Kit_DsdObjOffset( nFans );
103 // add the object
104 if ( pNtk->nNodes == pNtk->nNodesAlloc )
105 {
106 pNtk->nNodesAlloc *= 2;
107 pNtk->pNodes = ABC_REALLOC( Kit_DsdObj_t *, pNtk->pNodes, pNtk->nNodesAlloc );
108 }
109 assert( pNtk->nNodes < pNtk->nNodesAlloc );
110 pNtk->pNodes[pNtk->nNodes++] = pObj;
111 return pObj;
112}
113
125void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
126{
127 ABC_FREE( pObj );
128}
129
141Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
142{
143 Kit_DsdNtk_t * pNtk;
144 pNtk = ABC_ALLOC( Kit_DsdNtk_t, 1 );
145 memset( pNtk, 0, sizeof(Kit_DsdNtk_t) );
146 pNtk->pNodes = ABC_ALLOC( Kit_DsdObj_t *, nVars+1 );
147 pNtk->nVars = nVars;
148 pNtk->nNodesAlloc = nVars+1;
149 pNtk->pMem = ABC_ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
150 return pNtk;
151}
152
164void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
165{
166 Kit_DsdObj_t * pObj;
167 unsigned i;
168 Kit_DsdNtkForEachObj( pNtk, pObj, i )
169 ABC_FREE( pObj );
170 ABC_FREE( pNtk->pSupps );
171 ABC_FREE( pNtk->pNodes );
172 ABC_FREE( pNtk->pMem );
173 ABC_FREE( pNtk );
174}
175
187void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
188{
189 int nDigits, Digit, k;
190 nDigits = (1 << nFans) / 4;
191 for ( k = nDigits - 1; k >= 0; k-- )
192 {
193 Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15);
194 if ( Digit < 10 )
195 fprintf( pFile, "%d", Digit );
196 else
197 fprintf( pFile, "%c", 'A' + Digit-10 );
198 }
199}
200
212char * Kit_DsdWriteHex( char * pBuff, unsigned * pTruth, int nFans )
213{
214 int nDigits, Digit, k;
215 nDigits = (1 << nFans) / 4;
216 for ( k = nDigits - 1; k >= 0; k-- )
217 {
218 Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15);
219 if ( Digit < 10 )
220 *pBuff++ = '0' + Digit;
221 else
222 *pBuff++ = 'A' + Digit-10;
223 }
224 return pBuff;
225}
226
238void Kit_DsdPrint2_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id )
239{
240 Kit_DsdObj_t * pObj;
241 unsigned iLit, i;
242 char Symbol;
243
244 pObj = Kit_DsdNtkObj( pNtk, Id );
245 if ( pObj == NULL )
246 {
247 assert( Id < pNtk->nVars );
248 fprintf( pFile, "%c", 'a' + Id );
249 return;
250 }
251
252 if ( pObj->Type == KIT_DSD_CONST1 )
253 {
254 assert( pObj->nFans == 0 );
255 fprintf( pFile, "Const1" );
256 return;
257 }
258
259 if ( pObj->Type == KIT_DSD_VAR )
260 assert( pObj->nFans == 1 );
261
262 if ( pObj->Type == KIT_DSD_AND )
263 Symbol = '*';
264 else if ( pObj->Type == KIT_DSD_XOR )
265 Symbol = '+';
266 else
267 Symbol = ',';
268
269 if ( pObj->Type == KIT_DSD_PRIME )
270 fprintf( pFile, "[" );
271 else
272 fprintf( pFile, "(" );
273 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
274 {
275 if ( Abc_LitIsCompl(iLit) )
276 fprintf( pFile, "!" );
277 Kit_DsdPrint2_rec( pFile, pNtk, Abc_Lit2Var(iLit) );
278 if ( i < pObj->nFans - 1 )
279 fprintf( pFile, "%c", Symbol );
280 }
281 if ( pObj->Type == KIT_DSD_PRIME )
282 fprintf( pFile, "]" );
283 else
284 fprintf( pFile, ")" );
285}
286
298void Kit_DsdPrint2( FILE * pFile, Kit_DsdNtk_t * pNtk )
299{
300// fprintf( pFile, "F = " );
301 if ( Abc_LitIsCompl(pNtk->Root) )
302 fprintf( pFile, "!" );
303 Kit_DsdPrint2_rec( pFile, pNtk, Abc_Lit2Var(pNtk->Root) );
304// fprintf( pFile, "\n" );
305}
306
318void Kit_DsdPrint_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id )
319{
320 Kit_DsdObj_t * pObj;
321 unsigned iLit, i;
322 char Symbol;
323
324 pObj = Kit_DsdNtkObj( pNtk, Id );
325 if ( pObj == NULL )
326 {
327 assert( Id < pNtk->nVars );
328 fprintf( pFile, "%c", 'a' + Id );
329 return;
330 }
331
332 if ( pObj->Type == KIT_DSD_CONST1 )
333 {
334 assert( pObj->nFans == 0 );
335 fprintf( pFile, "Const1" );
336 return;
337 }
338
339 if ( pObj->Type == KIT_DSD_VAR )
340 assert( pObj->nFans == 1 );
341
342 if ( pObj->Type == KIT_DSD_AND )
343 Symbol = '*';
344 else if ( pObj->Type == KIT_DSD_XOR )
345 Symbol = '+';
346 else
347 Symbol = ',';
348
349 if ( pObj->Type == KIT_DSD_PRIME )
350 Kit_DsdPrintHex( pFile, Kit_DsdObjTruth(pObj), pObj->nFans );
351
352 fprintf( pFile, "(" );
353 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
354 {
355 if ( Abc_LitIsCompl(iLit) )
356 fprintf( pFile, "!" );
357 Kit_DsdPrint_rec( pFile, pNtk, Abc_Lit2Var(iLit) );
358 if ( i < pObj->nFans - 1 )
359 fprintf( pFile, "%c", Symbol );
360 }
361 fprintf( pFile, ")" );
362}
363
375void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
376{
377 fprintf( pFile, "F = " );
378 if ( Abc_LitIsCompl(pNtk->Root) )
379 fprintf( pFile, "!" );
380 Kit_DsdPrint_rec( pFile, pNtk, Abc_Lit2Var(pNtk->Root) );
381// fprintf( pFile, "\n" );
382}
383
395char * Kit_DsdWrite_rec( char * pBuff, Kit_DsdNtk_t * pNtk, int Id )
396{
397 Kit_DsdObj_t * pObj;
398 unsigned iLit, i;
399 char Symbol;
400
401 pObj = Kit_DsdNtkObj( pNtk, Id );
402 if ( pObj == NULL )
403 {
404 assert( Id < pNtk->nVars );
405 *pBuff++ = 'a' + Id;
406 return pBuff;
407 }
408
409 if ( pObj->Type == KIT_DSD_CONST1 )
410 {
411 assert( pObj->nFans == 0 );
412 sprintf( pBuff, "%s", "Const1" );
413 return pBuff + strlen("Const1");
414 }
415
416 if ( pObj->Type == KIT_DSD_VAR )
417 assert( pObj->nFans == 1 );
418
419 if ( pObj->Type == KIT_DSD_AND )
420 Symbol = '*';
421 else if ( pObj->Type == KIT_DSD_XOR )
422 Symbol = '+';
423 else
424 Symbol = ',';
425
426 if ( pObj->Type == KIT_DSD_PRIME )
427 pBuff = Kit_DsdWriteHex( pBuff, Kit_DsdObjTruth(pObj), pObj->nFans );
428
429 *pBuff++ = '(';
430 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
431 {
432 if ( Abc_LitIsCompl(iLit) )
433 *pBuff++ = '!';
434 pBuff = Kit_DsdWrite_rec( pBuff, pNtk, Abc_Lit2Var(iLit) );
435 if ( i < pObj->nFans - 1 )
436 *pBuff++ = Symbol;
437 }
438 *pBuff++ = ')';
439 return pBuff;
440}
441
453void Kit_DsdWrite( char * pBuff, Kit_DsdNtk_t * pNtk )
454{
455 if ( Abc_LitIsCompl(pNtk->Root) )
456 *pBuff++ = '!';
457 pBuff = Kit_DsdWrite_rec( pBuff, pNtk, Abc_Lit2Var(pNtk->Root) );
458 *pBuff = 0;
459}
460
472void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
473{
474 Kit_DsdNtk_t * pTemp;
475 pTemp = Kit_DsdExpand( pNtk );
476 Kit_DsdPrint( stdout, pTemp );
477 Kit_DsdNtkFree( pTemp );
478}
479
491void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
492{
493 Kit_DsdNtk_t * pTemp, * pTemp2;
494// pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
495 pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
496// Kit_DsdPrintExpanded( pTemp );
497 pTemp2 = Kit_DsdExpand( pTemp );
498 Kit_DsdPrint( stdout, pTemp2 );
499 Kit_DsdVerify( pTemp2, pTruth, nVars );
500 Kit_DsdNtkFree( pTemp2 );
501 Kit_DsdNtkFree( pTemp );
502}
503
515void Kit_DsdPrintFromTruth2( FILE * pFile, unsigned * pTruth, int nVars )
516{
517 Kit_DsdNtk_t * pTemp, * pTemp2;
518 pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 0 );
519 pTemp2 = Kit_DsdExpand( pTemp );
520 Kit_DsdPrint2( pFile, pTemp2 );
521 Kit_DsdVerify( pTemp2, pTruth, nVars );
522 Kit_DsdNtkFree( pTemp2 );
523 Kit_DsdNtkFree( pTemp );
524}
525
537void Kit_DsdWriteFromTruth( char * pBuffer, unsigned * pTruth, int nVars )
538{
539 Kit_DsdNtk_t * pTemp, * pTemp2;
540// pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
541 pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
542// Kit_DsdPrintExpanded( pTemp );
543 pTemp2 = Kit_DsdExpand( pTemp );
544 Kit_DsdWrite( pBuffer, pTemp2 );
545 Kit_DsdVerify( pTemp2, pTruth, nVars );
546 Kit_DsdNtkFree( pTemp2 );
547 Kit_DsdNtkFree( pTemp );
548}
549
561unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
562{
563 Kit_DsdObj_t * pObj;
564 unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
565 unsigned i, iLit, fCompl;
566// unsigned m, nMints, * pTruthPrime, * pTruthMint;
567
568 // get the node with this ID
569 pObj = Kit_DsdNtkObj( pNtk, Id );
570 pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
571
572 // special case: literal of an internal node
573 if ( pObj == NULL )
574 {
575 assert( Id < pNtk->nVars );
576 return pTruthRes;
577 }
578
579 // constant node
580 if ( pObj->Type == KIT_DSD_CONST1 )
581 {
582 assert( pObj->nFans == 0 );
583 Kit_TruthFill( pTruthRes, pNtk->nVars );
584 return pTruthRes;
585 }
586
587 // elementary variable node
588 if ( pObj->Type == KIT_DSD_VAR )
589 {
590 assert( pObj->nFans == 1 );
591 iLit = pObj->pFans[0];
592 pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Abc_Lit2Var(iLit) );
593 if ( Abc_LitIsCompl(iLit) )
594 Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
595 else
596 Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
597 return pTruthRes;
598 }
599
600 // collect the truth tables of the fanins
601 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
602 pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Abc_Lit2Var(iLit) );
603 // create the truth table
604
605 // simple gates
606 if ( pObj->Type == KIT_DSD_AND )
607 {
608 Kit_TruthFill( pTruthRes, pNtk->nVars );
609 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
610 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
611 return pTruthRes;
612 }
613 if ( pObj->Type == KIT_DSD_XOR )
614 {
615 Kit_TruthClear( pTruthRes, pNtk->nVars );
616 fCompl = 0;
617 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
618 {
619 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
620 fCompl ^= Abc_LitIsCompl(iLit);
621 }
622 if ( fCompl )
623 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
624 return pTruthRes;
625 }
626 assert( pObj->Type == KIT_DSD_PRIME );
627/*
628 // get the truth table of the prime node
629 pTruthPrime = Kit_DsdObjTruth( pObj );
630 // get storage for the temporary minterm
631 pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
632 // go through the minterms
633 nMints = (1 << pObj->nFans);
634 Kit_TruthClear( pTruthRes, pNtk->nVars );
635 for ( m = 0; m < nMints; m++ )
636 {
637 if ( !Kit_TruthHasBit(pTruthPrime, m) )
638 continue;
639 Kit_TruthFill( pTruthMint, pNtk->nVars );
640 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
641 Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Abc_LitIsCompl(iLit) );
642 Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
643 }
644*/
645 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
646 if ( Abc_LitIsCompl(iLit) )
647 Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
648 pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
649 Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
650 return pTruthRes;
651}
652
664unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
665{
666 unsigned * pTruthRes;
667 int i;
668 // assign elementary truth ables
669 assert( pNtk->nVars <= p->nVars );
670 for ( i = 0; i < (int)pNtk->nVars; i++ )
671 Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
672 // compute truth table for each node
673 pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Abc_Lit2Var(pNtk->Root) );
674 // complement the truth table if needed
675 if ( Abc_LitIsCompl(pNtk->Root) )
676 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
677 return pTruthRes;
678}
679
691unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
692{
693 Kit_DsdObj_t * pObj;
694 unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
695 unsigned i, iLit, fCompl, nPartial = 0;
696// unsigned m, nMints, * pTruthPrime, * pTruthMint;
697
698 // get the node with this ID
699 pObj = Kit_DsdNtkObj( pNtk, Id );
700 pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
701
702 // special case: literal of an internal node
703 if ( pObj == NULL )
704 {
705 assert( Id < pNtk->nVars );
706 assert( !uSupp || uSupp != (uSupp & ~(1<<Id)) );
707 return pTruthRes;
708 }
709
710 // constant node
711 if ( pObj->Type == KIT_DSD_CONST1 )
712 {
713 assert( pObj->nFans == 0 );
714 Kit_TruthFill( pTruthRes, pNtk->nVars );
715 return pTruthRes;
716 }
717
718 // elementary variable node
719 if ( pObj->Type == KIT_DSD_VAR )
720 {
721 assert( pObj->nFans == 1 );
722 iLit = pObj->pFans[0];
723 assert( Kit_DsdLitIsLeaf( pNtk, iLit ) );
724 pTruthFans[0] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp );
725 if ( Abc_LitIsCompl(iLit) )
726 Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
727 else
728 Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
729 return pTruthRes;
730 }
731
732 // collect the truth tables of the fanins
733 if ( uSupp )
734 {
735 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
736 if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) )
737 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp );
738 else
739 {
740 pTruthFans[i] = NULL;
741 nPartial = 1;
742 }
743 }
744 else
745 {
746 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
747 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp );
748 }
749 // create the truth table
750
751 // simple gates
752 if ( pObj->Type == KIT_DSD_AND )
753 {
754 Kit_TruthFill( pTruthRes, pNtk->nVars );
755 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
756 if ( pTruthFans[i] )
757 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
758 return pTruthRes;
759 }
760 if ( pObj->Type == KIT_DSD_XOR )
761 {
762 Kit_TruthClear( pTruthRes, pNtk->nVars );
763 fCompl = 0;
764 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
765 {
766 if ( pTruthFans[i] )
767 {
768 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
769 fCompl ^= Abc_LitIsCompl(iLit);
770 }
771 }
772 if ( fCompl )
773 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
774 return pTruthRes;
775 }
776 assert( pObj->Type == KIT_DSD_PRIME );
777
778 if ( uSupp && nPartial )
779 {
780 // find the only non-empty component
781 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
782 if ( pTruthFans[i] )
783 break;
784 assert( i < pObj->nFans );
785 return pTruthFans[i];
786 }
787/*
788 // get the truth table of the prime node
789 pTruthPrime = Kit_DsdObjTruth( pObj );
790 // get storage for the temporary minterm
791 pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
792 // go through the minterms
793 nMints = (1 << pObj->nFans);
794 Kit_TruthClear( pTruthRes, pNtk->nVars );
795 for ( m = 0; m < nMints; m++ )
796 {
797 if ( !Kit_TruthHasBit(pTruthPrime, m) )
798 continue;
799 Kit_TruthFill( pTruthMint, pNtk->nVars );
800 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
801 Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Abc_LitIsCompl(iLit) );
802 Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
803 }
804*/
805 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
806 if ( Abc_LitIsCompl(iLit) )
807 Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
808 pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
809 Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
810 return pTruthRes;
811}
812
824unsigned * Kit_DsdTruthComputeOne( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
825{
826 unsigned * pTruthRes;
827 int i;
828 // if support is specified, request that supports are available
829 if ( uSupp )
830 Kit_DsdGetSupports( pNtk );
831 // assign elementary truth tables
832 assert( pNtk->nVars <= p->nVars );
833 for ( i = 0; i < (int)pNtk->nVars; i++ )
834 Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
835 // compute truth table for each node
836 pTruthRes = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(pNtk->Root), uSupp );
837 // complement the truth table if needed
838 if ( Abc_LitIsCompl(pNtk->Root) )
839 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
840 return pTruthRes;
841}
842
854unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp, int iVar, unsigned * pTruthDec )
855{
856 Kit_DsdObj_t * pObj;
857 int pfBoundSet[16];
858 unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
859 unsigned i, iLit, fCompl, nPartial, uSuppFan, uSuppCur;
860// unsigned m, nMints, * pTruthPrime, * pTruthMint;
861 assert( uSupp > 0 );
862
863 // get the node with this ID
864 pObj = Kit_DsdNtkObj( pNtk, Id );
865 pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
866 if ( pObj == NULL )
867 {
868 assert( Id < pNtk->nVars );
869 return pTruthRes;
870 }
871 assert( pObj->Type != KIT_DSD_CONST1 );
872 assert( pObj->Type != KIT_DSD_VAR );
873
874 // count the number of intersecting fanins
875 // collect the total support of the intersecting fanins
876 nPartial = 0;
877 uSuppFan = 0;
878 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
879 {
880 uSuppCur = Kit_DsdLitSupport(pNtk, iLit);
881 if ( uSupp & uSuppCur )
882 {
883 nPartial++;
884 uSuppFan |= uSuppCur;
885 }
886 }
887
888 // if there is no intersection, or full intersection, use simple procedure
889 if ( nPartial == 0 || nPartial == pObj->nFans )
890 return Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Id, 0 );
891
892 // if support of the component includes some other variables
893 // we need to continue constructing it as usual by the two-function procedure
894 if ( uSuppFan != (uSuppFan & uSupp) )
895 {
896 assert( nPartial == 1 );
897// return Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Id, uSupp, iVar, pTruthDec );
898 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
899 {
900 if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) )
901 pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Abc_Lit2Var(iLit), uSupp, iVar, pTruthDec );
902 else
903 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), 0 );
904 }
905
906 // create composition/decomposition functions
907 if ( pObj->Type == KIT_DSD_AND )
908 {
909 Kit_TruthFill( pTruthRes, pNtk->nVars );
910 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
911 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
912 return pTruthRes;
913 }
914 if ( pObj->Type == KIT_DSD_XOR )
915 {
916 Kit_TruthClear( pTruthRes, pNtk->nVars );
917 fCompl = 0;
918 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
919 {
920 fCompl ^= Abc_LitIsCompl(iLit);
921 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
922 }
923 if ( fCompl )
924 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
925 return pTruthRes;
926 }
927 assert( pObj->Type == KIT_DSD_PRIME );
928 }
929 else
930 {
931 assert( uSuppFan == (uSuppFan & uSupp) );
932 assert( nPartial < pObj->nFans );
933 // the support of the insecting component(s) is contained in the bound-set
934 // and yet there are components that are not contained in the bound set
935
936 // solve the fanins and collect info, which components belong to the bound set
937 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
938 {
939 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Abc_Lit2Var(iLit), 0 );
940 pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0);
941 }
942
943 // create composition/decomposition functions
944 if ( pObj->Type == KIT_DSD_AND )
945 {
946 Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
947 Kit_TruthFill( pTruthDec, pNtk->nVars );
948 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
949 if ( pfBoundSet[i] )
950 Kit_TruthAndPhase( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
951 else
952 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Abc_LitIsCompl(iLit) );
953 return pTruthRes;
954 }
955 if ( pObj->Type == KIT_DSD_XOR )
956 {
957 Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
958 Kit_TruthClear( pTruthDec, pNtk->nVars );
959 fCompl = 0;
960 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
961 {
962 fCompl ^= Abc_LitIsCompl(iLit);
963 if ( pfBoundSet[i] )
964 Kit_TruthXor( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars );
965 else
966 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
967 }
968 if ( fCompl )
969 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
970 return pTruthRes;
971 }
972 assert( pObj->Type == KIT_DSD_PRIME );
973 assert( nPartial == 1 );
974
975 // find the only non-empty component
976 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
977 if ( pfBoundSet[i] )
978 break;
979 assert( i < pObj->nFans );
980
981 // save this component as the decomposed function
982 Kit_TruthCopy( pTruthDec, pTruthFans[i], pNtk->nVars );
983 // set the corresponding component to be the new variable
984 Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar );
985 }
986/*
987 // get the truth table of the prime node
988 pTruthPrime = Kit_DsdObjTruth( pObj );
989 // get storage for the temporary minterm
990 pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
991 // go through the minterms
992 nMints = (1 << pObj->nFans);
993 Kit_TruthClear( pTruthRes, pNtk->nVars );
994 for ( m = 0; m < nMints; m++ )
995 {
996 if ( !Kit_TruthHasBit(pTruthPrime, m) )
997 continue;
998 Kit_TruthFill( pTruthMint, pNtk->nVars );
999 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1000 Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Abc_LitIsCompl(iLit) );
1001 Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
1002 }
1003*/
1004// Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1005// assert( !Abc_LitIsCompl(iLit) );
1006 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1007 if ( Abc_LitIsCompl(iLit) )
1008 Kit_TruthNot( pTruthFans[i], pTruthFans[i], pNtk->nVars );
1009 pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
1010 Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
1011 return pTruthRes;
1012}
1013
1025unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthDec )
1026{
1027 unsigned * pTruthRes, uSuppAll;
1028 int i;
1029 assert( uSupp > 0 );
1030 assert( pNtk->nVars <= p->nVars );
1031 // compute support of all nodes
1032 uSuppAll = Kit_DsdGetSupports( pNtk );
1033 // consider special case - there is no overlap
1034 if ( (uSupp & uSuppAll) == 0 )
1035 {
1036 Kit_TruthClear( pTruthDec, pNtk->nVars );
1037 return Kit_DsdTruthCompute( p, pNtk );
1038 }
1039 // consider special case - support is fully contained
1040 if ( (uSupp & uSuppAll) == uSuppAll )
1041 {
1042 pTruthRes = Kit_DsdTruthCompute( p, pNtk );
1043 Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars );
1044 Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
1045 return pTruthRes;
1046 }
1047 // assign elementary truth tables
1048 for ( i = 0; i < (int)pNtk->nVars; i++ )
1049 Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
1050 // compute truth table for each node
1051 pTruthRes = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Abc_Lit2Var(pNtk->Root), uSupp, iVar, pTruthDec );
1052 // complement the truth table if needed
1053 if ( Abc_LitIsCompl(pNtk->Root) )
1054 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
1055 return pTruthRes;
1056}
1057
1069void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
1070{
1071 Kit_DsdMan_t * p;
1072 unsigned * pTruth;
1073 p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
1074 pTruth = Kit_DsdTruthCompute( p, pNtk );
1075 Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
1076 Kit_DsdManFree( p );
1077}
1078
1090void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec )
1091{
1092 unsigned * pTruth = Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar, pTruthDec );
1093 if ( pTruthCo )
1094 Kit_TruthCopy( pTruthCo, pTruth, pNtk->nVars );
1095}
1096
1108void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
1109{
1110 unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp );
1111 Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
1112/*
1113 // verification
1114 {
1115 // compute the same function using different procedure
1116 unsigned * pTruthTemp = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes + 1);
1117 pNtk->pSupps = NULL;
1118 Kit_DsdTruthComputeTwo( p, pNtk, uSupp, -1, pTruthTemp );
1119// if ( !Kit_TruthIsEqual( pTruthTemp, pTruthRes, pNtk->nVars ) )
1120 if ( !Kit_TruthIsEqualWithPhase( pTruthTemp, pTruthRes, pNtk->nVars ) )
1121 {
1122 printf( "Verification FAILED!\n" );
1123 Kit_DsdPrint( stdout, pNtk );
1124 Kit_DsdPrintFromTruth( pTruthRes, pNtk->nVars );
1125 Kit_DsdPrintFromTruth( pTruthTemp, pNtk->nVars );
1126 }
1127// else
1128// printf( "Verification successful.\n" );
1129 }
1130*/
1131}
1132
1144int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCounter )
1145{
1146 Kit_DsdObj_t * pObj;
1147 unsigned iLit, i, Res0, Res1;
1148 pObj = Kit_DsdNtkObj( pNtk, Id );
1149 if ( pObj == NULL )
1150 return 0;
1151 if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
1152 {
1153 assert( pObj->nFans == 2 );
1154 Res0 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(pObj->pFans[0]), pCounter );
1155 Res1 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(pObj->pFans[1]), pCounter );
1156 if ( Res0 == 0 && Res1 > 0 )
1157 return Res1 - 1;
1158 if ( Res0 > 0 && Res1 == 0 )
1159 return Res0 - 1;
1160 (*pCounter)++;
1161 return nLutSize - 2;
1162 }
1163 assert( pObj->Type == KIT_DSD_PRIME );
1164 if ( (int)pObj->nFans > nLutSize ) //+ 1 )
1165 {
1166 *pCounter = 1000;
1167 return 0;
1168 }
1169 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1170 Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(iLit), pCounter );
1171 (*pCounter)++;
1172// if ( (int)pObj->nFans == nLutSize + 1 )
1173// (*pCounter)++;
1174 return nLutSize - pObj->nFans;
1175}
1176
1188int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
1189{
1190 int Counter = 0;
1191 if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_CONST1 )
1192 return 0;
1193 if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_VAR )
1194 return 0;
1195 Kit_DsdCountLuts_rec( pNtk, nLutSize, Abc_Lit2Var(pNtk->Root), &Counter );
1196 if ( Counter >= 1000 )
1197 return -1;
1198 return Counter;
1199}
1200
1212int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
1213{
1214 Kit_DsdObj_t * pObj;
1215 unsigned i, nSizeMax = 0;
1216 Kit_DsdNtkForEachObj( pNtk, pObj, i )
1217 {
1218 if ( pObj->Type != KIT_DSD_PRIME )
1219 continue;
1220 if ( nSizeMax < pObj->nFans )
1221 nSizeMax = pObj->nFans;
1222 }
1223 return nSizeMax;
1224}
1225
1237Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk )
1238{
1239 Kit_DsdObj_t * pObj, * pObjMax = NULL;
1240 unsigned i, nSizeMax = 0;
1241 Kit_DsdNtkForEachObj( pNtk, pObj, i )
1242 {
1243 if ( pObj->Type != KIT_DSD_PRIME )
1244 continue;
1245 if ( nSizeMax < pObj->nFans )
1246 {
1247 nSizeMax = pObj->nFans;
1248 pObjMax = pObj;
1249 }
1250 }
1251 return pObjMax;
1252}
1253
1265unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk )
1266{
1267 Kit_DsdObj_t * pObj;
1268 unsigned i, uSupport = 0;
1269// ABC_FREE( pNtk->pSupps );
1270 Kit_DsdGetSupports( pNtk );
1271 Kit_DsdNtkForEachObj( pNtk, pObj, i )
1272 {
1273 if ( pObj->Type != KIT_DSD_PRIME )
1274 continue;
1275 uSupport |= Kit_DsdLitSupport( pNtk, Abc_Var2Lit(pObj->Id,0) );
1276 }
1277 return uSupport;
1278}
1279
1280
1292void Kit_DsdExpandCollectAnd_rec( Kit_DsdNtk_t * p, unsigned iLit, unsigned * piLitsNew, int * nLitsNew )
1293{
1294 Kit_DsdObj_t * pObj;
1295 unsigned i, iLitFanin;
1296 // check the end of the supergate
1297 pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1298 if ( Abc_LitIsCompl(iLit) || Abc_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND )
1299 {
1300 piLitsNew[(*nLitsNew)++] = iLit;
1301 return;
1302 }
1303 // iterate through the fanins
1304 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1305 Kit_DsdExpandCollectAnd_rec( p, iLitFanin, piLitsNew, nLitsNew );
1306}
1307
1319void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, unsigned iLit, unsigned * piLitsNew, int * nLitsNew )
1320{
1321 Kit_DsdObj_t * pObj;
1322 unsigned i, iLitFanin;
1323 // check the end of the supergate
1324 pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1325 if ( Abc_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR )
1326 {
1327 piLitsNew[(*nLitsNew)++] = iLit;
1328 return;
1329 }
1330 // iterate through the fanins
1331 pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1332 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1333 Kit_DsdExpandCollectXor_rec( p, iLitFanin, piLitsNew, nLitsNew );
1334 // if the literal was complemented, pass the complemented attribute somewhere
1335 if ( Abc_LitIsCompl(iLit) )
1336 piLitsNew[0] = Abc_LitNot( piLitsNew[0] );
1337}
1338
1350int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
1351{
1352 unsigned * pTruth, * pTruthNew;
1353 unsigned i, iLitFanin, piLitsNew[16], nLitsNew = 0;
1354 Kit_DsdObj_t * pObj, * pObjNew;
1355
1356 // consider the case of simple gate
1357 pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1358 if ( pObj == NULL )
1359 return iLit;
1360 if ( pObj->Type == KIT_DSD_AND )
1361 {
1362 Kit_DsdExpandCollectAnd_rec( p, Abc_LitRegular(iLit), piLitsNew, (int *)&nLitsNew );
1363 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
1364 for ( i = 0; i < pObjNew->nFans; i++ )
1365 pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
1366 return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1367 }
1368 if ( pObj->Type == KIT_DSD_XOR )
1369 {
1370 int fCompl = Abc_LitIsCompl(iLit);
1371 Kit_DsdExpandCollectXor_rec( p, Abc_LitRegular(iLit), piLitsNew, (int *)&nLitsNew );
1372 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
1373 for ( i = 0; i < pObjNew->nFans; i++ )
1374 {
1375 pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Abc_LitRegular(piLitsNew[i]) );
1376 fCompl ^= Abc_LitIsCompl(piLitsNew[i]);
1377 }
1378 return Abc_Var2Lit( pObjNew->Id, fCompl );
1379 }
1380 assert( pObj->Type == KIT_DSD_PRIME );
1381
1382 // create new PRIME node
1383 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
1384 // copy the truth table
1385 pTruth = Kit_DsdObjTruth( pObj );
1386 pTruthNew = Kit_DsdObjTruth( pObjNew );
1387 Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
1388 // create fanins
1389 Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
1390 {
1391 pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, iLitFanin );
1392 // complement the corresponding inputs of the truth table
1393 if ( Abc_LitIsCompl(pObjNew->pFans[i]) )
1394 {
1395 pObjNew->pFans[i] = Abc_LitRegular(pObjNew->pFans[i]);
1396 Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
1397 }
1398 }
1399
1400 if ( pObj->nFans == 3 &&
1401 (pTruthNew[0] == 0xCACACACA || pTruthNew[0] == 0xC5C5C5C5 ||
1402 pTruthNew[0] == 0x3A3A3A3A || pTruthNew[0] == 0x35353535) )
1403 {
1404 // translate into regular MUXes
1405 if ( pTruthNew[0] == 0xC5C5C5C5 )
1406 pObjNew->pFans[0] = Abc_LitNot(pObjNew->pFans[0]);
1407 else if ( pTruthNew[0] == 0x3A3A3A3A )
1408 pObjNew->pFans[1] = Abc_LitNot(pObjNew->pFans[1]);
1409 else if ( pTruthNew[0] == 0x35353535 )
1410 {
1411 pObjNew->pFans[0] = Abc_LitNot(pObjNew->pFans[0]);
1412 pObjNew->pFans[1] = Abc_LitNot(pObjNew->pFans[1]);
1413 }
1414 pTruthNew[0] = 0xCACACACA;
1415 // resolve the complemented control input
1416 if ( Abc_LitIsCompl(pObjNew->pFans[2]) )
1417 {
1418 unsigned char Temp = pObjNew->pFans[0];
1419 pObjNew->pFans[0] = pObjNew->pFans[1];
1420 pObjNew->pFans[1] = Temp;
1421 pObjNew->pFans[2] = Abc_LitNot(pObjNew->pFans[2]);
1422 }
1423 // resolve the complemented true input
1424 if ( Abc_LitIsCompl(pObjNew->pFans[1]) )
1425 {
1426 iLit = Abc_LitNot(iLit);
1427 pObjNew->pFans[0] = Abc_LitNot(pObjNew->pFans[0]);
1428 pObjNew->pFans[1] = Abc_LitNot(pObjNew->pFans[1]);
1429 }
1430 return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1431 }
1432 else
1433 {
1434 // if the incoming phase is complemented, absorb it into the prime node
1435 if ( Abc_LitIsCompl(iLit) )
1436 Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
1437 return Abc_Var2Lit( pObjNew->Id, 0 );
1438 }
1439}
1440
1452Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
1453{
1454 Kit_DsdNtk_t * pNew;
1455 Kit_DsdObj_t * pObjNew;
1456 assert( p->nVars <= 16 );
1457 // create a new network
1458 pNew = Kit_DsdNtkAlloc( p->nVars );
1459 // consider simple special cases
1460 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
1461 {
1462 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
1463 pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1464 return pNew;
1465 }
1466 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
1467 {
1468 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
1469 pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
1470 pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1471 return pNew;
1472 }
1473 // convert the root node
1474 pNew->Root = Kit_DsdExpandNode_rec( pNew, p, p->Root );
1475 return pNew;
1476}
1477
1489void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned short * piLits, int nVars, unsigned piLitsRes[] )
1490{
1491 int nSuppSizes[16], Priority[16], pOrder[16];
1492 int i, k, iVarBest, SuppMax, PrioMax;
1493 // compute support sizes and priorities of the components
1494 for ( i = 0; i < nVars; i++ )
1495 {
1496 assert( uSupps[i] );
1497 pOrder[i] = i;
1498 Priority[i] = KIT_INFINITY;
1499 for ( k = 0; k < 16; k++ )
1500 if ( uSupps[i] & (1 << k) )
1501 Priority[i] = KIT_MIN( Priority[i], pPrios[k] );
1502 assert( Priority[i] != 16 );
1503 nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
1504 }
1505 // sort the components by pririty
1506 Extra_BubbleSort( pOrder, Priority, nVars, 0 );
1507 // find the component by with largest size and lowest priority
1508 iVarBest = -1;
1509 SuppMax = 0;
1510 PrioMax = 0;
1511 for ( i = 0; i < nVars; i++ )
1512 {
1513 if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMax < Priority[i]) )
1514 {
1515 SuppMax = nSuppSizes[i];
1516 PrioMax = Priority[i];
1517 iVarBest = i;
1518 }
1519 }
1520 assert( iVarBest != -1 );
1521 // copy the resulting literals
1522 k = 0;
1523 piLitsRes[k++] = piLits[iVarBest];
1524 for ( i = 0; i < nVars; i++ )
1525 {
1526 if ( pOrder[i] == iVarBest )
1527 continue;
1528 piLitsRes[k++] = piLits[pOrder[i]];
1529 }
1530 assert( k == nVars );
1531}
1532
1544int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPrios[] )
1545{
1546 Kit_DsdObj_t * pObj;
1547 Kit_DsdObj_t * pObjNew = NULL; // Suppress "might be used uninitialized"
1548 unsigned * pTruth, * pTruthNew;
1549 unsigned i, piLitsNew[16], uSupps[16];
1550 int iLitFanin, iLitNew;
1551
1552 // consider the case of simple gate
1553 pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1554 if ( pObj == NULL )
1555 return iLit;
1556 if ( pObj->Type == KIT_DSD_AND )
1557 {
1558 // get the supports
1559 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1560 uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
1561 // put the largest component last
1562 // sort other components in the decreasing order of priority of their vars
1563 Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
1564 // construct the two-input node network
1565 iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
1566 for ( i = 1; i < pObj->nFans; i++ )
1567 {
1568 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
1569 pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
1570 pObjNew->pFans[1] = iLitNew;
1571 iLitNew = Abc_Var2Lit( pObjNew->Id, 0 );
1572 }
1573 return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1574 }
1575 if ( pObj->Type == KIT_DSD_XOR )
1576 {
1577 // get the supports
1578 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
1579 {
1580 assert( !Abc_LitIsCompl(iLitFanin) );
1581 uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
1582 }
1583 // put the largest component last
1584 // sort other components in the decreasing order of priority of their vars
1585 Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
1586 // construct the two-input node network
1587 iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
1588 for ( i = 1; i < pObj->nFans; i++ )
1589 {
1590 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
1591 pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
1592 pObjNew->pFans[1] = iLitNew;
1593 iLitNew = Abc_Var2Lit( pObjNew->Id, 0 );
1594 }
1595 return Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(iLit) );
1596 }
1597 assert( pObj->Type == KIT_DSD_PRIME );
1598
1599 // create new PRIME node
1600 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
1601 // copy the truth table
1602 pTruth = Kit_DsdObjTruth( pObj );
1603 pTruthNew = Kit_DsdObjTruth( pObjNew );
1604 Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
1605 // create fanins
1606 Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
1607 {
1608 pObjNew->pFans[i] = Kit_DsdShrink_rec( pNew, p, iLitFanin, pPrios );
1609 // complement the corresponding inputs of the truth table
1610 if ( Abc_LitIsCompl(pObjNew->pFans[i]) )
1611 {
1612 pObjNew->pFans[i] = Abc_LitRegular(pObjNew->pFans[i]);
1613 Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
1614 }
1615 }
1616 // if the incoming phase is complemented, absorb it into the prime node
1617 if ( Abc_LitIsCompl(iLit) )
1618 Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
1619 return Abc_Var2Lit( pObjNew->Id, 0 );
1620}
1621
1634Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] )
1635{
1636 Kit_DsdNtk_t * pNew;
1637 Kit_DsdObj_t * pObjNew;
1638 assert( p->nVars <= 16 );
1639 // create a new network
1640 pNew = Kit_DsdNtkAlloc( p->nVars );
1641 // consider simple special cases
1642 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
1643 {
1644 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
1645 pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1646 return pNew;
1647 }
1648 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
1649 {
1650 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
1651 pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
1652 pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
1653 return pNew;
1654 }
1655 // convert the root node
1656 pNew->Root = Kit_DsdShrink_rec( pNew, p, p->Root, pPrios );
1657 return pNew;
1658}
1659
1672void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
1673{
1674 Kit_DsdObj_t * pObj;
1675 unsigned * pIn, * pOut, * pTemp, k;
1676 int i, v, Temp, uSuppFanin, iFaninLit, WeightMax, FaninMax, nSwaps;
1677 int Weights[16];
1678 // go through the prime nodes
1679 Kit_DsdNtkForEachObj( p, pObj, i )
1680 {
1681 if ( pObj->Type != KIT_DSD_PRIME )
1682 continue;
1683 // count the fanin frequencies
1684 Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
1685 {
1686 uSuppFanin = Kit_DsdLitSupport( p, iFaninLit );
1687 Weights[k] = 0;
1688 for ( v = 0; v < 16; v++ )
1689 if ( uSuppFanin & (1 << v) )
1690 Weights[k] += pFreqs[v] - 1;
1691 }
1692 // find the most frequent fanin
1693 WeightMax = 0;
1694 FaninMax = -1;
1695 for ( k = 0; k < pObj->nFans; k++ )
1696 if ( WeightMax < Weights[k] )
1697 {
1698 WeightMax = Weights[k];
1699 FaninMax = k;
1700 }
1701 // no need to reorder if there are no frequent fanins
1702 if ( FaninMax == -1 )
1703 continue;
1704 // move the fanins number k to the first place
1705 nSwaps = 0;
1706 pIn = Kit_DsdObjTruth(pObj);
1707 pOut = p->pMem;
1708// for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ )
1709 for ( v = FaninMax-1; v >= 0; v-- )
1710 {
1711 // swap the fanins
1712 Temp = pObj->pFans[v];
1713 pObj->pFans[v] = pObj->pFans[v+1];
1714 pObj->pFans[v+1] = Temp;
1715 // swap the truth table variables
1716 Kit_TruthSwapAdjacentVars( pOut, pIn, pObj->nFans, v );
1717 pTemp = pIn; pIn = pOut; pOut = pTemp;
1718 nSwaps++;
1719 }
1720 if ( nSwaps & 1 )
1721 Kit_TruthCopy( pOut, pIn, pObj->nFans );
1722 }
1723}
1724
1736unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit )
1737{
1738 Kit_DsdObj_t * pObj;
1739 unsigned uSupport, k;
1740 int iFaninLit;
1741 pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
1742 if ( pObj == NULL )
1743 return Kit_DsdLitSupport( p, iLit );
1744 uSupport = 0;
1745 Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
1746 uSupport |= Kit_DsdGetSupports_rec( p, iFaninLit );
1747 p->pSupps[pObj->Id - p->nVars] = uSupport;
1748 assert( uSupport <= 0xFFFF );
1749 return uSupport;
1750}
1751
1763unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p )
1764{
1765 Kit_DsdObj_t * pRoot;
1766 unsigned uSupport;
1767 assert( p->pSupps == NULL );
1768 p->pSupps = ABC_ALLOC( unsigned, p->nNodes );
1769 // consider simple special cases
1770 pRoot = Kit_DsdNtkRoot(p);
1771 if ( pRoot->Type == KIT_DSD_CONST1 )
1772 {
1773 assert( p->nNodes == 1 );
1774 uSupport = p->pSupps[0] = 0;
1775 }
1776 if ( pRoot->Type == KIT_DSD_VAR )
1777 {
1778 assert( p->nNodes == 1 );
1779 uSupport = p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
1780 }
1781 else
1782 uSupport = Kit_DsdGetSupports_rec( p, p->Root );
1783 assert( uSupport <= 0xFFFF );
1784 return uSupport;
1785}
1786
1798int Kit_DsdFindLargeBox_rec( Kit_DsdNtk_t * pNtk, int Id, int Size )
1799{
1800 Kit_DsdObj_t * pObj;
1801 unsigned iLit, i, RetValue;
1802 pObj = Kit_DsdNtkObj( pNtk, Id );
1803 if ( pObj == NULL )
1804 return 0;
1805 if ( pObj->Type == KIT_DSD_PRIME && (int)pObj->nFans > Size )
1806 return 1;
1807 RetValue = 0;
1808 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1809 RetValue |= Kit_DsdFindLargeBox_rec( pNtk, Abc_Lit2Var(iLit), Size );
1810 return RetValue;
1811}
1812
1824int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
1825{
1826 return Kit_DsdFindLargeBox_rec( pNtk, Abc_Lit2Var(pNtk->Root), Size );
1827}
1828
1840int Kit_DsdCountAigNodes_rec( Kit_DsdNtk_t * pNtk, int Id )
1841{
1842 Kit_DsdObj_t * pObj;
1843 unsigned iLit, i, RetValue = 0;
1844 pObj = Kit_DsdNtkObj( pNtk, Id );
1845 if ( pObj == NULL )
1846 return 0;
1847 if ( pObj->Type == KIT_DSD_CONST1 || pObj->Type == KIT_DSD_VAR )
1848 return 0;
1849 if ( pObj->nFans < 2 ) // why this happens? - need to figure out
1850 return 0;
1851 assert( pObj->nFans > 1 );
1852 if ( pObj->Type == KIT_DSD_AND )
1853 RetValue = ((int)pObj->nFans - 1);
1854 else if ( pObj->Type == KIT_DSD_XOR )
1855 RetValue = ((int)pObj->nFans - 1) * 3;
1856 else if ( pObj->Type == KIT_DSD_PRIME )
1857 {
1858 // assuming MUX decomposition
1859 assert( (int)pObj->nFans == 3 );
1860 RetValue = 3;
1861 }
1862 else assert( 0 );
1863 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
1864 RetValue += Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(iLit) );
1865 return RetValue;
1866}
1867
1868
1880int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk )
1881{
1882 return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) );
1883}
1884
1896int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk )
1897{
1898 Kit_DsdObj_t * pObj;
1899 int i, Counter = 0;
1900 for ( i = 0; i < pNtk->nNodes; i++ )
1901 {
1902 pObj = pNtk->pNodes[i];
1903 if ( pObj->Type == KIT_DSD_AND )
1904 Counter += ((int)pObj->nFans - 1);
1905 else if ( pObj->Type == KIT_DSD_XOR )
1906 Counter += ((int)pObj->nFans - 1) * 3;
1907 else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition
1908 Counter += 3;
1909 }
1910 return Counter;
1911}
1912
1924int Kit_DsdRootNodeHasCommonVars( Kit_DsdObj_t * pObj0, Kit_DsdObj_t * pObj1 )
1925{
1926 unsigned i, k;
1927 for ( i = 0; i < pObj0->nFans; i++ )
1928 {
1929 if ( Abc_Lit2Var(pObj0->pFans[i]) >= 4 )
1930 continue;
1931 for ( k = 0; k < pObj1->nFans; k++ )
1932 if ( Abc_Lit2Var(pObj0->pFans[i]) == Abc_Lit2Var(pObj1->pFans[k]) )
1933 return 1;
1934 }
1935 return 0;
1936}
1937
1949int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
1950{
1951 assert( pNtk0->nVars == 4 );
1952 assert( pNtk1->nVars == 4 );
1953 if ( Kit_DsdFindLargeBox(pNtk0, 2) )
1954 return 0;
1955 if ( Kit_DsdFindLargeBox(pNtk1, 2) )
1956 return 0;
1957 return Kit_DsdRootNodeHasCommonVars( Kit_DsdNtkRoot(pNtk0), Kit_DsdNtkRoot(pNtk1) );
1958}
1959
1971void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned short * pPar, int nDecMux )
1972{
1973 Kit_DsdObj_t * pRes, * pRes0, * pRes1;
1974 int nWords = Kit_TruthWordNum(pObj->nFans);
1975 unsigned * pTruth = Kit_DsdObjTruth(pObj);
1976 unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
1977 unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
1978 int i, iLit0, iLit1, nFans0, nFans1, nPairs;
1979 int fEquals[2][2], fOppos, fPairs[4][4];
1980 unsigned j, k, nFansNew, uSupp0, uSupp1;
1981
1982 assert( pObj->nFans > 0 );
1983 assert( pObj->Type == KIT_DSD_PRIME );
1984 assert( uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
1985
1986 // compress the truth table
1987 if ( uSupp != Kit_BitMask(pObj->nFans) )
1988 {
1989 nFansNew = Kit_WordCountOnes(uSupp);
1990 Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, uSupp, 1 );
1991 for ( j = k = 0; j < pObj->nFans; j++ )
1992 if ( uSupp & (1 << j) )
1993 pObj->pFans[k++] = pObj->pFans[j];
1994 assert( k == nFansNew );
1995 pObj->nFans = k;
1996 uSupp = Kit_BitMask(pObj->nFans);
1997 }
1998
1999 // consider the single variable case
2000 if ( pObj->nFans == 1 )
2001 {
2002 pObj->Type = KIT_DSD_NONE;
2003 if ( pTruth[0] == 0x55555555 )
2004 pObj->pFans[0] = Abc_LitNot(pObj->pFans[0]);
2005 else
2006 assert( pTruth[0] == 0xAAAAAAAA );
2007 // update the parent pointer
2008 *pPar = Abc_LitNotCond( pObj->pFans[0], Abc_LitIsCompl(*pPar) );
2009 return;
2010 }
2011
2012 // decompose the output
2013 if ( !pObj->fMark )
2014 for ( i = pObj->nFans - 1; i >= 0; i-- )
2015 {
2016 // get the two-variable cofactors
2017 Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
2018 Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
2019// assert( !Kit_TruthVarInSupport( pCofs2[0], pObj->nFans, i) );
2020// assert( !Kit_TruthVarInSupport( pCofs2[1], pObj->nFans, i) );
2021 // get the constant cofs
2022 fEquals[0][0] = Kit_TruthIsConst0( pCofs2[0], pObj->nFans );
2023 fEquals[0][1] = Kit_TruthIsConst0( pCofs2[1], pObj->nFans );
2024 fEquals[1][0] = Kit_TruthIsConst1( pCofs2[0], pObj->nFans );
2025 fEquals[1][1] = Kit_TruthIsConst1( pCofs2[1], pObj->nFans );
2026 fOppos = Kit_TruthIsOpposite( pCofs2[0], pCofs2[1], pObj->nFans );
2027 assert( !Kit_TruthIsEqual(pCofs2[0], pCofs2[1], pObj->nFans) );
2028 if ( fEquals[0][0] + fEquals[0][1] + fEquals[1][0] + fEquals[1][1] + fOppos == 0 )
2029 {
2030 // check the MUX decomposition
2031 uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
2032 uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
2033 assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
2034 if ( uSupp0 & uSupp1 )
2035 continue;
2036 // perform MUX decomposition
2037 pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2038 pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2039 for ( k = 0; k < pObj->nFans; k++ )
2040 {
2041 pRes0->pFans[k] = (uSupp0 & (1 << k))? pObj->pFans[k] : 127;
2042 pRes1->pFans[k] = (uSupp1 & (1 << k))? pObj->pFans[k] : 127;
2043 }
2044 Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );
2045 Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans );
2046 // update the current one
2047 assert( pObj->Type == KIT_DSD_PRIME );
2048 pTruth[0] = 0xCACACACA;
2049 pObj->nFans = 3;
2050 pObj->pFans[2] = pObj->pFans[i];
2051 pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
2052 pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
2053 // call recursively
2054 Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
2055 Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
2056 return;
2057 }
2058
2059 // create the new node
2060 pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
2061 pRes->nRefs++;
2062 pRes->nFans = 2;
2063 pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i);
2064 pRes->pFans[1] = 2*pObj->Id;
2065 // update the parent pointer
2066 *pPar = Abc_LitNotCond( 2 * pRes->Id, Abc_LitIsCompl(*pPar) );
2067 // consider different decompositions
2068 if ( fEquals[0][0] )
2069 {
2070 Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
2071 }
2072 else if ( fEquals[0][1] )
2073 {
2074 pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2075 Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
2076 }
2077 else if ( fEquals[1][0] )
2078 {
2079 *pPar = Abc_LitNot(*pPar);
2080 pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2081 Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
2082 }
2083 else if ( fEquals[1][1] )
2084 {
2085 *pPar = Abc_LitNot(*pPar);
2086 pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2087 pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2088 Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
2089 }
2090 else if ( fOppos )
2091 {
2092 pRes->Type = KIT_DSD_XOR;
2093 Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
2094 }
2095 else
2096 assert( 0 );
2097 // decompose the remainder
2098 assert( Kit_DsdObjTruth(pObj) == pTruth );
2099 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1, nDecMux );
2100 return;
2101 }
2102 pObj->fMark = 1;
2103
2104 // decompose the input
2105 for ( i = pObj->nFans - 1; i >= 0; i-- )
2106 {
2107 assert( Kit_TruthVarInSupport( pTruth, pObj->nFans, i ) );
2108 // get the single variale cofactors
2109 Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
2110 Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
2111 // check the existence of MUX decomposition
2112 uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
2113 uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
2114 assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
2115 // if one of the cofs is a constant, it is time to check the output again
2116 if ( uSupp0 == 0 || uSupp1 == 0 )
2117 {
2118 pObj->fMark = 0;
2119 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
2120 return;
2121 }
2122 assert( uSupp0 && uSupp1 );
2123 // get the number of unique variables
2124 nFans0 = Kit_WordCountOnes( uSupp0 & ~uSupp1 );
2125 nFans1 = Kit_WordCountOnes( uSupp1 & ~uSupp0 );
2126 if ( nFans0 == 1 && nFans1 == 1 )
2127 {
2128 // get the cofactors w.r.t. the unique variables
2129 iLit0 = Kit_WordFindFirstBit( uSupp0 & ~uSupp1 );
2130 iLit1 = Kit_WordFindFirstBit( uSupp1 & ~uSupp0 );
2131 // get four cofactors
2132 Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iLit0 );
2133 Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iLit0 );
2134 Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iLit1 );
2135 Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iLit1 );
2136 // check existence conditions
2137 fEquals[0][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
2138 fEquals[0][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
2139 fEquals[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
2140 fEquals[1][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
2141 if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) )
2142 {
2143 // construct the MUX
2144 pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, 3 );
2145 Kit_DsdObjTruth(pRes)[0] = 0xCACACACA;
2146 pRes->nRefs++;
2147 pRes->nFans = 3;
2148 pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127; uSupp &= ~(1 << iLit0);
2149 pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127; uSupp &= ~(1 << iLit1);
2150 pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support
2151 // update the node
2152// if ( fEquals[0][0] && fEquals[0][1] )
2153// Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
2154// else
2155// Kit_TruthMuxVar( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
2156 Kit_TruthMuxVar( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
2157 if ( fEquals[1][0] && fEquals[1][1] )
2158 pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2159 // decompose the remainder
2160 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
2161 return;
2162 }
2163 }
2164
2165 // try other inputs
2166 for ( k = i+1; k < pObj->nFans; k++ )
2167 {
2168 // get four cofactors ik
2169 Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, k ); // 00
2170 Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, k ); // 01
2171 Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, k ); // 10
2172 Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, k ); // 11
2173 // compare equal pairs
2174 fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[0][1], pObj->nFans );
2175 fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
2176 fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
2177 fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
2178 fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
2179 fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual( pCofs4[1][0], pCofs4[1][1], pObj->nFans );
2180 nPairs = fPairs[0][1] + fPairs[0][2] + fPairs[0][3] + fPairs[1][2] + fPairs[1][3] + fPairs[2][3];
2181 if ( nPairs != 3 && nPairs != 2 )
2182 continue;
2183
2184 // decomposition exists
2185 pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
2186 pRes->nRefs++;
2187 pRes->nFans = 2;
2188 pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id; // remains in support
2189 pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i);
2190 if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
2191 {
2192 pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2193 pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2194 Kit_TruthMuxVar( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
2195 }
2196 else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
2197 {
2198 pRes->pFans[1] = Abc_LitNot(pRes->pFans[1]);
2199 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
2200 }
2201 else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
2202 {
2203 pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]);
2204 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
2205 }
2206 else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
2207 {
2208// unsigned uSupp0 = Kit_TruthSupport(pCofs4[0][0], pObj->nFans);
2209// unsigned uSupp1 = Kit_TruthSupport(pCofs4[1][1], pObj->nFans);
2210// unsigned uSupp;
2211// Extra_PrintBinary( stdout, &uSupp0, pObj->nFans ); printf( "\n" );
2212// Extra_PrintBinary( stdout, &uSupp1, pObj->nFans ); printf( "\n" );
2213 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
2214// uSupp = Kit_TruthSupport(pTruth, pObj->nFans);
2215// Extra_PrintBinary( stdout, &uSupp, pObj->nFans ); printf( "\n" ); printf( "\n" );
2216 }
2217 else
2218 {
2219 assert( fPairs[0][3] && fPairs[1][2] );
2220 pRes->Type = KIT_DSD_XOR;;
2221 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
2222 }
2223 // decompose the remainder
2224 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
2225 return;
2226 }
2227 }
2228
2229 // if all decomposition methods failed and we are still above the limit, perform MUX-decomposition
2230 if ( nDecMux > 0 && (int)pObj->nFans > nDecMux )
2231 {
2232 int iBestVar = Kit_TruthBestCofVar( pTruth, pObj->nFans, pCofs2[0], pCofs2[1] );
2233 uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
2234 uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
2235 // perform MUX decomposition
2236 pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2237 pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
2238 for ( k = 0; k < pObj->nFans; k++ )
2239 pRes0->pFans[k] = pRes1->pFans[k] = pObj->pFans[k];
2240 Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );
2241 Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans );
2242 // update the current one
2243 assert( pObj->Type == KIT_DSD_PRIME );
2244 pTruth[0] = 0xCACACACA;
2245 pObj->nFans = 3;
2246 pObj->pFans[2] = pObj->pFans[iBestVar];
2247 pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
2248 pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
2249 // call recursively
2250 Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
2251 Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
2252 }
2253
2254}
2255
2267Kit_DsdNtk_t * Kit_DsdDecomposeInt( unsigned * pTruth, int nVars, int nDecMux )
2268{
2269 Kit_DsdNtk_t * pNtk;
2270 Kit_DsdObj_t * pObj;
2271 unsigned uSupp;
2272 int i, nVarsReal;
2273 assert( nVars <= 16 );
2274 pNtk = Kit_DsdNtkAlloc( nVars );
2275 pNtk->Root = Abc_Var2Lit( pNtk->nVars, 0 );
2276 // create the first node
2277 pObj = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
2278 assert( pNtk->pNodes[0] == pObj );
2279 for ( i = 0; i < nVars; i++ )
2280 pObj->pFans[i] = Abc_Var2Lit( i, 0 );
2281 Kit_TruthCopy( Kit_DsdObjTruth(pObj), pTruth, nVars );
2282 uSupp = Kit_TruthSupport( pTruth, nVars );
2283 // consider special cases
2284 nVarsReal = Kit_WordCountOnes( uSupp );
2285 if ( nVarsReal == 0 )
2286 {
2287 pObj->Type = KIT_DSD_CONST1;
2288 pObj->nFans = 0;
2289 if ( pTruth[0] == 0 )
2290 pNtk->Root = Abc_LitNot(pNtk->Root);
2291 return pNtk;
2292 }
2293 if ( nVarsReal == 1 )
2294 {
2295 pObj->Type = KIT_DSD_VAR;
2296 pObj->nFans = 1;
2297 pObj->pFans[0] = Abc_Var2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
2298 return pNtk;
2299 }
2300 Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root, nDecMux );
2301 return pNtk;
2302}
2303
2315Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
2316{
2317 return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
2318}
2319
2331Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars )
2332{
2333 Kit_DsdNtk_t * pNtk, * pTemp;
2334 pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 );
2335 pNtk = Kit_DsdExpand( pTemp = pNtk );
2336 Kit_DsdNtkFree( pTemp );
2337 return pNtk;
2338}
2339
2351Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux )
2352{
2353/*
2354 Kit_DsdNtk_t * pNew;
2355 Kit_DsdObj_t * pObjNew;
2356 assert( nVars <= 16 );
2357 // create a new network
2358 pNew = Kit_DsdNtkAlloc( nVars );
2359 // consider simple special cases
2360 if ( nVars == 0 )
2361 {
2362 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
2363 pNew->Root = Abc_Var2Lit( pObjNew->Id, (int)(pTruth[0] == 0) );
2364 return pNew;
2365 }
2366 if ( nVars == 1 )
2367 {
2368 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
2369 pObjNew->pFans[0] = Abc_Var2Lit( 0, 0 );
2370 pNew->Root = Abc_Var2Lit( pObjNew->Id, (int)(pTruth[0] != 0xAAAAAAAA) );
2371 return pNew;
2372 }
2373*/
2374 return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
2375}
2376
2388int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
2389{
2390 Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
2391// Kit_DsdObj_t * pRoot;
2392 unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
2393 unsigned i, * pTruth;
2394 int fVerbose = 1;
2395 int RetValue = 0;
2396
2397 pTruth = pTruthInit;
2398// pRoot = Kit_DsdNtkRoot(pNtk);
2399// pTruth = Kit_DsdObjTruth(pRoot);
2400// assert( pRoot->nFans == pNtk->nVars );
2401
2402 if ( fVerbose )
2403 {
2404 printf( "Function: " );
2405// Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) );
2406 Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars );
2407 printf( "\n" );
2408 Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
2409 }
2410 for ( i = 0; i < pNtk->nVars; i++ )
2411 {
2412 Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i );
2413 pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars );
2414 pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
2415 Kit_DsdNtkFree( pTemp );
2416
2417 if ( fVerbose )
2418 {
2419 printf( "Cof%d0: ", i );
2420 Kit_DsdPrint( stdout, pNtk0 ), printf( "\n" );
2421 }
2422
2423 Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i );
2424 pNtk1 = Kit_DsdDecompose( pCofs2[1], pNtk->nVars );
2425 pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
2426 Kit_DsdNtkFree( pTemp );
2427
2428 if ( fVerbose )
2429 {
2430 printf( "Cof%d1: ", i );
2431 Kit_DsdPrint( stdout, pNtk1 ), printf( "\n" );
2432 }
2433
2434// if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
2435// RetValue = 1;
2436
2437 Kit_DsdNtkFree( pNtk0 );
2438 Kit_DsdNtkFree( pNtk1 );
2439 }
2440 if ( fVerbose )
2441 printf( "\n" );
2442
2443 return RetValue;
2444}
2445
2457int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
2458{
2459 Kit_DsdMan_t * p;
2460 Kit_DsdNtk_t * pNtk;
2461 unsigned * pTruthC;
2462 int Result;
2463
2464 // decompose the function
2465 pNtk = Kit_DsdDecompose( pTruth, nVars );
2466 Result = Kit_DsdCountLuts( pNtk, nLutSize );
2467// printf( "\n" );
2468// Kit_DsdPrint( stdout, pNtk );
2469// printf( "Eval = %d.\n", Result );
2470
2471 // recompute the truth table
2472 p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
2473 pTruthC = Kit_DsdTruthCompute( p, pNtk );
2474 if ( !Kit_TruthIsEqual( pTruth, pTruthC, nVars ) )
2475 printf( "Verification failed.\n" );
2476 Kit_DsdManFree( p );
2477
2478 Kit_DsdNtkFree( pNtk );
2479 return Result;
2480}
2481
2493void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
2494{
2495 Kit_DsdMan_t * p;
2496 unsigned * pTruthC;
2497 p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
2498 pTruthC = Kit_DsdTruthCompute( p, pNtk );
2499 if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
2500 printf( "Verification failed for gate with %d inputs.\n", nVars );
2501 Kit_DsdManFree( p );
2502}
2503
2515void Kit_DsdTest( unsigned * pTruth, int nVars )
2516{
2517 Kit_DsdMan_t * p;
2518 unsigned * pTruthC;
2519 Kit_DsdNtk_t * pNtk, * pTemp;
2520 pNtk = Kit_DsdDecompose( pTruth, nVars );
2521
2522// if ( Kit_DsdFindLargeBox(pNtk, Abc_Lit2Var(pNtk->Root)) )
2523// Kit_DsdPrint( stdout, pNtk );
2524
2525// if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
2526
2527// printf( "\n" );
2528// Kit_DsdPrint( stdout, pNtk );
2529
2530 pNtk = Kit_DsdExpand( pTemp = pNtk );
2531 Kit_DsdNtkFree( pTemp );
2532
2533 Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
2534
2535// if ( Kit_DsdFindLargeBox(pNtk, Abc_Lit2Var(pNtk->Root)) )
2536// Kit_DsdTestCofs( pNtk, pTruth );
2537
2538 // recompute the truth table
2539 p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
2540 pTruthC = Kit_DsdTruthCompute( p, pNtk );
2541// Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
2542// Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
2543 if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
2544 {
2545// printf( "Verification is okay.\n" );
2546 }
2547 else
2548 printf( "Verification failed.\n" );
2549 Kit_DsdManFree( p );
2550
2551
2552 Kit_DsdNtkFree( pNtk );
2553}
2554
2566void Kit_DsdPrecompute4Vars()
2567{
2568 Kit_DsdMan_t * p;
2569 Kit_DsdNtk_t * pNtk, * pTemp;
2570 FILE * pFile;
2571 unsigned uTruth;
2572 unsigned * pTruthC;
2573 char Buffer[256];
2574 int i, RetValue;
2575 int Counter1 = 0, Counter2 = 0;
2576
2577 pFile = fopen( "5npn/npn4.txt", "r" );
2578 for ( i = 0; fgets( Buffer, 100, pFile ); i++ )
2579 {
2580 Buffer[6] = 0;
2581 Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
2582 uTruth = ((uTruth & 0xffff) << 16) | (uTruth & 0xffff);
2583 pNtk = Kit_DsdDecompose( &uTruth, 4 );
2584
2585 pNtk = Kit_DsdExpand( pTemp = pNtk );
2586 Kit_DsdNtkFree( pTemp );
2587
2588
2589 if ( Kit_DsdFindLargeBox(pNtk, 3) )
2590 {
2591// RetValue = 0;
2592 RetValue = Kit_DsdTestCofs( pNtk, &uTruth );
2593 printf( "\n" );
2594 printf( "%3d : Non-DSD function %s %s\n", i, Buffer + 2, RetValue? "implementable" : "" );
2595 Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
2596
2597 Counter1++;
2598 Counter2 += RetValue;
2599 }
2600
2601/*
2602 printf( "%3d : Function %s ", i, Buffer + 2 );
2603 if ( !Kit_DsdFindLargeBox(pNtk, 3) )
2604 Kit_DsdPrint( stdout, pNtk );
2605 else
2606 printf( "\n" );
2607*/
2608
2609 p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
2610 pTruthC = Kit_DsdTruthCompute( p, pNtk );
2611 if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
2612 printf( "Verification failed.\n" );
2613 Kit_DsdManFree( p );
2614
2615 Kit_DsdNtkFree( pNtk );
2616 }
2617 fclose( pFile );
2618 printf( "non-DSD = %d implementable = %d\n", Counter1, Counter2 );
2619}
2620
2621
2633int Kit_DsdCofactoringGetVars( Kit_DsdNtk_t ** ppNtk, int nSize, int * pVars )
2634{
2635 Kit_DsdObj_t * pObj;
2636 unsigned m;
2637 int i, k, v, Var, nVars, iFaninLit;
2638 // go through all the networks
2639 nVars = 0;
2640 for ( i = 0; i < nSize; i++ )
2641 {
2642 // go through the prime objects of each networks
2643 Kit_DsdNtkForEachObj( ppNtk[i], pObj, k )
2644 {
2645 if ( pObj->Type != KIT_DSD_PRIME )
2646 continue;
2647 if ( pObj->nFans == 3 )
2648 continue;
2649 // collect direct fanin variables
2650 Kit_DsdObjForEachFanin( ppNtk[i], pObj, iFaninLit, m )
2651 {
2652 if ( !Kit_DsdLitIsLeaf(ppNtk[i], iFaninLit) )
2653 continue;
2654 // add it to the array
2655 Var = Abc_Lit2Var( iFaninLit );
2656 for ( v = 0; v < nVars; v++ )
2657 if ( pVars[v] == Var )
2658 break;
2659 if ( v == nVars )
2660 pVars[nVars++] = Var;
2661 }
2662 }
2663 }
2664 return nVars;
2665}
2666
2679int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose )
2680{
2681 Kit_DsdNtk_t * ppNtks[5][16] = {
2682 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2683 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2684 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2685 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
2686 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
2687 };
2688 Kit_DsdNtk_t * pTemp;
2689 unsigned * ppCofs[5][16];
2690 int pTryVars[16], nTryVars;
2691 int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur;
2692 int nSuppSizeMin, nSuppSizeMax, iVarBest;
2693 int i, k, v, nStep, nSize, nMemSize;
2694 assert( nLimit < 5 );
2695
2696 // allocate storage for cofactors
2697 nMemSize = Kit_TruthWordNum(nVars);
2698 ppCofs[0][0] = ABC_ALLOC( unsigned, 80 * nMemSize );
2699 nSize = 0;
2700 for ( i = 0; i < 5; i++ )
2701 for ( k = 0; k < 16; k++ )
2702 ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
2703 assert( nSize == 80 );
2704
2705 // copy the function
2706 Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
2707 ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars );
2708
2709 if ( fVerbose )
2710 printf( "\nProcessing prime function with %d support variables:\n", nVars );
2711
2712 // perform recursive cofactoring
2713 for ( nStep = 0; nStep < nLimit; nStep++ )
2714 {
2715 nSize = (1 << nStep);
2716 // find the variables to use in the cofactoring step
2717 nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars );
2718 if ( nTryVars == 0 )
2719 break;
2720 // cofactor w.r.t. the above variables
2721 iVarBest = -1;
2722 nPrimeSizeMin = 10000;
2723 nSuppSizeMin = 10000;
2724 for ( v = 0; v < nTryVars; v++ )
2725 {
2726 nPrimeSizeMax = 0;
2727 nSuppSizeMax = 0;
2728 for ( i = 0; i < nSize; i++ )
2729 {
2730 // cofactor and decompose cofactors
2731 Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] );
2732 Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] );
2733 ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
2734 ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
2735 // compute the largest non-decomp block
2736 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]);
2737 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2738 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]);
2739 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2740 // compute the sum total of supports
2741 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
2742 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
2743 // free the networks
2744 Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
2745 Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
2746 }
2747 // find the min max support size of the prime component
2748 if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) )
2749 {
2750 nPrimeSizeMin = nPrimeSizeMax;
2751 nSuppSizeMin = nSuppSizeMax;
2752 iVarBest = pTryVars[v];
2753 }
2754 }
2755 assert( iVarBest != -1 );
2756 // save the variable
2757 if ( pCofVars )
2758 pCofVars[nStep] = iVarBest;
2759 // cofactor w.r.t. the best
2760 for ( i = 0; i < nSize; i++ )
2761 {
2762 Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest );
2763 Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest );
2764 ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
2765 ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
2766 if ( fVerbose )
2767 {
2768 ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] );
2769 Kit_DsdNtkFree( pTemp );
2770 ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] );
2771 Kit_DsdNtkFree( pTemp );
2772
2773 printf( "Cof%d%d: ", nStep+1, 2*i+0 );
2774 Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] ), printf( "\n" );
2775 printf( "Cof%d%d: ", nStep+1, 2*i+1 );
2776 Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] ), printf( "\n" );
2777 }
2778 }
2779 }
2780
2781 // free the networks
2782 for ( i = 0; i < 5; i++ )
2783 for ( k = 0; k < 16; k++ )
2784 if ( ppNtks[i][k] )
2785 Kit_DsdNtkFree( ppNtks[i][k] );
2786 ABC_FREE( ppCofs[0][0] );
2787
2788 assert( nStep <= nLimit );
2789 return nStep;
2790}
2791
2804void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose )
2805{
2806 Kit_DsdNtk_t * ppNtks[32] = {0}, * pTemp;
2807 unsigned * ppCofs[5][16];
2808 int piCofVar[5];
2809 int nPrimeSizeMax, nPrimeSizeCur, nSuppSizeMax;
2810 int i, k, v1, v2, v3, v4, s, nSteps, nSize, nMemSize;
2811 assert( nCofLevel < 5 );
2812
2813 // print the function
2814 ppNtks[0] = Kit_DsdDecompose( pTruth, nVars );
2815 ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
2816 Kit_DsdNtkFree( pTemp );
2817 if ( fVerbose )
2818 Kit_DsdPrint( stdout, ppNtks[0] ), printf( "\n" );
2819 Kit_DsdNtkFree( ppNtks[0] );
2820
2821 // allocate storage for cofactors
2822 nMemSize = Kit_TruthWordNum(nVars);
2823 ppCofs[0][0] = ABC_ALLOC( unsigned, 80 * nMemSize );
2824 nSize = 0;
2825 for ( i = 0; i < 5; i++ )
2826 for ( k = 0; k < 16; k++ )
2827 ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
2828 assert( nSize == 80 );
2829
2830 // copy the function
2831 Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
2832
2833 if ( nCofLevel == 1 )
2834 for ( v1 = 0; v1 < nVars; v1++ )
2835 {
2836 nSteps = 0;
2837 piCofVar[nSteps++] = v1;
2838
2839 printf( " Variables { " );
2840 for ( i = 0; i < nSteps; i++ )
2841 printf( "%c ", 'a' + piCofVar[i] );
2842 printf( "}\n" );
2843
2844 // single cofactors
2845 for ( s = 1; s <= nSteps; s++ )
2846 {
2847 for ( k = 0; k < s; k++ )
2848 {
2849 nSize = (1 << k);
2850 for ( i = 0; i < nSize; i++ )
2851 {
2852 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
2853 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
2854 }
2855 }
2856 }
2857 // compute DSD networks
2858 nSize = (1 << nSteps);
2859 nPrimeSizeMax = 0;
2860 nSuppSizeMax = 0;
2861 for ( i = 0; i < nSize; i++ )
2862 {
2863 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
2864 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
2865 Kit_DsdNtkFree( pTemp );
2866 if ( fVerbose )
2867 {
2868 printf( "Cof%d%d: ", nSteps, i );
2869 Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
2870 }
2871 // compute the largest non-decomp block
2872 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
2873 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2874 Kit_DsdNtkFree( ppNtks[i] );
2875 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
2876 }
2877 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
2878 }
2879
2880 if ( nCofLevel == 2 )
2881 for ( v1 = 0; v1 < nVars; v1++ )
2882 for ( v2 = v1+1; v2 < nVars; v2++ )
2883 {
2884 nSteps = 0;
2885 piCofVar[nSteps++] = v1;
2886 piCofVar[nSteps++] = v2;
2887
2888 printf( " Variables { " );
2889 for ( i = 0; i < nSteps; i++ )
2890 printf( "%c ", 'a' + piCofVar[i] );
2891 printf( "}\n" );
2892
2893 // single cofactors
2894 for ( s = 1; s <= nSteps; s++ )
2895 {
2896 for ( k = 0; k < s; k++ )
2897 {
2898 nSize = (1 << k);
2899 for ( i = 0; i < nSize; i++ )
2900 {
2901 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
2902 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
2903 }
2904 }
2905 }
2906 // compute DSD networks
2907 nSize = (1 << nSteps);
2908 nPrimeSizeMax = 0;
2909 nSuppSizeMax = 0;
2910 for ( i = 0; i < nSize; i++ )
2911 {
2912 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
2913 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
2914 Kit_DsdNtkFree( pTemp );
2915 if ( fVerbose )
2916 {
2917 printf( "Cof%d%d: ", nSteps, i );
2918 Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
2919 }
2920 // compute the largest non-decomp block
2921 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
2922 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2923 Kit_DsdNtkFree( ppNtks[i] );
2924 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
2925 }
2926 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
2927 }
2928
2929 if ( nCofLevel == 3 )
2930 for ( v1 = 0; v1 < nVars; v1++ )
2931 for ( v2 = v1+1; v2 < nVars; v2++ )
2932 for ( v3 = v2+1; v3 < nVars; v3++ )
2933 {
2934 nSteps = 0;
2935 piCofVar[nSteps++] = v1;
2936 piCofVar[nSteps++] = v2;
2937 piCofVar[nSteps++] = v3;
2938
2939 printf( " Variables { " );
2940 for ( i = 0; i < nSteps; i++ )
2941 printf( "%c ", 'a' + piCofVar[i] );
2942 printf( "}\n" );
2943
2944 // single cofactors
2945 for ( s = 1; s <= nSteps; s++ )
2946 {
2947 for ( k = 0; k < s; k++ )
2948 {
2949 nSize = (1 << k);
2950 for ( i = 0; i < nSize; i++ )
2951 {
2952 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
2953 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
2954 }
2955 }
2956 }
2957 // compute DSD networks
2958 nSize = (1 << nSteps);
2959 nPrimeSizeMax = 0;
2960 nSuppSizeMax = 0;
2961 for ( i = 0; i < nSize; i++ )
2962 {
2963 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
2964 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
2965 Kit_DsdNtkFree( pTemp );
2966 if ( fVerbose )
2967 {
2968 printf( "Cof%d%d: ", nSteps, i );
2969 Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
2970 }
2971 // compute the largest non-decomp block
2972 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
2973 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
2974 Kit_DsdNtkFree( ppNtks[i] );
2975 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
2976 }
2977 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
2978 }
2979
2980 if ( nCofLevel == 4 )
2981 for ( v1 = 0; v1 < nVars; v1++ )
2982 for ( v2 = v1+1; v2 < nVars; v2++ )
2983 for ( v3 = v2+1; v3 < nVars; v3++ )
2984 for ( v4 = v3+1; v4 < nVars; v4++ )
2985 {
2986 nSteps = 0;
2987 piCofVar[nSteps++] = v1;
2988 piCofVar[nSteps++] = v2;
2989 piCofVar[nSteps++] = v3;
2990 piCofVar[nSteps++] = v4;
2991
2992 printf( " Variables { " );
2993 for ( i = 0; i < nSteps; i++ )
2994 printf( "%c ", 'a' + piCofVar[i] );
2995 printf( "}\n" );
2996
2997 // single cofactors
2998 for ( s = 1; s <= nSteps; s++ )
2999 {
3000 for ( k = 0; k < s; k++ )
3001 {
3002 nSize = (1 << k);
3003 for ( i = 0; i < nSize; i++ )
3004 {
3005 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
3006 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
3007 }
3008 }
3009 }
3010 // compute DSD networks
3011 nSize = (1 << nSteps);
3012 nPrimeSizeMax = 0;
3013 nSuppSizeMax = 0;
3014 for ( i = 0; i < nSize; i++ )
3015 {
3016 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
3017 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
3018 Kit_DsdNtkFree( pTemp );
3019 if ( fVerbose )
3020 {
3021 printf( "Cof%d%d: ", nSteps, i );
3022 Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
3023 }
3024 // compute the largest non-decomp block
3025 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
3026 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
3027 Kit_DsdNtkFree( ppNtks[i] );
3028 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
3029 }
3030 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
3031 }
3032
3033
3034 ABC_FREE( ppCofs[0][0] );
3035}
3036
3037
3049char ** Kit_DsdNpn4ClassNames()
3050{
3051 static const char * pNames[222] = {
3052 "F = 0", /* 0 */
3053 "F = (!d*(!c*(!b*!a)))", /* 1 */
3054 "F = (!d*(!c*!b))", /* 2 */
3055 "F = (!d*(!c*(b+a)))", /* 3 */
3056 "F = (!d*(!c*!(b*a)))", /* 4 */
3057 "F = (!d*!c)", /* 5 */
3058 "F = (!d*16(a,b,c))", /* 6 */
3059 "F = (!d*17(a,b,c))", /* 7 */
3060 "F = (!d*18(a,b,c))", /* 8 */
3061 "F = (!d*19(a,b,c))", /* 9 */
3062 "F = (!d*CA(!b,!c,a))", /* 10 */
3063 "F = (!d*(c+!(!b*!a)))", /* 11 */
3064 "F = (!d*!(c*!(!b*!a)))", /* 12 */
3065 "F = (!d*(c+b))", /* 13 */
3066 "F = (!d*3D(a,b,c))", /* 14 */
3067 "F = (!d*!(c*b))", /* 15 */
3068 "F = (!d*(c+(b+!a)))", /* 16 */
3069 "F = (!d*6B(a,b,c))", /* 17 */
3070 "F = (!d*!(c*!(b+a)))", /* 18 */
3071 "F = (!d*7E(a,b,c))", /* 19 */
3072 "F = (!d*!(c*(b*a)))", /* 20 */
3073 "F = (!d)", /* 21 */
3074 "F = 0116(a,b,c,d)", /* 22 */
3075 "F = 0117(a,b,c,d)", /* 23 */
3076 "F = 0118(a,b,c,d)", /* 24 */
3077 "F = 0119(a,b,c,d)", /* 25 */
3078 "F = 011A(a,b,c,d)", /* 26 */
3079 "F = 011B(a,b,c,d)", /* 27 */
3080 "F = 29((!b*!a),c,d)", /* 28 */
3081 "F = 2B((!b*!a),c,d)", /* 29 */
3082 "F = 012C(a,b,c,d)", /* 30 */
3083 "F = 012D(a,b,c,d)", /* 31 */
3084 "F = 012F(a,b,c,d)", /* 32 */
3085 "F = 013C(a,b,c,d)", /* 33 */
3086 "F = 013D(a,b,c,d)", /* 34 */
3087 "F = 013E(a,b,c,d)", /* 35 */
3088 "F = 013F(a,b,c,d)", /* 36 */
3089 "F = 0168(a,b,c,d)", /* 37 */
3090 "F = 0169(a,b,c,d)", /* 38 */
3091 "F = 016A(a,b,c,d)", /* 39 */
3092 "F = 016B(a,b,c,d)", /* 40 */
3093 "F = 016E(a,b,c,d)", /* 41 */
3094 "F = 016F(a,b,c,d)", /* 42 */
3095 "F = 017E(a,b,c,d)", /* 43 */
3096 "F = 017F(a,b,c,d)", /* 44 */
3097 "F = 0180(a,b,c,d)", /* 45 */
3098 "F = 0181(a,b,c,d)", /* 46 */
3099 "F = 0182(a,b,c,d)", /* 47 */
3100 "F = 0183(a,b,c,d)", /* 48 */
3101 "F = 0186(a,b,c,d)", /* 49 */
3102 "F = 0187(a,b,c,d)", /* 50 */
3103 "F = 0189(a,b,c,d)", /* 51 */
3104 "F = 018B(a,b,c,d)", /* 52 */
3105 "F = 018F(a,b,c,d)", /* 53 */
3106 "F = 0196(a,b,c,d)", /* 54 */
3107 "F = 0197(a,b,c,d)", /* 55 */
3108 "F = 0198(a,b,c,d)", /* 56 */
3109 "F = 0199(a,b,c,d)", /* 57 */
3110 "F = 019A(a,b,c,d)", /* 58 */
3111 "F = 019B(a,b,c,d)", /* 59 */
3112 "F = 019E(a,b,c,d)", /* 60 */
3113 "F = 019F(a,b,c,d)", /* 61 */
3114 "F = 42(a,(!c*!b),d)", /* 62 */
3115 "F = 46(a,(!c*!b),d)", /* 63 */
3116 "F = 4A(a,(!c*!b),d)", /* 64 */
3117 "F = CA((!c*!b),!d,a)", /* 65 */
3118 "F = 01AC(a,b,c,d)", /* 66 */
3119 "F = 01AD(a,b,c,d)", /* 67 */
3120 "F = 01AE(a,b,c,d)", /* 68 */
3121 "F = 01AF(a,b,c,d)", /* 69 */
3122 "F = 01BC(a,b,c,d)", /* 70 */
3123 "F = 01BD(a,b,c,d)", /* 71 */
3124 "F = 01BE(a,b,c,d)", /* 72 */
3125 "F = 01BF(a,b,c,d)", /* 73 */
3126 "F = 01E8(a,b,c,d)", /* 74 */
3127 "F = 01E9(a,b,c,d)", /* 75 */
3128 "F = 01EA(a,b,c,d)", /* 76 */
3129 "F = 01EB(a,b,c,d)", /* 77 */
3130 "F = 25((!b*!a),c,d)", /* 78 */
3131 "F = !CA(d,c,(!b*!a))", /* 79 */
3132 "F = (d+!(!c*(!b*!a)))", /* 80 */
3133 "F = 16(b,c,d)", /* 81 */
3134 "F = 033D(a,b,c,d)", /* 82 */
3135 "F = 17(b,c,d)", /* 83 */
3136 "F = ((!d*!a)+(!c*!b))", /* 84 */
3137 "F = !(!(!c*!b)*!(!d*!a))", /* 85 */
3138 "F = 0358(a,b,c,d)", /* 86 */
3139 "F = 0359(a,b,c,d)", /* 87 */
3140 "F = 035A(a,b,c,d)", /* 88 */
3141 "F = 035B(a,b,c,d)", /* 89 */
3142 "F = 035E(a,b,c,d)", /* 90 */
3143 "F = 035F(a,b,c,d)", /* 91 */
3144 "F = 0368(a,b,c,d)", /* 92 */
3145 "F = 0369(a,b,c,d)", /* 93 */
3146 "F = 036A(a,b,c,d)", /* 94 */
3147 "F = 036B(a,b,c,d)", /* 95 */
3148 "F = 036C(a,b,c,d)", /* 96 */
3149 "F = 036D(a,b,c,d)", /* 97 */
3150 "F = 036E(a,b,c,d)", /* 98 */
3151 "F = 036F(a,b,c,d)", /* 99 */
3152 "F = 037C(a,b,c,d)", /* 100 */
3153 "F = 037D(a,b,c,d)", /* 101 */
3154 "F = 037E(a,b,c,d)", /* 102 */
3155 "F = 18(b,c,d)", /* 103 */
3156 "F = 03C1(a,b,c,d)", /* 104 */
3157 "F = 19(b,c,d)", /* 105 */
3158 "F = 03C5(a,b,c,d)", /* 106 */
3159 "F = 03C6(a,b,c,d)", /* 107 */
3160 "F = 03C7(a,b,c,d)", /* 108 */
3161 "F = CA(!c,!d,b)", /* 109 */
3162 "F = 03D4(a,b,c,d)", /* 110 */
3163 "F = 03D5(a,b,c,d)", /* 111 */
3164 "F = 03D6(a,b,c,d)", /* 112 */
3165 "F = 03D7(a,b,c,d)", /* 113 */
3166 "F = 03D8(a,b,c,d)", /* 114 */
3167 "F = 03D9(a,b,c,d)", /* 115 */
3168 "F = 03DB(a,b,c,d)", /* 116 */
3169 "F = 03DC(a,b,c,d)", /* 117 */
3170 "F = 03DD(a,b,c,d)", /* 118 */
3171 "F = 03DE(a,b,c,d)", /* 119 */
3172 "F = (d+!(!c*!b))", /* 120 */
3173 "F = ((d+c)*(b+a))", /* 121 */
3174 "F = 0661(a,b,c,d)", /* 122 */
3175 "F = 0662(a,b,c,d)", /* 123 */
3176 "F = 0663(a,b,c,d)", /* 124 */
3177 "F = (!(d*c)*(b+a))", /* 125 */
3178 "F = 0667(a,b,c,d)", /* 126 */
3179 "F = 29((b+a),c,d)", /* 127 */
3180 "F = 066B(a,b,c,d)", /* 128 */
3181 "F = 2B((b+a),c,d)", /* 129 */
3182 "F = 0672(a,b,c,d)", /* 130 */
3183 "F = 0673(a,b,c,d)", /* 131 */
3184 "F = 0676(a,b,c,d)", /* 132 */
3185 "F = 0678(a,b,c,d)", /* 133 */
3186 "F = 0679(a,b,c,d)", /* 134 */
3187 "F = 067A(a,b,c,d)", /* 135 */
3188 "F = 067B(a,b,c,d)", /* 136 */
3189 "F = 067E(a,b,c,d)", /* 137 */
3190 "F = 24((b+a),c,d)", /* 138 */
3191 "F = 0691(a,b,c,d)", /* 139 */
3192 "F = 0693(a,b,c,d)", /* 140 */
3193 "F = 26((b+a),c,d)", /* 141 */
3194 "F = 0697(a,b,c,d)", /* 142 */
3195 "F = !CA(d,c,(b+a))", /* 143 */
3196 "F = 06B0(a,b,c,d)", /* 144 */
3197 "F = 06B1(a,b,c,d)", /* 145 */
3198 "F = 06B2(a,b,c,d)", /* 146 */
3199 "F = 06B3(a,b,c,d)", /* 147 */
3200 "F = 06B4(a,b,c,d)", /* 148 */
3201 "F = 06B5(a,b,c,d)", /* 149 */
3202 "F = 06B6(a,b,c,d)", /* 150 */
3203 "F = 06B7(a,b,c,d)", /* 151 */
3204 "F = 06B9(a,b,c,d)", /* 152 */
3205 "F = 06BD(a,b,c,d)", /* 153 */
3206 "F = 2C((b+a),c,d)", /* 154 */
3207 "F = 06F1(a,b,c,d)", /* 155 */
3208 "F = 06F2(a,b,c,d)", /* 156 */
3209 "F = CA((b+a),!d,c)", /* 157 */
3210 "F = (d+!(!c*!(b+!a)))", /* 158 */
3211 "F = 0776(a,b,c,d)", /* 159 */
3212 "F = 16((b*a),c,d)", /* 160 */
3213 "F = 0779(a,b,c,d)", /* 161 */
3214 "F = 077A(a,b,c,d)", /* 162 */
3215 "F = 077E(a,b,c,d)", /* 163 */
3216 "F = 07B0(a,b,c,d)", /* 164 */
3217 "F = 07B1(a,b,c,d)", /* 165 */
3218 "F = 07B4(a,b,c,d)", /* 166 */
3219 "F = 07B5(a,b,c,d)", /* 167 */
3220 "F = 07B6(a,b,c,d)", /* 168 */
3221 "F = 07BC(a,b,c,d)", /* 169 */
3222 "F = 07E0(a,b,c,d)", /* 170 */
3223 "F = 07E1(a,b,c,d)", /* 171 */
3224 "F = 07E2(a,b,c,d)", /* 172 */
3225 "F = 07E3(a,b,c,d)", /* 173 */
3226 "F = 07E6(a,b,c,d)", /* 174 */
3227 "F = 07E9(a,b,c,d)", /* 175 */
3228 "F = 1C((b*a),c,d)", /* 176 */
3229 "F = 07F1(a,b,c,d)", /* 177 */
3230 "F = 07F2(a,b,c,d)", /* 178 */
3231 "F = (d+!(!c*!(b*a)))", /* 179 */
3232 "F = (d+c)", /* 180 */
3233 "F = 1668(a,b,c,d)", /* 181 */
3234 "F = 1669(a,b,c,d)", /* 182 */
3235 "F = 166A(a,b,c,d)", /* 183 */
3236 "F = 166B(a,b,c,d)", /* 184 */
3237 "F = 166E(a,b,c,d)", /* 185 */
3238 "F = 167E(a,b,c,d)", /* 186 */
3239 "F = 1681(a,b,c,d)", /* 187 */
3240 "F = 1683(a,b,c,d)", /* 188 */
3241 "F = 1686(a,b,c,d)", /* 189 */
3242 "F = 1687(a,b,c,d)", /* 190 */
3243 "F = 1689(a,b,c,d)", /* 191 */
3244 "F = 168B(a,b,c,d)", /* 192 */
3245 "F = 168E(a,b,c,d)", /* 193 */
3246 "F = 1696(a,b,c,d)", /* 194 */
3247 "F = 1697(a,b,c,d)", /* 195 */
3248 "F = 1698(a,b,c,d)", /* 196 */
3249 "F = 1699(a,b,c,d)", /* 197 */
3250 "F = 169A(a,b,c,d)", /* 198 */
3251 "F = 169B(a,b,c,d)", /* 199 */
3252 "F = 169E(a,b,c,d)", /* 200 */
3253 "F = 16A9(a,b,c,d)", /* 201 */
3254 "F = 16AC(a,b,c,d)", /* 202 */
3255 "F = 16AD(a,b,c,d)", /* 203 */
3256 "F = 16BC(a,b,c,d)", /* 204 */
3257 "F = (d+E9(a,b,c))", /* 205 */
3258 "F = 177E(a,b,c,d)", /* 206 */
3259 "F = 178E(a,b,c,d)", /* 207 */
3260 "F = 1796(a,b,c,d)", /* 208 */
3261 "F = 1798(a,b,c,d)", /* 209 */
3262 "F = 179A(a,b,c,d)", /* 210 */
3263 "F = 17AC(a,b,c,d)", /* 211 */
3264 "F = (d+E8(a,b,c))", /* 212 */
3265 "F = (d+E7(a,b,c))", /* 213 */
3266 "F = 19E1(a,b,c,d)", /* 214 */
3267 "F = 19E3(a,b,c,d)", /* 215 */
3268 "F = (d+E6(a,b,c))", /* 216 */
3269 "F = 1BD8(a,b,c,d)", /* 217 */
3270 "F = (d+CA(b,c,a))", /* 218 */
3271 "F = (d+(c+(!b*!a)))", /* 219 */
3272 "F = (d+(c+!b))", /* 220 */
3273 "F = (d+(c+(b+a)))" /* 221 */
3274 };
3275 return (char **)pNames;
3276}
3277
3278
3282
3283
3284ABC_NAMESPACE_IMPL_END
3285
nWords
int nWords
Definition abcNpn.c:127
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
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
Cloud_Quit
void Cloud_Quit(CloudManager *dd)
Definition cloud.c:144
Cloud_Init
CloudManager * Cloud_Init(int nVars, int nBits)
FUNCTION DEFINITIONS ///.
Definition cloud.c:70
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
Extra_BubbleSort
void Extra_BubbleSort(int Order[], int Costs[], int nSize, int fIncreasing)
Definition extraUtilMisc.c:2045
Extra_ReadHexadecimal
int Extra_ReadHexadecimal(unsigned Sign[], char *pString, int nVars)
Definition extraUtilFile.c:559
Extra_PrintHexadecimal
void Extra_PrintHexadecimal(FILE *pFile, unsigned Sign[], int nVars)
Definition extraUtilFile.c:584
Kit_DsdManAlloc
ABC_NAMESPACE_IMPL_START Kit_DsdMan_t * Kit_DsdManAlloc(int nVars, int nNodes)
DECLARATIONS ///.
Definition kitDsd.c:46
Kit_DsdNonDsdSizeMax
int Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1212
Kit_DsdDecompose
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition kitDsd.c:2315
Kit_DsdShrink_rec
int Kit_DsdShrink_rec(Kit_DsdNtk_t *pNew, Kit_DsdNtk_t *p, int iLit, int pPrios[])
Definition kitDsd.c:1544
Kit_DsdGetSupports_rec
unsigned Kit_DsdGetSupports_rec(Kit_DsdNtk_t *p, int iLit)
Definition kitDsd.c:1736
Kit_DsdWrite
void Kit_DsdWrite(char *pBuff, Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:453
Kit_DsdDecomposeInt
Kit_DsdNtk_t * Kit_DsdDecomposeInt(unsigned *pTruth, int nVars, int nDecMux)
Definition kitDsd.c:2267
Kit_DsdExpandCollectXor_rec
void Kit_DsdExpandCollectXor_rec(Kit_DsdNtk_t *p, unsigned iLit, unsigned *piLitsNew, int *nLitsNew)
Definition kitDsd.c:1319
Kit_DsdVerify
void Kit_DsdVerify(Kit_DsdNtk_t *pNtk, unsigned *pTruth, int nVars)
Definition kitDsd.c:2493
Kit_DsdPrint
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:375
Kit_DsdRootNodeHasCommonVars
int Kit_DsdRootNodeHasCommonVars(Kit_DsdObj_t *pObj0, Kit_DsdObj_t *pObj1)
Definition kitDsd.c:1924
Kit_DsdObjAlloc
Kit_DsdObj_t * Kit_DsdObjAlloc(Kit_DsdNtk_t *pNtk, Kit_Dsd_t Type, int nFans)
Definition kitDsd.c:93
Kit_DsdNpn4ClassNames
char ** Kit_DsdNpn4ClassNames()
Definition kitDsd.c:3049
Kit_DsdManFree
void Kit_DsdManFree(Kit_DsdMan_t *p)
Definition kitDsd.c:72
Kit_DsdTruth
void Kit_DsdTruth(Kit_DsdNtk_t *pNtk, unsigned *pTruthRes)
Definition kitDsd.c:1069
Kit_DsdFindLargeBox_rec
int Kit_DsdFindLargeBox_rec(Kit_DsdNtk_t *pNtk, int Id, int Size)
Definition kitDsd.c:1798
Kit_DsdDecomposeExpand
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition kitDsd.c:2331
Kit_DsdWrite_rec
char * Kit_DsdWrite_rec(char *pBuff, Kit_DsdNtk_t *pNtk, int Id)
Definition kitDsd.c:395
Kit_DsdNtkAlloc
Kit_DsdNtk_t * Kit_DsdNtkAlloc(int nVars)
Definition kitDsd.c:141
Kit_DsdCofactoring
int Kit_DsdCofactoring(unsigned *pTruth, int nVars, int *pCofVars, int nLimit, int fVerbose)
Definition kitDsd.c:2679
Kit_DsdWriteFromTruth
void Kit_DsdWriteFromTruth(char *pBuffer, unsigned *pTruth, int nVars)
Definition kitDsd.c:537
Kit_DsdCountAigNodes_rec
int Kit_DsdCountAigNodes_rec(Kit_DsdNtk_t *pNtk, int Id)
Definition kitDsd.c:1840
Kit_DsdExpandNode_rec
int Kit_DsdExpandNode_rec(Kit_DsdNtk_t *pNew, Kit_DsdNtk_t *p, int iLit)
Definition kitDsd.c:1350
Kit_DsdCountLuts_rec
int Kit_DsdCountLuts_rec(Kit_DsdNtk_t *pNtk, int nLutSize, int Id, int *pCounter)
Definition kitDsd.c:1144
Kit_DsdTruthComputeNodeTwo_rec
unsigned * Kit_DsdTruthComputeNodeTwo_rec(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id, unsigned uSupp, int iVar, unsigned *pTruthDec)
Definition kitDsd.c:854
Kit_DsdTruthComputeNodeOne_rec
unsigned * Kit_DsdTruthComputeNodeOne_rec(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id, unsigned uSupp)
Definition kitDsd.c:691
Kit_DsdNtkFree
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:164
Kit_DsdShrink
Kit_DsdNtk_t * Kit_DsdShrink(Kit_DsdNtk_t *p, int pPrios[])
Definition kitDsd.c:1634
Kit_DsdDecompose_rec
void Kit_DsdDecompose_rec(Kit_DsdNtk_t *pNtk, Kit_DsdObj_t *pObj, unsigned uSupp, unsigned short *pPar, int nDecMux)
Definition kitDsd.c:1971
Kit_DsdPrint2_rec
void Kit_DsdPrint2_rec(FILE *pFile, Kit_DsdNtk_t *pNtk, int Id)
Definition kitDsd.c:238
Kit_DsdCheckVar4Dec2
int Kit_DsdCheckVar4Dec2(Kit_DsdNtk_t *pNtk0, Kit_DsdNtk_t *pNtk1)
Definition kitDsd.c:1949
Kit_DsdEval
int Kit_DsdEval(unsigned *pTruth, int nVars, int nLutSize)
Definition kitDsd.c:2457
Kit_DsdTruthCompute
unsigned * Kit_DsdTruthCompute(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:664
Kit_DsdTruthPartialTwo
void Kit_DsdTruthPartialTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
Definition kitDsd.c:1090
Kit_DsdCompSort
void Kit_DsdCompSort(int pPrios[], unsigned uSupps[], unsigned short *piLits, int nVars, unsigned piLitsRes[])
Definition kitDsd.c:1489
Kit_DsdTestCofs
int Kit_DsdTestCofs(Kit_DsdNtk_t *pNtk, unsigned *pTruthInit)
Definition kitDsd.c:2388
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
Kit_DsdWriteHex
char * Kit_DsdWriteHex(char *pBuff, unsigned *pTruth, int nFans)
Definition kitDsd.c:212
Kit_DsdPrint2
void Kit_DsdPrint2(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:298
Kit_DsdGetSupports
unsigned Kit_DsdGetSupports(Kit_DsdNtk_t *p)
Definition kitDsd.c:1763
Kit_DsdNonDsdSupports
unsigned Kit_DsdNonDsdSupports(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1265
Kit_DsdCountLuts
int Kit_DsdCountLuts(Kit_DsdNtk_t *pNtk, int nLutSize)
Definition kitDsd.c:1188
Kit_DsdCofactoringGetVars
int Kit_DsdCofactoringGetVars(Kit_DsdNtk_t **ppNtk, int nSize, int *pVars)
Definition kitDsd.c:2633
Kit_DsdPrintFromTruth2
void Kit_DsdPrintFromTruth2(FILE *pFile, unsigned *pTruth, int nVars)
Definition kitDsd.c:515
Kit_DsdTest
void Kit_DsdTest(unsigned *pTruth, int nVars)
Definition kitDsd.c:2515
Kit_DsdCountAigNodes
int Kit_DsdCountAigNodes(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1896
Kit_DsdPrint_rec
void Kit_DsdPrint_rec(FILE *pFile, Kit_DsdNtk_t *pNtk, int Id)
Definition kitDsd.c:318
Kit_DsdDecomposeMux
Kit_DsdNtk_t * Kit_DsdDecomposeMux(unsigned *pTruth, int nVars, int nDecMux)
Definition kitDsd.c:2351
Kit_DsdExpand
Kit_DsdNtk_t * Kit_DsdExpand(Kit_DsdNtk_t *p)
Definition kitDsd.c:1452
Kit_DsdCountAigNodes2
int Kit_DsdCountAigNodes2(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1880
Kit_DsdPrintHex
void Kit_DsdPrintHex(FILE *pFile, unsigned *pTruth, int nFans)
Definition kitDsd.c:187
Kit_DsdObjFree
void Kit_DsdObjFree(Kit_DsdNtk_t *p, Kit_DsdObj_t *pObj)
Definition kitDsd.c:125
Kit_DsdTruthPartial
void Kit_DsdTruthPartial(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned *pTruthRes, unsigned uSupp)
Definition kitDsd.c:1108
Kit_DsdPrintExpanded
void Kit_DsdPrintExpanded(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:472
Kit_DsdPrintCofactors
void Kit_DsdPrintCofactors(unsigned *pTruth, int nVars, int nCofLevel, int fVerbose)
Definition kitDsd.c:2804
Kit_DsdPrecompute4Vars
void Kit_DsdPrecompute4Vars()
Definition kitDsd.c:2566
Kit_DsdTruthComputeOne
unsigned * Kit_DsdTruthComputeOne(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp)
Definition kitDsd.c:824
Kit_DsdTruthComputeNode_rec
unsigned * Kit_DsdTruthComputeNode_rec(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id)
Definition kitDsd.c:561
Kit_DsdRotate
void Kit_DsdRotate(Kit_DsdNtk_t *p, int pFreqs[])
Definition kitDsd.c:1672
Kit_DsdNonDsdPrimeMax
Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1237
Kit_DsdFindLargeBox
int Kit_DsdFindLargeBox(Kit_DsdNtk_t *pNtk, int Size)
Definition kitDsd.c:1824
Kit_DsdTruthComputeTwo
unsigned * Kit_DsdTruthComputeTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthDec)
Definition kitDsd.c:1025
Kit_DsdExpandCollectAnd_rec
void Kit_DsdExpandCollectAnd_rec(Kit_DsdNtk_t *p, unsigned iLit, unsigned *piLitsNew, int *nLitsNew)
Definition kitDsd.c:1292
Kit_TruthSwapAdjacentVars
void Kit_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int Start)
DECLARATIONS ///.
Definition kitTruth.c:46
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_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:573
Kit_TruthBestCofVar
int Kit_TruthBestCofVar(unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
Definition kitTruth.c:1365
Kit_TruthChangePhase
void Kit_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:1259
Kit_Dsd_t
Kit_Dsd_t
Definition kit.h:101
KIT_DSD_XOR
@ KIT_DSD_XOR
Definition kit.h:106
KIT_DSD_CONST1
@ KIT_DSD_CONST1
Definition kit.h:103
KIT_DSD_PRIME
@ KIT_DSD_PRIME
Definition kit.h:107
KIT_DSD_AND
@ KIT_DSD_AND
Definition kit.h:105
KIT_DSD_NONE
@ KIT_DSD_NONE
Definition kit.h:102
KIT_DSD_VAR
@ KIT_DSD_VAR
Definition kit.h:104
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:521
Kit_DsdObj_t
struct Kit_DsdObj_t_ Kit_DsdObj_t
Definition kit.h:111
Kit_TruthSupportSize
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition kitTruth.c:327
Kit_TruthCompose
unsigned * Kit_TruthCompose(CloudManager *dd, unsigned *pTruth, int nVars, unsigned **pInputs, int nVarsAll, Vec_Ptr_t *vStore, Vec_Int_t *vNodes)
Definition kitCloud.c:263
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:270
Kit_DsdObjForEachFanin
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition kit.h:160
Kit_TruthShrink
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:200
KIT_MIN
#define KIT_MIN(a, b)
MACRO DEFINITIONS ///.
Definition kit.h:174
KIT_MAX
#define KIT_MAX(a, b)
Definition kit.h:175
KIT_INFINITY
#define KIT_INFINITY
Definition kit.h:176
Kit_DsdNtk_t
struct Kit_DsdNtk_t_ Kit_DsdNtk_t
Definition kit.h:124
Kit_DsdMan_t
struct Kit_DsdMan_t_ Kit_DsdMan_t
Definition kit.h:137
Kit_DsdNtkForEachObj
#define Kit_DsdNtkForEachObj(pNtk, pObj, i)
Definition kit.h:158
Kit_DsdNtk_t_::pSupps
unsigned * pSupps
Definition kit.h:132
Kit_DsdNtk_t_::Root
unsigned short Root
Definition kit.h:130
Kit_DsdNtk_t_::pMem
unsigned * pMem
Definition kit.h:131
Kit_DsdNtk_t_::nNodesAlloc
unsigned short nNodesAlloc
Definition kit.h:128
Kit_DsdNtk_t_::nVars
unsigned short nVars
Definition kit.h:127
Kit_DsdNtk_t_::pNodes
Kit_DsdObj_t ** pNodes
Definition kit.h:133
Kit_DsdNtk_t_::nNodes
unsigned short nNodes
Definition kit.h:129
Kit_DsdObj_t_::Type
unsigned Type
Definition kit.h:115
Kit_DsdObj_t_::Offset
unsigned Offset
Definition kit.h:117
Kit_DsdObj_t_::nRefs
unsigned nRefs
Definition kit.h:118
Kit_DsdObj_t_::nFans
unsigned nFans
Definition kit.h:119
Kit_DsdObj_t_::pFans
unsigned short pFans[0]
Definition kit.h:120
Kit_DsdObj_t_::Id
unsigned Id
Definition kit.h:114
Kit_DsdObj_t_::fMark
unsigned fMark
Definition kit.h:116
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
strlen
int strlen()
sprintf
char * sprintf()