abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaIso.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaIso.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Graph isomorphism.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 #define ISO_MASK 0xFF
27 static int s_256Primes[ISO_MASK+1] =
28 {
29  0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
30  0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,
31  0x50d66b74,0x2f01ae9e,0xa1a80123,0x3e1ce2dc,0xebedbc57,0x4e68bc34,0x855ee0cf,0x17275120,
32  0x2ae7f2df,0xf71039eb,0x7c283eec,0x70cd1137,0x7cf651f3,0xa87bfa7a,0x14d87f02,0xe82e197d,
33  0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035,
34  0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10,
35  0x8fa783f7,0x252062ce,0x3dc46b4b,0xf70f6432,0x3f378276,0x44b137a1,0x2bf74b77,0x04892ed6,
36  0xfd318de1,0xd58c235e,0x94c6d25b,0x7aa5f218,0x35c9e921,0x5732fbbb,0x06026481,0xf584a44f,
37  0x946e1b5f,0x8463d5b2,0x4ebca7b2,0x54887b15,0x08d1e804,0x5b22067d,0x794580f6,0xb351ea43,
38  0xbce555b9,0x19ae2194,0xd32f1396,0x6fc1a7f1,0x1fd8a867,0x3a89fdb0,0xea49c61c,0x25f8a879,
39  0xde1e6437,0x7c74afca,0x8ba63e50,0xb1572074,0xe4655092,0xdb6f8b1c,0xc2955f3c,0x327f85ba,
40  0x60a17021,0x95bd261d,0xdea94f28,0x04528b65,0xbe0109cc,0x26dd5688,0x6ab2729d,0xc4f029ce,
41  0xacf7a0be,0x4c912f55,0x34c06e65,0x4fbb938e,0x1533fb5f,0x03da06bd,0x48262889,0xc2523d7d,
42  0x28a71d57,0x89f9713a,0xf574c551,0x7a99deb5,0x52834d91,0x5a6f4484,0xc67ba946,0x13ae698f,
43  0x3e390f34,0x34fc9593,0x894c7932,0x6cf414a3,0xdb7928ab,0x13a3b8a3,0x4b381c1d,0xa10b54cb,
44  0x55359d9d,0x35a3422a,0x58d1b551,0x0fd4de20,0x199eb3f4,0x167e09e2,0x3ee6a956,0x5371a7fa,
45  0xd424efda,0x74f521c5,0xcb899ff6,0x4a42e4f4,0x747917b6,0x4b08df0b,0x090c7a39,0x11e909e4,
46  0x258e2e32,0xd9fad92d,0x48fe5f69,0x0545cde6,0x55937b37,0x9b4ae4e4,0x1332b40e,0xc3792351,
47  0xaff982ef,0x4dba132a,0x38b81ef1,0x28e641bf,0x227208c1,0xec4bbe37,0xc4e1821c,0x512c9d09,
48  0xdaef1257,0xb63e7784,0x043e04d7,0x9c2cea47,0x45a0e59a,0x281315ca,0x849f0aac,0xa4071ed3,
49  0x0ef707b3,0xfe8dac02,0x12173864,0x471f6d46,0x24a53c0a,0x35ab9265,0xbbf77406,0xa2144e79,
50  0xb39a884a,0x0baf5b6d,0xcccee3dd,0x12c77584,0x2907325b,0xfd1adcd2,0xd16ee972,0x345ad6c1,
51  0x315ebe66,0xc7ad2b8d,0x99e82c8d,0xe52da8c8,0xba50f1d3,0x66689cd8,0x2e8e9138,0x43e15e74,
52  0xf1ced14d,0x188ec52a,0xe0ef3cbb,0xa958aedc,0x4107a1bc,0x5a9e7a3e,0x3bde939f,0xb5b28d5a,
53  0x596fe848,0xe85ad00c,0x0b6b3aae,0x44503086,0x25b5695c,0xc0c31dcd,0x5ee617f0,0x74d40c3a,
54  0xd2cb2b9f,0x1e19f5fa,0x81e24faf,0xa01ed68f,0xcee172fc,0x7fdf2e4d,0x002f4774,0x664f82dd,
55  0xc569c39a,0xa2d4dcbe,0xaadea306,0xa4c947bf,0xa413e4e3,0x81fb5486,0x8a404970,0x752c980c,
56  0x98d1d881,0x5c932c1e,0xeee65dfb,0x37592cdd,0x0fd4e65b,0xad1d383f,0x62a1452f,0x8872f68d,
57  0xb58c919b,0x345c8ee3,0xb583a6d6,0x43d72cb3,0x77aaa0aa,0xeb508242,0xf2db64f8,0x86294328,
58  0x82211731,0x1239a9d5,0x673ba5de,0xaf4af007,0x44203b19,0x2399d955,0xa175cd12,0x595928a7,
59  0x6918928b,0xde3126bb,0x6c99835c,0x63ba1fa2,0xdebbdff0,0x3d02e541,0xd6f7aac6,0xe80b4cd0,
60  0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d
61 };
62 
63 ////////////////////////////////////////////////////////////////////////
64 /// DECLARATIONS ///
65 ////////////////////////////////////////////////////////////////////////
66 
67 typedef struct Gia_IsoMan_t_ Gia_IsoMan_t;
68 struct Gia_IsoMan_t_
69 {
70  Gia_Man_t * pGia;
71  int nObjs;
72  int nUniques;
73  int nSingles;
74  int nEntries;
75  // internal data
76  int * pLevels;
77  int * pUniques;
78  word * pStoreW;
79  unsigned * pStoreU;
80  // equivalence classes
81  Vec_Int_t * vLevCounts;
82  Vec_Int_t * vClasses;
83  Vec_Int_t * vClasses2;
84  // statistics
85  abctime timeStart;
86  abctime timeSim;
87  abctime timeRefine;
88  abctime timeSort;
89  abctime timeOther;
90  abctime timeTotal;
91 };
92 
93 static inline unsigned Gia_IsoGetValue( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i]); }
94 static inline unsigned Gia_IsoGetItem( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i] >> 32); }
95 
96 static inline void Gia_IsoSetValue( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[0] = v; }
97 static inline void Gia_IsoSetItem( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[1] = v; }
98 
99 ////////////////////////////////////////////////////////////////////////
100 /// FUNCTION DEFINITIONS ///
101 ////////////////////////////////////////////////////////////////////////
102 
103 /**Function*************************************************************
104 
105  Synopsis []
106 
107  Description []
108 
109  SideEffects []
110 
111  SeeAlso []
112 
113 ***********************************************************************/
114 Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia )
115 {
116  Gia_IsoMan_t * p;
117  p = ABC_CALLOC( Gia_IsoMan_t, 1 );
118  p->pGia = pGia;
119  p->nObjs = Gia_ManObjNum( pGia );
120  p->nUniques = 1;
121  p->nEntries = p->nObjs;
122  // internal data
123  p->pLevels = ABC_CALLOC( int, p->nObjs );
124  p->pUniques = ABC_CALLOC( int, p->nObjs );
125  p->pStoreW = ABC_CALLOC( word, p->nObjs );
126  // class representation
127  p->vClasses = Vec_IntAlloc( p->nObjs/4 );
128  p->vClasses2 = Vec_IntAlloc( p->nObjs/4 );
129  return p;
130 }
131 void Gia_IsoManStop( Gia_IsoMan_t * p )
132 {
133  // class representation
134  Vec_IntFree( p->vClasses );
135  Vec_IntFree( p->vClasses2 );
136  // internal data
137  ABC_FREE( p->pLevels );
138  ABC_FREE( p->pUniques );
139  ABC_FREE( p->pStoreW );
140  ABC_FREE( p );
141 }
142 void Gia_IsoManTransferUnique( Gia_IsoMan_t * p )
143 {
144  Gia_Obj_t * pObj;
145  int i;
146  // copy unique numbers into the nodes
147  Gia_ManForEachObj( p->pGia, pObj, i )
148  pObj->Value = p->pUniques[i];
149 }
150 
151 
152 /**Function*************************************************************
153 
154  Synopsis []
155 
156  Description []
157 
158  SideEffects []
159 
160  SeeAlso []
161 
162 ***********************************************************************/
163 void Gia_IsoPrintClasses( Gia_IsoMan_t * p )
164 {
165  int fVerbose = 0;
166  int i, k, iBegin, nSize;
167  printf( "The total of %d classes:\n", Vec_IntSize(p->vClasses)/2 );
168  Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
169  {
170  printf( "%5d : (%3d,%3d) ", i/2, iBegin, nSize );
171  if ( fVerbose )
172  {
173  printf( "{" );
174  for ( k = 0; k < nSize; k++ )
175  printf( " %3d,%08x", Gia_IsoGetItem(p, iBegin+k), Gia_IsoGetValue(p, iBegin+k) );
176  printf( " }" );
177  }
178  printf( "\n" );
179  }
180 }
181 void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, abctime Time )
182 {
183  printf( "Iter %4d : ", Iter );
184  printf( "Entries =%8d. ", p->nEntries );
185 // printf( "Classes =%8d. ", Vec_IntSize(p->vClasses)/2 );
186  printf( "Uniques =%8d. ", p->nUniques );
187  printf( "Singles =%8d. ", p->nSingles );
188  printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
189  printf( "\n" );
190  fflush( stdout );
191 }
192 
193 /**Function*************************************************************
194 
195  Synopsis []
196 
197  Description []
198 
199  SideEffects []
200 
201  SeeAlso []
202 
203 ***********************************************************************/
204 void Gia_IsoPrepare( Gia_IsoMan_t * p )
205 {
206  Gia_Obj_t * pObj;
207  int * pLevBegins, * pLevSizes;
208  int i, iObj, MaxLev = 0;
209  // assign levels
210  p->pLevels[0] = 0;
211  Gia_ManForEachCi( p->pGia, pObj, i )
212  p->pLevels[Gia_ObjId(p->pGia, pObj)] = 0;
213  Gia_ManForEachAnd( p->pGia, pObj, i )
214  p->pLevels[i] = 1 + Abc_MaxInt( p->pLevels[Gia_ObjFaninId0(pObj, i)], p->pLevels[Gia_ObjFaninId1(pObj, i)] );
215  Gia_ManForEachCo( p->pGia, pObj, i )
216  {
217  iObj = Gia_ObjId(p->pGia, pObj);
218  p->pLevels[iObj] = 1 + p->pLevels[Gia_ObjFaninId0(pObj, iObj)]; // "1 +" is different!
219  MaxLev = Abc_MaxInt( MaxLev, p->pLevels[Gia_ObjId(p->pGia, pObj)] );
220  }
221 
222  // count nodes on each level
223  pLevSizes = ABC_CALLOC( int, MaxLev+1 );
224  for ( i = 1; i < p->nObjs; i++ )
225  pLevSizes[p->pLevels[i]]++;
226  // start classes
227  Vec_IntClear( p->vClasses );
228  Vec_IntPush( p->vClasses, 0 );
229  Vec_IntPush( p->vClasses, 1 );
230  // find beginning of each level
231  pLevBegins = ABC_CALLOC( int, MaxLev+2 );
232  pLevBegins[0] = 1;
233  for ( i = 0; i <= MaxLev; i++ )
234  {
235  assert( pLevSizes[i] > 0 ); // we do not allow AIG with a const node and no PIs
236  Vec_IntPush( p->vClasses, pLevBegins[i] );
237  Vec_IntPush( p->vClasses, pLevSizes[i] );
238  pLevBegins[i+1] = pLevBegins[i] + pLevSizes[i];
239  }
240  assert( pLevBegins[MaxLev+1] == p->nObjs );
241  // put them into the structure
242  for ( i = 1; i < p->nObjs; i++ )
243  Gia_IsoSetItem( p, pLevBegins[p->pLevels[i]]++, i );
244  ABC_FREE( pLevBegins );
245  ABC_FREE( pLevSizes );
246 /*
247  // print the results
248  for ( i = 0; i < p->nObjs; i++ )
249  printf( "%3d : (%d,%d)\n", i, Gia_IsoGetItem(p, i), Gia_IsoGetValue(p, i) );
250  printf( "\n" );
251 */
252 }
253 
254 /**Function*************************************************************
255 
256  Synopsis []
257 
258  Description []
259 
260  SideEffects []
261 
262  SeeAlso []
263 
264 ***********************************************************************/
265 void Gia_IsoAssignUnique( Gia_IsoMan_t * p )
266 {
267  int i, iBegin, nSize;
268  p->nSingles = 0;
269  Vec_IntClear( p->vClasses2 );
270  Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
271  {
272  if ( nSize == 1 )
273  {
274  assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
275  p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
276  p->nSingles++;
277  }
278  else
279  {
280  Vec_IntPush( p->vClasses2, iBegin );
281  Vec_IntPush( p->vClasses2, nSize );
282  }
283  }
284  ABC_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 );
285  p->nEntries -= p->nSingles;
286 }
287 
288 /**Function*************************************************************
289 
290  Synopsis []
291 
292  Description []
293 
294  SideEffects []
295 
296  SeeAlso []
297 
298 ***********************************************************************/
299 int Gia_IsoSort( Gia_IsoMan_t * p )
300 {
301  Gia_Obj_t * pObj, * pObj0;
302  int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew;
303  int fRefined = 0;
304  abctime clk;
305 
306  // go through the equiv classes
307  p->nSingles = 0;
308  Vec_IntClear( p->vClasses2 );
309  Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
310  {
311  assert( nSize > 1 );
312  fSameValue = 1;
313  pObj0 = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin) );
314  for ( k = 0; k < nSize; k++ )
315  {
316  pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
317  Gia_IsoSetValue( p, iBegin+k, pObj->Value );
318  if ( pObj->Value != pObj0->Value )
319  fSameValue = 0;
320  }
321  if ( fSameValue )
322  {
323  Vec_IntPush( p->vClasses2, iBegin );
324  Vec_IntPush( p->vClasses2, nSize );
325  continue;
326  }
327  fRefined = 1;
328  // sort objects
329  clk = Abc_Clock();
330  Abc_QuickSort3( p->pStoreW + iBegin, nSize, 0 );
331  p->timeSort += Abc_Clock() - clk;
332  // divide into new classes
333  iBeginOld = iBegin;
334  pObj0 = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin) );
335  for ( k = 1; k < nSize; k++ )
336  {
337  pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
338  if ( pObj0->Value == pObj->Value )
339  continue;
340  nSizeNew = iBegin + k - iBeginOld;
341  if ( nSizeNew == 1 )
342  {
343  assert( p->pUniques[Gia_IsoGetItem(p, iBeginOld)] == 0 );
344  p->pUniques[Gia_IsoGetItem(p, iBeginOld)] = p->nUniques++;
345  p->nSingles++;
346  }
347  else
348  {
349  Vec_IntPush( p->vClasses2, iBeginOld );
350  Vec_IntPush( p->vClasses2, nSizeNew );
351  }
352  iBeginOld = iBegin + k;
353  pObj0 = pObj;
354  }
355  // add the last one
356  nSizeNew = iBegin + k - iBeginOld;
357  if ( nSizeNew == 1 )
358  {
359  assert( p->pUniques[Gia_IsoGetItem(p, iBeginOld)] == 0 );
360  p->pUniques[Gia_IsoGetItem(p, iBeginOld)] = p->nUniques++;
361  p->nSingles++;
362  }
363  else
364  {
365  Vec_IntPush( p->vClasses2, iBeginOld );
366  Vec_IntPush( p->vClasses2, nSizeNew );
367  }
368  }
369 
370  ABC_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 );
371  p->nEntries -= p->nSingles;
372  return fRefined;
373 }
374 
375 /**Function*************************************************************
376 
377  Synopsis []
378 
379  Description []
380 
381  SideEffects []
382 
383  SeeAlso []
384 
385 ***********************************************************************/
386 Vec_Ptr_t * Gia_IsoCollectCosClasses( Gia_IsoMan_t * p, int fVerbose )
387 {
388  Vec_Ptr_t * vGroups;
389  Vec_Int_t * vLevel;
390  Gia_Obj_t * pObj;
391  int i, k, iBegin, nSize;
392  // add singletons
393  vGroups = Vec_PtrAlloc( 1000 );
394  Gia_ManForEachPo( p->pGia, pObj, i )
395  if ( p->pUniques[Gia_ObjId(p->pGia, pObj)] > 0 )
396  {
397  vLevel = Vec_IntAlloc( 1 );
398  Vec_IntPush( vLevel, i );
399  Vec_PtrPush( vGroups, vLevel );
400  }
401 
402  // add groups
403  Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
404  {
405  for ( k = 0; k < nSize; k++ )
406  {
407  pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
408  if ( Gia_ObjIsPo(p->pGia, pObj) )
409  break;
410  }
411  if ( k == nSize )
412  continue;
413  vLevel = Vec_IntAlloc( 8 );
414  for ( k = 0; k < nSize; k++ )
415  {
416  pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
417  if ( Gia_ObjIsPo(p->pGia, pObj) )
418  Vec_IntPush( vLevel, Gia_ObjCioId(pObj) );
419  }
420  Vec_PtrPush( vGroups, vLevel );
421  }
422  // canonicize order
423  Vec_PtrForEachEntry( Vec_Int_t *, vGroups, vLevel, i )
424  Vec_IntSort( vLevel, 0 );
425  Vec_VecSortByFirstInt( (Vec_Vec_t *)vGroups, 0 );
426 // Vec_VecFree( (Vec_Vec_t *)vGroups );
427 // return NULL;
428  return vGroups;
429 }
430 
431 /**Function*************************************************************
432 
433  Synopsis []
434 
435  Description []
436 
437  SideEffects []
438 
439  SeeAlso []
440 
441 ***********************************************************************/
442 static inline unsigned Gia_IsoUpdateValue( int Value, int fCompl )
443 {
444  return (Value+1) * s_256Primes[Abc_Var2Lit(Value, fCompl) & ISO_MASK];
445 }
446 static inline unsigned Gia_IsoUpdate( Gia_IsoMan_t * p, int Iter, int iObj, int fCompl )
447 {
448  if ( Iter == 0 ) return Gia_IsoUpdateValue( p->pLevels[iObj], fCompl );
449  if ( p->pUniques[iObj] > 0 ) return Gia_IsoUpdateValue( p->pUniques[iObj], fCompl );
450 // if ( p->pUniques[iObj] > 0 ) return Gia_IsoUpdateValue( 11, fCompl );
451  return 0;
452 }
453 void Gia_IsoSimulate( Gia_IsoMan_t * p, int Iter )
454 {
455  Gia_Obj_t * pObj, * pObjF;
456  int i, iObj;
457  // initialize constant, inputs, and flops in the first frame
458  Gia_ManConst0(p->pGia)->Value += s_256Primes[ISO_MASK];
459  Gia_ManForEachPi( p->pGia, pObj, i )
460  pObj->Value += s_256Primes[ISO_MASK-1];
461  if ( Iter == 0 )
462  Gia_ManForEachRo( p->pGia, pObj, i )
463  pObj->Value += s_256Primes[ISO_MASK-2];
464  // simulate nodes
465  Gia_ManForEachAnd( p->pGia, pObj, i )
466  {
467  pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj));
468  pObj->Value += Gia_ObjFanin1(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId1(pObj, i), Gia_ObjFaninC1(pObj));
469  }
470  // simulate COs
471  Gia_ManForEachCo( p->pGia, pObj, i )
472  {
473  iObj = Gia_ObjId(p->pGia, pObj);
474  pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj));
475  }
476  // transfer flop values
477  Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i )
478  pObj->Value += pObjF->Value;
479 }
480 void Gia_IsoSimulateBack( Gia_IsoMan_t * p, int Iter )
481 {
482  Gia_Obj_t * pObj, * pObjF;
483  int i, iObj;
484  // simulate COs
485  Gia_ManForEachCo( p->pGia, pObj, i )
486  {
487  iObj = Gia_ObjId(p->pGia, pObj);
488  Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, iObj, Gia_ObjFaninC0(pObj));
489  }
490  // simulate objects
491  Gia_ManForEachAndReverse( p->pGia, pObj, i )
492  {
493  Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC0(pObj));
494  Gia_ObjFanin1(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC1(pObj));
495  }
496  // transfer flop values
497  Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i )
498  pObjF->Value += pObj->Value;
499 }
500 
501 /**Function*************************************************************
502 
503  Synopsis []
504 
505  Description []
506 
507  SideEffects []
508 
509  SeeAlso []
510 
511 ***********************************************************************/
512 void Gia_IsoAssignOneClass2( Gia_IsoMan_t * p )
513 {
514  int i, iBegin = -1, nSize = -1;
515  // find two variable class
516  assert( Vec_IntSize(p->vClasses) > 0 );
517  Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
518  {
519  if ( nSize == 2 )
520  break;
521  }
522  assert( nSize > 1 );
523 
524  if ( nSize == 2 )
525  {
526  assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
527  p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
528  p->nSingles++;
529  p->nEntries--;
530 
531  assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 );
532  p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++;
533  p->nSingles++;
534  p->nEntries--;
535  }
536  else
537  {
538  assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
539  p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
540  p->nSingles++;
541  p->nEntries--;
542  }
543 
544  for ( ; i < Vec_IntSize(p->vClasses) - 2; i += 2 )
545  {
546  p->vClasses->pArray[i+0] = p->vClasses->pArray[i+2];
547  p->vClasses->pArray[i+1] = p->vClasses->pArray[i+3];
548  }
549  Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
550 
551  printf( "Broke ties in class %d of size %d at level %d.\n", i/2, nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
552 }
553 
554 void Gia_IsoAssignOneClass3( Gia_IsoMan_t * p )
555 {
556  int iBegin, nSize;
557  // find the last class
558  assert( Vec_IntSize(p->vClasses) > 0 );
559  iBegin = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
560  nSize = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 1 );
561  Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
562 
563  // assign the class
564  assert( nSize > 1 );
565  if ( nSize == 2 )
566  {
567  assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
568  p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
569  p->nSingles++;
570  p->nEntries--;
571 
572  assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 );
573  p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++;
574  p->nSingles++;
575  p->nEntries--;
576  }
577  else
578  {
579  assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
580  p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
581  p->nSingles++;
582  p->nEntries--;
583  }
584  printf( "Broke ties in last class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
585 }
586 
587 void Gia_IsoAssignOneClass( Gia_IsoMan_t * p, int fVerbose )
588 {
589  int i, k, iBegin0, iBegin, nSize, Shrink;
590  // find the classes with the highest level
591  assert( Vec_IntSize(p->vClasses) > 0 );
592  iBegin0 = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
593  for ( i = Vec_IntSize(p->vClasses) - 2; i >= 0; i -= 2 )
594  {
595  iBegin = Vec_IntEntry( p->vClasses, i );
596  if ( p->pLevels[Gia_IsoGetItem(p, iBegin)] != p->pLevels[Gia_IsoGetItem(p, iBegin0)] )
597  break;
598  }
599  i += 2;
600  assert( i >= 0 );
601  // assign all classes starting with this one
602  for ( Shrink = i; i < Vec_IntSize(p->vClasses); i += 2 )
603  {
604  iBegin = Vec_IntEntry( p->vClasses, i );
605  nSize = Vec_IntEntry( p->vClasses, i + 1 );
606  for ( k = 0; k < nSize; k++ )
607  {
608  assert( p->pUniques[Gia_IsoGetItem(p, iBegin+k)] == 0 );
609  p->pUniques[Gia_IsoGetItem(p, iBegin+k)] = p->nUniques++;
610 // Gia_ManObj(p->pGia, Gia_IsoGetItem(p, iBegin+k))->Value += s_256Primes[0]; /// new addition!!!
611  p->nSingles++;
612  p->nEntries--;
613  }
614  if ( fVerbose )
615  printf( "Broke ties in class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
616  }
617  Vec_IntShrink( p->vClasses, Shrink );
618 }
619 
620 /**Function*************************************************************
621 
622  Synopsis [Report topmost equiv nodes.]
623 
624  Description []
625 
626  SideEffects []
627 
628  SeeAlso []
629 
630 ***********************************************************************/
631 void Gia_IsoReportTopmost( Gia_IsoMan_t * p )
632 {
633  Gia_Obj_t * pObj;
634  int i, k, iBegin, nSize, Counter = 0;
635  // go through equivalence classes
636  Gia_ManIncrementTravId( p->pGia );
637  Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
638  {
639 // printf( "%d(%d) ", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
640  for ( k = 0; k < nSize; k++ )
641  {
642  pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p, iBegin+k) );
643  if ( Gia_ObjIsAnd(pObj) )
644  {
645  Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin0(pObj) );
646  Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin1(pObj) );
647  }
648  else if ( Gia_ObjIsRo(p->pGia, pObj) )
649  Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)) );
650  }
651  }
652 // printf( "\n" );
653 
654  // report non-labeled nodes
655  Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
656  {
657  for ( k = 0; k < nSize; k++ )
658  {
659  pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p, iBegin+k) );
660  if ( !Gia_ObjIsTravIdCurrent(p->pGia, pObj) )
661  {
662  printf( "%5d : ", ++Counter );
663  printf( "Obj %6d : Level = %4d. iBegin = %4d. Size = %4d.\n",
664  Gia_ObjId(p->pGia, pObj), p->pLevels[Gia_ObjId(p->pGia, pObj)], iBegin, nSize );
665  break;
666  }
667  }
668  }
669 }
670 
671 /**Function*************************************************************
672 
673  Synopsis []
674 
675  Description []
676 
677  SideEffects []
678 
679  SeeAlso []
680 
681 ***********************************************************************/
682 void Gia_IsoRecognizeMuxes( Gia_Man_t * pGia )
683 {
684  Gia_Obj_t * pObj, * pObjC, * pObj1, * pObj0;
685  int i;
686  Gia_ManForEachAnd( pGia, pObj, i )
687  {
688  if ( !Gia_ObjIsMuxType(pObj) )
689  continue;
690  pObjC = Gia_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
691  if ( Gia_Regular(pObj0) == Gia_Regular(pObj1) )
692  {
693  // this is XOR
694  Gia_Regular(pObj)->Value += s_256Primes[233];
695  Gia_Regular(pObjC)->Value += s_256Primes[234];
696  Gia_Regular(pObj0)->Value += s_256Primes[234];
697  }
698  else
699  {
700  // this is MUX
701  Gia_Regular(pObj)->Value += s_256Primes[235];
702  Gia_Regular(pObjC)->Value += s_256Primes[236];
703  Gia_Regular(pObj0)->Value += s_256Primes[237];
704  Gia_Regular(pObj1)->Value += s_256Primes[237];
705  }
706  }
707 }
708 
709 /**Function*************************************************************
710 
711  Synopsis []
712 
713  Description []
714 
715  SideEffects []
716 
717  SeeAlso []
718 
719 ***********************************************************************/
720 Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose )
721 {
722  int nIterMax = 10000;
723  int nFixedPoint = 1;
724  Gia_IsoMan_t * p;
725  Vec_Ptr_t * vEquivs = NULL;
726  int fRefined, fRefinedAll;
727  int i, c;
728  abctime clk = Abc_Clock(), clkTotal = Abc_Clock();
729  assert( Gia_ManCiNum(pGia) > 0 );
730  assert( Gia_ManPoNum(pGia) > 0 );
731 
732  Gia_ManCleanValue( pGia );
733  p = Gia_IsoManStart( pGia );
734  Gia_IsoPrepare( p );
735  Gia_IsoAssignUnique( p );
736  p->timeStart = Abc_Clock() - clk;
737  if ( fVerbose )
738  Gia_IsoPrint( p, 0, Abc_Clock() - clkTotal );
739 
740 // Gia_IsoRecognizeMuxes( pGia );
741 
742  i = 0;
743  if ( fForward )
744  {
745  for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
746  {
747  clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
748  clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
749  if ( fVerbose )
750  Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
751  }
752  }
753  else
754  {
755  while ( Vec_IntSize(p->vClasses) > 0 )
756  {
757  for ( fRefinedAll = 1; i < nIterMax && fRefinedAll; )
758  {
759  fRefinedAll = 0;
760  for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
761  {
762  clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
763  clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
764  if ( fVerbose )
765  Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
766  fRefinedAll |= fRefined;
767  }
768  for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
769  {
770  clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk;
771  clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
772  if ( fVerbose )
773  Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
774  fRefinedAll |= fRefined;
775  }
776  }
777  if ( !fRefinedAll )
778  break;
779  }
780 
781 // Gia_IsoReportTopmost( p );
782 
783  while ( Vec_IntSize(p->vClasses) > 0 )
784  {
785  Gia_IsoAssignOneClass( p, fVerbose );
786  for ( fRefinedAll = 1; i < nIterMax && fRefinedAll; )
787  {
788  fRefinedAll = 0;
789  for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 )
790  {
791  clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk;
792  clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
793  if ( fVerbose )
794  Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
795  fRefinedAll |= fRefined;
796  }
797  for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 )
798  {
799  clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
800  clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
801  if ( fVerbose )
802  Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
803  fRefinedAll |= fRefined;
804 // if ( fRefined )
805 // printf( "Refinedment happened.\n" );
806  }
807  }
808  }
809 
810  if ( fVerbose )
811  Gia_IsoPrint( p, i+2, Abc_Clock() - clkTotal );
812  }
813 // Gia_IsoPrintClasses( p );
814  if ( fVerbose )
815  {
816  p->timeTotal = Abc_Clock() - clkTotal;
817  p->timeOther = p->timeTotal - p->timeStart - p->timeSim - p->timeRefine;
818  ABC_PRTP( "Start ", p->timeStart, p->timeTotal );
819  ABC_PRTP( "Simulate ", p->timeSim, p->timeTotal );
820  ABC_PRTP( "Refine ", p->timeRefine-p->timeSort, p->timeTotal );
821  ABC_PRTP( "Sort ", p->timeSort, p->timeTotal );
822  ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
823  ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
824  }
825 
826  if ( Gia_ManPoNum(p->pGia) > 1 )
827  vEquivs = Gia_IsoCollectCosClasses( p, fVerbose );
828  Gia_IsoManTransferUnique( p );
829  Gia_IsoManStop( p );
830 
831  return vEquivs;
832 }
833 
834 
835 
836 
837 /**Function*************************************************************
838 
839  Synopsis [Finds canonical ordering of CIs/COs/nodes.]
840 
841  Description []
842 
843  SideEffects []
844 
845  SeeAlso []
846 
847 ***********************************************************************/
848 int Gia_ObjCompareByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 )
849 {
850  Gia_Obj_t * pObj1 = *pp1;
851  Gia_Obj_t * pObj2 = *pp2;
852 // assert( pObj1->Value != pObj2->Value );
853  return (int)pObj1->Value - (int)pObj2->Value;
854 }
855 void Gia_ManFindCaninicalOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vAnds )
856 {
857  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
858  return;
859  Gia_ObjSetTravIdCurrent(p, pObj);
860  assert( Gia_ObjIsAnd(pObj) );
861  if ( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) || !Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) )
862  {
863  Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
864  Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
865  }
866  else
867  {
868  assert( Gia_ObjFanin0(pObj)->Value != Gia_ObjFanin1(pObj)->Value );
869  if ( Gia_ObjFanin0(pObj)->Value < Gia_ObjFanin1(pObj)->Value )
870  {
871  Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
872  Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
873  }
874  else
875  {
876  Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
877  Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
878  }
879  }
880  Vec_IntPush( vAnds, Gia_ObjId(p, pObj) );
881 }
882 void Gia_ManFindCaninicalOrder( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, Vec_Int_t ** pvPiPerm )
883 {
884  Vec_Ptr_t * vTemp;
885  Gia_Obj_t * pObj;
886  int i;
887 
888  vTemp = Vec_PtrAlloc( 1000 );
889  Vec_IntClear( vCis );
890  Vec_IntClear( vAnds );
891  Vec_IntClear( vCos );
892 
893  // assign unique IDs to PIs
894  Vec_PtrClear( vTemp );
895  Gia_ManForEachPi( p, pObj, i )
896  Vec_PtrPush( vTemp, pObj );
897  Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
898  // create the result
899  Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
900  Vec_IntPush( vCis, Gia_ObjId(p, pObj) );
901  // remember PI permutation
902  if ( pvPiPerm )
903  {
904  *pvPiPerm = Vec_IntAlloc( Gia_ManPiNum(p) );
905  Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
906  Vec_IntPush( *pvPiPerm, Gia_ObjCioId(pObj) );
907  }
908 
909  // assign unique IDs to POs
910  if ( Gia_ManPoNum(p) == 1 )
911  Vec_IntPush( vCos, Gia_ObjId(p, Gia_ManPo(p, 0)) );
912  else
913  {
914  Vec_PtrClear( vTemp );
915  Gia_ManForEachPo( p, pObj, i )
916  {
917  pObj->Value = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
918  Vec_PtrPush( vTemp, pObj );
919  }
920  Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
921  Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
922  Vec_IntPush( vCos, Gia_ObjId(p, pObj) );
923  }
924 
925  // assign unique IDs to ROs
926  Vec_PtrClear( vTemp );
927  Gia_ManForEachRo( p, pObj, i )
928  Vec_PtrPush( vTemp, pObj );
929  Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
930  // create the result
931  Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
932  {
933  Vec_IntPush( vCis, Gia_ObjId(p, pObj) );
934  Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
935  }
936  Vec_PtrFree( vTemp );
937 
938  // assign unique IDs to internal nodes
939  Gia_ManIncrementTravId( p );
940  Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
941  Gia_ManForEachObjVec( vCis, p, pObj, i )
942  Gia_ObjSetTravIdCurrent( p, pObj );
943  Gia_ManForEachObjVec( vCos, p, pObj, i )
944  Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
945 }
946 
947 /**Function*************************************************************
948 
949  Synopsis []
950 
951  Description []
952 
953  SideEffects []
954 
955  SeeAlso []
956 
957 ***********************************************************************/
958 Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose )
959 {
960  Gia_Man_t * pRes = NULL;
961  Vec_Int_t * vCis, * vAnds, * vCos;
962  Vec_Ptr_t * vEquiv;
963  if ( Gia_ManCiNum(p) == 0 ) // const AIG
964  {
965  assert( Gia_ManPoNum(p) == 1 );
966  assert( Gia_ManObjNum(p) == 2 );
967  return Gia_ManDup(p);
968  }
969  // derive canonical values
970  vEquiv = Gia_IsoDeriveEquivPos( p, 0, fVerbose );
971  Vec_VecFreeP( (Vec_Vec_t **)&vEquiv );
972  // find canonical order of CIs/COs/nodes
973  // find canonical order
974  vCis = Vec_IntAlloc( Gia_ManCiNum(p) );
975  vAnds = Vec_IntAlloc( Gia_ManAndNum(p) );
976  vCos = Vec_IntAlloc( Gia_ManCoNum(p) );
977  Gia_ManFindCaninicalOrder( p, vCis, vAnds, vCos, NULL );
978  // derive the new AIG
979  pRes = Gia_ManDupFromVecs( p, vCis, vAnds, vCos, Gia_ManRegNum(p) );
980  // cleanup
981  Vec_IntFree( vCis );
982  Vec_IntFree( vAnds );
983  Vec_IntFree( vCos );
984  return pRes;
985 }
986 
987 /**Function*************************************************************
988 
989  Synopsis []
990 
991  Description []
992 
993  SideEffects []
994 
995  SeeAlso []
996 
997 ***********************************************************************/
998 Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_t ** pvPiPerm )
999 {
1000  Gia_Man_t * pPart;
1001  Vec_Ptr_t * vEquiv;
1002  Vec_Int_t * vCis, * vAnds, * vCos;
1003  Vec_Str_t * vStr;
1004  // duplicate
1005  pPart = Gia_ManDupCones( p, &iPo, 1, 1 );
1006 //Gia_ManPrint( pPart );
1007  assert( Gia_ManPoNum(pPart) == 1 );
1008  if ( Gia_ManCiNum(pPart) == 0 ) // const AIG
1009  {
1010  assert( Gia_ManPoNum(pPart) == 1 );
1011  assert( Gia_ManObjNum(pPart) == 2 );
1012  vStr = Gia_AigerWriteIntoMemoryStr( pPart );
1013  Gia_ManStop( pPart );
1014  if ( pvPiPerm )
1015  *pvPiPerm = Vec_IntAlloc( 0 );
1016  return vStr;
1017  }
1018  // derive canonical values
1019  vEquiv = Gia_IsoDeriveEquivPos( pPart, 0, fVerbose );
1020  Vec_VecFreeP( (Vec_Vec_t **)&vEquiv );
1021  // find canonical order
1022  vCis = Vec_IntAlloc( Gia_ManCiNum(pPart) );
1023  vAnds = Vec_IntAlloc( Gia_ManAndNum(pPart) );
1024  vCos = Vec_IntAlloc( Gia_ManCoNum(pPart) );
1025  Gia_ManFindCaninicalOrder( pPart, vCis, vAnds, vCos, pvPiPerm );
1026 //printf( "Internal: " );
1027 //Vec_IntPrint( vCis );
1028  // derive the AIGER string
1029  vStr = Gia_AigerWriteIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) );
1030  // cleanup
1031  Vec_IntFree( vCis );
1032  Vec_IntFree( vAnds );
1033  Vec_IntFree( vCos );
1034  Gia_ManStop( pPart );
1035  return vStr;
1036 }
1037 
1038 /**Function*************************************************************
1039 
1040  Synopsis []
1041 
1042  Description []
1043 
1044  SideEffects []
1045 
1046  SeeAlso []
1047 
1048 ***********************************************************************/
1049 int Vec_IntCountNonTrivial( Vec_Ptr_t * vEquivs, int * pnUsed )
1050 {
1051  Vec_Int_t * vClass;
1052  int i, nClasses = 0;
1053  *pnUsed = 0;
1054  Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vClass, i )
1055  {
1056  if ( Vec_IntSize(vClass) < 2 )
1057  continue;
1058  nClasses++;
1059  (*pnUsed) += Vec_IntSize(vClass);
1060  }
1061  return nClasses;
1062 }
1063 
1064 /**Function*************************************************************
1065 
1066  Synopsis []
1067 
1068  Description []
1069 
1070  SideEffects []
1071 
1072  SeeAlso []
1073 
1074 ***********************************************************************/
1075 Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose )
1076 {
1077  Gia_Man_t * p, * pPart;
1078  Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings;
1079  Vec_Int_t * vRemain, * vLevel, * vLevel2;
1080  Vec_Str_t * vStr, * vStr2;
1081  int i, k, s, sStart, iPo, Counter;
1082  int nClasses, nUsedPos;
1083  abctime clk = Abc_Clock();
1084  if ( pvPosEquivs )
1085  *pvPosEquivs = NULL;
1086  if ( pvPiPerms )
1087  *pvPiPerms = Vec_PtrStart( Gia_ManPoNum(pInit) );
1088 
1089  if ( fDualOut )
1090  {
1091  assert( (Gia_ManPoNum(pInit) & 1) == 0 );
1092  if ( Gia_ManPoNum(pInit) == 2 )
1093  return Gia_ManDup(pInit);
1094  p = Gia_ManTransformMiter( pInit );
1095  p = Gia_ManSeqStructSweep( pPart = p, 1, 1, 0 );
1096  Gia_ManStop( pPart );
1097  }
1098  else
1099  {
1100  if ( Gia_ManPoNum(pInit) == 1 )
1101  return Gia_ManDup(pInit);
1102  p = pInit;
1103  }
1104 
1105  // create preliminary equivalences
1106  vEquivs = Gia_IsoDeriveEquivPos( p, 1, fVeryVerbose );
1107  if ( vEquivs == NULL )
1108  {
1109  if ( fDualOut )
1110  Gia_ManStop( p );
1111  return NULL;
1112  }
1113  nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos );
1114  printf( "Reduced %d outputs to %d candidate classes (%d outputs are in %d non-trivial classes). ",
1115  Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
1116  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1117  if ( fEstimate )
1118  {
1119  Vec_VecFree( (Vec_Vec_t *)vEquivs );
1120  return Gia_ManDup(pInit);
1121  }
1122 
1123  // perform refinement of equivalence classes
1124  Counter = 0;
1125  vEquivs2 = Vec_PtrAlloc( 100 );
1126  Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
1127  {
1128  if ( Vec_IntSize(vLevel) < 2 )
1129  {
1130  Vec_PtrPush( vEquivs2, Vec_IntDup(vLevel) );
1131  for ( k = 0; k < Vec_IntSize(vLevel); k++ )
1132  if ( ++Counter % 100 == 0 )
1133  printf( "%6d finished...\r", Counter );
1134  continue;
1135  }
1136 
1137  if ( fVerbose )
1138  {
1139  iPo = Vec_IntEntry(vLevel, 0);
1140  printf( "%6d %6d %6d : ", i, Vec_IntSize(vLevel), iPo );
1141  pPart = Gia_ManDupCones( p, &iPo, 1, 1 );
1142  Gia_ManPrintStats(pPart, NULL);
1143  Gia_ManStop( pPart );
1144  }
1145 
1146  sStart = Vec_PtrSize( vEquivs2 );
1147  vStrings = Vec_PtrAlloc( 100 );
1148  Vec_IntForEachEntry( vLevel, iPo, k )
1149  {
1150  if ( ++Counter % 100 == 0 )
1151  printf( "%6d finished...\r", Counter );
1152  assert( pvPiPerms == NULL || Vec_PtrArray(*pvPiPerms)[iPo] == NULL );
1153  vStr = Gia_ManIsoFindString( p, iPo, 0, pvPiPerms ? (Vec_Int_t **)Vec_PtrArray(*pvPiPerms) + iPo : NULL );
1154 
1155 // printf( "Output %2d : ", iPo );
1156 // Vec_IntPrint( Vec_PtrArray(*pvPiPerms)[iPo] );
1157 
1158  // check if this string already exists
1159  Vec_PtrForEachEntry( Vec_Str_t *, vStrings, vStr2, s )
1160  if ( Vec_StrCompareVec(vStr, vStr2) == 0 )
1161  break;
1162  if ( s == Vec_PtrSize(vStrings) )
1163  {
1164  Vec_PtrPush( vStrings, vStr );
1165  Vec_PtrPush( vEquivs2, Vec_IntAlloc(8) );
1166  }
1167  else
1168  Vec_StrFree( vStr );
1169  // add this entry to the corresponding level
1170  vLevel2 = (Vec_Int_t *)Vec_PtrEntry( vEquivs2, sStart + s );
1171  Vec_IntPush( vLevel2, iPo );
1172  }
1173 // if ( Vec_PtrSize(vEquivs2) - sStart > 1 )
1174 // printf( "Refined class %d into %d classes.\n", i, Vec_PtrSize(vEquivs2) - sStart );
1175  Vec_VecFree( (Vec_Vec_t *)vStrings );
1176  }
1177  assert( Counter == Gia_ManPoNum(p) );
1178  Vec_VecSortByFirstInt( (Vec_Vec_t *)vEquivs2, 0 );
1179  Vec_VecFree( (Vec_Vec_t *)vEquivs );
1180  vEquivs = vEquivs2;
1181 
1182  // collect the first ones
1183  vRemain = Vec_IntAlloc( 100 );
1184  Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
1185  Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) );
1186 
1187  if ( fDualOut )
1188  {
1189  Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vRemain) );
1190  int i, Entry;
1191  Vec_IntForEachEntry( vRemain, Entry, i )
1192  {
1193 // printf( "%d ", Entry );
1194  Vec_IntPush( vTemp, 2*Entry );
1195  Vec_IntPush( vTemp, 2*Entry+1 );
1196  }
1197 // printf( "\n" );
1198  Vec_IntFree( vRemain );
1199  vRemain = vTemp;
1200  Gia_ManStop( p );
1201  p = pInit;
1202  }
1203 
1204 
1205  // derive the resulting AIG
1206  pPart = Gia_ManDupCones( p, Vec_IntArray(vRemain), Vec_IntSize(vRemain), 0 );
1207  Vec_IntFree( vRemain );
1208  // report the results
1209  nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos );
1210  if ( !fDualOut )
1211  printf( "Reduced %d outputs to %d equivalence classes (%d outputs are in %d non-trivial classes). ",
1212  Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
1213  else
1214  printf( "Reduced %d dual outputs to %d dual outputs. ", Gia_ManPoNum(p)/2, Gia_ManPoNum(pPart)/2 );
1215  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1216  if ( fVerbose )
1217  {
1218  printf( "Nontrivial classes:\n" );
1219  Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
1220  }
1221  if ( pvPosEquivs )
1222  *pvPosEquivs = vEquivs;
1223  else
1224  Vec_VecFree( (Vec_Vec_t *)vEquivs );
1225 // Gia_ManStopP( &pPart );
1226  return pPart;
1227 }
1228 
1229 
1230 /**Function*************************************************************
1231 
1232  Synopsis []
1233 
1234  Description []
1235 
1236  SideEffects []
1237 
1238  SeeAlso []
1239 
1240 ***********************************************************************/
1241 void Gia_IsoTestOld( Gia_Man_t * p, int fVerbose )
1242 {
1243  Vec_Ptr_t * vEquivs;
1244  abctime clk = Abc_Clock();
1245  vEquivs = Gia_IsoDeriveEquivPos( p, 0, fVerbose );
1246  printf( "Reduced %d outputs to %d. ", Gia_ManPoNum(p), vEquivs ? Vec_PtrSize(vEquivs) : 1 );
1247  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1248  if ( fVerbose && vEquivs && Gia_ManPoNum(p) != Vec_PtrSize(vEquivs) )
1249  {
1250  printf( "Nontrivial classes:\n" );
1251 // Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
1252  }
1253  Vec_VecFreeP( (Vec_Vec_t **)&vEquivs );
1254 }
1255 
1256 /**Function*************************************************************
1257 
1258  Synopsis [Test remapping of CEXes for isomorphic POs.]
1259 
1260  Description []
1261 
1262  SideEffects []
1263 
1264  SeeAlso []
1265 
1266 ***********************************************************************/
1267 Vec_Int_t * Gia_IsoTestGenPerm( int nPis )
1268 {
1269  Vec_Int_t * vPerm;
1270  int i, * pArray;
1271  vPerm = Vec_IntStartNatural( nPis );
1272  pArray = Vec_IntArray( vPerm );
1273  for ( i = 0; i < nPis; i++ )
1274  {
1275  int iNew = rand() % nPis;
1276  ABC_SWAP( int, pArray[i], pArray[iNew] );
1277  }
1278  return vPerm;
1279 }
1280 void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
1281 {
1282  Abc_Cex_t * pCexNew;
1283  Vec_Int_t * vPiPerm;
1284  Vec_Ptr_t * vPosEquivs, * vPisPerm;
1285  Vec_Int_t * vPerm0, * vPerm1;
1286  Gia_Man_t * pPerm, * pDouble, * pAig;
1287  assert( Gia_ManPoNum(p) == 1 );
1288  assert( Gia_ManRegNum(p) > 0 );
1289  // generate random permutation of PIs
1290  vPiPerm = Gia_IsoTestGenPerm( Gia_ManPiNum(p) );
1291  printf( "Considering random permutation of the primary inputs of the AIG:\n" );
1292  Vec_IntPrint( vPiPerm );
1293  // create AIG with two primary outputs (original and permuted)
1294  pPerm = Gia_ManDupPerm( p, vPiPerm );
1295  pDouble = Gia_ManDupAppendNew( p, pPerm );
1296 //Gia_AigerWrite( pDouble, "test.aig", 0, 0 );
1297 
1298  // analyze the two-output miter
1299  pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0, 0 );
1300  Vec_VecFree( (Vec_Vec_t *)vPosEquivs );
1301 
1302  // given CEX for output 0, derive CEX for output 1
1303  vPerm0 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 0 );
1304  vPerm1 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 1 );
1305  pCexNew = Abc_CexPermuteTwo( pCex, vPerm0, vPerm1 );
1306  Vec_VecFree( (Vec_Vec_t *)vPisPerm );
1307 
1308  // check that original CEX and the resulting CEX is valid
1309  if ( Gia_ManVerifyCex(p, pCex, 0) )
1310  printf( "CEX for the init AIG is valid.\n" );
1311  else
1312  printf( "CEX for the init AIG is not valid.\n" );
1313  if ( Gia_ManVerifyCex(pPerm, pCexNew, 0) )
1314  printf( "CEX for the perm AIG is valid.\n" );
1315  else
1316  printf( "CEX for the perm AIG is not valid.\n" );
1317  // delete
1318  Gia_ManStop( pAig );
1319  Gia_ManStop( pDouble );
1320  Gia_ManStop( pPerm );
1321  Vec_IntFree( vPiPerm );
1322  Abc_CexFree( pCexNew );
1323 }
1324 
1325 ////////////////////////////////////////////////////////////////////////
1326 /// END OF FILE ///
1327 ////////////////////////////////////////////////////////////////////////
1328 
1329 
1330 ABC_NAMESPACE_IMPL_END
1331 
ISO_MASK
#define ISO_MASK
Definition: giaIso.c:26
Gia_ManIsoReduce
Gia_Man_t * Gia_ManIsoReduce(Gia_Man_t *pInit, Vec_Ptr_t **pvPosEquivs, Vec_Ptr_t **pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose)
Definition: giaIso.c:1075
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_IsoMan_t_::pUniques
int * pUniques
Definition: giaIso.c:77
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Gia_IsoMan_t_::timeStart
abctime timeStart
Definition: giaIso.c:85
Gia_IsoMan_t_::vClasses2
Vec_Int_t * vClasses2
Definition: giaIso.c:83
Gia_ManDupCones
Gia_Man_t * Gia_ManDupCones(Gia_Man_t *p, int *pPos, int nPos, int fTrimPis)
Definition: giaDup.c:2691
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_IsoAssignOneClass
void Gia_IsoAssignOneClass(Gia_IsoMan_t *p, int fVerbose)
Definition: giaIso.c:587
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManTransformMiter
Gia_Man_t * Gia_ManTransformMiter(Gia_Man_t *p)
Definition: giaDup.c:2324
Gia_ManFindCaninicalOrder_rec
void Gia_ManFindCaninicalOrder_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vAnds)
Definition: giaIso.c:855
Vec_IntDup
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Gia_IsoMan_t_::nSingles
int nSingles
Definition: giaIso.c:73
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Gia_IsoManStop
void Gia_IsoManStop(Gia_IsoMan_t *p)
Definition: giaIso.c:131
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManIsoCanonicize
Gia_Man_t * Gia_ManIsoCanonicize(Gia_Man_t *p, int fVerbose)
Definition: giaIso.c:958
Gia_ManDupPerm
Gia_Man_t * Gia_ManDupPerm(Gia_Man_t *p, Vec_Int_t *vPiPerm)
Definition: giaDup.c:632
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Gia_IsoMan_t_::pGia
Gia_Man_t * pGia
Definition: giaIso.c:70
Gia_IsoSetValue
static void Gia_IsoSetValue(Gia_IsoMan_t *p, int i, unsigned v)
Definition: giaIso.c:96
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Gia_IsoSort
int Gia_IsoSort(Gia_IsoMan_t *p)
Definition: giaIso.c:299
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition: giaUtil.c:310
Gia_IsoAssignOneClass2
void Gia_IsoAssignOneClass2(Gia_IsoMan_t *p)
Definition: giaIso.c:512
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_PtrSort
static void Vec_PtrSort(Vec_Ptr_t *p, int(*Vec_PtrSortCompare)()) ___unused
Definition: vecPtr.h:851
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Gia_IsoPrintClasses
void Gia_IsoPrintClasses(Gia_IsoMan_t *p)
Definition: giaIso.c:163
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Gia_IsoTestGenPerm
Vec_Int_t * Gia_IsoTestGenPerm(int nPis)
Definition: giaIso.c:1267
Vec_IntStartNatural
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Definition: bblif.c:192
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
Gia_IsoAssignUnique
void Gia_IsoAssignUnique(Gia_IsoMan_t *p)
Definition: giaIso.c:265
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_ManDupFromVecs
Gia_Man_t * Gia_ManDupFromVecs(Gia_Man_t *p, Vec_Int_t *vCis, Vec_Int_t *vAnds, Vec_Int_t *vCos, int nRegs)
Definition: giaDup.c:2853
Gia_IsoAssignOneClass3
void Gia_IsoAssignOneClass3(Gia_IsoMan_t *p)
Definition: giaIso.c:554
Gia_ManFindCaninicalOrder
void Gia_ManFindCaninicalOrder(Gia_Man_t *p, Vec_Int_t *vCis, Vec_Int_t *vAnds, Vec_Int_t *vCos, Vec_Int_t **pvPiPerm)
Definition: giaIso.c:882
Gia_Obj_t_
Definition: gia.h:75
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Gia_IsoManStart
Gia_IsoMan_t * Gia_IsoManStart(Gia_Man_t *pGia)
FUNCTION DEFINITIONS ///.
Definition: giaIso.c:114
Gia_IsoCollectCosClasses
Vec_Ptr_t * Gia_IsoCollectCosClasses(Gia_IsoMan_t *p, int fVerbose)
Definition: giaIso.c:386
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_ManDupAppendNew
Gia_Man_t * Gia_ManDupAppendNew(Gia_Man_t *pOne, Gia_Man_t *pTwo)
Definition: giaDup.c:783
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_IsoGetItem
static unsigned Gia_IsoGetItem(Gia_IsoMan_t *p, int i)
Definition: giaIso.c:94
Gia_IsoMan_t_::pStoreU
unsigned * pStoreU
Definition: giaIso.c:79
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_IsoTestOld
void Gia_IsoTestOld(Gia_Man_t *p, int fVerbose)
Definition: giaIso.c:1241
Gia_IsoMan_t_::pLevels
int * pLevels
Definition: giaIso.c:76
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_IsoMan_t_::nObjs
int nObjs
Definition: giaIso.c:71
Gia_AigerWriteIntoMemoryStrPart
Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart(Gia_Man_t *p, Vec_Int_t *vCis, Vec_Int_t *vAnds, Vec_Int_t *vCos, int nRegs)
Definition: giaAiger.c:940
Vec_IntCountNonTrivial
int Vec_IntCountNonTrivial(Vec_Ptr_t *vEquivs, int *pnUsed)
Definition: giaIso.c:1049
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Gia_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition: gia.h:1010
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Gia_IsoPrint
void Gia_IsoPrint(Gia_IsoMan_t *p, int Iter, abctime Time)
Definition: giaIso.c:181
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_VecPrintInt
static void Vec_VecPrintInt(Vec_Vec_t *p, int fSkipSingles)
Definition: vecVec.h:616
s_256Primes
static int s_256Primes[ISO_MASK+1]
Definition: giaIso.c:27
Vec_VecSortByFirstInt
static void Vec_VecSortByFirstInt(Vec_Vec_t *p, int fReverse)
Definition: vecVec.h:595
Gia_IsoMan_t_::pStoreW
word * pStoreW
Definition: giaIso.c:78
Gia_ManIsoFindString
Vec_Str_t * Gia_ManIsoFindString(Gia_Man_t *p, int iPo, int fVerbose, Vec_Int_t **pvPiPerm)
Definition: giaIso.c:998
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ManSeqStructSweep
Gia_Man_t * Gia_ManSeqStructSweep(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition: giaScl.c:258
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_QuickSort3
void Abc_QuickSort3(word *pData, int nSize, int fDecrease)
Definition: utilSort.c:680
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_IsoMan_t_
Definition: giaIso.c:68
Gia_IsoUpdate
static unsigned Gia_IsoUpdate(Gia_IsoMan_t *p, int Iter, int iObj, int fCompl)
Definition: giaIso.c:446
Gia_IsoTest
void Gia_IsoTest(Gia_Man_t *p, Abc_Cex_t *pCex, int fVerbose)
Definition: giaIso.c:1280
Gia_IsoSimulate
void Gia_IsoSimulate(Gia_IsoMan_t *p, int Iter)
Definition: giaIso.c:453
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Gia_IsoMan_t_::vLevCounts
Vec_Int_t * vLevCounts
Definition: giaIso.c:81
Gia_IsoGetValue
static unsigned Gia_IsoGetValue(Gia_IsoMan_t *p, int i)
Definition: giaIso.c:93
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition: vecInt.h:66
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Gia_IsoMan_t_::timeOther
abctime timeOther
Definition: giaIso.c:89
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Gia_IsoSimulateBack
void Gia_IsoSimulateBack(Gia_IsoMan_t *p, int Iter)
Definition: giaIso.c:480
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_IsoMan_t_::nEntries
int nEntries
Definition: giaIso.c:74
Vec_StrCompareVec
static int Vec_StrCompareVec(Vec_Str_t *p1, Vec_Str_t *p2)
Definition: vecStr.h:793
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Vec_Str_t_
Definition: bblif.c:47
Gia_IsoManTransferUnique
void Gia_IsoManTransferUnique(Gia_IsoMan_t *p)
Definition: giaIso.c:142
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gia_IsoRecognizeMuxes
void Gia_IsoRecognizeMuxes(Gia_Man_t *pGia)
Definition: giaIso.c:682
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ObjCompareByValue
int Gia_ObjCompareByValue(Gia_Obj_t **pp1, Gia_Obj_t **pp2)
Definition: giaIso.c:848
Gia_IsoUpdateValue
static unsigned Gia_IsoUpdateValue(int Value, int fCompl)
Definition: giaIso.c:442
Gia_ObjIsPo
static int Gia_ObjIsPo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:442
Abc_CexPermuteTwo
Abc_Cex_t * Abc_CexPermuteTwo(Abc_Cex_t *p, Vec_Int_t *vPermOld, Vec_Int_t *vPermNew)
Definition: utilCex.c:515
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Vec_VecFreeP
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_IsoSetItem
static void Gia_IsoSetItem(Gia_IsoMan_t *p, int i, unsigned v)
Definition: giaIso.c:97
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Vec_IntPrint
static void Vec_IntPrint(Vec_Int_t *vVec)
Definition: vecInt.h:1803
Gia_IsoReportTopmost
void Gia_IsoReportTopmost(Gia_IsoMan_t *p)
Definition: giaIso.c:631
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_IsoMan_t_::vClasses
Vec_Int_t * vClasses
Definition: giaIso.c:82
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_IsoPrepare
void Gia_IsoPrepare(Gia_IsoMan_t *p)
Definition: giaIso.c:204
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_IsoMan_t_::timeSim
abctime timeSim
Definition: giaIso.c:86
Gia_AigerWriteIntoMemoryStr
Vec_Str_t * Gia_AigerWriteIntoMemoryStr(Gia_Man_t *p)
Definition: giaAiger.c:866
Vec_PtrArray
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_IsoMan_t_::timeTotal
abctime timeTotal
Definition: giaIso.c:90
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_IsoMan_t_::timeSort
abctime timeSort
Definition: giaIso.c:88
Gia_IsoMan_t_::timeRefine
abctime timeRefine
Definition: giaIso.c:87
Gia_IsoDeriveEquivPos
Vec_Ptr_t * Gia_IsoDeriveEquivPos(Gia_Man_t *pGia, int fForward, int fVerbose)
Definition: giaIso.c:720
Gia_IsoMan_t_::nUniques
int nUniques
Definition: giaIso.c:72
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387