abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
aigCanon.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [aigCanon.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [AIG package.]
8 
9  Synopsis [Processing the library of semi-canonical AIGs.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: aigCanon.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "aig.h"
22 #include "bool/kit/kit.h"
23 #include "bool/bdc/bdc.h"
24 #include "aig/ioa/ioa.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 #define RMAN_MAXVARS 12
34 #define RMAX_MAXWORD (RMAN_MAXVARS <= 5 ? 1 : (1 << (RMAN_MAXVARS - 5)))
35 
36 typedef struct Aig_VSig_t_ Aig_VSig_t;
37 struct Aig_VSig_t_
38 {
39  int nOnes;
40  int nCofOnes[RMAN_MAXVARS];
41 };
42 
43 typedef struct Aig_Tru_t_ Aig_Tru_t;
44 struct Aig_Tru_t_
45 {
46  Aig_Tru_t * pNext;
47  int Id;
48  unsigned nVisits : 27;
49  unsigned nVars : 5;
50  unsigned pTruth[0];
51 };
52 
53 typedef struct Aig_RMan_t_ Aig_RMan_t;
54 struct Aig_RMan_t_
55 {
56  int nVars; // the largest variable number
57  Aig_Man_t * pAig; // recorded subgraphs
58  // hash table
59  int nBins;
60  Aig_Tru_t ** pBins;
61  int nEntries;
62  Aig_MmFlex_t* pMemTrus;
63  // bidecomposion
64  Bdc_Man_t * pBidec;
65  // temporaries
66  unsigned pTruthInit[RMAX_MAXWORD]; // canonical truth table
67  unsigned pTruth[RMAX_MAXWORD]; // current truth table
68  unsigned pTruthC[RMAX_MAXWORD]; // canonical truth table
69  unsigned pTruthTemp[RMAX_MAXWORD]; // temporary truth table
70  Aig_VSig_t pMints[2*RMAN_MAXVARS]; // minterm count
71  char pPerm[RMAN_MAXVARS]; // permutation
72  char pPermR[RMAN_MAXVARS]; // reverse permutation
73  // statistics
74  int nVarFuncs[RMAN_MAXVARS+1];
75  int nTotal;
76  int nTtDsd;
77  int nTtDsdPart;
78  int nTtDsdNot;
79  int nUniqueVars;
80 };
81 
82 static Aig_RMan_t * s_pRMan = NULL;
83 
84 ////////////////////////////////////////////////////////////////////////
85 /// FUNCTION DEFINITIONS ///
86 ////////////////////////////////////////////////////////////////////////
87 
88 /**Function*************************************************************
89 
90  Synopsis [Allocates recording manager.]
91 
92  Description []
93 
94  SideEffects []
95 
96  SeeAlso []
97 
98 ***********************************************************************/
99 Aig_RMan_t * Aig_RManStart()
100 {
101  static Bdc_Par_t Pars = {0}, * pPars = &Pars;
102  Aig_RMan_t * p;
103  p = ABC_ALLOC( Aig_RMan_t, 1 );
104  memset( p, 0, sizeof(Aig_RMan_t) );
105  p->nVars = RMAN_MAXVARS;
106  p->pAig = Aig_ManStart( 1000000 );
107  Aig_IthVar( p->pAig, p->nVars-1 );
108  // create hash table
109  p->nBins = Abc_PrimeCudd(5000);
110  p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
111  p->pMemTrus = Aig_MmFlexStart();
112  // bi-decomposition manager
113  pPars->nVarsMax = p->nVars;
114  pPars->fVerbose = 0;
115  p->pBidec = Bdc_ManAlloc( pPars );
116  return p;
117 }
118 
119 /**Function*************************************************************
120 
121  Synopsis [Returns the hash key.]
122 
123  Description []
124 
125  SideEffects []
126 
127  SeeAlso []
128 
129 ***********************************************************************/
130 static inline int Aig_RManTableHash( unsigned * pTruth, int nVars, int nBins, int * pPrimes )
131 {
132  int i, nWords = Kit_TruthWordNum( nVars );
133  unsigned uHash = 0;
134  for ( i = 0; i < nWords; i++ )
135  uHash ^= pTruth[i] * pPrimes[i & 0xf];
136  return (int)(uHash % nBins);
137 }
138 
139 /**Function*************************************************************
140 
141  Synopsis [Returns the given record.]
142 
143  Description []
144 
145  SideEffects []
146 
147  SeeAlso []
148 
149 ***********************************************************************/
150 Aig_Tru_t ** Aig_RManTableLookup( Aig_RMan_t * p, unsigned * pTruth, int nVars )
151 {
152  static int s_Primes[16] = {
153  1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
154  4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
155  Aig_Tru_t ** ppSpot, * pEntry;
156  ppSpot = p->pBins + Aig_RManTableHash( pTruth, nVars, p->nBins, s_Primes );
157  for ( pEntry = *ppSpot; pEntry; ppSpot = &pEntry->pNext, pEntry = pEntry->pNext )
158  if ( Kit_TruthIsEqual( pEntry->pTruth, pTruth, nVars ) )
159  return ppSpot;
160  return ppSpot;
161 }
162 
163 /**Function*************************************************************
164 
165  Synopsis [Find or add new entry.]
166 
167  Description []
168 
169  SideEffects []
170 
171  SeeAlso []
172 
173 ***********************************************************************/
174 void Aig_RManTableResize( Aig_RMan_t * p )
175 {
176  Aig_Tru_t * pEntry, * pNext;
177  Aig_Tru_t ** pBinsOld, ** ppPlace;
178  int nBinsOld, Counter, i;
179  abctime clk;
180  assert( p->pBins != NULL );
181 clk = Abc_Clock();
182  // save the old Bins
183  pBinsOld = p->pBins;
184  nBinsOld = p->nBins;
185  // get the new Bins
186  p->nBins = Abc_PrimeCudd( 3 * nBinsOld );
187  p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
188  // rehash the entries from the old table
189  Counter = 0;
190  for ( i = 0; i < nBinsOld; i++ )
191  for ( pEntry = pBinsOld[i], pNext = pEntry? pEntry->pNext : NULL;
192  pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
193  {
194  // get the place where this entry goes in the Bins
195  ppPlace = Aig_RManTableLookup( p, pEntry->pTruth, pEntry->nVars );
196  assert( *ppPlace == NULL ); // should not be there
197  // add the entry to the list
198  *ppPlace = pEntry;
199  pEntry->pNext = NULL;
200  Counter++;
201  }
202  assert( Counter == p->nEntries );
203 // ABC_PRT( "Time", Abc_Clock() - clk );
204  ABC_FREE( pBinsOld );
205 }
206 
207 /**Function*************************************************************
208 
209  Synopsis [Find or add new entry.]
210 
211  Description [Returns 1 if this is a new entry.]
212 
213  SideEffects []
214 
215  SeeAlso []
216 
217 ***********************************************************************/
218 int Aig_RManTableFindOrAdd( Aig_RMan_t * p, unsigned * pTruth, int nVars )
219 {
220  Aig_Tru_t ** ppSpot, * pEntry;
221  int nBytes;
222  ppSpot = Aig_RManTableLookup( p, pTruth, nVars );
223  if ( *ppSpot )
224  {
225  (*ppSpot)->nVisits++;
226  return 0;
227  }
228  nBytes = sizeof(Aig_Tru_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars);
229  if ( p->nEntries == 3*p->nBins )
230  Aig_RManTableResize( p );
231  pEntry = (Aig_Tru_t *)Aig_MmFlexEntryFetch( p->pMemTrus, nBytes );
232  pEntry->Id = p->nEntries++;
233  pEntry->nVars = nVars;
234  pEntry->nVisits = 1;
235  pEntry->pNext = NULL;
236  memcpy( pEntry->pTruth, pTruth, sizeof(unsigned) * Kit_TruthWordNum(nVars) );
237  *ppSpot = pEntry;
238  return 1;
239 }
240 
241 /**Function*************************************************************
242 
243  Synopsis [Deallocates recording manager.]
244 
245  Description []
246 
247  SideEffects []
248 
249  SeeAlso []
250 
251 ***********************************************************************/
252 void Aig_RManStop( Aig_RMan_t * p )
253 {
254  int i;
255  printf( "Total funcs = %10d\n", p->nTotal );
256  printf( "Full DSD funcs = %10d\n", p->nTtDsd );
257  printf( "Part DSD funcs = %10d\n", p->nTtDsdPart );
258  printf( "Non- DSD funcs = %10d\n", p->nTtDsdNot );
259  printf( "Uniq-var funcs = %10d\n", p->nUniqueVars );
260  printf( "Unique funcs = %10d\n", p->nEntries );
261  printf( "Distribution of functions:\n" );
262  for ( i = 5; i <= p->nVars; i++ )
263  printf( "%2d = %8d\n", i, p->nVarFuncs[i] );
264  Aig_MmFlexStop( p->pMemTrus, 0 );
265  Aig_ManStop( p->pAig );
266  Bdc_ManFree( p->pBidec );
267  ABC_FREE( p->pBins );
268  ABC_FREE( p );
269 }
270 
271 
272 /**Function*************************************************************
273 
274  Synopsis [Stops recording.]
275 
276  Description []
277 
278  SideEffects []
279 
280  SeeAlso []
281 
282 ***********************************************************************/
283 void Aig_RManQuit()
284 {
285 // extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
286  char Buffer[20];
287  if ( s_pRMan == NULL )
288  return;
289  // dump the library file
290  sprintf( Buffer, "aiglib%02d.aig", s_pRMan->nVars );
291  Ioa_WriteAiger( s_pRMan->pAig, Buffer, 0, 1 );
292  // quit the manager
293  Aig_RManStop( s_pRMan );
294  s_pRMan = NULL;
295 }
296 
297 /**Function*************************************************************
298 
299  Synopsis [Returns 1 if all variables are unique.]
300 
301  Description []
302 
303  SideEffects []
304 
305  SeeAlso []
306 
307 ***********************************************************************/
308 void Aig_RManPrintVarProfile( unsigned * pTruth, int nVars, unsigned * pTruthAux )
309 {
310  int pStore2[32];
311  int i;
312  Kit_TruthCountOnesInCofsSlow( pTruth, nVars, pStore2, pTruthAux );
313  for ( i = 0; i < nVars; i++ )
314  printf( "%2d/%2d ", pStore2[2*i], pStore2[2*i+1] );
315  printf( "\n" );
316 }
317 
318 /**Function*************************************************************
319 
320  Synopsis [Sorts numbers in the increasing order.]
321 
322  Description []
323 
324  SideEffects []
325 
326  SeeAlso []
327 
328 ***********************************************************************/
329 void Aig_RManSortNums( int * pArray, int nVars )
330 {
331  int i, j, best_i, tmp;
332  for ( i = 0; i < nVars-1; i++ )
333  {
334  best_i = i;
335  for ( j = i+1; j < nVars; j++ )
336  if ( pArray[j] > pArray[best_i] )
337  best_i = j;
338  tmp = pArray[i]; pArray[i] = pArray[best_i]; pArray[best_i] = tmp;
339  }
340 }
341 
342 /**Function*************************************************************
343 
344  Synopsis [Prints signatures for all variables.]
345 
346  Description []
347 
348  SideEffects []
349 
350  SeeAlso []
351 
352 ***********************************************************************/
353 void Aig_RManPrintSigs( Aig_VSig_t * pSigs, int nVars )
354 {
355  int v, i, k;
356  for ( v = 0; v < nVars; v++ )
357  {
358  printf( "%2d : ", v );
359  for ( k = 0; k < 2; k++ )
360  {
361  printf( "%5d ", pSigs[2*v+k].nOnes );
362  printf( "(" );
363  for ( i = 0; i < nVars; i++ )
364  printf( "%4d ", pSigs[2*v+k].nCofOnes[i] );
365  printf( ") " );
366  }
367  printf( "\n" );
368  }
369 }
370 
371 /**Function*************************************************************
372 
373  Synopsis [Computes signatures for all variables.]
374 
375  Description []
376 
377  SideEffects []
378 
379  SeeAlso []
380 
381 ***********************************************************************/
382 void Aig_RManComputeVSigs( unsigned * pTruth, int nVars, Aig_VSig_t * pSigs, unsigned * pAux )
383 {
384  int v;
385  for ( v = 0; v < nVars; v++ )
386  {
387  Kit_TruthCofactor0New( pAux, pTruth, nVars, v );
388  pSigs[2*v+0].nOnes = Kit_TruthCountOnes( pAux, nVars );
389  Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+0].nCofOnes );
390  Aig_RManSortNums( pSigs[2*v+0].nCofOnes, nVars );
391 
392  Kit_TruthCofactor1New( pAux, pTruth, nVars, v );
393  pSigs[2*v+1].nOnes = Kit_TruthCountOnes( pAux, nVars );
394  Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+1].nCofOnes );
395  Aig_RManSortNums( pSigs[2*v+1].nCofOnes, nVars );
396  }
397 }
398 
399 /**Function*************************************************************
400 
401  Synopsis [Computs signatures for all variables.]
402 
403  Description []
404 
405  SideEffects []
406 
407  SeeAlso []
408 
409 ***********************************************************************/
410 static inline int Aig_RManCompareSigs( Aig_VSig_t * p0, Aig_VSig_t * p1, int nVars )
411 {
412 // return memcmp( p0, p1, sizeof(int) + sizeof(int) * nVars );
413  return memcmp( p0, p1, sizeof(int) );
414 }
415 
416 /**Function*************************************************************
417 
418  Synopsis [Returns 1 if all variables are unique.]
419 
420  Description []
421 
422  SideEffects []
423 
424  SeeAlso []
425 
426 ***********************************************************************/
427 int Aig_RManVarsAreUnique( Aig_VSig_t * pMints, int nVars )
428 {
429  int i;
430  for ( i = 0; i < nVars - 1; i++ )
431  if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*(i+1)], nVars ) == 0 )
432  return 0;
433  return 1;
434 }
435 
436 /**Function*************************************************************
437 
438  Synopsis [Returns 1 if all variables are unique.]
439 
440  Description []
441 
442  SideEffects []
443 
444  SeeAlso []
445 
446 ***********************************************************************/
447 void Aig_RManPrintUniqueVars( Aig_VSig_t * pMints, int nVars )
448 {
449  int i;
450  for ( i = 0; i < nVars; i++ )
451  if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*i+1], nVars ) == 0 )
452  printf( "=" );
453  else
454  printf( "x" );
455  printf( "\n" );
456 
457  printf( "0" );
458  for ( i = 1; i < nVars; i++ )
459  if ( Aig_RManCompareSigs( &pMints[2*(i-1)], &pMints[2*i], nVars ) == 0 )
460  printf( "-" );
461  else if ( i < 10 )
462  printf( "%c", '0' + i );
463  else
464  printf( "%c", 'A' + i-10 );
465  printf( "\n" );
466 }
467 
468 /**Function*************************************************************
469 
470  Synopsis [Canonicize the truth table.]
471 
472  Description [Returns the phase. ]
473 
474  SideEffects []
475 
476  SeeAlso []
477 
478 ***********************************************************************/
479 unsigned Aig_RManSemiCanonicize( unsigned * pOut, unsigned * pIn, int nVars, char * pCanonPerm, Aig_VSig_t * pSigs, int fReturnIn )
480 {
481  Aig_VSig_t TempSig;
482  int i, Temp, fChange, Counter;
483  unsigned * pTemp, uCanonPhase = 0;
484  // collect signatures
485  Aig_RManComputeVSigs( pIn, nVars, pSigs, pOut );
486  // canonicize phase
487  for ( i = 0; i < nVars; i++ )
488  {
489 // if ( pStore[2*i+0] <= pStore[2*i+1] )
490  if ( Aig_RManCompareSigs( &pSigs[2*i+0], &pSigs[2*i+1], nVars ) <= 0 )
491  continue;
492  uCanonPhase |= (1 << i);
493  TempSig = pSigs[2*i+0];
494  pSigs[2*i+0] = pSigs[2*i+1];
495  pSigs[2*i+1] = TempSig;
496  Kit_TruthChangePhase( pIn, nVars, i );
497  }
498  // permute
499  Counter = 0;
500  do {
501  fChange = 0;
502  for ( i = 0; i < nVars-1; i++ )
503  {
504 // if ( pStore[2*i] <= pStore[2*(i+1)] )
505  if ( Aig_RManCompareSigs( &pSigs[2*i], &pSigs[2*(i+1)], nVars ) <= 0 )
506  continue;
507  Counter++;
508  fChange = 1;
509 
510  Temp = pCanonPerm[i];
511  pCanonPerm[i] = pCanonPerm[i+1];
512  pCanonPerm[i+1] = Temp;
513 
514  TempSig = pSigs[2*i];
515  pSigs[2*i] = pSigs[2*(i+1)];
516  pSigs[2*(i+1)] = TempSig;
517 
518  TempSig = pSigs[2*i+1];
519  pSigs[2*i+1] = pSigs[2*(i+1)+1];
520  pSigs[2*(i+1)+1] = TempSig;
521 
522  Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
523  pTemp = pIn; pIn = pOut; pOut = pTemp;
524  }
525  } while ( fChange );
526 
527  // swap if it was moved an even number of times
528  if ( fReturnIn ^ !(Counter & 1) )
529  Kit_TruthCopy( pOut, pIn, nVars );
530  return uCanonPhase;
531 }
532 
533 /**Function*************************************************************
534 
535  Synopsis []
536 
537  Description []
538 
539  SideEffects []
540 
541  SeeAlso []
542 
543 ***********************************************************************/
544 static inline Aig_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )
545 { return Aig_NotCond( (Aig_Obj_t *)Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); }
546 
547 /**Function*************************************************************
548 
549  Synopsis [Records one function.]
550 
551  Description []
552 
553  SideEffects []
554 
555  SeeAlso []
556 
557 ***********************************************************************/
558 void Aig_RManSaveOne( Aig_RMan_t * p, unsigned * pTruth, int nVars )
559 {
560  int i, nNodes, RetValue;
561  Bdc_Fun_t * pFunc;
562  Aig_Obj_t * pTerm;
563  // perform decomposition
564  RetValue = Bdc_ManDecompose( p->pBidec, pTruth, NULL, nVars, NULL, 1000 );
565  if ( RetValue < 0 )
566  {
567  printf( "Decomposition failed.\n" );
568  return;
569  }
570  // convert back into HOP
571  Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, 0 ), Aig_ManConst1(p->pAig) );
572  for ( i = 0; i < nVars; i++ )
573  Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, i+1 ), Aig_IthVar(p->pAig, i) );
574  nNodes = Bdc_ManNodeNum(p->pBidec);
575  for ( i = nVars + 1; i < nNodes; i++ )
576  {
577  pFunc = Bdc_ManFunc( p->pBidec, i );
578  Bdc_FuncSetCopy( pFunc, Aig_And( p->pAig,
579  Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)),
580  Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
581  }
582  pTerm = Bdc_FunCopyHop( Bdc_ManRoot(p->pBidec) );
583  pTerm = Aig_ObjCreateCo( p->pAig, pTerm );
584 // assert( pTerm->fPhase == 0 );
585 }
586 
587 /**Function*************************************************************
588 
589  Synopsis [Records one function.]
590 
591  Description []
592 
593  SideEffects []
594 
595  SeeAlso []
596 
597 ***********************************************************************/
598 void Aig_RManRecord( unsigned * pTruth, int nVarsInit )
599 {
600  int fVerify = 1;
601  Kit_DsdNtk_t * pNtk;
602  Kit_DsdObj_t * pObj;
603  unsigned uPhaseC;
604  int i, nVars, nWords;
605  int fUniqueVars;
606 
607  if ( nVarsInit > RMAN_MAXVARS )
608  {
609  printf( "The number of variables in too large.\n" );
610  return;
611  }
612 
613  if ( s_pRMan == NULL )
614  s_pRMan = Aig_RManStart();
615  s_pRMan->nTotal++;
616  // canonicize the function
617  pNtk = Kit_DsdDecompose( pTruth, nVarsInit );
618  pObj = Kit_DsdNonDsdPrimeMax( pNtk );
619  if ( pObj == NULL || pObj->nFans == 3 )
620  {
621  s_pRMan->nTtDsd++;
622  Kit_DsdNtkFree( pNtk );
623  return;
624  }
625  nVars = pObj->nFans;
626  s_pRMan->nVarFuncs[nVars]++;
627  if ( nVars < nVarsInit )
628  s_pRMan->nTtDsdPart++;
629  else
630  s_pRMan->nTtDsdNot++;
631  // compute the number of words
632  nWords = Abc_TruthWordNum( nVars );
633  // copy the function
634  memcpy( s_pRMan->pTruthInit, Kit_DsdObjTruth(pObj), 4*nWords );
635  Kit_DsdNtkFree( pNtk );
636  // canonicize the output
637  if ( s_pRMan->pTruthInit[0] & 1 )
638  Kit_TruthNot( s_pRMan->pTruthInit, s_pRMan->pTruthInit, nVars );
639  memcpy( s_pRMan->pTruth, s_pRMan->pTruthInit, 4*nWords );
640 
641  // canonize the function
642  for ( i = 0; i < nVars; i++ )
643  s_pRMan->pPerm[i] = i;
644  uPhaseC = Aig_RManSemiCanonicize( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPerm, s_pRMan->pMints, 1 );
645  // check unique variables
646  fUniqueVars = Aig_RManVarsAreUnique( s_pRMan->pMints, nVars );
647  s_pRMan->nUniqueVars += fUniqueVars;
648 
649 /*
650  printf( "%4d : ", s_pRMan->nTotal );
651  printf( "%2d %2d ", nVarsInit, nVars );
652  Extra_PrintBinary( stdout, &uPhaseC, nVars );
653  printf( " " );
654  for ( i = 0; i < nVars; i++ )
655  printf( "%2d/%2d ", s_pRMan->pMints[2*i], s_pRMan->pMints[2*i+1] );
656  printf( "\n" );
657  Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars );
658 Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n\n" );
659 */
660 /*
661  printf( "\n" );
662  printf( "%4d : ", s_pRMan->nTotal );
663  printf( "%2d %2d ", nVarsInit, nVars );
664  printf( " " );
665  printf( "\n" );
666  Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars );
667 // Aig_RManPrintSigs( s_pRMan->pMints, nVars );
668 */
669 
670 //Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n\n" );
671 
672  if ( Aig_RManTableFindOrAdd( s_pRMan, s_pRMan->pTruth, nVars ) )
673  Aig_RManSaveOne( s_pRMan, s_pRMan->pTruth, nVars );
674 
675  if ( fVerify )
676  {
677  // derive reverse permutation
678  for ( i = 0; i < nVars; i++ )
679  s_pRMan->pPermR[i] = s_pRMan->pPerm[i];
680  // implement permutation
681  Kit_TruthPermute( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPermR, 1 );
682  // implement polarity
683  for ( i = 0; i < nVars; i++ )
684  if ( uPhaseC & (1 << i) )
685  Kit_TruthChangePhase( s_pRMan->pTruth, nVars, i );
686 
687  // perform verification
688  if ( fUniqueVars && !Kit_TruthIsEqual( s_pRMan->pTruth, s_pRMan->pTruthInit, nVars ) )
689  printf( "Verification failed.\n" );
690  }
691 //Aig_RManPrintVarProfile( s_pRMan->pTruth, nVars, s_pRMan->pTruthTemp );
692 //Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n" );
693 }
694 
695 ////////////////////////////////////////////////////////////////////////
696 /// END OF FILE ///
697 ////////////////////////////////////////////////////////////////////////
698 
699 
700 ABC_NAMESPACE_IMPL_END
701 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Bdc_ManRoot
Bdc_Fun_t * Bdc_ManRoot(Bdc_Man_t *p)
Definition: bdcCore.c:47
Aig_RMan_t_::pAig
Aig_Man_t * pAig
Definition: aigCanon.c:57
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Aig_Tru_t_::nVars
unsigned nVars
Definition: aigCanon.c:49
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
Aig_Tru_t
struct Aig_Tru_t_ Aig_Tru_t
Definition: aigCanon.c:43
Aig_RManComputeVSigs
void Aig_RManComputeVSigs(unsigned *pTruth, int nVars, Aig_VSig_t *pSigs, unsigned *pAux)
Definition: aigCanon.c:382
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_RMan_t_::pPermR
char pPermR[RMAN_MAXVARS]
Definition: aigCanon.c:72
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Kit_TruthSwapAdjacentVars
void Kit_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int Start)
DECLARATIONS ///.
Definition: kitTruth.c:46
Aig_RMan_t_::nTtDsd
int nTtDsd
Definition: aigCanon.c:76
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Kit_DsdObj_t_::nFans
unsigned nFans
Definition: kit.h:116
Kit_TruthPermute
void Kit_TruthPermute(unsigned *pOut, unsigned *pIn, int nVars, char *pPerm, int fReturnIn)
Definition: kitTruth.c:233
Aig_RMan_t_::nTtDsdPart
int nTtDsdPart
Definition: aigCanon.c:77
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_MmFlexEntryFetch
char * Aig_MmFlexEntryFetch(Aig_MmFlex_t *p, int nBytes)
Definition: aigMem.c:366
Bdc_ManAlloc
Bdc_Man_t * Bdc_ManAlloc(Bdc_Par_t *pPars)
MACRO DEFINITIONS ///.
Definition: bdcCore.c:68
Aig_RMan_t_::pBins
Aig_Tru_t ** pBins
Definition: aigCanon.c:60
Kit_TruthChangePhase
void Kit_TruthChangePhase(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:1259
Aig_VSig_t_
Definition: aigCanon.c:37
memcpy
char * memcpy()
Kit_TruthCountOnesInCofsSlow
void Kit_TruthCountOnesInCofsSlow(unsigned *pTruth, int nVars, int *pStore, unsigned *pAux)
Definition: kitTruth.c:1537
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Kit_TruthIsEqual
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
Aig_RMan_t_::nUniqueVars
int nUniqueVars
Definition: aigCanon.c:79
Aig_RManPrintUniqueVars
void Aig_RManPrintUniqueVars(Aig_VSig_t *pMints, int nVars)
Definition: aigCanon.c:447
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
Aig_RManTableHash
static int Aig_RManTableHash(unsigned *pTruth, int nVars, int nBins, int *pPrimes)
Definition: aigCanon.c:130
Bdc_ManDecompose
int Bdc_ManDecompose(Bdc_Man_t *p, unsigned *puFunc, unsigned *puCare, int nVars, Vec_Ptr_t *vDivs, int nNodesMax)
Definition: bdcCore.c:291
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Kit_DsdNonDsdPrimeMax
Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1236
Aig_RMan_t_::pBidec
Bdc_Man_t * pBidec
Definition: aigCanon.c:64
nWords
int nWords
Definition: abcNpn.c:127
Aig_RManPrintVarProfile
void Aig_RManPrintVarProfile(unsigned *pTruth, int nVars, unsigned *pTruthAux)
Definition: aigCanon.c:308
Aig_Tru_t_::nVisits
unsigned nVisits
Definition: aigCanon.c:48
Kit_TruthCountOnesInCofs0
void Kit_TruthCountOnesInCofs0(unsigned *pTruth, int nVars, int *pStore)
Definition: kitTruth.c:1486
Kit_DsdDecompose
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2314
Aig_MmFlex_t_
Definition: aigMem.c:50
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_RManSortNums
void Aig_RManSortNums(int *pArray, int nVars)
Definition: aigCanon.c:329
s_pRMan
static Aig_RMan_t * s_pRMan
Definition: aigCanon.c:82
Bdc_ManFunc
Bdc_Fun_t * Bdc_ManFunc(Bdc_Man_t *p, int i)
DECLARATIONS ///.
Definition: bdcCore.c:46
Aig_RManStart
Aig_RMan_t * Aig_RManStart()
FUNCTION DEFINITIONS ///.
Definition: aigCanon.c:99
Aig_RManTableLookup
Aig_Tru_t ** Aig_RManTableLookup(Aig_RMan_t *p, unsigned *pTruth, int nVars)
Definition: aigCanon.c:150
Kit_DsdNtk_t_
Definition: kit.h:122
Kit_DsdObj_t_
Definition: kit.h:109
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
Aig_RManSemiCanonicize
unsigned Aig_RManSemiCanonicize(unsigned *pOut, unsigned *pIn, int nVars, char *pCanonPerm, Aig_VSig_t *pSigs, int fReturnIn)
Definition: aigCanon.c:479
Bdc_FuncSetCopy
void Bdc_FuncSetCopy(Bdc_Fun_t *p, void *pCopy)
Definition: bdcCore.c:54
Aig_Tru_t_::Id
int Id
Definition: aigCanon.c:47
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
Aig_Tru_t_::pNext
Aig_Tru_t * pNext
Definition: aigCanon.c:46
Aig_RManRecord
void Aig_RManRecord(unsigned *pTruth, int nVarsInit)
Definition: aigCanon.c:598
Aig_RMan_t_::pTruthTemp
unsigned pTruthTemp[RMAX_MAXWORD]
Definition: aigCanon.c:69
Aig_RManVarsAreUnique
int Aig_RManVarsAreUnique(Aig_VSig_t *pMints, int nVars)
Definition: aigCanon.c:427
Bdc_Fun_t
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition: bdc.h:42
Aig_RMan_t_::pMemTrus
Aig_MmFlex_t * pMemTrus
Definition: aigCanon.c:62
Aig_IthVar
Aig_Obj_t * Aig_IthVar(Aig_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition: aigOper.c:63
Aig_RMan_t_::nTotal
int nTotal
Definition: aigCanon.c:75
Kit_DsdObjTruth
static unsigned * Kit_DsdObjTruth(Kit_DsdObj_t *pObj)
Definition: kit.h:148
Aig_RMan_t_::nVarFuncs
int nVarFuncs[RMAN_MAXVARS+1]
Definition: aigCanon.c:74
Aig_VSig_t_::nOnes
int nOnes
Definition: aigCanon.c:39
Aig_RManTableResize
void Aig_RManTableResize(Aig_RMan_t *p)
Definition: aigCanon.c:174
RMAN_MAXVARS
#define RMAN_MAXVARS
DECLARATIONS ///.
Definition: aigCanon.c:33
Aig_RMan_t_::pTruthInit
unsigned pTruthInit[RMAX_MAXWORD]
Definition: aigCanon.c:66
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Kit_TruthCountOnes
static int Kit_TruthCountOnes(unsigned *pIn, int nVars)
Definition: kit.h:251
Aig_RManTableFindOrAdd
int Aig_RManTableFindOrAdd(Aig_RMan_t *p, unsigned *pTruth, int nVars)
Definition: aigCanon.c:218
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
memcmp
int memcmp()
Aig_Obj_t_
Definition: aig.h:69
sprintf
char * sprintf()
Aig_RMan_t_::pTruthC
unsigned pTruthC[RMAX_MAXWORD]
Definition: aigCanon.c:68
Aig_RManStop
void Aig_RManStop(Aig_RMan_t *p)
Definition: aigCanon.c:252
Counter
static int Counter
Definition: extraBddMisc.c:1877
Aig_RManSaveOne
void Aig_RManSaveOne(Aig_RMan_t *p, unsigned *pTruth, int nVars)
Definition: aigCanon.c:558
Aig_RMan_t_::nVars
int nVars
Definition: aigCanon.c:56
Aig_RMan_t_::pMints
Aig_VSig_t pMints[2 *RMAN_MAXVARS]
Definition: aigCanon.c:70
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Ioa_WriteAiger
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioaWriteAig.c:446
Aig_VSig_t_::nCofOnes
int nCofOnes[RMAN_MAXVARS]
Definition: aigCanon.c:40
Aig_RMan_t_::pTruth
unsigned pTruth[RMAX_MAXWORD]
Definition: aigCanon.c:67
Bdc_FuncFanin0
Bdc_Fun_t * Bdc_FuncFanin0(Bdc_Fun_t *p)
Definition: bdcCore.c:50
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_Tru_t_
Definition: aigCanon.c:44
Bdc_IsComplement
static int Bdc_IsComplement(Bdc_Fun_t *p)
Definition: bdc.h:54
Aig_RManPrintSigs
void Aig_RManPrintSigs(Aig_VSig_t *pSigs, int nVars)
Definition: aigCanon.c:353
Aig_Tru_t_::pTruth
unsigned pTruth[0]
Definition: aigCanon.c:50
Bdc_Par_t_
Definition: bdc.h:45
Aig_MmFlexStart
Aig_MmFlex_t * Aig_MmFlexStart()
Definition: aigMem.c:305
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Aig_MmFlexStop
void Aig_MmFlexStop(Aig_MmFlex_t *p, int fVerbose)
Definition: aigMem.c:337
Bdc_Man_t_
Definition: bdcInt.h:81
Kit_TruthCopy
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_RMan_t_::nEntries
int nEntries
Definition: aigCanon.c:61
Aig_RManCompareSigs
static int Aig_RManCompareSigs(Aig_VSig_t *p0, Aig_VSig_t *p1, int nVars)
Definition: aigCanon.c:410
Bdc_FunCopyHop
static Aig_Obj_t * Bdc_FunCopyHop(Bdc_Fun_t *pObj)
Definition: aigCanon.c:544
Kit_DsdNtkFree
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
Bdc_ManNodeNum
int Bdc_ManNodeNum(Bdc_Man_t *p)
Definition: bdcCore.c:48
assert
#define assert(ex)
Definition: util_old.h:213
Bdc_ManFree
void Bdc_ManFree(Bdc_Man_t *p)
Definition: bdcCore.c:113
Aig_RManQuit
void Aig_RManQuit()
Definition: aigCanon.c:283
Bdc_FuncFanin1
Bdc_Fun_t * Bdc_FuncFanin1(Bdc_Fun_t *p)
Definition: bdcCore.c:51
Bdc_FuncCopy
void * Bdc_FuncCopy(Bdc_Fun_t *p)
Definition: bdcCore.c:52
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Aig_RMan_t_::pPerm
char pPerm[RMAN_MAXVARS]
Definition: aigCanon.c:71
Bdc_Regular
static Bdc_Fun_t * Bdc_Regular(Bdc_Fun_t *p)
Definition: bdc.h:55
RMAX_MAXWORD
#define RMAX_MAXWORD
Definition: aigCanon.c:34
Aig_RMan_t_::nTtDsdNot
int nTtDsdNot
Definition: aigCanon.c:78
Aig_RMan_t_::nBins
int nBins
Definition: aigCanon.c:59
Aig_RMan_t_
Definition: aigCanon.c:54