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