1 /**CFile****************************************************************
2 
3   FileName    [dauNpn2.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Functional enumeration.]
8 
9   Synopsis    [Functional enumeration.]
10 
11   Author      [Siang-Yun Lee]
12 
13   Affiliation [National Taiwan University]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: dauNpn2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "dauInt.h"
22 #include "misc/util/utilTruth.h"
23 #include "misc/extra/extra.h"
24 #include "aig/gia/gia.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 ////////////////////////////////////////////////////////////////////////
29 ///                        DECLARATIONS                              ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 typedef struct Dtt_Man_t_ Dtt_Man_t;
33 struct Dtt_Man_t_
34 {
35     int            nVars;          // variable number
36     int            nPerms;         // number of permutations
37     int            nComps;         // number of complementations
38     int *          pPerms;         // permutations
39     int *          pComps;         // complementations
40     word *         pPres;          // function marks
41     Vec_Int_t *    vFanins;        // node fanins
42     Vec_Int_t *    vTruths;        // node truth tables
43     Vec_Int_t *    vConfigs;       // configurations
44     Vec_Int_t *    vClasses;       // node NPN classes
45     Vec_Int_t *    vTruthNpns;     // truth tables of the classes
46     Vec_Wec_t *    vFunNodes;      // nodes by NPN class
47     Vec_Int_t *    vTemp;          // temporary
48     Vec_Int_t *    vTemp2;         // temporary
49     unsigned       FunMask;        // function mask
50     unsigned       CmpMask;        // function mask
51     unsigned       BinMask;        // hash mask
52     unsigned *     pBins;          // hash bins
53     Vec_Int_t *    vUsedBins;      // used bins
54     int            Counts[32];     // node counts
55     int            nClasses;       // count of classes
56     unsigned *     pTable;         // mapping of funcs into their classes
57     int *          pNodes;         // the number of nodes in min-node network
58     int *          pTimes;         // the number of different min-node networks
59     char *         pVisited;       // visited classes
60     Vec_Int_t *    vVisited;       // the number of visited classes
61 };
62 
63 ////////////////////////////////////////////////////////////////////////
64 ///                     FUNCTION DEFINITIONS                         ///
65 ////////////////////////////////////////////////////////////////////////
66 
67 /**Function*************************************************************
68 
69   Synopsis    [Parse one formula into a truth table.]
70 
71   Description []
72 
73   SideEffects []
74 
75   SeeAlso     []
76 
77 ***********************************************************************/
Dau_ParseFormulaEndToken(char * pForm)78 char * Dau_ParseFormulaEndToken( char * pForm )
79 {
80     int Counter = 0;
81     char * pThis;
82     for ( pThis = pForm; *pThis; pThis++ )
83     {
84         if ( *pThis == '~' )
85             continue;
86         if ( *pThis == '(' )
87             Counter++;
88         else if ( *pThis == ')' )
89             Counter--;
90         if ( Counter == 0 )
91             return pThis + 1;
92     }
93     assert( 0 );
94     return NULL;
95 }
Dau_ParseFormula_rec(char * pBeg,char * pEnd)96 word Dau_ParseFormula_rec( char * pBeg, char * pEnd )
97 {
98     word iFans[2], Res, Oper = -1;
99     char * pEndNew;
100     int fCompl = 0;
101     while ( pBeg[0] == '~' )
102     {
103         pBeg++;
104         fCompl ^= 1;
105     }
106     if ( pBeg + 1 == pEnd )
107     {
108         if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' )
109             return fCompl ? ~s_Truths6[pBeg[0] - 'a'] : s_Truths6[pBeg[0] - 'a'];
110         assert( 0 );
111         return -1;
112     }
113     if ( pBeg[0] == '(' )
114     {
115         pEndNew = Dau_ParseFormulaEndToken( pBeg );
116         if ( pEndNew == pEnd )
117         {
118             assert( pBeg[0] == '(' );
119             assert( pBeg[pEnd-pBeg-1] == ')' );
120             Res = Dau_ParseFormula_rec( pBeg + 1, pEnd - 1 );
121             return fCompl ? ~Res : Res;
122         }
123     }
124     // get first part
125     pEndNew  = Dau_ParseFormulaEndToken( pBeg );
126     iFans[0] = Dau_ParseFormula_rec( pBeg, pEndNew );
127     iFans[0] = fCompl ? ~iFans[0] : iFans[0];
128     Oper     = pEndNew[0];
129     // get second part
130     pBeg     = pEndNew + 1;
131     pEndNew  = Dau_ParseFormulaEndToken( pBeg );
132     iFans[1] = Dau_ParseFormula_rec( pBeg, pEndNew );
133     // derive the formula
134     if ( Oper == '&' )
135         return iFans[0] & iFans[1];
136     if ( Oper == '^' )
137         return iFans[0] ^ iFans[1];
138     assert( 0 );
139     return -1;
140 }
Dau_ParseFormula(char * p)141 word Dau_ParseFormula( char * p )
142 {
143     return Dau_ParseFormula_rec( p, p + strlen(p) );
144 }
Dau_ParseFormulaTest()145 void Dau_ParseFormulaTest()
146 {
147     char * p = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))";
148     word r = ABC_CONST(0x037d037d037d037d);
149     word t = Dau_ParseFormula( p );
150     assert( r == t );
151 }
152 
153 
154 /**Function*************************************************************
155 
156   Synopsis    [Parse one formula into a AIG.]
157 
158   Description []
159 
160   SideEffects []
161 
162   SeeAlso     []
163 
164 ***********************************************************************/
Dau_ParseFormulaAig_rec(Gia_Man_t * p,char * pBeg,char * pEnd)165 int Dau_ParseFormulaAig_rec( Gia_Man_t * p, char * pBeg, char * pEnd )
166 {
167     int iFans[2], Res, Oper = -1;
168     char * pEndNew;
169     int fCompl = 0;
170     while ( pBeg[0] == '~' )
171     {
172         pBeg++;
173         fCompl ^= 1;
174     }
175     if ( pBeg + 1 == pEnd )
176     {
177         if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' )
178             return Abc_Var2Lit( 1 + pBeg[0] - 'a', fCompl );
179         assert( 0 );
180         return -1;
181     }
182     if ( pBeg[0] == '(' )
183     {
184         pEndNew = Dau_ParseFormulaEndToken( pBeg );
185         if ( pEndNew == pEnd )
186         {
187             assert( pBeg[0] == '(' );
188             assert( pBeg[pEnd-pBeg-1] == ')' );
189             Res = Dau_ParseFormulaAig_rec( p, pBeg + 1, pEnd - 1 );
190             return Abc_LitNotCond( Res, fCompl );
191         }
192     }
193     // get first part
194     pEndNew  = Dau_ParseFormulaEndToken( pBeg );
195     iFans[0] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew );
196     iFans[0] = Abc_LitNotCond( iFans[0], fCompl );
197     Oper     = pEndNew[0];
198     // get second part
199     pBeg     = pEndNew + 1;
200     pEndNew  = Dau_ParseFormulaEndToken( pBeg );
201     iFans[1] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew );
202     // derive the formula
203     if ( Oper == '&' )
204         return Gia_ManHashAnd( p, iFans[0], iFans[1] );
205     if ( Oper == '^' )
206         return Gia_ManHashXor( p, iFans[0], iFans[1] );
207     assert( 0 );
208     return -1;
209 }
Dau_ParseFormulaAig(Gia_Man_t * p,char * pStr)210 int Dau_ParseFormulaAig( Gia_Man_t * p, char * pStr )
211 {
212     return Dau_ParseFormulaAig_rec( p, pStr, pStr + strlen(pStr) );
213 }
Dau_ParseFormulaAigTest()214 Gia_Man_t * Dau_ParseFormulaAigTest()
215 {
216     int i;
217     char * pStr = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))";
218     Gia_Man_t * p = Gia_ManStart( 1000 );
219     p->pName = Abc_UtilStrsav( "func_enum_aig" );
220     Gia_ManHashAlloc( p );
221     for ( i = 0; i < 5; i++ )
222         Gia_ManAppendCi( p );
223     Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, pStr) );
224     return p;
225 }
226 
227 
228 /**Function*************************************************************
229 
230   Synopsis    [Verify one file.]
231 
232   Description []
233 
234   SideEffects []
235 
236   SeeAlso     []
237 
238 ***********************************************************************/
Dau_VerifyFile(char * pFileName)239 void Dau_VerifyFile( char * pFileName )
240 {
241     char Buffer[1000];
242     unsigned uTruth, uTruth2;
243     int nFails = 0, nLines = 0;
244     FILE * pFile = fopen( pFileName, "rb" );
245     while ( fgets( Buffer, 1000, pFile ) )
246     {
247         if ( Buffer[strlen(Buffer)-1] == '\n' )
248             Buffer[strlen(Buffer)-1] = 0;
249         if ( Buffer[strlen(Buffer)-1] == '\r' )
250             Buffer[strlen(Buffer)-1] = 0;
251         Extra_ReadHexadecimal( &uTruth2, Buffer, 5 );
252         uTruth = (unsigned)Dau_ParseFormula( Buffer + 11 );
253         if ( uTruth != uTruth2 )
254             printf( "Verification failed in line %d:  %s\n", nLines, Buffer ), nFails++;
255         nLines++;
256     }
257     printf( "Verification succeeded for %d functions and failed for %d functions.\n", nLines-nFails, nFails );
258 }
Dau_VerifyFileTest()259 void Dau_VerifyFileTest()
260 {
261     char * pFileName = "lib4var.txt";
262     Dau_VerifyFile( pFileName );
263 }
264 
265 
266 /**Function*************************************************************
267 
268   Synopsis    [Create AIG for one file.]
269 
270   Description []
271 
272   SideEffects []
273 
274   SeeAlso     []
275 
276 ***********************************************************************/
Dau_ConstructAigFromFile(char * pFileName)277 Gia_Man_t * Dau_ConstructAigFromFile( char * pFileName )
278 {
279     char Buffer[1000];
280     int i, nLines = 0;
281     FILE * pFile = fopen( pFileName, "rb" );
282     Gia_Man_t * p = Gia_ManStart( 1000 );
283     p->pName = Abc_UtilStrsav( "func_enum_aig" );
284     Gia_ManHashAlloc( p );
285     for ( i = 0; i < 5; i++ )
286         Gia_ManAppendCi( p );
287     while ( fgets( Buffer, 1000, pFile ) )
288     {
289         if ( Buffer[strlen(Buffer)-1] == '\n' )
290             Buffer[strlen(Buffer)-1] = 0;
291         if ( Buffer[strlen(Buffer)-1] == '\r' )
292             Buffer[strlen(Buffer)-1] = 0;
293         Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, Buffer + 11) );
294         nLines++;
295     }
296     printf( "Finish constructing AIG for %d structures.\n", nLines );
297     return p;
298 }
299 
300 /**Function*************************************************************
301 
302   Synopsis    []
303 
304   Description []
305 
306   SideEffects []
307 
308   SeeAlso     []
309 
310 ***********************************************************************/
Dau_ReadFile2(char * pFileName,int nSizeW)311 unsigned * Dau_ReadFile2( char * pFileName, int nSizeW )
312 {
313     abctime clk = Abc_Clock();
314     unsigned * p;
315     int RetValue;
316     FILE * pFile = fopen( pFileName, "rb" );
317     if (pFile == NULL) return NULL;
318     p = (unsigned *)ABC_CALLOC(word, nSizeW);
319     RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
320     RetValue = 0;
321     if ( pFile )
322     {
323         printf( "Finished reading file \"%s\".\n", pFileName );
324         fclose( pFile );
325     }
326     else
327         printf( "Cannot open input file \"%s\".\n", pFileName );
328     Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
329     return p;
330 }
Dtt_ManRenum(int nVars,unsigned * pTable,int * pnClasses)331 void Dtt_ManRenum( int nVars, unsigned * pTable, int * pnClasses )
332 {
333     unsigned i, Limit = 1 << ((1 << nVars)-1), Count = 0;
334     for ( i = 0; i < Limit; i++ )
335         if ( pTable[i] == i )
336             pTable[i] = Count++;
337         else
338         {
339             assert( pTable[i] < i );
340             pTable[i] = pTable[pTable[i]];
341         }
342     printf( "The total number of NPN classes = %d.\n", Count );
343     *pnClasses = Count;
344 }
Dtt_ManLoadClasses(int nVars,int * pnClasses)345 unsigned * Dtt_ManLoadClasses( int nVars, int * pnClasses )
346 {
347     extern void Dau_TruthEnum(int nVars);
348     unsigned * pTable = NULL;
349     int nSizeLog = (1<<nVars) -2;
350     int nSizeW = 1 << nSizeLog;
351     char pFileName[200];
352     sprintf( pFileName, "tableW%d.data", nSizeLog );
353     pTable = Dau_ReadFile2( pFileName, nSizeW );
354     if (pTable == NULL)
355     {
356         Dau_TruthEnum(nVars);
357         pTable = Dau_ReadFile2( pFileName, nSizeW );
358     }
359     Dtt_ManRenum( nVars, pTable, pnClasses );
360     return pTable;
361 }
362 
363 /**Function*************************************************************
364 
365   Synopsis    []
366 
367   Description []
368 
369   SideEffects []
370 
371   SeeAlso     []
372 
373 ***********************************************************************/
Dtt_ManAddVisited(Dtt_Man_t * p,unsigned Truth2,int n)374 void Dtt_ManAddVisited( Dtt_Man_t * p, unsigned Truth2, int n )
375 {
376     unsigned Truth = Truth2 & p->CmpMask ? ~Truth2 : Truth2;
377     unsigned Class = p->pTable[Truth & p->FunMask];
378     assert( Class < (unsigned)p->nClasses );
379     if ( p->pNodes[Class] < n )
380         return;
381     assert( p->pNodes[Class] == n );
382     if ( p->pVisited[Class] )
383         return;
384     p->pVisited[Class] = 1;
385     Vec_IntPush( p->vVisited, Class );
386 }
Dtt_ManProcessVisited(Dtt_Man_t * p)387 void Dtt_ManProcessVisited( Dtt_Man_t * p )
388 {
389     int i, Class;
390     Vec_IntForEachEntry( p->vVisited, Class, i )
391     {
392         assert( p->pVisited[Class] );
393         p->pVisited[Class] = 0;
394         p->pTimes[Class]++;
395     }
396     Vec_IntClear( p->vVisited );
397 }
398 
399 /**Function*************************************************************
400 
401   Synopsis    []
402 
403   Description []
404 
405   SideEffects []
406 
407   SeeAlso     []
408 
409 ***********************************************************************/
Dtt_ManAlloc(int nVars,int fMulti)410 Dtt_Man_t * Dtt_ManAlloc( int nVars, int fMulti )
411 {
412     Dtt_Man_t * p = ABC_CALLOC( Dtt_Man_t, 1 );
413     p->nVars      = nVars;
414     p->nPerms     = Extra_Factorial( nVars );
415     p->nComps     = 1 << nVars;
416     p->pPerms     = Extra_PermSchedule( nVars );
417     p->pComps     = Extra_GreyCodeSchedule( nVars );
418     p->pPres      = ABC_CALLOC( word, 1 << (p->nComps - 7) );
419     p->vFanins    = Vec_IntAlloc( 2*617000 );
420     p->vTruths    = Vec_IntAlloc( 617000 );
421     p->vConfigs   = Vec_IntAlloc( 617000 );
422     p->vClasses   = Vec_IntAlloc( 617000 );
423     p->vTruthNpns = Vec_IntAlloc( 617000 );
424     p->vFunNodes  = Vec_WecStart( 16 );
425     p->vTemp      = Vec_IntAlloc( 4000 );
426     p->vTemp2     = Vec_IntAlloc( 4000 );
427     p->FunMask    = nVars == 5 ?      ~0 : (nVars == 4 ?  0xFFFF :   0xFF);
428     p->CmpMask    = nVars == 5 ? 1 << 31 : (nVars == 4 ? 1 << 15 : 1 << 7);
429     p->BinMask    = 0x3FFF;
430     p->pBins      = ABC_FALLOC( unsigned, p->BinMask + 1 );
431     p->vUsedBins  = Vec_IntAlloc( 4000 );
432     if ( !fMulti ) return p;
433     p->pTable     = Dtt_ManLoadClasses( p->nVars, &p->nClasses );
434     p->pNodes     = ABC_CALLOC( int, p->nClasses );
435     p->pTimes     = ABC_CALLOC( int, p->nClasses );
436     p->pVisited   = ABC_CALLOC( char, p->nClasses );
437     p->vVisited   = Vec_IntAlloc( 1000 );
438     return p;
439 }
Dtt_ManFree(Dtt_Man_t * p)440 void Dtt_ManFree( Dtt_Man_t * p )
441 {
442     Vec_IntFreeP( &p->vVisited );
443     ABC_FREE( p->pTable );
444     ABC_FREE( p->pNodes );
445     ABC_FREE( p->pTimes );
446     ABC_FREE( p->pVisited );
447     Vec_IntFreeP( &p->vFanins );
448     Vec_IntFreeP( &p->vTruths );
449     Vec_IntFreeP( &p->vConfigs );
450     Vec_IntFreeP( &p->vClasses );
451     Vec_IntFreeP( &p->vTruthNpns );
452     Vec_WecFreeP( &p->vFunNodes );
453     Vec_IntFreeP( &p->vTemp );
454     Vec_IntFreeP( &p->vTemp2 );
455     Vec_IntFreeP( &p->vUsedBins );
456     ABC_FREE( p->pPerms );
457     ABC_FREE( p->pComps );
458     ABC_FREE( p->pPres );
459     ABC_FREE( p->pBins );
460     ABC_FREE( p );
461 }
462 
463 /**Function*************************************************************
464 
465   Synopsis    [Collect representatives of the same class.]
466 
467   Description []
468 
469   SideEffects []
470 
471   SeeAlso     []
472 
473 ***********************************************************************/
Dtt_ManHashKey(Dtt_Man_t * p,unsigned Truth)474 static inline unsigned Dtt_ManHashKey( Dtt_Man_t * p, unsigned Truth )
475 {
476     static unsigned s_P[4] = { 1699, 5147, 7103, 8147 };
477     unsigned char * pD = (unsigned char*)&Truth;
478     return pD[0] * s_P[0] + pD[1] * s_P[1] + pD[2] * s_P[2] + pD[3] * s_P[3];
479 }
Dtt_ManCheckHash(Dtt_Man_t * p,unsigned Truth)480 int Dtt_ManCheckHash( Dtt_Man_t * p, unsigned Truth )
481 {
482     unsigned Hash = Dtt_ManHashKey(p, Truth);
483     unsigned * pSpot = p->pBins + (Hash & p->BinMask);
484     for ( ; ~*pSpot; Hash++, pSpot = p->pBins + (Hash & p->BinMask) )
485         if ( *pSpot == Truth ) // equal
486             return 0;
487     Vec_IntPush( p->vUsedBins, pSpot - p->pBins );
488     *pSpot = Truth;
489     return 1;
490 }
Dtt_ManCollect(Dtt_Man_t * p,unsigned Truth,Vec_Int_t * vFuns)491 Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns )
492 {
493     int i, k, Entry;
494     word tCur = ((word)Truth << 32) | (word)Truth;
495     Vec_IntClear( vFuns );
496     for ( i = 0; i < p->nPerms; i++ )
497     {
498         for ( k = 0; k < p->nComps; k++ )
499         {
500 //            unsigned tTemp = (unsigned)(tCur & 1 ? ~tCur : tCur);
501             unsigned tTemp = (unsigned)(tCur & p->CmpMask ? ~tCur : tCur);
502             if ( Dtt_ManCheckHash( p, tTemp ) )
503                 Vec_IntPush( vFuns, tTemp );
504             tCur = Abc_Tt6Flip( tCur, p->pComps[k] );
505         }
506         tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] );
507     }
508     assert( tCur == (((word)Truth << 32) | (word)Truth) );
509     // clean hash table
510     Vec_IntForEachEntry( p->vUsedBins, Entry, i )
511         p->pBins[Entry] = ~0;
512     Vec_IntClear( p->vUsedBins );
513     //printf( "%d ", Vec_IntSize(vFuns) );
514     return vFuns;
515 }
516 
517 /**Function*************************************************************
518 
519   Synopsis    []
520 
521   Description []
522 
523   SideEffects []
524 
525   SeeAlso     []
526 
527 ***********************************************************************/
Dtt_ManGetFun(Dtt_Man_t * p,unsigned tFun,int n)528 static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun, int n )
529 {
530     unsigned Class;
531     tFun = tFun & p->CmpMask ? ~tFun : tFun;
532     //return Abc_TtGetBit( p->pPres, tFun & p->FunMask );
533     if ( !Abc_TtGetBit( p->pPres, tFun & p->FunMask ) ) return 0;
534     if ( p->pTable == NULL ) return 1;
535 
536     Class = p->pTable[tFun & p->FunMask];
537     assert( Class < (unsigned)p->nClasses );
538     if ( p->pNodes[Class] < n )
539         return 1;
540     assert( p->pNodes[Class] == n );
541     if ( p->pVisited[Class] )
542         return 1;
543 
544     return 0;
545 }
Dtt_ManSetFun(Dtt_Man_t * p,unsigned tFun)546 static inline void Dtt_ManSetFun( Dtt_Man_t * p, unsigned tFun )
547 {
548     tFun = tFun & p->CmpMask ? ~tFun : tFun;
549     //assert( !Dtt_ManGetFun(p, fFun & p->FunMask );
550     Abc_TtSetBit( p->pPres, tFun & p->FunMask );
551 }
Dtt_ManAddFunction(Dtt_Man_t * p,int n,int FanI,int FanJ,int Type,unsigned Truth)552 void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, unsigned Truth )
553 {
554     Vec_Int_t * vFuncs = Dtt_ManCollect( p, Truth, p->vTemp2 );
555     unsigned Min = Vec_IntFindMin( vFuncs );
556     int i, nObjs = Vec_IntSize(p->vFanins)/2;
557     int nNodesI = 0xF & (Vec_IntEntry(p->vConfigs, FanI) >> 3);
558     int nNodesJ = 0xF & (Vec_IntEntry(p->vConfigs, FanJ) >> 3);
559     int nNodes  = nNodesI + nNodesJ + 1;
560     assert( nObjs == Vec_IntSize(p->vTruths) );
561     assert( nObjs == Vec_IntSize(p->vConfigs) );
562     assert( nObjs == Vec_IntSize(p->vClasses) );
563     Vec_WecPush( p->vFunNodes, n, nObjs );
564     Vec_IntPushTwo( p->vFanins, FanI, FanJ );
565     Vec_IntPush( p->vTruths, Truth );
566     Vec_IntPush( p->vConfigs, (nNodes << 3) | Type );
567     Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
568     Vec_IntPush( p->vTruthNpns, Min );
569     Vec_IntForEachEntry( vFuncs, Min, i )
570         Dtt_ManSetFun( p, Min );
571     assert( nNodes < 32 );
572     p->Counts[nNodes]++;
573 
574     if ( p->pTable == NULL )
575         return;
576     Truth = Truth & p->CmpMask ? ~Truth : Truth;
577     Truth &= p->FunMask;
578     //assert( p->pNodes[p->pTable[Truth]] == 0 );
579     p->pNodes[p->pTable[Truth]] = n;
580 }
581 
Dtt_PrintStats(int nNodes,int nVars,Vec_Wec_t * vFunNodes,word nSteps,abctime clk,int fDelay,word nMultis)582 int Dtt_PrintStats( int nNodes, int nVars, Vec_Wec_t * vFunNodes, word nSteps, abctime clk, int fDelay, word nMultis )
583 {
584     int nNew = Vec_IntSize(Vec_WecEntry(vFunNodes, nNodes));
585     printf("%c =%2d  |  ",     fDelay ? 'D':'N', nNodes );
586     printf("C =%12.0f  |  ",   (double)(iword)nSteps );
587     printf("New%d =%10d   ",   nVars, nNew + (int)(nNodes==0) );
588     printf("All%d =%10d  |  ", nVars, Vec_WecSizeSize(vFunNodes)+1 );
589     printf("Multi =%10d  |  ", (int)nMultis );
590     Abc_PrintTime( 1, "Time",  Abc_Clock() - clk );
591     //Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
592     fflush(stdout);
593     return nNew;
594 }
Dtt_PrintDistrib(Dtt_Man_t * p)595 void Dtt_PrintDistrib( Dtt_Man_t * p )
596 {
597     int i;
598     printf( "NPN classes for each node count (N):\n" );
599     for ( i = 0; i < 32; i++ )
600         if ( p->Counts[i] )
601             printf( "N = %2d : NPN = %6d\n", i, p->Counts[i] );
602 }
Dtt_PrintMulti2(Dtt_Man_t * p)603 void Dtt_PrintMulti2( Dtt_Man_t * p )
604 {
605     int i, n;
606     for ( n = 0; n <= 7; n++ )
607     {
608         printf( "n=%d : ", n);
609         for ( i = 0; i < p->nClasses; i++ )
610             if ( p->pNodes[i] == n )
611                 printf( "%d ", p->pTimes[i] );
612         printf( "\n" );
613     }
614 }
Dtt_PrintMulti1(Dtt_Man_t * p)615 void Dtt_PrintMulti1( Dtt_Man_t * p )
616 {
617     int i, n, Entry, Count, Prev;
618     for ( n = 0; n < 16; n++ )
619     {
620         Vec_Int_t * vTimes = Vec_IntAlloc( 100 );
621         Vec_Int_t * vUsed  = Vec_IntAlloc( 100 );
622         for ( i = 0; i < p->nClasses; i++ )
623             if ( p->pNodes[i] == n )
624                 Vec_IntPush( vTimes, p->pTimes[i] );
625         if ( Vec_IntSize(vTimes) == 0 )
626         {
627             Vec_IntFree(vTimes);
628             Vec_IntFree(vUsed);
629             break;
630         }
631         Vec_IntSort( vTimes, 0 );
632         Count = 1;
633         Prev = Vec_IntEntry( vTimes, 0 );
634         Vec_IntForEachEntryStart( vTimes, Entry, i, 1 )
635             if ( Prev == Entry )
636                 Count++;
637             else
638             {
639                 assert( Prev < Entry );
640                 Vec_IntPushTwo( vUsed, Prev, Count );
641                 Count = 1;
642                 Prev = Entry;
643             }
644         if ( Count > 0 )
645             Vec_IntPushTwo( vUsed, Prev, Count );
646         printf( "n=%d : ", n);
647         Vec_IntForEachEntryDouble( vUsed, Prev, Entry, i )
648             printf( "%d=%d ", Prev, Entry );
649         printf( "\n" );
650         Vec_IntFree( vTimes );
651         Vec_IntFree( vUsed );
652     }
653 }
Dtt_PrintMulti(Dtt_Man_t * p)654 void Dtt_PrintMulti( Dtt_Man_t * p )
655 {
656     int n, Counts[13][15] = {{0}};
657     for ( n = 0; n < 13; n++ )
658     {
659         int i, Total = 0, Count = 0;
660         for ( i = 0; i < p->nClasses; i++ )
661             if ( p->pNodes[i] == n )
662             {
663                 int Log = Abc_Base2Log(p->pTimes[i]);
664                 assert( Log < 15 );
665                 if ( p->pTimes[i] < 2 )
666                     Counts[n][0]++;
667                 else
668                     Counts[n][Log]++;
669                 Total += p->pTimes[i];
670                 Count++;
671             }
672         if ( Count == 0 )
673             break;
674         printf( "n=%2d : ", n );
675         printf( "All = %7d  ", Count );
676         printf( "Ave = %6.2f  ", 1.0*Total/Count );
677         for ( i = 0; i < 15; i++ )
678             if ( Counts[n][i] )
679                 printf( "%6d", Counts[n][i] );
680             else
681                 printf( "%6s", "" );
682         printf( "\n" );
683     }
684 }
685 
686 /**Function*************************************************************
687 
688   Synopsis    []
689 
690   Description []
691 
692   SideEffects []
693 
694   SeeAlso     []
695 
696 ***********************************************************************/
697 typedef struct Dtt_FunImpl_t_ Dtt_FunImpl_t;
698 struct Dtt_FunImpl_t_
699 {
700     int Type;
701     int NP1;     // 4 bits for an input (NPPP)
702     int FI1;     // the id (in vLibFun) of the first fanin function
703     int NP2;
704     int FI2;     // the id (in vLibFun) of the second fanin function
705 };
706 
Dtt_FunImplFI2Str(int FI,int NP,Vec_Int_t * vLibFun,char * str)707 void Dtt_FunImplFI2Str( int FI, int NP, Vec_Int_t* vLibFun, char* str )
708 {
709     int i, P[5], N[5];
710     for ( i = 0; i < 5; i++ )
711     {
712         P[i] = NP & 0x7;
713         NP = NP >> 3;
714         N[i] = NP & 0x1;
715         NP = NP >> 1 ;
716     }
717     sprintf( str, "[%08x(%03d),%d%d%d%d%d,%d%d%d%d%d]", Vec_IntEntry( vLibFun, FI ), FI, P[0], P[1], P[2], P[3], P[4], N[0], N[1], N[2], N[3], N[4] );
718 }
719 
Dtt_FunImpl2Str(int Type,char * sFI1,char * sFI2,char * str)720 void Dtt_FunImpl2Str( int Type, char* sFI1, char* sFI2, char* str )
721 {
722     // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
723     // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
724     switch( Type )
725     {
726         case 0: sprintf( str, "(%s&%s)", sFI1, sFI2 ); break;
727         case 1: sprintf( str, "(~%s&%s)", sFI1, sFI2 ); break;
728         case 2: sprintf( str, "(%s&~%s)", sFI1, sFI2 ); break;
729         case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break;
730         case 4: sprintf( str, "(%s^%s)", sFI1, sFI2 ); break;
731         case 5: sprintf( str, "~(%s&%s)", sFI1, sFI2 ); break;
732         case 6: sprintf( str, "~(~%s&%s)", sFI1, sFI2 ); break;
733         case 7: sprintf( str, "~(%s&~%s)", sFI1, sFI2 ); break;
734         case 8: sprintf( str, "(~%s&~%s)", sFI1, sFI2 ); break;
735         case 9: sprintf( str, "~(%s^%s)", sFI1, sFI2 ); break;
736         /*case 0: sprintf( str, " ( %s& %s)", sFI1, sFI2 ); break;
737         case 1: sprintf( str, " (~%s& %s)", sFI1, sFI2 ); break;
738         case 2: sprintf( str, " ( %s&~%s)", sFI1, sFI2 ); break;
739         case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break;
740         case 4: sprintf( str, " ( %s^ %s)", sFI1, sFI2 ); break;
741         case 5: sprintf( str, "~( %s& %s)", sFI1, sFI2 ); break;
742         case 6: sprintf( str, "~(~%s& %s)", sFI1, sFI2 ); break;
743         case 7: sprintf( str, "~( %s&~%s)", sFI1, sFI2 ); break;
744         case 8: sprintf( str, " (~%s&~%s)", sFI1, sFI2 ); break;
745         case 9: sprintf( str, "~( %s^ %s)", sFI1, sFI2 ); break;*/
746     }
747 }
748 
Dtt_ComposeNP(int NP1,int NP2)749 int Dtt_ComposeNP( int NP1, int NP2 )
750 {
751     // NP[i] = NP1[NP2[i]]
752     int NP = 0, i;
753     for ( i = 0; i < 5; i++ )
754     {
755         NP |= ( ( NP1 >> ((NP2&0x7)<<2) ) & 0x7 ) << (i<<2); // P'[i] = P1[P2[i]]
756         NP |= ( ( NP1 >> ((NP2&0x7)<<2) ^ NP2 ) & 0x8 ) << (i<<2); // N'[i] = N1[P2[i]] ^ N2[i]
757         NP2 = NP2 >> 4;
758     }
759     return NP;
760 }
761 
Dtt_MakePI(int NP,char * str)762 void Dtt_MakePI( int NP, char* str )
763 {
764     // apply P'[i], find the i s.t. P'[i]==0, correspond to N'[i]
765     int i;
766     for ( i = 0; i < 5; i++ )
767     {
768         if ( ( NP & 0x7 ) == 0 )
769         {
770             if ( NP & 0x8 )
771                 sprintf( str, "~%c", 'a'+i );
772             else
773                 sprintf( str, "%c", 'a'+i );
774             return;
775         }
776         NP = NP >> 4;
777     }
778     assert(0);
779 }
780 
781 void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile );
Dtt_MakeFormulaFI2(unsigned tFun,Dtt_FunImpl_t * pFun,Vec_Vec_t * vLibImpl,int NP,char * sFI1,char * sF,int fPrint,FILE * pFile)782 void Dtt_MakeFormulaFI2( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sFI1, char* sF, int fPrint, FILE* pFile )
783 {
784     int j;
785     Dtt_FunImpl_t* pImpl2;
786     char sFI2[100] = {0}; //sprintf( sFI2, "" );
787 
788     if ( pFun->FI2 == 0 ) // PI
789     {
790         Dtt_MakePI( Dtt_ComposeNP( pFun->NP2, NP ), sFI2 );
791         Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF );
792         if (fPrint)
793             fprintf(pFile, "%08x = %s\n", tFun, sF);
794     }
795     else
796     {
797         Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl2, j, pFun->FI2 )
798         {
799             Dtt_MakeFormula( tFun, pImpl2, vLibImpl, Dtt_ComposeNP( pFun->NP2, NP ), sFI2, 0, pFile );
800             Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF );
801             if (fPrint)
802                 fprintf(pFile, "%08x = %s\n", tFun, sF);
803         }
804     }
805 }
806 
Dtt_MakeFormula(unsigned tFun,Dtt_FunImpl_t * pFun,Vec_Vec_t * vLibImpl,int NP,char * sF,int fPrint,FILE * pFile)807 void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile )
808 {
809     int j;
810     Dtt_FunImpl_t* pImpl1;
811     char sFI1[100], sCopy[100] = {0}; //sprintf( sFI1, "" );
812 
813     if ( pFun->FI1 == 0 ) // PI
814     {
815         Dtt_MakePI( Dtt_ComposeNP( pFun->NP1, NP ), sFI1 );
816         sprintf( sCopy, "%s", sF );
817         Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile );
818     }
819     else
820     {
821         Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl1, j, pFun->FI1 )
822         {
823             Dtt_MakeFormula( tFun, pImpl1, vLibImpl, Dtt_ComposeNP( pFun->NP1, NP ), sFI1, 0, pFile );
824             sprintf( sCopy, "%s", sF );
825             Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile );
826         }
827     }
828 }
829 
Dtt_ProcessType(int * Type,int nFanin)830 void Dtt_ProcessType( int* Type, int nFanin )
831 {
832     // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
833     // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
834     if ( nFanin == 3 ) // for output negation
835         *Type += (*Type<5)? 5: -5;
836     else if ( *Type == 0 || *Type == 5 )
837         *Type += nFanin;
838     else if ( *Type == nFanin ) // 1,1 ; 2,2
839         *Type = 0;
840     else if ( *Type + nFanin == 3 ) // 1,2 ; 2,1
841         *Type = 8;
842     else if ( *Type == 3 )
843         *Type = (nFanin==1)? 7: 6;
844     else if ( *Type == 4 )
845         *Type = 9;
846     else if ( *Type == nFanin+5 ) // 6,1 ; 7,2
847         *Type = 5;
848     else if ( *Type + nFanin == 8 ) // 6,2 ; 7,1
849         *Type = 3;
850     else if ( *Type == 8 )
851         *Type = (nFanin==1)? 2: 1;
852     else if ( *Type == 9 )
853         *Type = 4;
854     else
855         assert( 0 );
856 }
857 
Dtt_Check(unsigned tFun,unsigned tGoal,unsigned tCur,int * pType)858 int Dtt_Check( unsigned tFun, unsigned tGoal, unsigned tCur, int* pType )
859 {
860     if (!tGoal) //for Fanin2 and output
861         return ( tCur == tFun || ~tCur == tFun );
862     //for Fanin1: check if tFun(Type)tCur==tGoal
863     switch (*pType)
864     {
865     // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
866     // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
867         case 0: case 5: if ( (~tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
868                 else return ( (tCur & tFun) == tGoal );
869         case 1: case 6: if ( (tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
870                 else return ( (~tCur & tFun) == tGoal );
871         case 2: case 7: if ( (~tCur & ~tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
872                 else return ( (tCur & ~tFun) == tGoal );
873         case 3: case 8: if ( (~tCur | tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
874                 else return ( (tCur | tFun) == tGoal );
875         case 4: case 9: if ( (~tCur ^ tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
876                 else return ( (tCur ^ tFun) == tGoal );
877         default: assert(0);
878     }
879     return -1;
880 }
881 
Dtt_FindNP(Dtt_Man_t * p,unsigned tFun,unsigned tGoal,unsigned tNpn,int * NP,int * pType,int NPout)882 void Dtt_FindNP( Dtt_Man_t * p, unsigned tFun, unsigned tGoal, unsigned tNpn, int * NP, int* pType, int NPout )
883 {
884     int i, k, j;
885     int P[5] = { 0, 1, 2, 3, 4 };
886     int N[5] = { 0, 0, 0, 0, 0 };
887     int temp;
888 
889     word tCur = ((word)tNpn << 32) | (word)tNpn;
890     for ( i = 0; i < p->nPerms; i++ )
891     {
892         for ( k = 0; k < p->nComps; k++ )
893         {
894             if ( Dtt_Check( tFun, tGoal, (unsigned)tCur, pType ))
895             {
896                 if ( !tGoal && ( tFun == (unsigned)~tCur ) ) // !tGoal: not FI1
897                 {
898                     if (!NPout) Dtt_ProcessType( pType, 3 );
899                     else Dtt_ProcessType( pType, 2 );
900                 }
901                 *NP = 0;
902                 if (!NPout)
903                 {
904                     for ( j = 0; j < 5; j++ )
905                         *NP |= ( ( ( N[j] & 0x1 ) << 3 ) | ( P[j] & 0x7 ) ) << (j<<2) ;
906                 }
907                 else
908                 {
909                     for ( j = 0; j < 5; j++ )
910                     {
911                         *NP |= P[NPout&0x7] << (j<<2); // P'[j] = P[Pout[j]]
912                         *NP |= ( N[NPout&0x7] ^ ( (NPout>>3) & 0x1 )) << (j<<2) << 3; // N'[i] = N1[P2[i]] ^ N2[i]
913                         NPout = NPout >> 4;
914                     }
915                 }
916 
917                 return;
918             }
919             tCur = Abc_Tt6Flip( tCur, p->pComps[k] );
920             N[p->pComps[k]] ^= 0x1;
921         }
922         tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] );
923         temp = P[p->pPerms[i]]; P[p->pPerms[i]] = P[p->pPerms[i]+1]; P[p->pPerms[i]+1] = temp;
924     }
925     assert(0);
926 }
927 
Dtt_DumpLibrary(Dtt_Man_t * p,char * FileName)928 void Dtt_DumpLibrary( Dtt_Man_t * p, char* FileName )
929 {
930     FILE * pFile;
931     char str[100], sFI1[50], sFI2[50];
932     int i, j, Entry, fRepeat;
933     Dtt_FunImpl_t * pFun, * pFun2;
934     Vec_Int_t * vLibFun = Vec_IntDup( p->vTruthNpns );  // none-duplicating vector of NPN representitives
935     Vec_Vec_t * vLibImpl;
936     Vec_IntUniqify( vLibFun );
937     vLibImpl = Vec_VecStart( Vec_IntSize( vLibFun ) );
938     Vec_IntForEachEntry( p->vTruths, Entry, i )
939     {
940         int NP, Fanin2, Fanin1Npn, Fanin2Npn;
941         if (i<2) continue; // skip const 0
942         pFun = ABC_CALLOC( Dtt_FunImpl_t, 1 );
943         pFun->Type = (int)( 0x7 & Vec_IntEntry(p->vConfigs, i) );
944         //word Fanin1 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2 ) );
945         Fanin2 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2+1 ) );
946         Fanin1Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2 ) );
947         Fanin2Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2+1 ) );
948         pFun->FI1 = Vec_IntFind( vLibFun, Fanin1Npn );
949         pFun->FI2 = Vec_IntFind( vLibFun, Fanin2Npn );
950 
951         fRepeat = 0;
952         Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun2, j, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ) )
953         {
954             if ( ( pFun2->FI1 == pFun->FI1 && pFun2->FI2 == pFun->FI2 ) || ( pFun2->FI2 == pFun->FI1 && pFun2->FI1 == pFun->FI2 ) )
955             {
956                 fRepeat = 1;
957                 break;
958             }
959         }
960         if (fRepeat)
961         {
962             ABC_FREE( pFun );
963             continue;
964         }
965 
966         Dtt_FindNP( p, Vec_IntEntry( p->vTruthNpns, i ), 0, Entry, &NP, &(pFun->Type), 0 ); //out: tGoal=0, NPout=0
967         Dtt_FindNP( p, Fanin2, Entry, Fanin1Npn, &(pFun->NP1), &(pFun->Type), NP ); //FI1
968         Dtt_FindNP( p, Fanin2, 0, Fanin2Npn, &(pFun->NP2), &(pFun->Type), NP ); //FI2: tGoal=0
969 
970         Vec_VecPush( vLibImpl, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ), pFun );
971     }
972 
973     // print to file
974     pFile = fopen( FileName, "wb" );
975 
976     if (0)
977     Vec_IntForEachEntry( vLibFun, Entry, i )
978     {
979         if (!Entry) continue; // skip const 0
980         fprintf( pFile, "%08x: ", (unsigned)Entry );
981         Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i )
982         {
983             Dtt_FunImplFI2Str( pFun->FI1, pFun->NP1, vLibFun, sFI1 );
984             Dtt_FunImplFI2Str( pFun->FI2, pFun->NP2, vLibFun, sFI2 );
985             Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, str );
986             fprintf( pFile, "%s, ", str );
987         }
988         fprintf( pFile, "\n" );
989     }
990 
991     // formula format
992     Vec_IntForEachEntry( vLibFun, Entry, i )
993     {
994         if ( i<2 ) continue; // skip const 0 and buffer
995         Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i )
996         {
997             str[0] = 0; //sprintf( str, "" );
998             Dtt_MakeFormula( (unsigned)Entry, pFun, vLibImpl, (4<<16)+(3<<12)+(2<<8)+(1<<4), str, 1, pFile );
999         }
1000     }
1001 
1002     fclose( pFile );
1003     printf( "Dumped file \"%s\". \n", FileName );
1004     fflush( stdout );
1005 }
1006 
Dtt_EnumerateLf(int nVars,int nNodeMax,int fDelay,int fMulti,int fVerbose,char * pFileName)1007 void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose, char* pFileName )
1008 {
1009     abctime clk = Abc_Clock(); word nSteps = 0, nMultis = 0;
1010     Dtt_Man_t * p = Dtt_ManAlloc( nVars, fMulti ); int n, i, j;
1011 
1012     // constant zero class
1013     Vec_IntPushTwo( p->vFanins, 0, 0 );
1014     Vec_IntPush( p->vTruths, 0 );
1015     Vec_IntPush( p->vConfigs, 0 );
1016     Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
1017     Vec_IntPush( p->vTruthNpns, 0 );
1018     Dtt_ManSetFun( p, 0 );
1019     // buffer class
1020     Vec_WecPush( p->vFunNodes, 0, Vec_IntSize(p->vFanins)/2 );
1021     Vec_IntPushTwo( p->vFanins, 0, 0 );
1022     Vec_IntPush( p->vTruths, (unsigned)s_Truths6[0] );
1023     Vec_IntPush( p->vConfigs, 0 );
1024     Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
1025     Vec_IntPush( p->vTruthNpns, (unsigned)s_Truths6[0] );
1026     for ( i = 0; i < nVars; i++ )
1027         Dtt_ManSetFun( p, (unsigned)s_Truths6[i] );
1028     p->Counts[0] = 2;
1029     // enumerate
1030     Dtt_PrintStats(0, nVars, p->vFunNodes, nSteps, clk, fDelay, 0);
1031     for ( n = 1; n <= nNodeMax; n++ )
1032     {
1033         for ( i = 0, j = n - 1; i < n; i++, j = j - 1 + fDelay ) if ( i <= j )
1034         {
1035             Vec_Int_t * vFaninI = Vec_WecEntry( p->vFunNodes, i );
1036             Vec_Int_t * vFaninJ = Vec_WecEntry( p->vFunNodes, j );
1037             int k, i0, j0, EntryI, EntryJ;
1038             Vec_IntForEachEntry( vFaninI, EntryI, i0 )
1039             {
1040                 unsigned TruthI = Vec_IntEntry(p->vTruths, EntryI);
1041                 Vec_Int_t * vFuns = Dtt_ManCollect( p, TruthI, p->vTemp );
1042                 int Start = i == j ? i0 : 0;
1043                 Vec_IntForEachEntryStart( vFaninJ, EntryJ, j0, Start )
1044                 {
1045                     unsigned Truth, TruthJ = Vec_IntEntry(p->vTruths, EntryJ);
1046                     Vec_IntForEachEntry( vFuns, Truth, k )
1047                     {
1048                         if ( !Dtt_ManGetFun(p,  TruthJ &  Truth, n) )
1049                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 0,  TruthJ &  Truth );
1050                         if ( !Dtt_ManGetFun(p,  TruthJ & ~Truth, n) )
1051                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 1,  TruthJ & ~Truth );
1052                         if ( !Dtt_ManGetFun(p, ~TruthJ &  Truth, n) )
1053                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 2, ~TruthJ &  Truth );
1054                         if ( !Dtt_ManGetFun(p,  TruthJ |  Truth, n) )
1055                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 3,  TruthJ |  Truth );
1056                         if ( !Dtt_ManGetFun(p,  TruthJ ^  Truth, n) )
1057                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 4,  TruthJ ^  Truth );
1058                         nSteps += 5;
1059 
1060                         if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ &  Truth, n );
1061                         if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ & ~Truth, n );
1062                         if ( p->pTable ) Dtt_ManAddVisited( p, ~TruthJ &  Truth, n );
1063                         if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ |  Truth, n );
1064                         if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ ^  Truth, n );
1065                     }
1066                     nMultis++;
1067                     if ( p->pTable ) Dtt_ManProcessVisited( p );
1068                 }
1069             }
1070         }
1071         if ( Dtt_PrintStats(n, nVars, p->vFunNodes, nSteps, clk, fDelay, nMultis) == 0 )
1072             break;
1073     }
1074     if ( fDelay )
1075         Dtt_PrintDistrib( p );
1076     //if ( p->pTable )
1077         //Dtt_PrintMulti( p );
1078     if ( !fDelay && pFileName!=NULL )
1079         Dtt_DumpLibrary( p, pFileName );
1080     Dtt_ManFree( p );
1081 }
1082 
1083 ////////////////////////////////////////////////////////////////////////
1084 ///                       END OF FILE                                ///
1085 ////////////////////////////////////////////////////////////////////////
1086 
1087 ABC_NAMESPACE_IMPL_END
1088 
1089