ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaIso.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
26#define ISO_MASK 0xFF
27static unsigned 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
66
67typedef struct Gia_IsoMan_t_ Gia_IsoMan_t;
92
93static inline unsigned Gia_IsoGetValue( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i]); }
94static inline unsigned Gia_IsoGetItem( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i] >> 32); }
95
96static inline void Gia_IsoSetValue( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[0] = v; }
97static inline void Gia_IsoSetItem( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[1] = v; }
98
102
114Gia_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}
131void 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}
142void 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
163void 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}
181void 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
204void 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
265void 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
299int 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
386Vec_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
442static inline unsigned Gia_IsoUpdateValue( int Value, int fCompl )
443{
444 return (Value+1) * s_256Primes[Abc_Var2Lit(Value, fCompl) & ISO_MASK];
445}
446static 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}
453void 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}
480void 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
512void 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
554void 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
587void 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
631void 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
682void 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
720Vec_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
848int 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}
855void 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}
882void 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 (*)(const void *, const 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 (*)(const void *, const 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 (*)(const void *, const 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
958Gia_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
998Vec_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
1049int 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
1075Gia_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
1241void 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
1267Vec_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}
1280void 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, 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
1328
1329
1330ABC_NAMESPACE_IMPL_END
1331
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
Abc_QuickSort3
void Abc_QuickSort3(word *pData, int nSize, int fDecrease)
Definition utilSort.c:884
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
p
Cube * p
Definition exorList.c:222
Gia_IsoSort
int Gia_IsoSort(Gia_IsoMan_t *p)
Definition giaIso.c:299
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_IsoAssignOneClass2
void Gia_IsoAssignOneClass2(Gia_IsoMan_t *p)
Definition giaIso.c:512
Gia_IsoRecognizeMuxes
void Gia_IsoRecognizeMuxes(Gia_Man_t *pGia)
Definition giaIso.c:682
Gia_IsoDeriveEquivPos
Vec_Ptr_t * Gia_IsoDeriveEquivPos(Gia_Man_t *pGia, int fForward, int fVerbose)
Definition giaIso.c:720
Gia_IsoTest
void Gia_IsoTest(Gia_Man_t *p, Abc_Cex_t *pCex, int fVerbose)
Definition giaIso.c:1280
Gia_IsoAssignUnique
void Gia_IsoAssignUnique(Gia_IsoMan_t *p)
Definition giaIso.c:265
Gia_IsoTestOld
void Gia_IsoTestOld(Gia_Man_t *p, int fVerbose)
Definition giaIso.c:1241
Gia_IsoTestGenPerm
Vec_Int_t * Gia_IsoTestGenPerm(int nPis)
Definition giaIso.c:1267
Gia_IsoPrintClasses
void Gia_IsoPrintClasses(Gia_IsoMan_t *p)
Definition giaIso.c:163
Gia_IsoSimulate
void Gia_IsoSimulate(Gia_IsoMan_t *p, int Iter)
Definition giaIso.c:453
Gia_IsoReportTopmost
void Gia_IsoReportTopmost(Gia_IsoMan_t *p)
Definition giaIso.c:631
Gia_IsoManStop
void Gia_IsoManStop(Gia_IsoMan_t *p)
Definition giaIso.c:131
Gia_IsoCollectCosClasses
Vec_Ptr_t * Gia_IsoCollectCosClasses(Gia_IsoMan_t *p, int fVerbose)
Definition giaIso.c:386
Gia_ManFindCaninicalOrder_rec
void Gia_ManFindCaninicalOrder_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vAnds)
Definition giaIso.c:855
Gia_ManIsoFindString
Vec_Str_t * Gia_ManIsoFindString(Gia_Man_t *p, int iPo, int fVerbose, Vec_Int_t **pvPiPerm)
Definition giaIso.c:998
Gia_IsoManTransferUnique
void Gia_IsoManTransferUnique(Gia_IsoMan_t *p)
Definition giaIso.c:142
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
Gia_IsoMan_t
struct Gia_IsoMan_t_ Gia_IsoMan_t
DECLARATIONS ///.
Definition giaIso.c:67
Gia_IsoAssignOneClass3
void Gia_IsoAssignOneClass3(Gia_IsoMan_t *p)
Definition giaIso.c:554
Gia_IsoSimulateBack
void Gia_IsoSimulateBack(Gia_IsoMan_t *p, int Iter)
Definition giaIso.c:480
Gia_IsoManStart
Gia_IsoMan_t * Gia_IsoManStart(Gia_Man_t *pGia)
FUNCTION DEFINITIONS ///.
Definition giaIso.c:114
Gia_IsoPrepare
void Gia_IsoPrepare(Gia_IsoMan_t *p)
Definition giaIso.c:204
Gia_IsoAssignOneClass
void Gia_IsoAssignOneClass(Gia_IsoMan_t *p, int fVerbose)
Definition giaIso.c:587
Vec_IntCountNonTrivial
int Vec_IntCountNonTrivial(Vec_Ptr_t *vEquivs, int *pnUsed)
Definition giaIso.c:1049
Gia_ManIsoCanonicize
Gia_Man_t * Gia_ManIsoCanonicize(Gia_Man_t *p, int fVerbose)
Definition giaIso.c:958
Gia_IsoPrint
void Gia_IsoPrint(Gia_IsoMan_t *p, int Iter, abctime Time)
Definition giaIso.c:181
ISO_MASK
#define ISO_MASK
Definition giaIso.c:26
Gia_ObjCompareByValue
int Gia_ObjCompareByValue(Gia_Obj_t **pp1, Gia_Obj_t **pp2)
Definition giaIso.c:848
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition giaUtil.c:1056
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition gia.h:1250
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_AigerWriteIntoMemoryStr
Vec_Str_t * Gia_AigerWriteIntoMemoryStr(Gia_Man_t *p)
Definition giaAiger.c:1062
Gia_ManTransformMiter
Gia_Man_t * Gia_ManTransformMiter(Gia_Man_t *p)
Definition giaDup.c:3376
Gia_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition gia.h:1222
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManDupPerm
Gia_Man_t * Gia_ManDupPerm(Gia_Man_t *p, Vec_Int_t *vPiPerm)
Definition giaDup.c:929
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition giaUtil.c:982
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
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:4176
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManDupCones
Gia_Man_t * Gia_ManDupCones(Gia_Man_t *p, int *pPos, int nPos, int fTrimPis)
Definition giaDup.c:3880
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition giaUtil.c:351
Gia_ManSeqStructSweep
Gia_Man_t * Gia_ManSeqStructSweep(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition giaScl.c:258
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition giaCex.c:48
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Gia_ManDupAppendNew
Gia_Man_t * Gia_ManDupAppendNew(Gia_Man_t *pOne, Gia_Man_t *pTwo)
Definition giaDup.c:1174
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:1136
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Gia_IsoMan_t_
Definition giaIso.c:69
Gia_IsoMan_t_::timeStart
abctime timeStart
Definition giaIso.c:85
Gia_IsoMan_t_::nObjs
int nObjs
Definition giaIso.c:71
Gia_IsoMan_t_::pGia
Gia_Man_t * pGia
Definition giaIso.c:70
Gia_IsoMan_t_::timeOther
abctime timeOther
Definition giaIso.c:89
Gia_IsoMan_t_::vClasses2
Vec_Int_t * vClasses2
Definition giaIso.c:83
Gia_IsoMan_t_::vLevCounts
Vec_Int_t * vLevCounts
Definition giaIso.c:81
Gia_IsoMan_t_::timeSim
abctime timeSim
Definition giaIso.c:86
Gia_IsoMan_t_::vClasses
Vec_Int_t * vClasses
Definition giaIso.c:82
Gia_IsoMan_t_::pUniques
int * pUniques
Definition giaIso.c:77
Gia_IsoMan_t_::nEntries
int nEntries
Definition giaIso.c:74
Gia_IsoMan_t_::pStoreU
unsigned * pStoreU
Definition giaIso.c:79
Gia_IsoMan_t_::timeSort
abctime timeSort
Definition giaIso.c:88
Gia_IsoMan_t_::nSingles
int nSingles
Definition giaIso.c:73
Gia_IsoMan_t_::pStoreW
word * pStoreW
Definition giaIso.c:78
Gia_IsoMan_t_::pLevels
int * pLevels
Definition giaIso.c:76
Gia_IsoMan_t_::timeTotal
abctime timeTotal
Definition giaIso.c:90
Gia_IsoMan_t_::nUniques
int nUniques
Definition giaIso.c:72
Gia_IsoMan_t_::timeRefine
abctime timeRefine
Definition giaIso.c:87
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Abc_CexPermuteTwo
Abc_Cex_t * Abc_CexPermuteTwo(Abc_Cex_t *p, Vec_Int_t *vPermOld, Vec_Int_t *vPermNew)
Definition utilCex.c:526
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42