ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dauNpn.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 "bool/lucky/lucky.h"
25
26ABC_NAMESPACE_IMPL_START
27
31
32
36
48void Dau_TruthEnum(int nVars)
49{
50 int fUseTable = 1;
51 abctime clk = Abc_Clock();
52 int nSizeLog = (1<<nVars) -2;
53 int nSizeW = 1 << nSizeLog;
54 int nPerms = Extra_Factorial( nVars );
55 int nMints = 1 << nVars;
56 int * pPerm = Extra_PermSchedule( nVars );
57 int * pComp = Extra_GreyCodeSchedule( nVars );
58 word nFuncs = ((word)1 << (((word)1 << nVars)-1));
59 word * pPres = ABC_CALLOC( word, 1 << ((1<<nVars)-7) );
60 unsigned * pTable = fUseTable ? (unsigned *)ABC_CALLOC(word, nSizeW) : NULL;
61 Vec_Int_t * vNpns = Vec_IntAlloc( 1000 );
62 word tMask = Abc_Tt6Mask( 1 << nVars );
63 word tTemp, tCur;
64 int i, k;
65 if ( pPres == NULL )
66 {
67 printf( "Cannot alloc memory for marks.\n" );
68 return;
69 }
70 if ( pTable == NULL )
71 printf( "Cannot alloc memory for table.\n" );
72 for ( tCur = 0; tCur < nFuncs; tCur++ )
73 {
74 if ( (tCur & 0x3FFFF) == 0 )
75 {
76 printf( "Finished %08x. Classes = %6d. ", (int)tCur, Vec_IntSize(vNpns) );
77 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
78 fflush(stdout);
79 }
80 if ( Abc_TtGetBit(pPres, (int)tCur) )
81 continue;
82 //Extra_PrintBinary( stdout, (unsigned *)&tCur, 16 ); printf( " %04x\n", (int)tCur );
83 //Dau_DsdPrintFromTruth( &tCur, 4 ); printf( "\n" );
84 Vec_IntPush( vNpns, (int)tCur );
85 tTemp = tCur;
86 for ( i = 0; i < nPerms; i++ )
87 {
88 for ( k = 0; k < nMints; k++ )
89 {
90 if ( tCur < nFuncs )
91 {
92 if ( pTable ) pTable[(int)tCur] = tTemp;
93 Abc_TtSetBit( pPres, (int)tCur );
94 }
95 if ( (tMask & ~tCur) < nFuncs )
96 {
97 if ( pTable ) pTable[(int)(tMask & ~tCur)] = tTemp;
98 Abc_TtSetBit( pPres, (int)(tMask & ~tCur) );
99 }
100 tCur = Abc_Tt6Flip( tCur, pComp[k] );
101 }
102 tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[i] );
103 }
104 assert( tTemp == tCur );
105 }
106 printf( "Computed %d NPN classes of %d variables. ", Vec_IntSize(vNpns), nVars );
107 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
108 fflush(stdout);
109 Vec_IntFree( vNpns );
110 ABC_FREE( pPres );
111 ABC_FREE( pPerm );
112 ABC_FREE( pComp );
113 // write into file
114 if ( pTable )
115 {
116 FILE * pFile;
117 int RetValue;
118 char pFileName[200];
119 sprintf( pFileName, "tableW%d.data", nSizeLog );
120 pFile = fopen( pFileName, "wb" );
121 RetValue = fwrite( pTable, 8, nSizeW, pFile );
122 RetValue = 0;
123 fclose( pFile );
124 ABC_FREE( pTable );
125 }
126}
127
128
140unsigned * Dau_ReadFile( char * pFileName, int nSizeW )
141{
142 abctime clk = Abc_Clock();
143 FILE * pFile = fopen( pFileName, "rb" );
144 unsigned * p = (unsigned *)ABC_CALLOC(word, nSizeW);
145 int RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
146 RetValue = 0;
147 if ( pFile )
148 {
149 printf( "Finished reading file \"%s\".\n", pFileName );
150 fclose( pFile );
151 }
152 else
153 printf( "Cannot open input file \"%s\".\n", pFileName );
154 Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
155 return p;
156}
157int Dau_AddFunction( word tCur, int nVars, unsigned * pTable, Vec_Int_t * vNpns, Vec_Int_t * vNpns_ )
158{
159 int Digit = (1 << nVars)-1;
160 word tMask = Abc_Tt6Mask( 1 << nVars );
161 word tNorm = (tCur >> Digit) & 1 ? ~tCur : tCur;
162 unsigned t = (unsigned)(tNorm & tMask);
163 unsigned tRep = pTable[t] & 0x7FFFFFFF;
164 unsigned tRep2 = pTable[tRep];
165 assert( ((tNorm >> Digit) & 1) == 0 );
166 if ( (tRep2 >> 31) == 0 ) // first time
167 {
168 Vec_IntPush( vNpns, tRep2 );
169 if ( Abc_TtSupportSize(&tCur, nVars) < nVars )
170 Vec_IntPush( vNpns_, tRep2 );
171 pTable[tRep] = tRep2 | (1 << 31);
172 return tRep2;
173 }
174 return 0;
175}
176void Dau_NetworkEnum(int nVars)
177{
178 abctime clk = Abc_Clock();
179 int Limit = 2;
180 int UseTwo = 0;
181 int nSizeLog = (1<<nVars) -2;
182 int nSizeW = 1 << nSizeLog;
183 char pFileName[200];
184 unsigned * pTable;
185 Vec_Wec_t * vNpns = Vec_WecStart( 32 );
186 Vec_Wec_t * vNpns_ = Vec_WecStart( 32 );
187 int i, v, u, g, k, m, n, Res, Entry;
188 unsigned Inv = (unsigned)Abc_Tt6Mask(1 << (nVars-1));
189 sprintf( pFileName, "tableW%d.data", nSizeLog );
190 pTable = Dau_ReadFile( pFileName, nSizeW );
191 // create constant function and buffer/inverter function
192 pTable[0] |= (1 << 31);
193 pTable[Inv] |= (1 << 31);
194 Vec_IntPushTwo( Vec_WecEntry(vNpns, 0), 0, Inv );
195 Vec_IntPushTwo( Vec_WecEntry(vNpns_, 0), 0, Inv );
196 printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
197 0, Vec_IntSize(Vec_WecEntry(vNpns, 0)), Vec_WecSizeSize(vNpns),
198 Vec_IntSize(Vec_WecEntry(vNpns_, 0)), Vec_WecSizeSize(vNpns_) );
199 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
200 // numerate other functions based on how many nodes they have
201 for ( n = 1; n < 32; n++ )
202 {
203 Vec_Int_t * vFuncsN2 = n > 1 ? Vec_WecEntry( vNpns, n-2 ) : NULL;
204 Vec_Int_t * vFuncsN1 = Vec_WecEntry( vNpns, n-1 );
205 Vec_Int_t * vFuncsN = Vec_WecEntry( vNpns, n );
206 Vec_Int_t * vFuncsN_ = Vec_WecEntry( vNpns_,n );
207 Vec_IntForEachEntry( vFuncsN1, Entry, i )
208 {
209 word uTruth = (((word)Entry) << 32) | (word)Entry;
210 int nSupp = Abc_TtSupportSize( &uTruth, nVars );
211 assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
212 //printf( "Exploring function %4d with %d vars: ", i, nSupp );
213 //printf( " %04x\n", (int)uTruth );
214 //Dau_DsdPrintFromTruth( &uTruth, 4 );
215 for ( v = 0; v < nSupp; v++ )
216 {
217 word tGate, tCur;
218 word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
219 word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
220 for ( g = 0; g < Limit; g++ )
221 {
222 if ( nSupp < nVars )
223 {
224 if ( g == 0 )
225 {
226 tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-nSupp];
227 tCur = (tGate & Cof1) | (~tGate & Cof0);
228 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
229
230 tCur = (tGate & Cof0) | (~tGate & Cof1);
231 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
232 }
233 else
234 {
235 tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-nSupp];
236 tCur = (tGate & Cof1) | (~tGate & Cof0);
237 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
238 }
239 }
240 }
241 for ( g = 0; g < Limit; g++ )
242 {
243 // add one cross bar
244 for ( k = 0; k < nSupp; k++ ) if ( k != v )
245 {
246 if ( g == 0 )
247 {
248 tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-k];
249 tCur = (tGate & Cof1) | (~tGate & Cof0);
250 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
251
252 tCur = (tGate & Cof0) | (~tGate & Cof1);
253 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
254
255 tGate = s_Truths6[nVars-1-v] & ~s_Truths6[nVars-1-k];
256 tCur = (tGate & Cof1) | (~tGate & Cof0);
257 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
258
259 tCur = (tGate & Cof0) | (~tGate & Cof1);
260 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
261 }
262 else
263 {
264 tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-k];
265 tCur = (tGate & Cof1) | (~tGate & Cof0);
266 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
267 }
268 }
269 }
270 for ( g = 0; g < Limit; g++ )
271 {
272 // add two cross bars
273 for ( k = 0; k < nSupp; k++ ) if ( k != v )
274 for ( m = k+1; m < nSupp; m++ ) if ( m != v )
275 {
276 if ( g == 0 )
277 {
278 tGate = s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
279 tCur = (tGate & Cof1) | (~tGate & Cof0);
280 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
281
282 tCur = (tGate & Cof0) | (~tGate & Cof1);
283 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
284
285 tGate = s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
286 tCur = (tGate & Cof1) | (~tGate & Cof0);
287 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
288
289 tCur = (tGate & Cof0) | (~tGate & Cof1);
290 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
291
292 tGate = ~s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
293 tCur = (tGate & Cof1) | (~tGate & Cof0);
294 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
295
296 tCur = (tGate & Cof0) | (~tGate & Cof1);
297 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
298
299 tGate = ~s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
300 tCur = (tGate & Cof1) | (~tGate & Cof0);
301 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
302
303 tCur = (tGate & Cof0) | (~tGate & Cof1);
304 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
305 }
306 else
307 {
308 tGate = s_Truths6[nVars-1-m] ^ s_Truths6[nVars-1-k];
309 tCur = (tGate & Cof1) | (~tGate & Cof0);
310 Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
311 }
312 }
313 }
314 }
315 }
316 if ( UseTwo && vFuncsN2 )
317 Vec_IntForEachEntry( vFuncsN2, Entry, i )
318 {
319 word uTruth = (((word)Entry) << 32) | (word)Entry;
320 int nSupp = Abc_TtSupportSize( &uTruth, nVars );
321 assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
322 //printf( "Exploring function %4d with %d vars: ", i, nSupp );
323 //printf( " %04x\n", (int)uTruth );
324 //Dau_DsdPrintFromTruth( &uTruth, 4 );
325 for ( v = 0; v < nSupp; v++ )
326// for ( u = v+1; u < nSupp; u++ ) if ( u != v )
327 for ( u = 0; u < nSupp; u++ ) if ( u != v )
328 {
329 word tGate1, tGate2, tCur;
330 word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
331 word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
332
333 word Cof00 = Abc_Tt6Cofactor0( Cof0, nVars-1-u );
334 word Cof01 = Abc_Tt6Cofactor1( Cof0, nVars-1-u );
335 word Cof10 = Abc_Tt6Cofactor0( Cof1, nVars-1-u );
336 word Cof11 = Abc_Tt6Cofactor1( Cof1, nVars-1-u );
337
338 tGate1 = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-u];
339 tGate2 = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-u];
340
341 Cof0 = (tGate2 & Cof00) | (~tGate2 & Cof01);
342 Cof1 = (tGate2 & Cof10) | (~tGate2 & Cof11);
343
344 tCur = (tGate1 & Cof1) | (~tGate1 & Cof0);
345 Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
346 if ( Res )
347 printf( "Found function %d\n", Res );
348
349 tCur = (tGate1 & Cof0) | (~tGate1 & Cof1);
350 Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
351 if ( Res )
352 printf( "Found function %d\n", Res );
353 }
354 }
355 printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
356 n, Vec_IntSize(vFuncsN), Vec_WecSizeSize(vNpns), Vec_IntSize(vFuncsN_), Vec_WecSizeSize(vNpns_) );
357 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
358 fflush(stdout);
359 if ( Vec_IntSize(vFuncsN) == 0 )
360 break;
361 }
362// printf( "Functions with 7 nodes:\n" );
363// Vec_IntForEachEntry( Vec_WecEntry(vNpns_,7), Entry, i )
364// printf( "%04x ", Entry );
365// printf( "\n" );
366
367 Vec_WecFree( vNpns );
368 Vec_WecFree( vNpns_ );
369 ABC_FREE( pTable );
370 Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
371 fflush(stdout);
372}
373void Dau_NetworkEnumTest()
374{
375 //Dau_TruthEnum(3);
376 Dau_NetworkEnum(4);
377}
378
379
380
392int Dau_CountSymms( word t, int nVars )
393{
394 word Cof0, Cof1;
395 int i, j, nPairs = 0;
396 for ( i = 0; i < nVars; i++ )
397 for ( j = i+1; j < nVars; j++ )
398 nPairs += Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1);
399 return nPairs;
400}
401int Dau_CountSymms2( word t, int nVars )
402{
403 word Cof0, Cof1;
404 int i, j, SymVars = 0;
405 for ( i = 0; i < nVars; i++ )
406 for ( j = i+1; j < nVars; j++ )
407 if ( Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1) )
408 SymVars |= (1 << j);
409 return SymVars;
410}
411int Dau_CountCompl1( word t, int v, int nVars )
412{
413 word tNew = Abc_Tt6Flip(t, v);
414 int k;
415 if ( tNew == ~t )
416 return 1;
417 for ( k = 0; k < nVars; k++ ) if ( k != v )
418 if ( tNew == Abc_Tt6Flip(t, k) )
419 return 1;
420 return 0;
421}
422int Dau_CountCompl( word t, int nVars )
423{
424 int i, nPairs = 0;
425 for ( i = 0; i < nVars; i++ )
426 nPairs += Dau_CountCompl1(t, i, nVars);
427 return nPairs;
428}
429
441Vec_Wrd_t * Dau_ExactNpnForClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs )
442{
443 Vec_Wrd_t * vCanons = Vec_WrdStart( Vec_IntSize(vNodSup) );
444 word pAuxWord[1024], pAuxWord1[1024];
445 word uTruth; int i, Entry;
446 permInfo * pi = setPermInfoPtr(nVars);
447 Vec_IntForEachEntry( vNodSup, Entry, i )
448 {
449 if ( (Entry & 0xF) > nVars )
450 continue;
451 uTruth = *Vec_MemReadEntry( vTtMem, i );
452 simpleMinimal(&uTruth, pAuxWord, pAuxWord1, pi, nVars);
453 Vec_WrdWriteEntry( vCanons, i, uTruth );
454 }
455 freePermInfoPtr(pi);
456 return vCanons;
457}
458void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs, int nNodesMax )
459{
460 abctime clk = Abc_Clock(); int n, nTotal = 0;
461 Vec_Wrd_t * vCanons = Dau_ExactNpnForClasses( vTtMem, vNodSup, nVars, nInputs );
462 Vec_Mem_t * vTtMem2 = Vec_MemAlloc( Vec_MemEntrySize(vTtMem), 10 );
463 Vec_MemHashAlloc( vTtMem2, 1<<10 );
464 Abc_PrintTime( 1, "Exact NPN computation time", Abc_Clock() - clk );
465 printf( "Final results:\n" );
466 for ( n = 0; n <= nNodesMax; n++ )
467 {
468 int i, Entry, Entry2, nEntries2, Counter = 0, Counter2 = 0;
469 Vec_IntForEachEntry( vNodSup, Entry, i )
470 {
471 if ( (Entry & 0xF) > nVars || (Entry >> 16) != n )
472 continue;
473 Counter++;
474 nEntries2 = Vec_MemEntryNum(vTtMem2);
475 Entry2 = Vec_MemHashInsert( vTtMem2, Vec_WrdEntryP(vCanons, i) );
476 if ( nEntries2 == Vec_MemEntryNum(vTtMem2) ) // found in the table - not new
477 continue;
478 Counter2++;
479 }
480 nTotal += Counter2;
481 printf( "Nodes = %2d. ", n );
482 printf( "Semi-canonical = %8d. ", Counter );
483 printf( "Canonical = %8d. ", Counter2 );
484 printf( "Total = %8d.", nTotal );
485 printf( "\n" );
486 }
487 Vec_MemHashFree( vTtMem2 );
488 Vec_MemFreeP( &vTtMem2 );
489 Vec_WrdFree( vCanons );
490 fflush(stdout);
491}
492
504void Dau_TablesSave( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk )
505{
506 FILE * pFile;
507 char FileName[100];
508 int i, nWords = Abc_TtWordNum(nInputs);
509 // NPN classes
510 sprintf( FileName, "npn%d%d.ttd", nInputs, nVars );
511 pFile = fopen( FileName, "wb" );
512 for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
513 fwrite( Vec_MemReadEntry(vTtMem, i), 8, nWords, pFile );
514 fwrite( Vec_IntArray(vNodSup), 4, Vec_IntSize(vNodSup), pFile );
515 fclose( pFile );
516// printf( "Dumped files with %10d classes after exploring %10d frontiers.\n",
517// Vec_IntSize(vNodSup), nFronts );
518 printf( "Dumped file \"%s\" with %10d classes after exploring %10d frontiers. ",
519 FileName, Vec_IntSize(vNodSup), nFronts );
520 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
521 fflush(stdout);
522}
523
535void Dau_DumpFuncs( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nMax )
536{
537 FILE * pFile[20];
538 int Counters[20] = {0};
539 int n, i;
540 assert( nVars == 4 || nVars == 5 );
541 for ( n = 0; n <= nMax; n++ )
542 {
543 char FileName[100];
544 sprintf( FileName, "func%d_min%d.tt", nVars, n );
545 pFile[n] = fopen( FileName, "wb" );
546 }
547 for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
548 {
549 word * pTruth = Vec_MemReadEntry( vTtMem, i );
550 int NodSup = Vec_IntEntry( vNodSup, i );
551 if ( (NodSup & 0xF) != nVars )
552 continue;
553 Counters[NodSup >> 16]++;
554 if ( nVars == 4 )
555 fprintf( pFile[NodSup >> 16], "%04x\n", (int)(0xFFFF & pTruth[0]) );
556 else if ( nVars == 5 )
557 fprintf( pFile[NodSup >> 16], "%08x\n", (int)(0xFFFFFFFF & pTruth[0]) );
558 }
559 for ( n = 0; n <= nMax; n++ )
560 {
561 printf( "Dumped %8d %d-node %d-input functions into file.\n", Counters[n], n, nVars );
562 fclose( pFile[n] );
563 }
564}
565
577int Dau_CountFuncs( Vec_Int_t * vNodSup, int iStart, int iStop, int nVars )
578{
579 int i, Entry, Count = 0;
580 Vec_IntForEachEntryStartStop( vNodSup, Entry, i, iStart, iStop )
581 Count += ((Entry & 0xF) <= nVars);
582 return Count;
583}
584int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int iStart, int iStop, word nSteps, int Count2, abctime clk )
585{
586 int nNew;
587 printf("N =%2d | ", nNodes );
588 printf("C =%12.0f ", (double)(iword)nSteps );
589 printf("New%d =%10d ", nInputs, iStop-iStart );
590 printf("All%d =%10d | ", nInputs, iStop );
591 printf("New%d =%8d ", nVars, nNew = Dau_CountFuncs(vNodSup, iStart, iStop, nVars) );
592 printf("All%d =%8d ", nVars, Dau_CountFuncs(vNodSup, 0, iStop, nVars) );
593 printf("Two =%6d ", Count2 );
594 //Abc_PrintTime( 1, "T", Abc_Clock() - clk );
595 Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
596 fflush(stdout);
597 return nNew;
598}
599
600
601int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars0, int nVars,
602 Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk )
603{
604 int DumpDelta = 1000000;
605 char Perm[16] = {0};
606 int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs );
607 //unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 );
608 unsigned Phase = Abc_TtCanonicizeWrap( Abc_TtCanonicizeAda, pMan, pCur, nVarsNew, Perm, 99 );
609 int nEntries = Vec_MemEntryNum(vTtMem);
610 int Entry = Vec_MemHashInsert( vTtMem, pCur );
611 if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new
612 return 0;
613 Entry = 0;
614 Phase = 0;
615 // this is a new class
616 Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew );
617 assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) );
618 if ( Vec_IntSize(vNodSup) % DumpDelta == 0 )
619 Dau_TablesSave( nInputs, nVars0, vTtMem, vNodSup, nFronts, clk );
620 return 1;
621}
622void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fReduce, int fVerbose )
623{
624 abctime clk = Abc_Clock();
625 int nWords = Abc_TtWordNum(nInputs); word nSteps = 0;
626 Abc_TtHieMan_t * pMan = Abc_TtHieManStart( nInputs, 5 );
627 Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 16 );
628 Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 );
629 int v, u, k, m, n, Entry, nNew, Limit[32] = {1, 2};
630 word Truth[4] = {0};
631 assert( nVars >= 3 && nVars <= nInputs && nInputs <= 6 );
632 Vec_MemHashAlloc( vTtMem, 1<<16 );
633 // add constant 0
634 Vec_MemHashInsert( vTtMem, Truth );
635 Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0
636 // add buffer/inverter
637 Abc_TtIthVar( Truth, 0, nInputs );
638 Abc_TtNot( Truth, nWords );
639 Vec_MemHashInsert( vTtMem, Truth );
640 Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1
641 Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, nSteps, 0, clk );
642 // numerate other functions based on how many nodes they have
643 for ( n = 1; n <= nNodeMax; n++ )
644 {
645 int Count2 = 0;
646 int fExpand = !(fReduce && n == nNodeMax);
647 for ( Entry = Limit[n-1]; Entry < Limit[n]; Entry++ )
648 {
649 word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
650 int NodSup = Vec_IntEntry(vNodSup, Entry);
651 int nSupp = 0xF & NodSup;
652 int SymVars = Dau_CountSymms2( pTruth[0], nSupp );
653 assert( n-1 == (NodSup >> 16) );
654 assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
655 //printf( "Exploring function %4d with %d vars: ", i, nSupp );
656 //printf( " %04x\n", (int)uTruth );
657 //Dau_DsdPrintFromTruth( &uTruth, 4 );
658 for ( v = 0; v < nSupp; v++ ) if ( (SymVars & (1 << v)) == 0 )
659 {
660 word tGate, tCur;
661 word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
662 word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
663 // add one extra variable to support
664 if ( nSupp < nInputs && fExpand )
665 {
666 tGate = s_Truths6[v] & s_Truths6[nSupp];
667 tCur = (tGate & Cof1) | (~tGate & Cof0);
668 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
669
670 tCur = (tGate & Cof0) | (~tGate & Cof1);
671 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
672
673
674 tGate = s_Truths6[v] ^ s_Truths6[nSupp];
675 tCur = (tGate & Cof1) | (~tGate & Cof0);
676 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
677
678 nSteps += 3;
679 }
680 // add one cross bar
681 if ( fExpand )
682 for ( k = 0; k < nSupp; k++ ) if ( k != v && ((SymVars & (1 << k)) == 0 || k == v+1) )
683 {
684 tGate = s_Truths6[v] & s_Truths6[k];
685 tCur = (tGate & Cof1) | (~tGate & Cof0);
686 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
687
688 tCur = (tGate & Cof0) | (~tGate & Cof1);
689 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
690
691 tGate = s_Truths6[v] & ~s_Truths6[k];
692 tCur = (tGate & Cof1) | (~tGate & Cof0);
693 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
694
695 tCur = (tGate & Cof0) | (~tGate & Cof1);
696 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
697
698
699 tGate = s_Truths6[v] ^ s_Truths6[k];
700 tCur = (tGate & Cof1) | (~tGate & Cof0);
701 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
702
703 nSteps += 5;
704 }
705 // add two cross bars
706 for ( k = 0; k < nSupp; k++ ) if ( k != v )//&& ((SymVars & (1 << k)) == 0) )
707 for ( m = k+1; m < nSupp; m++ ) if ( m != v )//&& ((SymVars & (1 << m)) == 0 || m == k+1) )
708 {
709 tGate = s_Truths6[m] & s_Truths6[k];
710 tCur = (tGate & Cof1) | (~tGate & Cof0);
711 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
712
713 tCur = (tGate & Cof0) | (~tGate & Cof1);
714 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
715
716 tGate = s_Truths6[m] & ~s_Truths6[k];
717 tCur = (tGate & Cof1) | (~tGate & Cof0);
718 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
719
720 tCur = (tGate & Cof0) | (~tGate & Cof1);
721 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
722
723 tGate = ~s_Truths6[m] & s_Truths6[k];
724 tCur = (tGate & Cof1) | (~tGate & Cof0);
725 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
726
727 tCur = (tGate & Cof0) | (~tGate & Cof1);
728 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
729
730 tGate = ~s_Truths6[m] & ~s_Truths6[k];
731 tCur = (tGate & Cof1) | (~tGate & Cof0);
732 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
733
734 tCur = (tGate & Cof0) | (~tGate & Cof1);
735 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
736
737
738 tGate = s_Truths6[m] ^ s_Truths6[k];
739 tCur = (tGate & Cof1) | (~tGate & Cof0);
740 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
741
742 tGate = s_Truths6[m] ^ s_Truths6[k];
743 tCur = (tGate & Cof0) | (~tGate & Cof1);
744 Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
745
746 nSteps += 10;
747 }
748 }
749 }
750 if ( fUseTwo && n > 2 && fExpand )
751 for ( Entry = Limit[n-2]; Entry < Limit[n-1]; Entry++ )
752 {
753 word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
754 int NodSup = Vec_IntEntry(vNodSup, Entry);
755 int nSupp = 0xF & NodSup; int g1, g2;
756 assert( n-2 == (NodSup >> 16) );
757 assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
758 for ( v = 0; v < nSupp; v++ )
759 for ( u = 0; u < nSupp; u++ ) if ( u != v )
760 {
761 word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
762 word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
763
764 word Cof00 = Abc_Tt6Cofactor0( Cof0, u );
765 word Cof01 = Abc_Tt6Cofactor1( Cof0, u );
766 word Cof10 = Abc_Tt6Cofactor0( Cof1, u );
767 word Cof11 = Abc_Tt6Cofactor1( Cof1, u );
768
769 word tGates[5], tCur;
770 tGates[0] = s_Truths6[v] & s_Truths6[u];
771 tGates[1] = s_Truths6[v] & ~s_Truths6[u];
772 tGates[2] = ~s_Truths6[v] & s_Truths6[u];
773 tGates[3] = s_Truths6[v] | s_Truths6[u];
774 tGates[4] = s_Truths6[v] ^ s_Truths6[u];
775
776 for ( g1 = 0; g1 < 5; g1++ )
777 for ( g2 = g1+1; g2 < 5; g2++ )
778 {
779 Cof0 = (tGates[g1] & Cof01) | (~tGates[g1] & Cof00);
780 Cof1 = (tGates[g1] & Cof11) | (~tGates[g1] & Cof10);
781
782 tCur = (tGates[g2] & Cof1) | (~tGates[g2] & Cof0);
783 Count2 += Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
784 }
785 }
786 }
787 Limit[n+1] = Vec_IntSize(vNodSup);
788 nNew = Dau_PrintStats( n, nInputs, nVars, vNodSup, Limit[n], Limit[n+1], nSteps, Count2, clk );
789 if ( nNew == 0 )
790 break;
791 }
792 Dau_TablesSave( nInputs, nVars, vTtMem, vNodSup, Vec_IntSize(vNodSup), clk );
793 Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
794 //Dau_DumpFuncs( vTtMem, vNodSup, nVars, nNodeMax );
795 //Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n );
796 Abc_TtHieManStop( pMan );
797 Vec_MemHashFree( vTtMem );
798 Vec_MemFreeP( &vTtMem );
799 Vec_IntFree( vNodSup );
800 fflush(stdout);
801}
802
814Vec_Mem_t * Dau_CollectNpnFunctions( word * p, int nVars, int fVerbose )
815{
816 abctime clkStart = Abc_Clock();
817 Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVars );
818 int nWords = Abc_Truth6WordNum(nVars);
819 word * pCopy = ABC_ALLOC( word, nWords );
820 Abc_TtCopy( pCopy, p, nWords, p[0] & 1 );
821 Vec_MemHashInsert( vTtMem, pCopy );
822 int nPerms = Extra_Factorial( nVars );
823 int nMints = 1 << nVars;
824 int * pPerm = Extra_PermSchedule( nVars );
825 int * pComp = Extra_GreyCodeSchedule( nVars );
826 int m, i, k, nFuncs;
827 for ( m = 0; m < nMints; m++ ) {
828 Abc_TtFlip( pCopy, nWords, pComp[m] );
829 if ( pCopy[0] & 1 ) {
830 Abc_TtNot( pCopy, nWords );
831 assert( (pCopy[0] & 1) == 0 );
832 Vec_MemHashInsert( vTtMem, pCopy );
833 Abc_TtNot( pCopy, nWords );
834 }
835 else
836 Vec_MemHashInsert( vTtMem, pCopy );
837 }
838 assert( Abc_TtEqual(pCopy, Vec_MemReadEntry(vTtMem, 0), nWords) );
839 nFuncs = Vec_MemEntryNum(vTtMem);
840 if ( fVerbose )
841 printf( "Collected %d NN functions and ", nFuncs ), fflush(stdout);
842 for ( i = 0; i < nFuncs; i++ ) {
843 Abc_TtCopy( pCopy, Vec_MemReadEntry(vTtMem, i), nWords, 0 );
844 for ( k = 0; k < nPerms; k++ ) {
845 Abc_TtSwapAdjacent( pCopy, nWords, pPerm[k] );
846 assert( (pCopy[0] & 1) == 0 );
847 Vec_MemHashInsert( vTtMem, pCopy );
848 }
849 assert( Abc_TtEqual(pCopy, Vec_MemReadEntry(vTtMem, i), nWords) );
850 }
851 ABC_FREE( pPerm );
852 ABC_FREE( pComp );
853 ABC_FREE( pCopy );
854 nFuncs = Vec_MemEntryNum(vTtMem);
855 if ( fVerbose )
856 printf( "%d NPN functions. ", nFuncs ),
857 Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ),
858 fflush(stdout);
859 return vTtMem;
860}
861
873Vec_Mem_t * Dau_CollectNpnFunctionsArray( Vec_Wrd_t * vFuncs, int nVars, Vec_Int_t ** pvMap, int fVerbose )
874{
875 assert( nVars <= 10 );
876 abctime clkStart = Abc_Clock();
877 Vec_Int_t * vMap = Vec_IntAlloc( 100 );
878 Vec_Int_t * vCnts = Vec_IntAlloc( Vec_WrdSize(vFuncs) );
879 Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVars );
880 int nWords = Abc_Truth6WordNum(nVars);
881 int nPerms = Extra_Factorial( nVars );
882 int nMints = 1 << nVars;
883 int * pPerm = Extra_PermSchedule( nVars );
884 int * pComp = Extra_GreyCodeSchedule( nVars );
885 int m, i, k, t, Entry;
886 word * pCopy = ABC_ALLOC( word, nWords );
887 int nClasses = Vec_WrdSize(vFuncs) / nWords;
888 assert( nClasses * nWords == Vec_WrdSize(vFuncs) );
889 for ( t = 0; t < nClasses; t++ )
890 {
891 word * pTruth = Vec_WrdEntryP( vFuncs, nWords * t );
892 int nFuncs = Vec_MemEntryNum(vTtMem);
893 Abc_TtCopy( pCopy, pTruth, nWords, pTruth[0] & 1 );
894 Vec_MemHashInsert( vTtMem, pCopy );
895 for ( m = 0; m < nMints; m++ ) {
896 Abc_TtFlip( pCopy, nWords, pComp[m] );
897 if ( pCopy[0] & 1 ) {
898 Abc_TtNot( pCopy, nWords );
899 assert( (pCopy[0] & 1) == 0 );
900 Vec_MemHashInsert( vTtMem, pCopy );
901 Abc_TtNot( pCopy, nWords );
902 }
903 else
904 Vec_MemHashInsert( vTtMem, pCopy );
905 }
906 if ( pTruth[0] & 1 )
907 assert( Abc_TtOpposite(pCopy, pTruth, nWords) );
908 else
909 assert( Abc_TtEqual(pCopy, pTruth, nWords) );
910 int nFuncs2 = Vec_MemEntryNum(vTtMem);
911 for ( i = nFuncs; i < nFuncs2; i++ ) {
912 Abc_TtCopy( pCopy, Vec_MemReadEntry(vTtMem, i), nWords, 0 );
913 for ( k = 0; k < nPerms; k++ ) {
914 Abc_TtSwapAdjacent( pCopy, nWords, pPerm[k] );
915 assert( (pCopy[0] & 1) == 0 );
916 Vec_MemHashInsert( vTtMem, pCopy );
917 }
918 assert( Abc_TtEqual(pCopy, Vec_MemReadEntry(vTtMem, i), nWords) );
919 }
920 for ( i = nFuncs; i < Vec_MemEntryNum(vTtMem); i++ )
921 Vec_IntPush( vMap, t );
922 Vec_IntPush( vCnts, Vec_MemEntryNum(vTtMem) - nFuncs );
923 }
924 ABC_FREE( pCopy );
925 ABC_FREE( pPerm );
926 ABC_FREE( pComp );
927 if ( fVerbose ) {
928 int Lim = Abc_MinInt( Vec_IntSize(vCnts), 7 );
929 printf( "Collected %d", Vec_MemEntryNum(vTtMem) );
930 Vec_IntForEachEntryStop( vCnts, Entry, i, Lim )
931 printf( " %c %d", i ? '+' : '=', Entry );
932 if ( Vec_IntSize(vCnts) > Lim )
933 printf( " + ..." );
934 printf( " NPN class members. " );
935 Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
936 fflush(stdout);
937 }
938 Vec_IntFree( vCnts );
939 if ( pvMap )
940 *pvMap = vMap;
941 else
942 Vec_IntFree( vMap );
943 return vTtMem;
944}
945
957void Dau_CanonicizeArray( Vec_Wrd_t * vFuncs, int nVars, int fVerbose )
958{
959 abctime clkStart = Abc_Clock();
960 extern unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
961 if ( fVerbose ) printf( "Functions: %d (original) ", Vec_WrdSize(vFuncs) );
962 unsigned uCanonPhase; char pCanonPerm[16]; word Func; int i;
963 Vec_WrdUniqify( vFuncs );
964
965 if ( fVerbose ) printf( "-> %d (unique) ", Vec_WrdSize(vFuncs) );
966 Vec_WrdForEachEntry( vFuncs, Func, i ) {
967 uCanonPhase = Abc_TtCanonicize( &Func, nVars, pCanonPerm );
968 Vec_WrdWriteEntry( vFuncs, i, Func );
969 }
970 Vec_WrdUniqify( vFuncs );
971 if ( fVerbose ) printf( "-> %d (approx NPN) ", Vec_WrdSize(vFuncs) );
972 Abc_TtHieMan_t * pMan = Abc_TtHieManStart(nVars, 5);
973 Vec_WrdForEachEntry( vFuncs, Func, i ) {
974 uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeCA, pMan, &Func, nVars, pCanonPerm, 1);
975 Vec_WrdWriteEntry( vFuncs, i, Func );
976 }
977 Vec_WrdUniqify( vFuncs );
978 if ( fVerbose ) printf( "-> %d (exact NPN). ", Vec_WrdSize(vFuncs) );
979 Abc_TtHieManStop(pMan);
980 Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
981 fflush( stdout );
982}
983
987
988ABC_NAMESPACE_IMPL_END
989
nWords
int nWords
Definition abcNpn.c:127
iword
ABC_INT64_T iword
Definition abc_global.h:244
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
freePermInfoPtr
void freePermInfoPtr(permInfo *x)
Definition luckySimple.c:126
simpleMinimal
void simpleMinimal(word *x, word *pAux, word *minimal, permInfo *pi, int nVars)
Definition luckySimple.c:156
setPermInfoPtr
permInfo * setPermInfoPtr(int var)
Definition luckySimple.c:110
Abc_TtCanonicizeCA
unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int fCA)
Definition dauCanon.c:2637
Dau_CanonicizeArray
void Dau_CanonicizeArray(Vec_Wrd_t *vFuncs, int nVars, int fVerbose)
Definition dauNpn.c:957
Dau_AddFunction
int Dau_AddFunction(word tCur, int nVars, unsigned *pTable, Vec_Int_t *vNpns, Vec_Int_t *vNpns_)
Definition dauNpn.c:157
Dau_NetworkEnumTest
void Dau_NetworkEnumTest()
Definition dauNpn.c:373
Dau_CountFuncs
int Dau_CountFuncs(Vec_Int_t *vNodSup, int iStart, int iStop, int nVars)
Definition dauNpn.c:577
Dau_ExactNpnPrint
void Dau_ExactNpnPrint(Vec_Mem_t *vTtMem, Vec_Int_t *vNodSup, int nVars, int nInputs, int nNodesMax)
Definition dauNpn.c:458
Dau_InsertFunction
int Dau_InsertFunction(Abc_TtHieMan_t *pMan, word *pCur, int nNodes, int nInputs, int nVars0, int nVars, Vec_Mem_t *vTtMem, Vec_Int_t *vNodSup, int nFronts, abctime clk)
Definition dauNpn.c:601
Dau_TablesSave
void Dau_TablesSave(int nInputs, int nVars, Vec_Mem_t *vTtMem, Vec_Int_t *vNodSup, int nFronts, abctime clk)
Definition dauNpn.c:504
Dau_ExactNpnForClasses
Vec_Wrd_t * Dau_ExactNpnForClasses(Vec_Mem_t *vTtMem, Vec_Int_t *vNodSup, int nVars, int nInputs)
Definition dauNpn.c:441
Dau_DumpFuncs
void Dau_DumpFuncs(Vec_Mem_t *vTtMem, Vec_Int_t *vNodSup, int nVars, int nMax)
Definition dauNpn.c:535
Dau_CountSymms
int Dau_CountSymms(word t, int nVars)
Definition dauNpn.c:392
Dau_CountCompl
int Dau_CountCompl(word t, int nVars)
Definition dauNpn.c:422
Dau_CollectNpnFunctionsArray
Vec_Mem_t * Dau_CollectNpnFunctionsArray(Vec_Wrd_t *vFuncs, int nVars, Vec_Int_t **pvMap, int fVerbose)
Definition dauNpn.c:873
Dau_PrintStats
int Dau_PrintStats(int nNodes, int nInputs, int nVars, Vec_Int_t *vNodSup, int iStart, int iStop, word nSteps, int Count2, abctime clk)
Definition dauNpn.c:584
Dau_CountSymms2
int Dau_CountSymms2(word t, int nVars)
Definition dauNpn.c:401
Dau_ReadFile
unsigned * Dau_ReadFile(char *pFileName, int nSizeW)
Definition dauNpn.c:140
Dau_FunctionEnum
void Dau_FunctionEnum(int nInputs, int nVars, int nNodeMax, int fUseTwo, int fReduce, int fVerbose)
Definition dauNpn.c:622
Dau_NetworkEnum
void Dau_NetworkEnum(int nVars)
Definition dauNpn.c:176
Dau_CountCompl1
int Dau_CountCompl1(word t, int v, int nVars)
Definition dauNpn.c:411
Dau_CollectNpnFunctions
Vec_Mem_t * Dau_CollectNpnFunctions(word *p, int nVars, int fVerbose)
Definition dauNpn.c:814
Dau_TruthEnum
ABC_NAMESPACE_IMPL_START void Dau_TruthEnum(int nVars)
DECLARATIONS ///.
Definition dauNpn.c:48
Abc_TtHieMan_t
struct Abc_TtHieMan_t_ Abc_TtHieMan_t
Definition dau.h:62
Abc_TtCanonicizeAda
unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int iThres)
Definition dauCanon.c:2573
Abc_TtHieManStart
Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels)
Definition dauCanon.c:1255
Abc_TtHieManStop
void Abc_TtHieManStop(Abc_TtHieMan_t *p)
Definition dauCanon.c:1273
Abc_TtCanonicizeWrap
unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t *p, word *pTruth, int nVars, char *pCanonPerm, int flag)
Definition dauCanon.c:1530
Abc_TtCanonicize
unsigned Abc_TtCanonicize(word *pTruth, int nVars, char *pCanonPerm)
FUNCTION DECLARATIONS ///.
Definition dauCanon.c:1036
p
Cube * p
Definition exorList.c:222
Extra_PermSchedule
int * Extra_PermSchedule(int n)
Definition extraUtilMisc.c:2206
Extra_Factorial
int Extra_Factorial(int n)
Definition extraUtilMisc.c:217
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition extraUtilMisc.c:2170
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Vec_Mem_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition utilMem.c:35
assert
#define assert(ex)
Definition util_old.h:213
sprintf
char * sprintf()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStop
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition vecInt.h:58
Vec_IntForEachEntryStartStop
#define Vec_IntForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition vecInt.h:60
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42