ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dauNpn2.c
Go to the documentation of this file.
1
20
21#include "dauInt.h"
22#include "misc/util/utilTruth.h"
23#include "misc/extra/extra.h"
24#include "aig/gia/gia.h"
25
26ABC_NAMESPACE_IMPL_START
27
31
32typedef struct Dtt_Man_t_ Dtt_Man_t;
33struct 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
66
78char * 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}
96word 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}
141word Dau_ParseFormula( char * p )
142{
143 return Dau_ParseFormula_rec( p, p + strlen(p) );
144}
145void 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
165int 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}
210int Dau_ParseFormulaAig( Gia_Man_t * p, char * pStr )
211{
212 return Dau_ParseFormulaAig_rec( p, pStr, pStr + strlen(pStr) );
213}
214Gia_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
239void 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}
259void Dau_VerifyFileTest()
260{
261 char * pFileName = "lib4var.txt";
262 Dau_VerifyFile( pFileName );
263}
264
265
277Gia_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
311unsigned * 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}
331void 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}
345unsigned * 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
374void 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}
387void 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
410Dtt_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}
440void 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
474static 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}
480int 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}
491Vec_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
528static 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}
546static 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}
552void 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
582int 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}
595void 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}
603void 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}
615void 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}
654void 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
697typedef struct Dtt_FunImpl_t_ Dtt_FunImpl_t;
698struct 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
707void 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
720void 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
749int 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
762void 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
781void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile );
782void 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
807void 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
830void 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
858int 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
882void 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
928void 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
1007void 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
1086
1087ABC_NAMESPACE_IMPL_END
1088
iword
ABC_INT64_T iword
Definition abc_global.h:244
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Dau_ParseFormulaAigTest
Gia_Man_t * Dau_ParseFormulaAigTest()
Definition dauNpn2.c:214
Dau_ParseFormula_rec
word Dau_ParseFormula_rec(char *pBeg, char *pEnd)
Definition dauNpn2.c:96
Dau_ReadFile2
unsigned * Dau_ReadFile2(char *pFileName, int nSizeW)
Definition dauNpn2.c:311
Dtt_EnumerateLf
void Dtt_EnumerateLf(int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose, char *pFileName)
Definition dauNpn2.c:1007
Dtt_ManRenum
void Dtt_ManRenum(int nVars, unsigned *pTable, int *pnClasses)
Definition dauNpn2.c:331
Dtt_PrintMulti
void Dtt_PrintMulti(Dtt_Man_t *p)
Definition dauNpn2.c:654
Dtt_FunImplFI2Str
void Dtt_FunImplFI2Str(int FI, int NP, Vec_Int_t *vLibFun, char *str)
Definition dauNpn2.c:707
Dtt_ManAddVisited
void Dtt_ManAddVisited(Dtt_Man_t *p, unsigned Truth2, int n)
Definition dauNpn2.c:374
Dau_ParseFormulaAig
int Dau_ParseFormulaAig(Gia_Man_t *p, char *pStr)
Definition dauNpn2.c:210
Dtt_Check
int Dtt_Check(unsigned tFun, unsigned tGoal, unsigned tCur, int *pType)
Definition dauNpn2.c:858
Dtt_ComposeNP
int Dtt_ComposeNP(int NP1, int NP2)
Definition dauNpn2.c:749
Dau_VerifyFile
void Dau_VerifyFile(char *pFileName)
Definition dauNpn2.c:239
Dtt_ManAlloc
Dtt_Man_t * Dtt_ManAlloc(int nVars, int fMulti)
Definition dauNpn2.c:410
Dtt_ManLoadClasses
unsigned * Dtt_ManLoadClasses(int nVars, int *pnClasses)
Definition dauNpn2.c:345
Dtt_FunImpl2Str
void Dtt_FunImpl2Str(int Type, char *sFI1, char *sFI2, char *str)
Definition dauNpn2.c:720
Dtt_FunImpl_t
struct Dtt_FunImpl_t_ Dtt_FunImpl_t
Definition dauNpn2.c:697
Dau_VerifyFileTest
void Dau_VerifyFileTest()
Definition dauNpn2.c:259
Dau_ParseFormulaAig_rec
int Dau_ParseFormulaAig_rec(Gia_Man_t *p, char *pBeg, char *pEnd)
Definition dauNpn2.c:165
Dtt_PrintStats
int Dtt_PrintStats(int nNodes, int nVars, Vec_Wec_t *vFunNodes, word nSteps, abctime clk, int fDelay, word nMultis)
Definition dauNpn2.c:582
Dau_ParseFormulaEndToken
char * Dau_ParseFormulaEndToken(char *pForm)
FUNCTION DEFINITIONS ///.
Definition dauNpn2.c:78
Dtt_ManCheckHash
int Dtt_ManCheckHash(Dtt_Man_t *p, unsigned Truth)
Definition dauNpn2.c:480
Dtt_MakePI
void Dtt_MakePI(int NP, char *str)
Definition dauNpn2.c:762
Dtt_ProcessType
void Dtt_ProcessType(int *Type, int nFanin)
Definition dauNpn2.c:830
Dtt_PrintMulti1
void Dtt_PrintMulti1(Dtt_Man_t *p)
Definition dauNpn2.c:615
Dtt_MakeFormulaFI2
void Dtt_MakeFormulaFI2(unsigned tFun, Dtt_FunImpl_t *pFun, Vec_Vec_t *vLibImpl, int NP, char *sFI1, char *sF, int fPrint, FILE *pFile)
Definition dauNpn2.c:782
Dtt_DumpLibrary
void Dtt_DumpLibrary(Dtt_Man_t *p, char *FileName)
Definition dauNpn2.c:928
Dtt_ManAddFunction
void Dtt_ManAddFunction(Dtt_Man_t *p, int n, int FanI, int FanJ, int Type, unsigned Truth)
Definition dauNpn2.c:552
Dtt_Man_t
typedefABC_NAMESPACE_IMPL_START struct Dtt_Man_t_ Dtt_Man_t
DECLARATIONS ///.
Definition dauNpn2.c:32
Dtt_ManProcessVisited
void Dtt_ManProcessVisited(Dtt_Man_t *p)
Definition dauNpn2.c:387
Dtt_ManFree
void Dtt_ManFree(Dtt_Man_t *p)
Definition dauNpn2.c:440
Dtt_MakeFormula
void Dtt_MakeFormula(unsigned tFun, Dtt_FunImpl_t *pFun, Vec_Vec_t *vLibImpl, int NP, char *sF, int fPrint, FILE *pFile)
Definition dauNpn2.c:807
Dtt_PrintMulti2
void Dtt_PrintMulti2(Dtt_Man_t *p)
Definition dauNpn2.c:603
Dtt_PrintDistrib
void Dtt_PrintDistrib(Dtt_Man_t *p)
Definition dauNpn2.c:595
Dau_ParseFormulaTest
void Dau_ParseFormulaTest()
Definition dauNpn2.c:145
Dtt_FindNP
void Dtt_FindNP(Dtt_Man_t *p, unsigned tFun, unsigned tGoal, unsigned tNpn, int *NP, int *pType, int NPout)
Definition dauNpn2.c:882
Dtt_ManCollect
Vec_Int_t * Dtt_ManCollect(Dtt_Man_t *p, unsigned Truth, Vec_Int_t *vFuns)
Definition dauNpn2.c:491
Dau_ConstructAigFromFile
Gia_Man_t * Dau_ConstructAigFromFile(char *pFileName)
Definition dauNpn2.c:277
Dau_ParseFormula
word Dau_ParseFormula(char *p)
Definition dauNpn2.c:141
Dau_TruthEnum
ABC_NAMESPACE_IMPL_START void Dau_TruthEnum(int nVars)
DECLARATIONS ///.
Definition dauNpn.c:48
p
Cube * p
Definition exorList.c:222
Extra_PermSchedule
int * Extra_PermSchedule(int n)
Definition extraUtilMisc.c:2206
Extra_ReadHexadecimal
int Extra_ReadHexadecimal(unsigned Sign[], char *pString, int nVars)
Definition extraUtilFile.c:559
Extra_Factorial
int Extra_Factorial(int n)
Definition extraUtilMisc.c:217
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition extraUtilMisc.c:2170
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:668
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Dtt_FunImpl_t_
Definition dauNpn2.c:699
Dtt_FunImpl_t_::NP2
int NP2
Definition dauNpn2.c:703
Dtt_FunImpl_t_::FI2
int FI2
Definition dauNpn2.c:704
Dtt_FunImpl_t_::NP1
int NP1
Definition dauNpn2.c:701
Dtt_FunImpl_t_::Type
int Type
Definition dauNpn2.c:700
Dtt_FunImpl_t_::FI1
int FI1
Definition dauNpn2.c:702
Dtt_Man_t_
Definition dauNpn2.c:34
Dtt_Man_t_::pTable
unsigned * pTable
Definition dauNpn2.c:56
Dtt_Man_t_::CmpMask
unsigned CmpMask
Definition dauNpn2.c:50
Dtt_Man_t_::vConfigs
Vec_Int_t * vConfigs
Definition dauNpn2.c:43
Dtt_Man_t_::pNodes
int * pNodes
Definition dauNpn2.c:57
Dtt_Man_t_::pBins
unsigned * pBins
Definition dauNpn2.c:52
Dtt_Man_t_::Counts
int Counts[32]
Definition dauNpn2.c:54
Dtt_Man_t_::pComps
int * pComps
Definition dauNpn2.c:39
Dtt_Man_t_::nClasses
int nClasses
Definition dauNpn2.c:55
Dtt_Man_t_::vFanins
Vec_Int_t * vFanins
Definition dauNpn2.c:41
Dtt_Man_t_::vTemp2
Vec_Int_t * vTemp2
Definition dauNpn2.c:48
Dtt_Man_t_::FunMask
unsigned FunMask
Definition dauNpn2.c:49
Dtt_Man_t_::vTemp
Vec_Int_t * vTemp
Definition dauNpn2.c:47
Dtt_Man_t_::pTimes
int * pTimes
Definition dauNpn2.c:58
Dtt_Man_t_::BinMask
unsigned BinMask
Definition dauNpn2.c:51
Dtt_Man_t_::vTruthNpns
Vec_Int_t * vTruthNpns
Definition dauNpn2.c:45
Dtt_Man_t_::nComps
int nComps
Definition dauNpn2.c:37
Dtt_Man_t_::pPerms
int * pPerms
Definition dauNpn2.c:38
Dtt_Man_t_::pPres
word * pPres
Definition dauNpn2.c:40
Dtt_Man_t_::vUsedBins
Vec_Int_t * vUsedBins
Definition dauNpn2.c:53
Dtt_Man_t_::vFunNodes
Vec_Wec_t * vFunNodes
Definition dauNpn2.c:46
Dtt_Man_t_::vTruths
Vec_Int_t * vTruths
Definition dauNpn2.c:42
Dtt_Man_t_::vClasses
Vec_Int_t * vClasses
Definition dauNpn2.c:44
Dtt_Man_t_::vVisited
Vec_Int_t * vVisited
Definition dauNpn2.c:60
Dtt_Man_t_::nVars
int nVars
Definition dauNpn2.c:35
Dtt_Man_t_::pVisited
char * pVisited
Definition dauNpn2.c:59
Dtt_Man_t_::nPerms
int nPerms
Definition dauNpn2.c:36
assert
#define assert(ex)
Definition util_old.h:213
strlen
int strlen()
sprintf
char * sprintf()
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_VecForEachEntryLevel
#define Vec_VecForEachEntryLevel(Type, vGlob, pEntry, i, Level)
Definition vecVec.h:90
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42