1 /**CFile****************************************************************
2 
3   FileName    [kitDsd.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Computation kit.]
8 
9   Synopsis    [Performs disjoint-support decomposition based on truth tables.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - Dec 6, 2006.]
16 
17   Revision    [$Id: kitDsd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "kit.h"
22 #include "misc/extra/extra.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 ///                        DECLARATIONS                              ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 ///                     FUNCTION DEFINITIONS                         ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37   Synopsis    [Allocates the DSD manager.]
38 
39   Description []
40 
41   SideEffects []
42 
43   SeeAlso     []
44 
45 ***********************************************************************/
Kit_DsdManAlloc(int nVars,int nNodes)46 Kit_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 
61 /**Function*************************************************************
62 
63   Synopsis    [Deallocates the DSD manager.]
64 
65   Description []
66 
67   SideEffects []
68 
69   SeeAlso     []
70 
71 ***********************************************************************/
Kit_DsdManFree(Kit_DsdMan_t * p)72 void 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 
82 /**Function*************************************************************
83 
84   Synopsis    [Allocates the DSD node.]
85 
86   Description []
87 
88   SideEffects []
89 
90   SeeAlso     []
91 
92 ***********************************************************************/
Kit_DsdObjAlloc(Kit_DsdNtk_t * pNtk,Kit_Dsd_t Type,int nFans)93 Kit_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 
114 /**Function*************************************************************
115 
116   Synopsis    [Deallocates the DSD node.]
117 
118   Description []
119 
120   SideEffects []
121 
122   SeeAlso     []
123 
124 ***********************************************************************/
Kit_DsdObjFree(Kit_DsdNtk_t * p,Kit_DsdObj_t * pObj)125 void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
126 {
127     ABC_FREE( pObj );
128 }
129 
130 /**Function*************************************************************
131 
132   Synopsis    [Allocates the DSD network.]
133 
134   Description []
135 
136   SideEffects []
137 
138   SeeAlso     []
139 
140 ***********************************************************************/
Kit_DsdNtkAlloc(int nVars)141 Kit_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 
153 /**Function*************************************************************
154 
155   Synopsis    [Deallocate the DSD network.]
156 
157   Description []
158 
159   SideEffects []
160 
161   SeeAlso     []
162 
163 ***********************************************************************/
Kit_DsdNtkFree(Kit_DsdNtk_t * pNtk)164 void 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 
176 /**Function*************************************************************
177 
178   Synopsis    [Prints the hex unsigned into a file.]
179 
180   Description []
181 
182   SideEffects []
183 
184   SeeAlso     []
185 
186 ***********************************************************************/
Kit_DsdPrintHex(FILE * pFile,unsigned * pTruth,int nFans)187 void 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 
201 /**Function*************************************************************
202 
203   Synopsis    [Prints the hex unsigned into a file.]
204 
205   Description []
206 
207   SideEffects []
208 
209   SeeAlso     []
210 
211 ***********************************************************************/
Kit_DsdWriteHex(char * pBuff,unsigned * pTruth,int nFans)212 char * 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 
227 /**Function*************************************************************
228 
229   Synopsis    [Recursively print the DSD formula.]
230 
231   Description []
232 
233   SideEffects []
234 
235   SeeAlso     []
236 
237 ***********************************************************************/
Kit_DsdPrint2_rec(FILE * pFile,Kit_DsdNtk_t * pNtk,int Id)238 void 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 
287 /**Function*************************************************************
288 
289   Synopsis    [Print the DSD formula.]
290 
291   Description []
292 
293   SideEffects []
294 
295   SeeAlso     []
296 
297 ***********************************************************************/
Kit_DsdPrint2(FILE * pFile,Kit_DsdNtk_t * pNtk)298 void 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 
307 /**Function*************************************************************
308 
309   Synopsis    [Recursively print the DSD formula.]
310 
311   Description []
312 
313   SideEffects []
314 
315   SeeAlso     []
316 
317 ***********************************************************************/
Kit_DsdPrint_rec(FILE * pFile,Kit_DsdNtk_t * pNtk,int Id)318 void 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 
364 /**Function*************************************************************
365 
366   Synopsis    [Print the DSD formula.]
367 
368   Description []
369 
370   SideEffects []
371 
372   SeeAlso     []
373 
374 ***********************************************************************/
Kit_DsdPrint(FILE * pFile,Kit_DsdNtk_t * pNtk)375 void 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 
384 /**Function*************************************************************
385 
386   Synopsis    [Recursively print the DSD formula.]
387 
388   Description []
389 
390   SideEffects []
391 
392   SeeAlso     []
393 
394 ***********************************************************************/
Kit_DsdWrite_rec(char * pBuff,Kit_DsdNtk_t * pNtk,int Id)395 char * 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 
442 /**Function*************************************************************
443 
444   Synopsis    [Print the DSD formula.]
445 
446   Description []
447 
448   SideEffects []
449 
450   SeeAlso     []
451 
452 ***********************************************************************/
Kit_DsdWrite(char * pBuff,Kit_DsdNtk_t * pNtk)453 void 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 
461 /**Function*************************************************************
462 
463   Synopsis    [Print the DSD formula.]
464 
465   Description []
466 
467   SideEffects []
468 
469   SeeAlso     []
470 
471 ***********************************************************************/
Kit_DsdPrintExpanded(Kit_DsdNtk_t * pNtk)472 void 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 
480 /**Function*************************************************************
481 
482   Synopsis    [Print the DSD formula.]
483 
484   Description []
485 
486   SideEffects []
487 
488   SeeAlso     []
489 
490 ***********************************************************************/
Kit_DsdPrintFromTruth(unsigned * pTruth,int nVars)491 void 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 
504 /**Function*************************************************************
505 
506   Synopsis    [Print the DSD formula.]
507 
508   Description []
509 
510   SideEffects []
511 
512   SeeAlso     []
513 
514 ***********************************************************************/
Kit_DsdPrintFromTruth2(FILE * pFile,unsigned * pTruth,int nVars)515 void 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 
526 /**Function*************************************************************
527 
528   Synopsis    [Print the DSD formula.]
529 
530   Description []
531 
532   SideEffects []
533 
534   SeeAlso     []
535 
536 ***********************************************************************/
Kit_DsdWriteFromTruth(char * pBuffer,unsigned * pTruth,int nVars)537 void 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 
550 /**Function*************************************************************
551 
552   Synopsis    [Derives the truth table of the DSD node.]
553 
554   Description []
555 
556   SideEffects []
557 
558   SeeAlso     []
559 
560 ***********************************************************************/
Kit_DsdTruthComputeNode_rec(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk,int Id)561 unsigned * 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 
653 /**Function*************************************************************
654 
655   Synopsis    [Derives the truth table of the DSD network.]
656 
657   Description []
658 
659   SideEffects []
660 
661   SeeAlso     []
662 
663 ***********************************************************************/
Kit_DsdTruthCompute(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk)664 unsigned * 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 
680 /**Function*************************************************************
681 
682   Synopsis    [Derives the truth table of the DSD node.]
683 
684   Description []
685 
686   SideEffects []
687 
688   SeeAlso     []
689 
690 ***********************************************************************/
Kit_DsdTruthComputeNodeOne_rec(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk,int Id,unsigned uSupp)691 unsigned * 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 
813 /**Function*************************************************************
814 
815   Synopsis    [Derives the truth table of the DSD network.]
816 
817   Description []
818 
819   SideEffects []
820 
821   SeeAlso     []
822 
823 ***********************************************************************/
Kit_DsdTruthComputeOne(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk,unsigned uSupp)824 unsigned * 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 
843 /**Function*************************************************************
844 
845   Synopsis    [Derives the truth table of the DSD node.]
846 
847   Description []
848 
849   SideEffects []
850 
851   SeeAlso     []
852 
853 ***********************************************************************/
Kit_DsdTruthComputeNodeTwo_rec(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk,int Id,unsigned uSupp,int iVar,unsigned * pTruthDec)854 unsigned * 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 
1014 /**Function*************************************************************
1015 
1016   Synopsis    [Derives the truth table of the DSD network.]
1017 
1018   Description []
1019 
1020   SideEffects []
1021 
1022   SeeAlso     []
1023 
1024 ***********************************************************************/
Kit_DsdTruthComputeTwo(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk,unsigned uSupp,int iVar,unsigned * pTruthDec)1025 unsigned * 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 
1058 /**Function*************************************************************
1059 
1060   Synopsis    [Derives the truth table of the DSD network.]
1061 
1062   Description []
1063 
1064   SideEffects []
1065 
1066   SeeAlso     []
1067 
1068 ***********************************************************************/
Kit_DsdTruth(Kit_DsdNtk_t * pNtk,unsigned * pTruthRes)1069 void 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 
1079 /**Function*************************************************************
1080 
1081   Synopsis    [Derives the truth table of the DSD network.]
1082 
1083   Description []
1084 
1085   SideEffects []
1086 
1087   SeeAlso     []
1088 
1089 ***********************************************************************/
Kit_DsdTruthPartialTwo(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk,unsigned uSupp,int iVar,unsigned * pTruthCo,unsigned * pTruthDec)1090 void 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 
1097 /**Function*************************************************************
1098 
1099   Synopsis    [Derives the truth table of the DSD network.]
1100 
1101   Description []
1102 
1103   SideEffects []
1104 
1105   SeeAlso     []
1106 
1107 ***********************************************************************/
Kit_DsdTruthPartial(Kit_DsdMan_t * p,Kit_DsdNtk_t * pNtk,unsigned * pTruthRes,unsigned uSupp)1108 void 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 
1133 /**Function*************************************************************
1134 
1135   Synopsis    [Counts the number of blocks of the given number of inputs.]
1136 
1137   Description []
1138 
1139   SideEffects []
1140 
1141   SeeAlso     []
1142 
1143 ***********************************************************************/
Kit_DsdCountLuts_rec(Kit_DsdNtk_t * pNtk,int nLutSize,int Id,int * pCounter)1144 int 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 
1177 /**Function*************************************************************
1178 
1179   Synopsis    [Counts the number of blocks of the given number of inputs.]
1180 
1181   Description []
1182 
1183   SideEffects []
1184 
1185   SeeAlso     []
1186 
1187 ***********************************************************************/
Kit_DsdCountLuts(Kit_DsdNtk_t * pNtk,int nLutSize)1188 int 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 
1201 /**Function*************************************************************
1202 
1203   Synopsis    [Returns the size of the largest non-DSD block.]
1204 
1205   Description []
1206 
1207   SideEffects []
1208 
1209   SeeAlso     []
1210 
1211 ***********************************************************************/
Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t * pNtk)1212 int 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 
1226 /**Function*************************************************************
1227 
1228   Synopsis    [Returns the largest non-DSD block.]
1229 
1230   Description []
1231 
1232   SideEffects []
1233 
1234   SeeAlso     []
1235 
1236 ***********************************************************************/
Kit_DsdNonDsdPrimeMax(Kit_DsdNtk_t * pNtk)1237 Kit_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 
1254 /**Function*************************************************************
1255 
1256   Synopsis    [Finds the union of supports of the non-DSD blocks.]
1257 
1258   Description []
1259 
1260   SideEffects []
1261 
1262   SeeAlso     []
1263 
1264 ***********************************************************************/
Kit_DsdNonDsdSupports(Kit_DsdNtk_t * pNtk)1265 unsigned 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 
1281 /**Function*************************************************************
1282 
1283   Synopsis    [Expands the node.]
1284 
1285   Description [Returns the new literal.]
1286 
1287   SideEffects []
1288 
1289   SeeAlso     []
1290 
1291 ***********************************************************************/
Kit_DsdExpandCollectAnd_rec(Kit_DsdNtk_t * p,unsigned iLit,unsigned * piLitsNew,int * nLitsNew)1292 void 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 
1308 /**Function*************************************************************
1309 
1310   Synopsis    [Expands the node.]
1311 
1312   Description [Returns the new literal.]
1313 
1314   SideEffects []
1315 
1316   SeeAlso     []
1317 
1318 ***********************************************************************/
Kit_DsdExpandCollectXor_rec(Kit_DsdNtk_t * p,unsigned iLit,unsigned * piLitsNew,int * nLitsNew)1319 void 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 
1339 /**Function*************************************************************
1340 
1341   Synopsis    [Expands the node.]
1342 
1343   Description [Returns the new literal.]
1344 
1345   SideEffects []
1346 
1347   SeeAlso     []
1348 
1349 ***********************************************************************/
Kit_DsdExpandNode_rec(Kit_DsdNtk_t * pNew,Kit_DsdNtk_t * p,int iLit)1350 int 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 
1441 /**Function*************************************************************
1442 
1443   Synopsis    [Expands the network.]
1444 
1445   Description []
1446 
1447   SideEffects []
1448 
1449   SeeAlso     []
1450 
1451 ***********************************************************************/
Kit_DsdExpand(Kit_DsdNtk_t * p)1452 Kit_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 
1478 /**Function*************************************************************
1479 
1480   Synopsis    [Sorts the literals by their support.]
1481 
1482   Description []
1483 
1484   SideEffects []
1485 
1486   SeeAlso     []
1487 
1488 ***********************************************************************/
Kit_DsdCompSort(int pPrios[],unsigned uSupps[],unsigned short * piLits,int nVars,unsigned piLitsRes[])1489 void 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 
1533 /**Function*************************************************************
1534 
1535   Synopsis    [Shrinks multi-input nodes.]
1536 
1537   Description [Takes the array of variable priorities pPrios.]
1538 
1539   SideEffects []
1540 
1541   SeeAlso     []
1542 
1543 ***********************************************************************/
Kit_DsdShrink_rec(Kit_DsdNtk_t * pNew,Kit_DsdNtk_t * p,int iLit,int pPrios[])1544 int 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 
1622 /**Function*************************************************************
1623 
1624   Synopsis    [Shrinks the network.]
1625 
1626   Description [Transforms the network to have two-input nodes so that the
1627   higher-ordered nodes were decomposed out first.]
1628 
1629   SideEffects []
1630 
1631   SeeAlso     []
1632 
1633 ***********************************************************************/
Kit_DsdShrink(Kit_DsdNtk_t * p,int pPrios[])1634 Kit_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 
1660 /**Function*************************************************************
1661 
1662   Synopsis    [Rotates the network.]
1663 
1664   Description [Transforms prime nodes to have the fanin with the
1665   highest frequency of supports go first.]
1666 
1667   SideEffects []
1668 
1669   SeeAlso     []
1670 
1671 ***********************************************************************/
Kit_DsdRotate(Kit_DsdNtk_t * p,int pFreqs[])1672 void 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 
1725 /**Function*************************************************************
1726 
1727   Synopsis    [Compute the support.]
1728 
1729   Description []
1730 
1731   SideEffects []
1732 
1733   SeeAlso     []
1734 
1735 ***********************************************************************/
Kit_DsdGetSupports_rec(Kit_DsdNtk_t * p,int iLit)1736 unsigned 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 
1752 /**Function*************************************************************
1753 
1754   Synopsis    [Compute the support.]
1755 
1756   Description []
1757 
1758   SideEffects []
1759 
1760   SeeAlso     []
1761 
1762 ***********************************************************************/
Kit_DsdGetSupports(Kit_DsdNtk_t * p)1763 unsigned 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 
1787 /**Function*************************************************************
1788 
1789   Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
1790 
1791   Description []
1792 
1793   SideEffects []
1794 
1795   SeeAlso     []
1796 
1797 ***********************************************************************/
Kit_DsdFindLargeBox_rec(Kit_DsdNtk_t * pNtk,int Id,int Size)1798 int 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 
1813 /**Function*************************************************************
1814 
1815   Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
1816 
1817   Description []
1818 
1819   SideEffects []
1820 
1821   SeeAlso     []
1822 
1823 ***********************************************************************/
Kit_DsdFindLargeBox(Kit_DsdNtk_t * pNtk,int Size)1824 int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
1825 {
1826     return Kit_DsdFindLargeBox_rec( pNtk, Abc_Lit2Var(pNtk->Root), Size );
1827 }
1828 
1829 /**Function*************************************************************
1830 
1831   Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
1832 
1833   Description []
1834 
1835   SideEffects []
1836 
1837   SeeAlso     []
1838 
1839 ***********************************************************************/
Kit_DsdCountAigNodes_rec(Kit_DsdNtk_t * pNtk,int Id)1840 int 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 
1869 /**Function*************************************************************
1870 
1871   Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
1872 
1873   Description []
1874 
1875   SideEffects []
1876 
1877   SeeAlso     []
1878 
1879 ***********************************************************************/
Kit_DsdCountAigNodes2(Kit_DsdNtk_t * pNtk)1880 int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk )
1881 {
1882     return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) );
1883 }
1884 
1885 /**Function*************************************************************
1886 
1887   Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
1888 
1889   Description []
1890 
1891   SideEffects []
1892 
1893   SeeAlso     []
1894 
1895 ***********************************************************************/
Kit_DsdCountAigNodes(Kit_DsdNtk_t * pNtk)1896 int 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 
1913 /**Function*************************************************************
1914 
1915   Synopsis    [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
1916 
1917   Description []
1918 
1919   SideEffects []
1920 
1921   SeeAlso     []
1922 
1923 ***********************************************************************/
Kit_DsdRootNodeHasCommonVars(Kit_DsdObj_t * pObj0,Kit_DsdObj_t * pObj1)1924 int 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 
1938 /**Function*************************************************************
1939 
1940   Synopsis    [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
1941 
1942   Description []
1943 
1944   SideEffects []
1945 
1946   SeeAlso     []
1947 
1948 ***********************************************************************/
Kit_DsdCheckVar4Dec2(Kit_DsdNtk_t * pNtk0,Kit_DsdNtk_t * pNtk1)1949 int 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 
1960 /**Function*************************************************************
1961 
1962   Synopsis    [Performs decomposition of the node.]
1963 
1964   Description []
1965 
1966   SideEffects []
1967 
1968   SeeAlso     []
1969 
1970 ***********************************************************************/
Kit_DsdDecompose_rec(Kit_DsdNtk_t * pNtk,Kit_DsdObj_t * pObj,unsigned uSupp,unsigned short * pPar,int nDecMux)1971 void 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 
2256 /**Function*************************************************************
2257 
2258   Synopsis    [Performs decomposition of the truth table.]
2259 
2260   Description []
2261 
2262   SideEffects []
2263 
2264   SeeAlso     []
2265 
2266 ***********************************************************************/
Kit_DsdDecomposeInt(unsigned * pTruth,int nVars,int nDecMux)2267 Kit_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 
2304 /**Function*************************************************************
2305 
2306   Synopsis    [Performs decomposition of the truth table.]
2307 
2308   Description []
2309 
2310   SideEffects []
2311 
2312   SeeAlso     []
2313 
2314 ***********************************************************************/
Kit_DsdDecompose(unsigned * pTruth,int nVars)2315 Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
2316 {
2317     return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
2318 }
2319 
2320 /**Function*************************************************************
2321 
2322   Synopsis    [Performs decomposition of the truth table.]
2323 
2324   Description []
2325 
2326   SideEffects []
2327 
2328   SeeAlso     []
2329 
2330 ***********************************************************************/
Kit_DsdDecomposeExpand(unsigned * pTruth,int nVars)2331 Kit_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 
2340 /**Function*************************************************************
2341 
2342   Synopsis    [Performs decomposition of the truth table.]
2343 
2344   Description [Uses MUXes to break-down large prime nodes.]
2345 
2346   SideEffects []
2347 
2348   SeeAlso     []
2349 
2350 ***********************************************************************/
Kit_DsdDecomposeMux(unsigned * pTruth,int nVars,int nDecMux)2351 Kit_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 
2377 /**Function*************************************************************
2378 
2379   Synopsis    [Performs decomposition of the truth table.]
2380 
2381   Description []
2382 
2383   SideEffects []
2384 
2385   SeeAlso     []
2386 
2387 ***********************************************************************/
Kit_DsdTestCofs(Kit_DsdNtk_t * pNtk,unsigned * pTruthInit)2388 int 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 
2446 /**Function*************************************************************
2447 
2448   Synopsis    [Performs decomposition of the truth table.]
2449 
2450   Description []
2451 
2452   SideEffects []
2453 
2454   SeeAlso     []
2455 
2456 ***********************************************************************/
Kit_DsdEval(unsigned * pTruth,int nVars,int nLutSize)2457 int 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 
2482 /**Function*************************************************************
2483 
2484   Synopsis    [Performs decomposition of the truth table.]
2485 
2486   Description []
2487 
2488   SideEffects []
2489 
2490   SeeAlso     []
2491 
2492 ***********************************************************************/
Kit_DsdVerify(Kit_DsdNtk_t * pNtk,unsigned * pTruth,int nVars)2493 void 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.\n" );
2501     Kit_DsdManFree( p );
2502 }
2503 
2504 /**Function*************************************************************
2505 
2506   Synopsis    [Performs decomposition of the truth table.]
2507 
2508   Description []
2509 
2510   SideEffects []
2511 
2512   SeeAlso     []
2513 
2514 ***********************************************************************/
Kit_DsdTest(unsigned * pTruth,int nVars)2515 void 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 
2555 /**Function*************************************************************
2556 
2557   Synopsis    [Performs decomposition of the truth table.]
2558 
2559   Description []
2560 
2561   SideEffects []
2562 
2563   SeeAlso     []
2564 
2565 ***********************************************************************/
Kit_DsdPrecompute4Vars()2566 void 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 
2622 /**Function*************************************************************
2623 
2624   Synopsis    [Returns the set of cofactoring variables.]
2625 
2626   Description [If there is no DSD components returns 0.]
2627 
2628   SideEffects []
2629 
2630   SeeAlso     []
2631 
2632 ***********************************************************************/
Kit_DsdCofactoringGetVars(Kit_DsdNtk_t ** ppNtk,int nSize,int * pVars)2633 int 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 
2667 /**Function*************************************************************
2668 
2669   Synopsis    [Canonical decomposition into completely DSD-structure.]
2670 
2671   Description [Returns the number of cofactoring steps. Also returns
2672   the cofactoring variables in pVars.]
2673 
2674   SideEffects []
2675 
2676   SeeAlso     []
2677 
2678 ***********************************************************************/
Kit_DsdCofactoring(unsigned * pTruth,int nVars,int * pCofVars,int nLimit,int fVerbose)2679 int 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 
2792 /**Function*************************************************************
2793 
2794   Synopsis    [Canonical decomposition into completely DSD-structure.]
2795 
2796   Description [Returns the number of cofactoring steps. Also returns
2797   the cofactoring variables in pVars.]
2798 
2799   SideEffects []
2800 
2801   SeeAlso     []
2802 
2803 ***********************************************************************/
Kit_DsdPrintCofactors(unsigned * pTruth,int nVars,int nCofLevel,int fVerbose)2804 void 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 
3038 /**Function*************************************************************
3039 
3040   Synopsis    []
3041 
3042   Description []
3043 
3044   SideEffects []
3045 
3046   SeeAlso     []
3047 
3048 ***********************************************************************/
Kit_DsdNpn4ClassNames()3049 char ** 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 
3279 ////////////////////////////////////////////////////////////////////////
3280 ///                       END OF FILE                                ///
3281 ////////////////////////////////////////////////////////////////////////
3282 
3283 
3284 ABC_NAMESPACE_IMPL_END
3285 
3286