ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaEquiv.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "proof/cec/cec.h"
23#include "sat/bmc/bmc.h"
24
25ABC_NAMESPACE_IMPL_START
26
30
34
46void Gia_ManOrigIdsInit( Gia_Man_t * p )
47{
48 Vec_IntFreeP( &p->vIdsOrig );
49 p->vIdsOrig = Vec_IntStartNatural( Gia_ManObjNum(p) );
50}
51void Gia_ManOrigIdsStart( Gia_Man_t * p )
52{
53 Vec_IntFreeP( &p->vIdsOrig );
54 p->vIdsOrig = Vec_IntStartFull( Gia_ManObjNum(p) );
55}
56void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew )
57{
58 Gia_Obj_t * pObj; int i;
59 if ( p->vIdsOrig == NULL )
60 return;
61 Gia_ManOrigIdsStart( pNew );
62 Vec_IntWriteEntry( pNew->vIdsOrig, 0, 0 );
63 Gia_ManForEachObj1( p, pObj, i )
64 if ( ~pObj->Value && Abc_Lit2Var(pObj->Value) && Vec_IntEntry(p->vIdsOrig, i) != -1 && Vec_IntEntry(pNew->vIdsOrig, Abc_Lit2Var(pObj->Value)) == -1 )
65 Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pObj->Value), Vec_IntEntry(p->vIdsOrig, i) );
66 Gia_ManForEachObj( pNew, pObj, i )
67 assert( Vec_IntEntry(pNew->vIdsOrig, i) >= 0 );
68}
69// input is a set of equivalent node pairs in any order
70// output is the mapping of each node into the equiv node with the smallest ID
71void Gia_ManOrigIdsRemapPairsInsert( Vec_Int_t * vMap, int One, int Two )
72{
73 int Smo = One < Two ? One : Two;
74 int Big = One < Two ? Two : One;
75 assert( Smo != Big );
76 if ( Vec_IntEntry(vMap, Big) == -1 )
77 Vec_IntWriteEntry( vMap, Big, Smo );
78 else
79 Gia_ManOrigIdsRemapPairsInsert( vMap, Smo, Vec_IntEntry(vMap, Big) );
80}
81int Gia_ManOrigIdsRemapPairsExtract( Vec_Int_t * vMap, int One )
82{
83 if ( Vec_IntEntry(vMap, One) == -1 )
84 return One;
85 return Gia_ManOrigIdsRemapPairsExtract( vMap, Vec_IntEntry(vMap, One) );
86}
87Vec_Int_t * Gia_ManOrigIdsRemapPairs( Vec_Int_t * vEquivPairs, int nObjs )
88{
89 Vec_Int_t * vMapResult;
90 Vec_Int_t * vMap2Smaller;
91 int i, One, Two;
92 // map bigger into smaller one
93 vMap2Smaller = Vec_IntStartFull( nObjs );
94 Vec_IntForEachEntryDouble( vEquivPairs, One, Two, i )
95 Gia_ManOrigIdsRemapPairsInsert( vMap2Smaller, One, Two );
96 // collect results in the topo order
97 vMapResult = Vec_IntStartFull( nObjs );
98 Vec_IntForEachEntry( vMap2Smaller, One, i )
99 if ( One >= 0 )
100 Vec_IntWriteEntry( vMapResult, i, Gia_ManOrigIdsRemapPairsExtract(vMap2Smaller, One) );
101 Vec_IntFree( vMap2Smaller );
102 return vMapResult;
103}
104// remap the AIG using the equivalent pairs proved
105// returns the reduced AIG and the equivalence classes of the original AIG
106Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs )
107{
108 Gia_Man_t * pNew = NULL;
109 Gia_Obj_t * pObj, * pRepr; int i;
110 Vec_Int_t * vMap = Gia_ManOrigIdsRemapPairs( vPairs, Gia_ManObjNum(p) );
111 Gia_ManSetPhase( p );
112 pNew = Gia_ManStart( Gia_ManObjNum(p) );
113 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
114 pNew->pName = Abc_UtilStrsav( p->pName );
115 Gia_ManFillValue(p);
116 Gia_ManConst0(p)->Value = 0;
117 Gia_ManForEachCi( p, pObj, i )
118 pObj->Value = Gia_ManAppendCi(pNew);
119 Gia_ManHashAlloc( pNew );
120 Gia_ManForEachAnd( p, pObj, i )
121 {
122 if ( Vec_IntEntry(vMap, i) == -1 )
123 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
124 else
125 {
126 pRepr = Gia_ManObj( p, Vec_IntEntry(vMap, i) );
127 pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
128 }
129 }
130 Gia_ManHashStop( pNew );
131 Gia_ManForEachCo( p, pObj, i )
132 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
133 Vec_IntFree( vMap );
134 // compute equivalences
135 assert( !p->pReprs && !p->pNexts );
136 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
137 for ( i = 0; i < Gia_ManObjNum(p); i++ )
138 Gia_ObjSetRepr( p, i, GIA_VOID );
139 Gia_ManFillValue(pNew);
140 Gia_ManForEachAnd( p, pObj, i )
141 {
142 int iRepr = Abc_Lit2Var(pObj->Value);
143 if ( iRepr == 0 )
144 {
145 Gia_ObjSetRepr( p, i, 0 );
146 continue;
147 }
148 pRepr = Gia_ManObj( pNew, iRepr );
149 if ( !~pRepr->Value ) // first time
150 {
151 pRepr->Value = i;
152 continue;
153 }
154 // add equivalence
155 Gia_ObjSetRepr( p, i, pRepr->Value );
156 }
157 p->pNexts = Gia_ManDeriveNexts( p );
158 return pNew;
159}
160Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs )
161{
162 Gia_Man_t * pTemp, * pNew = Gia_ManOrigIdsReduce( p, vPairs );
163 Gia_ManPrintStats( p, NULL );
164 Gia_ManPrintStats( pNew, NULL );
165 //Gia_ManStop( pNew );
166 // cleanup the resulting one
167 pNew = Gia_ManCleanup( pTemp = pNew );
168 Gia_ManStop( pTemp );
169 return pNew;
170}
171
183Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
184{
185 Gia_Man_t * pTemp;
186 Cec_ParFra_t ParsFra, * pPars = &ParsFra;
187 Cec_ManFraSetDefaultParams( pPars );
188 pPars->nItersMax = 100;
189 pPars->fUseOrigIds = 1;
190 pPars->fSatSweeping = 1;
191 pPars->nBTLimit = nConfs;
192 pPars->fVerbose = fVerbose;
193 pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
194 Gia_ManStop( pTemp );
195 return Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
196}
197
209int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
210{
211 Gia_Obj_t * pRepr;
212 if ( pObj->Value == 0 )
213 return 1;
214 pObj->Value = 0;
215 assert( Gia_ObjIsAnd(pObj) );
216 if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) ) )
217 return 0;
218 if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) )
219 return 0;
220 pRepr = p->pReprs ? Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ) : NULL;
221 return pRepr == NULL || pRepr->Value == 0;
222}
223
236int Gia_ManCheckTopoOrder( Gia_Man_t * p )
237{
238 Gia_Obj_t * pObj;
239 int i, RetValue = 1;
240 Gia_ManFillValue( p );
241 Gia_ManConst0(p)->Value = 0;
242 Gia_ManForEachCi( p, pObj, i )
243 pObj->Value = 0;
244 Gia_ManForEachCo( p, pObj, i )
245 RetValue &= Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) );
246 return RetValue;
247}
248
260int * Gia_ManDeriveNexts( Gia_Man_t * p )
261{
262 unsigned * pNexts, * pTails;
263 int i;
264 assert( p->pReprs != NULL );
265 assert( p->pNexts == NULL );
266 pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
267 pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
268 for ( i = 0; i < Gia_ManObjNum(p); i++ )
269 pTails[i] = i;
270 for ( i = 0; i < Gia_ManObjNum(p); i++ )
271 {
272 //if ( p->pReprs[i].iRepr == GIA_VOID )
273 if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID )
274 continue;
275 pNexts[ pTails[p->pReprs[i].iRepr] ] = i;
276 pTails[p->pReprs[i].iRepr] = i;
277 }
278 ABC_FREE( pTails );
279 return (int *)pNexts;
280}
281
293void Gia_ManDeriveReprs( Gia_Man_t * p )
294{
295 int i, iObj;
296 assert( p->pReprs == NULL );
297 assert( p->pNexts != NULL );
298 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
299 for ( i = 0; i < Gia_ManObjNum(p); i++ )
300 Gia_ObjSetRepr( p, i, GIA_VOID );
301 for ( i = 0; i < Gia_ManObjNum(p); i++ )
302 {
303 if ( p->pNexts[i] == 0 )
304 continue;
305 if ( p->pReprs[i].iRepr != GIA_VOID )
306 continue;
307 // next is set, repr is not set
308 for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] )
309 p->pReprs[iObj].iRepr = i;
310 }
311}
312
324
325void Gia_ManDeriveReprsFromSibls( Gia_Man_t *p )
326{
327
328 int i, iObj;
329 assert( !p->pReprs && p->pSibls );
330 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
331 for ( i = 0; i < Gia_ManObjNum(p); i++ )
332 Gia_ObjSetRepr( p, i, GIA_VOID );
333 for ( i = 0; i < Gia_ManObjNum(p); i++ )
334 {
335 if ( p->pSibls[i] == 0 )
336 continue;
337 if ( p->pReprs[i].iRepr != GIA_VOID )
338 continue;
339 for ( iObj = p->pSibls[i]; iObj; iObj = p->pSibls[iObj] )
340 p->pReprs[iObj].iRepr = i;
341 }
342 ABC_FREE( p->pNexts );
343 p->pNexts = Gia_ManDeriveNexts( p );
344}
345
357int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
358{
359 int i, nLits = 0;
360 for ( i = 0; i < Gia_ManObjNum(p); i++ )
361 nLits += (Gia_ObjRepr(p, i) != GIA_VOID);
362 return nLits;
363}
364
376int Gia_ManEquivCountClasses( Gia_Man_t * p )
377{
378 int i, Counter = 0;
379 if ( p->pReprs == NULL )
380 return 0;
381 for ( i = 1; i < Gia_ManObjNum(p); i++ )
382 Counter += Gia_ObjIsHead(p, i);
383 return Counter;
384}
385
397int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
398{
399 int nLitsReal = Gia_ManEquivCountLitsAll( p );
400 if ( nLitsReal != nLits )
401 Abc_Print( 1, "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits );
402 return 1;
403}
404
416void Gia_ManPrintStatsClasses( Gia_Man_t * p )
417{
418 int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
419 for ( i = 1; i < Gia_ManObjNum(p); i++ )
420 {
421 if ( Gia_ObjIsHead(p, i) )
422 Counter++;
423 else if ( Gia_ObjIsConst(p, i) )
424 Counter0++;
425 else if ( Gia_ObjIsNone(p, i) )
426 CounterX++;
427 if ( Gia_ObjProved(p, i) )
428 Proved++;
429 }
430 CounterX -= Gia_ManCoNum(p);
431 nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
432
433// Abc_Print( 1, "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
434// Abc_Print( 1, "and =%5d ", Gia_ManAndNum(p) );
435// Abc_Print( 1, "lev =%3d ", Gia_ManLevelNum(p) );
436 Abc_Print( 1, "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits );
437}
438
450int Gia_ManEquivCountLits( Gia_Man_t * p )
451{
452 int i, Counter = 0, Counter0 = 0, CounterX = 0;
453 if ( p->pReprs == NULL || p->pNexts == NULL )
454 return 0;
455 for ( i = 1; i < Gia_ManObjNum(p); i++ )
456 {
457 if ( Gia_ObjIsHead(p, i) )
458 Counter++;
459 else if ( Gia_ObjIsConst(p, i) )
460 Counter0++;
461 else if ( Gia_ObjIsNone(p, i) )
462 CounterX++;
463 }
464 CounterX -= Gia_ManCoNum(p);
465 return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
466}
467
479int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
480{
481 int Ent, nLits = 1;
482 Gia_ClassForEachObj1( p, i, Ent )
483 {
484 assert( Gia_ObjRepr(p, Ent) == i );
485 nLits++;
486 }
487 return nLits;
488}
489void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
490{
491 int Ent;
492 Abc_Print( 1, "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
493 Gia_ClassForEachObj( p, i, Ent )
494 {
495 Abc_Print( 1," %d", Ent );
496 if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
497 Abc_Print( 1," <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
498 }
499 Abc_Print( 1, " }\n" );
500}
501void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
502{
503 int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
504 for ( i = 1; i < Gia_ManObjNum(p); i++ )
505 {
506 if ( Gia_ObjIsHead(p, i) )
507 Counter++;
508 else if ( Gia_ObjIsConst(p, i) )
509 Counter0++;
510 else if ( Gia_ObjIsNone(p, i) )
511 CounterX++;
512 if ( Gia_ObjProved(p, i) )
513 Proved++;
514 }
515 CounterX -= Gia_ManCoNum(p);
516 nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
517// Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
518// Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
519 Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d\n",
520 Counter0, Counter, nLits, CounterX, Proved );
521 assert( Gia_ManEquivCheckLits( p, nLits ) );
522 if ( fVerbose )
523 {
524// int Ent;
525 Abc_Print( 1, "Const0 (%d) = ", Counter0 );
526 Gia_ManForEachConst( p, i )
527 Abc_Print( 1, "%d ", i );
528 Abc_Print( 1, "\n" );
529 Counter = 0;
530 Gia_ManForEachClass( p, i )
531 Gia_ManEquivPrintOne( p, i, ++Counter );
532/*
533 Gia_ManLevelNum( p );
534 Gia_ManForEachClass( p, i )
535 if ( i % 100 == 0 )
536 {
537// Abc_Print( 1, "%d ", Gia_ManEquivCountOne(p, i) );
538 Gia_ClassForEachObj( p, i, Ent )
539 {
540 Abc_Print( 1, "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
541 }
542 Abc_Print( 1, "\n" );
543 }
544*/
545 }
546}
547
548
560int Gia_ManChoiceMinLevel_rec( Gia_Man_t * p, int iPivot, int fDiveIn, Vec_Int_t * vMap )
561{
562 int Level0, Level1, LevelMax;
563 Gia_Obj_t * pPivot = Gia_ManObj( p, iPivot );
564 if ( Gia_ObjIsCi(pPivot) || iPivot == 0 )
565 return 0;
566 if ( Gia_ObjLevel(p, pPivot) )
567 return Gia_ObjLevel(p, pPivot);
568 if ( fDiveIn && Gia_ObjIsClass(p, iPivot) )
569 {
570 int iObj, ObjMin = -1, iRepr = Gia_ObjRepr(p, iPivot), LevMin = ABC_INFINITY;
571 Gia_ClassForEachObj( p, iRepr, iObj )
572 {
573 int LevCur = Gia_ManChoiceMinLevel_rec( p, iObj, 0, vMap );
574 if ( LevMin > LevCur )
575 {
576 LevMin = LevCur;
577 ObjMin = iObj;
578 }
579 }
580 assert( LevMin > 0 );
581 Vec_IntWriteEntry( vMap, iRepr, ObjMin );
582 Gia_ClassForEachObj( p, iRepr, iObj )
583 Gia_ObjSetLevelId( p, iObj, LevMin );
584 return LevMin;
585 }
586 assert( Gia_ObjIsAnd(pPivot) );
587 Level0 = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId0(pPivot, iPivot), 1, vMap );
588 Level1 = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId1(pPivot, iPivot), 1, vMap );
589 LevelMax = 1 + Abc_MaxInt(Level0, Level1);
590 Gia_ObjSetLevel( p, pPivot, LevelMax );
591 return LevelMax;
592}
593Vec_Int_t * Gia_ManChoiceMinLevel( Gia_Man_t * p )
594{
595 Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
596 Gia_Obj_t * pObj;
597 int i, LevelCur, LevelMax = 0;
598// assert( Gia_ManRegNum(p) == 0 );
599 Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
600 Gia_ManForEachCo( p, pObj, i )
601 {
602 LevelCur = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId0p(p, pObj), 1, vMap );
603 LevelMax = Abc_MaxInt(LevelMax, LevelCur);
604 }
605 //printf( "Max level %d\n", LevelMax );
606 return vMap;
607}
608
620static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
621{
622 if ( fUseAll )
623 {
624 if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
625 return NULL;
626 }
627 else
628 {
629 if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
630 return NULL;
631 }
632// if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
633 if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
634 return NULL;
635 return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
636}
637
649void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
650{
651 Gia_Obj_t * pRepr;
652 if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
653 {
654 Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
655 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
656 return;
657 }
658 if ( ~pObj->Value )
659 return;
660 assert( Gia_ObjIsAnd(pObj) );
661 Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
662 Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
663 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
664}
665
677Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose )
678{
679 Gia_Man_t * pNew;
680 Gia_Obj_t * pObj;
681 int i;
682 if ( !p->pReprs && p->pSibls )
683 {
684 int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
685 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
686 for ( i = 0; i < Gia_ManObjNum(p); i++ )
687 Gia_ObjSetRepr( p, i, GIA_VOID );
688 for ( i = 0; i < Gia_ManObjNum(p); i++ )
689 if ( p->pSibls[i] > 0 )
690 {
691 if ( pMap[p->pSibls[i]] == -1 )
692 pMap[p->pSibls[i]] = p->pSibls[i];
693 pMap[i] = pMap[p->pSibls[i]];
694 }
695 for ( i = 0; i < Gia_ManObjNum(p); i++ )
696 if ( p->pSibls[i] > 0 )
697 Gia_ObjSetRepr( p, i, pMap[i] );
698 //printf( "Created equivalence classes.\n" );
699 ABC_FREE( p->pNexts );
700 p->pNexts = Gia_ManDeriveNexts( p );
701 ABC_FREE( pMap );
702 }
703 if ( !p->pReprs )
704 {
705 Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
706 return NULL;
707 }
708 if ( fDualOut && (Gia_ManPoNum(p) & 1) )
709 {
710 Abc_Print( 1, "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
711 return NULL;
712 }
713 // check if there are any equivalences defined
714 Gia_ManForEachObj( p, pObj, i )
715 if ( Gia_ObjReprObj(p, i) != NULL )
716 break;
717 if ( i == Gia_ManObjNum(p) )
718 {
719// Abc_Print( 1, "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
720// return NULL;
721 return Gia_ManDup( p );
722 }
723/*
724 if ( !Gia_ManCheckTopoOrder( p ) )
725 {
726 Abc_Print( 1, "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
727 return NULL;
728 }
729*/
730 if ( !fSkipPhase )
731 Gia_ManSetPhase( p );
732 if ( fDualOut )
733 Gia_ManEquivSetColors( p, fVerbose );
734 pNew = Gia_ManStart( Gia_ManObjNum(p) );
735 pNew->pName = Abc_UtilStrsav( p->pName );
736 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
737 Gia_ManFillValue( p );
738 Gia_ManConst0(p)->Value = 0;
739 Gia_ManForEachCi( p, pObj, i )
740 pObj->Value = Gia_ManAppendCi(pNew);
741 Gia_ManHashAlloc( pNew );
742 Gia_ManForEachCo( p, pObj, i )
743 Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
744 Gia_ManForEachCo( p, pObj, i )
745 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
746 Gia_ManHashStop( pNew );
747 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
748 return pNew;
749}
750
762Gia_Obj_t * Gia_MakeRandomChoice( Gia_Man_t * p, int iRepr )
763{
764 int iTemp, Rand, Count = 0;
765 Gia_ClassForEachObj( p, iRepr, iTemp )
766 Count++;
767 Rand = rand() % Count;
768 Count = 0;
769 Gia_ClassForEachObj( p, iRepr, iTemp )
770 if ( Count++ == Rand )
771 break;
772 return Gia_ManObj(p, iTemp);
773}
774
786void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap, int fDiveIn )
787{
788 Gia_Obj_t * pRepr;
789 if ( ~pObj->Value )
790 return;
791 assert( Gia_ObjIsAnd(pObj) );
792 if ( fDiveIn && (pRepr = Gia_ManEquivRepr(p, pObj, 1, 0)) )
793 {
794 int iTemp, iRepr = Gia_ObjId(p, pRepr);
795 Gia_Obj_t * pRepr2 = vMap ? Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) ) : Gia_MakeRandomChoice(p, iRepr);
796 Gia_ManEquivReduce2_rec( pNew, p, pRepr2, vMap, 0 );
797 Gia_ClassForEachObj( p, iRepr, iTemp )
798 {
799 Gia_Obj_t * pTemp = Gia_ManObj(p, iTemp);
800 pTemp->Value = Abc_LitNotCond( pRepr2->Value, Gia_ObjPhaseReal(pRepr2) ^ Gia_ObjPhaseReal(pTemp) );
801 }
802 assert( ~pObj->Value );
803 assert( ~pRepr->Value );
804 assert( ~pRepr2->Value );
805 return;
806 }
807 Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin0(pObj), vMap, 1 );
808 Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin1(pObj), vMap, 1 );
809 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
810}
811Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p, int fRandom )
812{
813 Vec_Int_t * vMap;
814 Gia_Man_t * pNew;
815 Gia_Obj_t * pObj;
816 int i;
817 if ( fRandom ) srand(time(NULL));
818 if ( !p->pReprs && p->pSibls )
819 {
820 int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
821 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
822 for ( i = 0; i < Gia_ManObjNum(p); i++ )
823 Gia_ObjSetRepr( p, i, GIA_VOID );
824 for ( i = 0; i < Gia_ManObjNum(p); i++ )
825 if ( p->pSibls[i] > 0 )
826 {
827 if ( pMap[p->pSibls[i]] == -1 )
828 pMap[p->pSibls[i]] = p->pSibls[i];
829 pMap[i] = pMap[p->pSibls[i]];
830 }
831 for ( i = 0; i < Gia_ManObjNum(p); i++ )
832 if ( p->pSibls[i] > 0 )
833 Gia_ObjSetRepr( p, i, pMap[i] );
834 //printf( "Created equivalence classes.\n" );
835 ABC_FREE( p->pNexts );
836 p->pNexts = Gia_ManDeriveNexts( p );
837 ABC_FREE( pMap );
838 }
839 if ( !p->pReprs )
840 {
841 Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
842 return NULL;
843 }
844 // check if there are any equivalences defined
845 Gia_ManForEachObj( p, pObj, i )
846 if ( Gia_ObjReprObj(p, i) != NULL )
847 break;
848 if ( i == Gia_ManObjNum(p) )
849 return Gia_ManDup( p );
850 vMap = fRandom ? NULL : Gia_ManChoiceMinLevel( p );
851 Gia_ManSetPhase( p );
852 pNew = Gia_ManStart( Gia_ManObjNum(p) );
853 pNew->pName = Abc_UtilStrsav( p->pName );
854 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
855 Gia_ManFillValue( p );
856 Gia_ManConst0(p)->Value = 0;
857 Gia_ManForEachCi( p, pObj, i )
858 pObj->Value = Gia_ManAppendCi(pNew);
859 Gia_ManHashAlloc( pNew );
860 Gia_ManForEachCo( p, pObj, i )
861 Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin0(pObj), vMap, 1 );
862 Gia_ManForEachCo( p, pObj, i )
863 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
864 Gia_ManHashStop( pNew );
865 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
866 Vec_IntFreeP( &vMap );
867 return pNew;
868}
869
870
882void Gia_ManEquivFixOutputPairs( Gia_Man_t * p )
883{
884 Gia_Obj_t * pObj0, * pObj1;
885 int i;
886 assert( (Gia_ManPoNum(p) & 1) == 0 );
887 Gia_ManForEachPo( p, pObj0, i )
888 {
889 pObj1 = Gia_ManPo( p, ++i );
890 if ( Gia_ObjChild0(pObj0) != Gia_ObjChild0(pObj1) )
891 continue;
892 pObj0->iDiff0 = Gia_ObjId(p, pObj0);
893 pObj0->fCompl0 = 0;
894 pObj1->iDiff0 = Gia_ObjId(p, pObj1);
895 pObj1->fCompl0 = 0;
896 }
897}
898
910void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew )
911{
912 Gia_Obj_t * pObj, * pObjNew;
913 int i;
914 Gia_ManForEachObj( p, pObj, i )
915 {
916 if ( !~pObj->Value )
917 continue;
918 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
919 if ( pObjNew->fMark0 )
920 pObj->Value = ~0;
921 }
922}
923
935void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFinal )
936{
937 Vec_Int_t * vClass;
938 Gia_Obj_t * pObj, * pObjNew;
939 int i, k, iNode, iRepr, iPrev;
940 // start representatives
941 pFinal->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pFinal) );
942 for ( i = 0; i < Gia_ManObjNum(pFinal); i++ )
943 Gia_ObjSetRepr( pFinal, i, GIA_VOID );
944 // iterate over constant candidates
945 Gia_ManForEachConst( p, i )
946 {
947 pObj = Gia_ManObj( p, i );
948 if ( !~pObj->Value )
949 continue;
950 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
951 if ( Abc_Lit2Var(pObjNew->Value) == 0 )
952 continue;
953 Gia_ObjSetRepr( pFinal, Abc_Lit2Var(pObjNew->Value), 0 );
954 }
955 // iterate over class candidates
956 vClass = Vec_IntAlloc( 100 );
957 Gia_ManForEachClass( p, i )
958 {
959 Vec_IntClear( vClass );
960 Gia_ClassForEachObj( p, i, k )
961 {
962 pObj = Gia_ManObj( p, k );
963 if ( !~pObj->Value )
964 continue;
965 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
966 Vec_IntPushUnique( vClass, Abc_Lit2Var(pObjNew->Value) );
967 }
968 if ( Vec_IntSize( vClass ) < 2 )
969 continue;
970 Vec_IntSort( vClass, 0 );
971 iRepr = iPrev = Vec_IntEntry( vClass, 0 );
972 Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
973 {
974 Gia_ObjSetRepr( pFinal, iNode, iRepr );
975 assert( iPrev < iNode );
976 iPrev = iNode;
977 }
978 }
979 Vec_IntFree( vClass );
980 pFinal->pNexts = Gia_ManDeriveNexts( pFinal );
981}
982
994Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
995{
996 Gia_Man_t * pNew;
997 Vec_Int_t * vClass;
998 int i, k, iNode, iRepr, iPrev;
999 pNew = Gia_ManDupDfs( p );
1000 // start representatives
1001 pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
1002 for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
1003 Gia_ObjSetRepr( pNew, i, GIA_VOID );
1004 // iterate over constant candidates
1005 Gia_ManForEachConst( p, i )
1006 Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
1007 // iterate over class candidates
1008 vClass = Vec_IntAlloc( 100 );
1009 Gia_ManForEachClass( p, i )
1010 {
1011 Vec_IntClear( vClass );
1012 Gia_ClassForEachObj( p, i, k )
1013 Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
1014 assert( Vec_IntSize( vClass ) > 1 );
1015 Vec_IntSort( vClass, 0 );
1016 iRepr = iPrev = Vec_IntEntry( vClass, 0 );
1017 Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
1018 {
1019 Gia_ObjSetRepr( pNew, iNode, iRepr );
1020 assert( iPrev < iNode );
1021 iPrev = iNode;
1022 }
1023 }
1024 Vec_IntFree( vClass );
1025 pNew->pNexts = Gia_ManDeriveNexts( pNew );
1026 return pNew;
1027}
1028
1040Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
1041{
1042 Gia_Man_t * pNew, * pFinal;
1043 pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
1044 if ( pNew == NULL )
1045 return NULL;
1046 Gia_ManOrigIdsRemap( p, pNew );
1047 if ( fMiterPairs )
1048 Gia_ManEquivFixOutputPairs( pNew );
1049 if ( fSeq )
1050 Gia_ManSeqMarkUsed( pNew );
1051 else
1052 Gia_ManCombMarkUsed( pNew );
1053 Gia_ManEquivUpdatePointers( p, pNew );
1054 pFinal = Gia_ManDupMarked( pNew );
1055 Gia_ManOrigIdsRemap( pNew, pFinal );
1056 Gia_ManEquivDeriveReprs( p, pNew, pFinal );
1057 Gia_ManStop( pNew );
1058 pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
1059 Gia_ManOrigIdsRemap( pNew, pFinal );
1060 Gia_ManStop( pNew );
1061 return pFinal;
1062}
1063
1075int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds )
1076{
1077 if ( Gia_ObjVisitColor( p, Gia_ObjId(p,pObj), fOdds ) )
1078 return 0;
1079 if ( Gia_ObjIsRo(p, pObj) )
1080 return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj)), fOdds );
1081 assert( Gia_ObjIsAnd(pObj) );
1082 return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), fOdds )
1083 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin1(pObj), fOdds );
1084}
1085
1097int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
1098{
1099 Gia_Obj_t * pObj;
1100 int i, nNodes[2], nDiffs[2];
1101 assert( (Gia_ManPoNum(p) & 1) == 0 );
1102 Gia_ObjSetColors( p, 0 );
1103 Gia_ManForEachPi( p, pObj, i )
1104 Gia_ObjSetColors( p, Gia_ObjId(p,pObj) );
1105 nNodes[0] = nNodes[1] = Gia_ManPiNum(p);
1106 Gia_ManForEachPo( p, pObj, i )
1107 nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 );
1108// Gia_ManForEachObj( p, pObj, i )
1109// if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
1110// assert( Gia_ObjColors(p, i) );
1111 nDiffs[0] = Gia_ManCandNum(p) - nNodes[0];
1112 nDiffs[1] = Gia_ManCandNum(p) - nNodes[1];
1113 if ( fVerbose )
1114 {
1115 Abc_Print( 1, "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n",
1116 Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1],
1117 Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] );
1118 }
1119 return (nDiffs[0] + nDiffs[1]) / 2;
1120}
1121
1133static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
1134{
1135 Gia_Obj_t * pRepr;
1136 unsigned iLitNew;
1137 pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
1138 if ( pRepr == NULL )
1139 return;
1140// if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1141 if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1142 return;
1143 iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1144 if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
1145 {
1146 if ( vTrace )
1147 Vec_IntPush( vTrace, 1 );
1148 if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) )
1149 {
1150 if ( vMap )
1151 Vec_IntPush( vMap, Gia_ObjId(p, pObj) );
1152 Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
1153 }
1154 }
1155 else
1156 {
1157 if ( vTrace )
1158 Vec_IntPush( vTrace, 0 );
1159 }
1160 if ( fSpeculate )
1161 pObj->Value = iLitNew;
1162}
1163
1175void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
1176{
1177 if ( ~pObj->Value )
1178 return;
1179 assert( Gia_ObjIsAnd(pObj) );
1180 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
1181 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
1182 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1183 Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
1184}
1185
1197Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMap )
1198{
1199 Vec_Int_t * vXorLits;
1200 Gia_Man_t * pNew, * pTemp;
1201 Gia_Obj_t * pObj;
1202 int i, iLitNew;
1203 if ( !p->pReprs )
1204 {
1205 Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
1206 return NULL;
1207 }
1208 Vec_IntClear( vTrace );
1209 vXorLits = Vec_IntAlloc( 1000 );
1210 Gia_ManSetPhase( p );
1211 Gia_ManFillValue( p );
1212 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1213 pNew->pName = Abc_UtilStrsav( p->pName );
1214 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1215 Gia_ManHashAlloc( pNew );
1216 Gia_ManConst0(p)->Value = 0;
1217 Gia_ManForEachCi( p, pObj, i )
1218 pObj->Value = Gia_ManAppendCi(pNew);
1219 Gia_ManForEachRo( p, pObj, i )
1220 Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL, vMap );
1221 Gia_ManForEachCo( p, pObj, i )
1222 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL, vMap );
1223 Gia_ManForEachPo( p, pObj, i )
1224 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1225 Vec_IntForEachEntry( vXorLits, iLitNew, i )
1226 Gia_ManAppendCo( pNew, iLitNew );
1227 if ( Vec_IntSize(vXorLits) == 0 )
1228 {
1229 Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
1230 Gia_ManAppendCo( pNew, 0 );
1231 }
1232 Gia_ManForEachRi( p, pObj, i )
1233 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1234 Gia_ManHashStop( pNew );
1235 Vec_IntFree( vXorLits );
1236 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1237 pNew = Gia_ManCleanup( pTemp = pNew );
1238 Gia_ManStop( pTemp );
1239 return pNew;
1240}
1241
1253Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose )
1254{
1255 Gia_Man_t * pNew, * pTemp;
1256 Gia_Obj_t * pObj;
1257 Vec_Int_t * vXorLits;
1258 int i, iLitNew;
1259 Vec_Int_t * vTrace = NULL, * vGuide = NULL;
1260 if ( !p->pReprs )
1261 {
1262 Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
1263 return NULL;
1264 }
1265 if ( fDualOut && (Gia_ManPoNum(p) & 1) )
1266 {
1267 Abc_Print( 1, "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
1268 return NULL;
1269 }
1270 if ( fSkipSome )
1271 {
1272 vGuide = Vec_IntAlloc( 100 );
1273 pTemp = Gia_ManSpecReduceTrace( p, vGuide, NULL );
1274 Gia_ManStop( pTemp );
1275 assert( Vec_IntSize(vGuide) == Gia_ManEquivCountLitsAll(p) );
1276 vTrace = Vec_IntAlloc( 100 );
1277 }
1278 vXorLits = Vec_IntAlloc( 1000 );
1279 Gia_ManSetPhase( p );
1280 Gia_ManFillValue( p );
1281 if ( fDualOut )
1282 Gia_ManEquivSetColors( p, fVerbose );
1283 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1284 pNew->pName = Abc_UtilStrsav( p->pName );
1285 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1286 Gia_ManHashAlloc( pNew );
1287 Gia_ManConst0(p)->Value = 0;
1288 Gia_ManForEachCi( p, pObj, i )
1289 pObj->Value = Gia_ManAppendCi(pNew);
1290 Gia_ManForEachRo( p, pObj, i )
1291 Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
1292 Gia_ManForEachCo( p, pObj, i )
1293 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
1294 if ( !fSynthesis )
1295 {
1296 Gia_ManForEachPo( p, pObj, i )
1297 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1298 }
1299 Vec_IntForEachEntry( vXorLits, iLitNew, i )
1300 Gia_ManAppendCo( pNew, iLitNew );
1301 if ( Vec_IntSize(vXorLits) == 0 )
1302 {
1303 Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
1304 Gia_ManAppendCo( pNew, 0 );
1305 }
1306 Gia_ManForEachRi( p, pObj, i )
1307 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1308 Gia_ManHashStop( pNew );
1309 Vec_IntFree( vXorLits );
1310 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1311 pNew = Gia_ManCleanup( pTemp = pNew );
1312 Gia_ManStop( pTemp );
1313
1314 // update using trace
1315 if ( fSkipSome )
1316 {
1317 // count the number of non-zero entries
1318 int iLit, nAddPos = 0;
1319 Vec_IntForEachEntry( vGuide, iLit, i )
1320 if ( iLit )
1321 nAddPos++;
1322 if ( nAddPos )
1323 assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) + nAddPos );
1324 }
1325 Vec_IntFreeP( &vTrace );
1326 Vec_IntFreeP( &vGuide );
1327 return pNew;
1328}
1329
1341void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
1342{
1343 Gia_Obj_t * pRepr;
1344 int iLitNew;
1345 pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
1346 if ( pRepr == NULL )
1347 return;
1348// if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1349 if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1350 return;
1351 iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1352 if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
1353 Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) );
1354 Gia_ObjSetCopyF( p, f, pObj, iLitNew );
1355}
1356
1368void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
1369{
1370 if ( ~Gia_ObjCopyF(p, f, pObj) )
1371 return;
1372 assert( Gia_ObjIsAnd(pObj) );
1373 Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
1374 Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f, fDualOut );
1375 Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) );
1376 Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
1377}
1378
1390Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut )
1391{
1392 Gia_Man_t * pNew, * pTemp;
1393 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
1394 Vec_Int_t * vXorLits;
1395 int f, i, iLitNew;
1396 if ( !p->pReprs )
1397 {
1398 Abc_Print( 1, "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" );
1399 return NULL;
1400 }
1401 if ( Gia_ManRegNum(p) == 0 )
1402 {
1403 Abc_Print( 1, "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" );
1404 return NULL;
1405 }
1406 if ( Gia_ManRegNum(p) != pInit->nRegs )
1407 {
1408 Abc_Print( 1, "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
1409 return NULL;
1410 }
1411 if ( fDualOut && (Gia_ManPoNum(p) & 1) )
1412 {
1413 Abc_Print( 1, "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
1414 return NULL;
1415 }
1416
1417/*
1418 if ( !Gia_ManCheckTopoOrder( p ) )
1419 {
1420 Abc_Print( 1, "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
1421 return NULL;
1422 }
1423*/
1424 assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
1425 Vec_IntFill( &p->vCopies, nFrames * Gia_ManObjNum(p), -1 );
1426 vXorLits = Vec_IntAlloc( 1000 );
1427 Gia_ManSetPhase( p );
1428 if ( fDualOut )
1429 Gia_ManEquivSetColors( p, 0 );
1430 pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
1431 pNew->pName = Abc_UtilStrsav( p->pName );
1432 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1433 Gia_ManHashAlloc( pNew );
1434 Gia_ManForEachRo( p, pObj, i )
1435 Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) );
1436 for ( f = 0; f < nFrames; f++ )
1437 {
1438 Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
1439 Gia_ManForEachPi( p, pObj, i )
1440 Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
1441 Gia_ManForEachRo( p, pObj, i )
1442 Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
1443 Gia_ManForEachCo( p, pObj, i )
1444 {
1445 Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
1446 Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) );
1447 }
1448 if ( f == nFrames - 1 )
1449 break;
1450 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
1451 Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) );
1452 }
1453 Vec_IntForEachEntry( vXorLits, iLitNew, i )
1454 Gia_ManAppendCo( pNew, iLitNew );
1455 if ( Vec_IntSize(vXorLits) == 0 )
1456 {
1457// Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
1458 Gia_ManAppendCo( pNew, 0 );
1459 }
1460 Vec_IntErase( &p->vCopies );
1461 Vec_IntFree( vXorLits );
1462 Gia_ManHashStop( pNew );
1463 pNew = Gia_ManCleanup( pTemp = pNew );
1464 Gia_ManStop( pTemp );
1465 return pNew;
1466}
1467
1480Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs )
1481{
1482 Gia_Man_t * pFrames;
1483 int f, nLits;
1484 nLits = Gia_ManEquivCountLits( p );
1485 for ( f = 1; ; f++ )
1486 {
1487 pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut );
1488 if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) ||
1489 (nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) )
1490 break;
1491 if ( f == nFramesMax )
1492 break;
1493 if ( Gia_ManAndNum(pFrames) > 500000 )
1494 {
1495 Gia_ManStop( pFrames );
1496 return NULL;
1497 }
1498 Gia_ManStop( pFrames );
1499 pFrames = NULL;
1500 }
1501 if ( f == nFramesMax )
1502 Abc_Print( 1, "Stopped unrolling after %d frames.\n", nFramesMax );
1503 if ( pnFrames )
1504 *pnFrames = f;
1505 return pFrames;
1506}
1507
1519void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
1520{
1521 extern void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass );
1522 Vec_Int_t * vClass, * vClassNew;
1523 int iRepr, iNode, Ent, k;
1524 int nRemovedLits = 0, nRemovedClas = 0;
1525 int nTotalLits = 0, nTotalClas = 0;
1526 Gia_Obj_t * pObj;
1527 int i;
1528 assert( p->pReprs && p->pNexts );
1529 vClass = Vec_IntAlloc( 100 );
1530 vClassNew = Vec_IntAlloc( 100 );
1531 Gia_ManForEachObj( p, pObj, i )
1532 if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
1533 assert( Gia_ObjColors(p, i) );
1534 Gia_ManForEachClassReverse( p, iRepr )
1535 {
1536 nTotalClas++;
1537 Vec_IntClear( vClass );
1538 Vec_IntClear( vClassNew );
1539 Gia_ClassForEachObj( p, iRepr, iNode )
1540 {
1541 nTotalLits++;
1542 Vec_IntPush( vClass, iNode );
1543 assert( Gia_ObjColors(p, iNode) );
1544 if ( Gia_ObjColors(p, iNode) != 3 )
1545 Vec_IntPush( vClassNew, iNode );
1546 else
1547 nRemovedLits++;
1548 }
1549 Vec_IntForEachEntry( vClass, Ent, k )
1550 {
1551 p->pReprs[Ent].fFailed = p->pReprs[Ent].fProved = 0;
1552 p->pReprs[Ent].iRepr = GIA_VOID;
1553 p->pNexts[Ent] = 0;
1554 }
1555 if ( Vec_IntSize(vClassNew) < 2 )
1556 {
1557 nRemovedClas++;
1558 continue;
1559 }
1560 Cec_ManSimClassCreate( p, vClassNew );
1561 }
1562 Vec_IntFree( vClass );
1563 Vec_IntFree( vClassNew );
1564 if ( fVerbose )
1565 Abc_Print( 1, "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n",
1566 nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
1567}
1568
1580void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerbose )
1581{
1582 Gia_Man_t * pMiter, * pTemp;
1583 Gia_Obj_t * pObj;
1584 int i, iLit, nAddPos, nLits = 0;
1585 int nLitsAll, Counter = 0;
1586 nLitsAll = Gia_ManEquivCountLitsAll( p );
1587 if ( nLitsAll == 0 )
1588 {
1589 Abc_Print( 1, "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" );
1590 return;
1591 }
1592 // read AIGER file
1593 pMiter = Gia_AigerRead( pFileName, 0, 0, 0 );
1594 if ( pMiter == NULL )
1595 {
1596 Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
1597 return;
1598 }
1599 if ( fSkipSome )
1600 {
1601 Vec_Int_t * vTrace = Vec_IntAlloc( 100 );
1602 pTemp = Gia_ManSpecReduceTrace( p, vTrace, NULL );
1603 Gia_ManStop( pTemp );
1604 assert( Vec_IntSize(vTrace) == nLitsAll );
1605 // count the number of non-zero entries
1606 nAddPos = 0;
1607 Vec_IntForEachEntry( vTrace, iLit, i )
1608 if ( iLit )
1609 nAddPos++;
1610 // check the number
1611 if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nAddPos )
1612 {
1613 Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGFilteredEquivNum(%d).\n",
1614 Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nAddPos );
1615 Gia_ManStop( pMiter );
1616 Vec_IntFreeP( &vTrace );
1617 return;
1618 }
1619 // mark corresponding POs as solved
1620 nLits = iLit = Counter = 0;
1621 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1622 {
1623 if ( Gia_ObjRepr(p, i) == GIA_VOID )
1624 continue;
1625 if ( Vec_IntEntry( vTrace, nLits++ ) == 0 )
1626 continue;
1627 pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + iLit++ );
1628 if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
1629 {
1630 Gia_ObjSetProved(p, i);
1631 Counter++;
1632 }
1633 }
1634 assert( nLits == nLitsAll );
1635 assert( iLit == nAddPos );
1636 Vec_IntFreeP( &vTrace );
1637 }
1638 else
1639 {
1640 if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
1641 {
1642 Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
1643 Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
1644 Gia_ManStop( pMiter );
1645 return;
1646 }
1647 // mark corresponding POs as solved
1648 nLits = 0;
1649 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1650 {
1651 if ( Gia_ObjRepr(p, i) == GIA_VOID )
1652 continue;
1653 pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ );
1654 if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
1655 {
1656 Gia_ObjSetProved(p, i);
1657 Counter++;
1658 }
1659 }
1660 assert( nLits == nLitsAll );
1661 }
1662 if ( fVerbose )
1663 Abc_Print( 1, "Set %d equivalences as proved.\n", Counter );
1664 Gia_ManStop( pMiter );
1665}
1666
1678void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose )
1679{
1680 Gia_Man_t * pSrm;
1681 Vec_Int_t * vTrace, * vMap;
1682 int i, iObjId, Entry, Prev = -1;
1683 // check if there are equivalences
1684 if ( p->pReprs == NULL || p->pNexts == NULL )
1685 {
1686 Abc_Print( 1, "Gia_ManEquivFilter(): Equivalence classes are not defined.\n" );
1687 return;
1688 }
1689 // check if PO indexes are available
1690 if ( vPoIds == NULL )
1691 {
1692 Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs is not available.\n" );
1693 return;
1694 }
1695 if ( Vec_IntSize(vPoIds) == 0 )
1696 return;
1697 // create SRM with mapping into POs
1698 vMap = Vec_IntAlloc( 1000 );
1699 vTrace = Vec_IntAlloc( 1000 );
1700 pSrm = Gia_ManSpecReduceTrace( p, vTrace, vMap );
1701 Vec_IntFree( vTrace );
1702 // the resulting array (vMap) maps PO indexes of the SRM into object IDs
1703 assert( Gia_ManPoNum(pSrm) == Gia_ManPoNum(p) + Vec_IntSize(vMap) );
1704 Gia_ManStop( pSrm );
1705 if ( fVerbose )
1706 printf( "Design POs = %d. SRM POs = %d. Spec POs = %d. Disproved POs = %d.\n",
1707 Gia_ManPoNum(p), Gia_ManPoNum(p) + Vec_IntSize(vMap), Vec_IntSize(vMap), Vec_IntSize(vPoIds) );
1708 // check if disproved POs satisfy the range
1709 Vec_IntSort( vPoIds, 0 );
1710 Vec_IntForEachEntry( vPoIds, Entry, i )
1711 {
1712 if ( Entry < 0 || Entry >= Gia_ManPoNum(p) + Vec_IntSize(vMap) )
1713 {
1714 Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains PO index (%d),\n", Entry );
1715 Abc_Print( 1, "which does not fit into the range of available PO indexes of the SRM: [%d; %d].\n", 0, Gia_ManPoNum(p) + Vec_IntSize(vMap)-1 );
1716 Vec_IntFree( vMap );
1717 return;
1718 }
1719 if ( Entry < Gia_ManPoNum(p) )
1720 Abc_Print( 0, "Gia_ManEquivFilter(): One of the original POs (%d) have failed.\n", Entry );
1721 if ( Prev == Entry )
1722 {
1723 Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains at least one duplicate entry (%d),\n", Entry );
1724 Vec_IntFree( vMap );
1725 return;
1726 }
1727 Prev = Entry;
1728 }
1729 // perform the reduction of the equivalence classes
1730 Vec_IntForEachEntry( vPoIds, Entry, i )
1731 {
1732 if ( Entry < Gia_ManPoNum(p) )
1733 continue;
1734 iObjId = Vec_IntEntry( vMap, Entry - Gia_ManPoNum(p) );
1735 Gia_ObjUnsetRepr( p, iObjId );
1736// Gia_ObjSetNext( p, iObjId, 0 );
1737 }
1738 Vec_IntFree( vMap );
1739 ABC_FREE( p->pNexts );
1740 p->pNexts = Gia_ManDeriveNexts( p );
1741}
1742
1754void Gia_ManEquivFilterTest( Gia_Man_t * p )
1755{
1756 Vec_Int_t * vPoIds;
1757 int i;
1758 vPoIds = Vec_IntAlloc( 1000 );
1759 for ( i = 0; i < 10; i++ )
1760 {
1761 Vec_IntPush( vPoIds, Gia_ManPoNum(p) + 2 * i + 2 );
1762 printf( "%d ", Gia_ManPoNum(p) + 2*i + 2 );
1763 }
1764 printf( "\n" );
1765 Gia_ManEquivFilter( p, vPoIds, 1 );
1766 Vec_IntFree( vPoIds );
1767}
1768
1780void Gia_ManEquivImprove( Gia_Man_t * p )
1781{
1782 Vec_Int_t * vClass;
1783 int i, k, iNode, iRepr;
1784 int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur;
1785 assert( p->pReprs != NULL && p->pNexts != NULL );
1786 Gia_ManLevelNum( p );
1787 Gia_ManCreateRefs( p );
1788 // iterate over class candidates
1789 vClass = Vec_IntAlloc( 100 );
1790 Gia_ManForEachClass( p, i )
1791 {
1792 Vec_IntClear( vClass );
1793 iReprBest = -1;
1794 iLevelBest = iMffcBest = ABC_INFINITY;
1795 Gia_ClassForEachObj( p, i, k )
1796 {
1797 iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) );
1798 iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) );
1799 if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) )
1800 {
1801 iReprBest = k;
1802 iLevelBest = iLevelCur;
1803 iMffcBest = iMffcCur;
1804 }
1805 Vec_IntPush( vClass, k );
1806 }
1807 assert( Vec_IntSize( vClass ) > 1 );
1808 assert( iReprBest > 0 );
1809 if ( i == iReprBest )
1810 continue;
1811/*
1812 Abc_Print( 1, "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
1813 i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ),
1814 Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) );
1815*/
1816 iRepr = iReprBest;
1817 Gia_ObjSetRepr( p, iRepr, GIA_VOID );
1818 Gia_ObjSetProved( p, i );
1819 Gia_ObjUnsetProved( p, iRepr );
1820 Vec_IntForEachEntry( vClass, iNode, k )
1821 if ( iNode != iRepr )
1822 Gia_ObjSetRepr( p, iNode, iRepr );
1823 }
1824 Vec_IntFree( vClass );
1825 ABC_FREE( p->pNexts );
1826// p->pNexts = Gia_ManDeriveNexts( p );
1827}
1828
1829
1841int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
1842{
1843 // check the trivial cases
1844 if ( pNode == NULL )
1845 return 0;
1846 if ( Gia_ObjIsCi(pNode) )
1847 return 0;
1848// if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
1849// return 0;
1850 if ( pNode == pOld )
1851 return 1;
1852 // skip the visited node
1853 if ( pNode->fMark0 )
1854 return 0;
1855 pNode->fMark0 = 1;
1856 Vec_PtrPush( vVisited, pNode );
1857 // check the children
1858 if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
1859 return 1;
1860 if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
1861 return 1;
1862 // check equivalent nodes
1863 return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
1864}
1865
1877int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
1878{
1879 Vec_Ptr_t * vVisited;
1880 Gia_Obj_t * pObj;
1881 int RetValue, i;
1882 assert( !Gia_IsComplement(pOld) );
1883 assert( !Gia_IsComplement(pNode) );
1884 vVisited = Vec_PtrAlloc( 100 );
1885 RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
1886 Vec_PtrForEachEntry( Gia_Obj_t *, vVisited, pObj, i )
1887 pObj->fMark0 = 0;
1888 Vec_PtrFree( vVisited );
1889 return RetValue;
1890}
1891
1892
1904void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
1905{
1906 if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
1907 {
1908 Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
1909 return;
1910 }
1911 Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
1912}
1913
1925void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
1926{
1927 Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
1928 if ( ~pObj->Value )
1929 return;
1930 if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) && !Gia_ObjFailed(p,Gia_ObjId(p,pObj)) )
1931 {
1932 if ( Gia_ObjIsConst0(pRepr) )
1933 {
1934 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1935 return;
1936 }
1937 Gia_ManEquivToChoices_rec( pNew, p, pRepr );
1938 assert( Gia_ObjIsAnd(pObj) );
1939 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
1940 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
1941 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1942 if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
1943 {
1944 assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
1945 return;
1946 }
1947 if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
1948 return;
1949 assert( pRepr->Value < pObj->Value );
1950 pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
1951 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
1952 if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
1953 {
1954// assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
1955 if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) != pReprNew )
1956 return;
1957 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1958 return;
1959 }
1960 if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
1961 {
1962 assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
1963 Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
1964 Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
1965 }
1966 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1967 return;
1968 }
1969 assert( Gia_ObjIsAnd(pObj) );
1970 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
1971 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
1972 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1973}
1974
1986void Gia_ManRemoveBadChoices( Gia_Man_t * p )
1987{
1988 Gia_Obj_t * pObj;
1989 int i, iObj, iPrev, Counter = 0;
1990 // mark nodes with fanout
1991 Gia_ManForEachObj( p, pObj, i )
1992 {
1993 pObj->fMark0 = 0;
1994 if ( Gia_ObjIsAnd(pObj) )
1995 {
1996 Gia_ObjFanin0(pObj)->fMark0 = 1;
1997 Gia_ObjFanin1(pObj)->fMark0 = 1;
1998 }
1999 else if ( Gia_ObjIsCo(pObj) )
2000 Gia_ObjFanin0(pObj)->fMark0 = 1;
2001 }
2002 // go through the classes and remove
2003 Gia_ManForEachClass( p, i )
2004 {
2005 for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
2006 {
2007 if ( !Gia_ManObj(p, iObj)->fMark0 )
2008 {
2009 iPrev = iObj;
2010 continue;
2011 }
2012 Gia_ObjSetRepr( p, iObj, GIA_VOID );
2013 Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
2014 Gia_ObjSetNext( p, iObj, 0 );
2015 Counter++;
2016 }
2017 }
2018 // remove the marks
2019 Gia_ManCleanMark0( p );
2020// Abc_Print( 1, "Removed %d bad choices.\n", Counter );
2021}
2022
2034Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
2035{
2036 Vec_Int_t * vNodes;
2037 Gia_Man_t * pNew, * pTemp;
2038 Gia_Obj_t * pObj, * pRepr;
2039 int i;
2040//Gia_ManEquivPrintClasses( p, 0, 0 );
2041 assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
2042 Gia_ManSetPhase( p );
2043 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2044 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2045 pNew->pName = Abc_UtilStrsav( p->pName );
2046 pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
2047 pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
2048 for ( i = 0; i < Gia_ManObjNum(p); i++ )
2049 pNew->pReprs[i].iRepr = GIA_VOID;
2050 Gia_ManFillValue( p );
2051 Gia_ManConst0(p)->Value = 0;
2052 Gia_ManForEachCi( p, pObj, i )
2053 pObj->Value = Gia_ManAppendCi(pNew);
2054 Gia_ManForEachRo( p, pObj, i )
2055 if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
2056 {
2057 assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
2058 pObj->Value = pRepr->Value;
2059 }
2060 Gia_ManHashAlloc( pNew );
2061 Gia_ManForEachCo( p, pObj, i )
2062 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
2063 vNodes = Gia_ManGetDangling( p );
2064 Gia_ManForEachObjVec( vNodes, p, pObj, i )
2065 Gia_ManEquivToChoices_rec( pNew, p, pObj );
2066 Vec_IntFree( vNodes );
2067 Gia_ManForEachCo( p, pObj, i )
2068 if ( i % nSnapshots == 0 )
2069 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2070 Gia_ManHashStop( pNew );
2071 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2072 Gia_ManRemoveBadChoices( pNew );
2073//Gia_ManEquivPrintClasses( pNew, 0, 0 );
2074 pNew = Gia_ManCleanup( pTemp = pNew );
2075 Gia_ManStop( pTemp );
2076//Gia_ManEquivPrintClasses( pNew, 0, 0 );
2077 return pNew;
2078}
2079
2091int Gia_ManCountChoiceNodes( Gia_Man_t * p )
2092{
2093 Gia_Obj_t * pObj;
2094 int i, Counter = 0;
2095 if ( p->pReprs == NULL || p->pNexts == NULL )
2096 return 0;
2097 Gia_ManForEachObj( p, pObj, i )
2098 Counter += Gia_ObjIsHead( p, i );
2099 return Counter;
2100}
2101
2113int Gia_ManCountChoices( Gia_Man_t * p )
2114{
2115 Gia_Obj_t * pObj;
2116 int i, Counter = 0;
2117 if ( p->pReprs == NULL || p->pNexts == NULL )
2118 return 0;
2119 Gia_ManForEachObj( p, pObj, i )
2120 Counter += (int)(Gia_ObjNext( p, i ) > 0);
2121 return Counter;
2122}
2123
2124ABC_NAMESPACE_IMPL_END
2125
2126#include "aig/aig/aig.h"
2127#include "aig/saig/saig.h"
2128#include "proof/cec/cec.h"
2129#include "giaAig.h"
2130
2131ABC_NAMESPACE_IMPL_START
2132
2133
2145int Gia_ManHasNoEquivs( Gia_Man_t * p )
2146{
2147 Gia_Obj_t * pObj;
2148 int i;
2149 if ( p->pReprs == NULL )
2150 return 1;
2151 Gia_ManForEachObj( p, pObj, i )
2152 if ( Gia_ObjReprObj(p, i) != NULL )
2153 break;
2154 return i == Gia_ManObjNum(p);
2155}
2156
2168int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose )
2169{
2170// extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
2171 Aig_Man_t * pTemp;
2172 Gia_Man_t * pSrm, * pReduce, * pAux;
2173 int nIter, nStart = 0;
2174 if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
2175 {
2176 Abc_Print( 1, "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
2177 return 0;
2178 }
2179 // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
2180 Gia_ManCleanMark0( pGia );
2181 Gia_ManPrintStats( pGia, NULL );
2182 for ( nIter = 0; ; nIter++ )
2183 {
2184 if ( Gia_ManHasNoEquivs(pGia) )
2185 {
2186 Abc_Print( 1, "Gia_CommandSpecI: No equivalences left.\n" );
2187 break;
2188 }
2189 Abc_Print( 1, "ITER %3d : ", nIter );
2190// if ( fVerbose )
2191// Abc_Print( 1, "Starting BMC from frame %d.\n", nStart );
2192// if ( fVerbose )
2193// Gia_ManPrintStats( pGia, 0 );
2194 Gia_ManPrintStatsClasses( pGia );
2195 // perform speculative reduction
2196// if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) )
2197 if ( !Cec_ManCheckNonTrivialCands(pGia) )
2198 {
2199 Abc_Print( 1, "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
2200 break;
2201 }
2202 pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
2203 // bmc2 -F 100 -C 25000
2204 {
2205 Abc_Cex_t * pCex;
2206 int nFrames = nFramesInit; // different from default
2207 int nNodeDelta = 2000;
2208 int nBTLimit = nBTLimitInit; // different from default
2209 int nBTLimitAll = 2000000;
2210 pTemp = Gia_ManToAig( pSrm, 0 );
2211// Aig_ManPrintStats( pTemp );
2212 Gia_ManStop( pSrm );
2213 Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0, 0 );
2214 pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
2215 Aig_ManStop( pTemp );
2216 if ( pCex == NULL )
2217 {
2218 Abc_Print( 1, "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
2219 break;
2220 }
2221 if ( fStart )
2222 nStart = pCex->iFrame;
2223 // perform simulation
2224 {
2225 Cec_ParSim_t Pars, * pPars = &Pars;
2226 Cec_ManSimSetDefaultParams( pPars );
2227 pPars->fCheckMiter = fCheckMiter;
2228 if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) )
2229 {
2230 ABC_FREE( pCex );
2231 break;
2232 }
2233 ABC_FREE( pCex );
2234 }
2235 }
2236 // write equivalence classes
2237 Gia_AigerWrite( pGia, "gore.aig", 0, 0, 0 );
2238 // reduce the model
2239 pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
2240 if ( pReduce )
2241 {
2242 pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
2243 Gia_ManStop( pAux );
2244 Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0, 0 );
2245// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
2246// Gia_ManPrintStatsShort( pReduce );
2247 Gia_ManStop( pReduce );
2248 }
2249 }
2250 return 1;
2251}
2252
2253
2254
2255
2267int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2, int fLatchA, int fLatchB )
2268{
2269 Gia_Man_t * pGia1, * pGia2, * pMiter;
2270 Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj;
2271 int i, iObj, iNext, Counter = 0;
2272 if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
2273 {
2274 Abc_Print( 1, "Equivalences are not defined.\n" );
2275 return 0;
2276 }
2277 pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
2278 if ( pGia1 == NULL )
2279 {
2280 Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
2281 return 0;
2282 }
2283 pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
2284 if ( pGia2 == NULL )
2285 {
2286 Gia_ManStop( pGia2 );
2287 Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
2288 return 0;
2289 }
2290 pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
2291 if ( pMiter == NULL )
2292 {
2293 Gia_ManStop( pGia1 );
2294 Gia_ManStop( pGia2 );
2295 Abc_Print( 1, "Cannot create sequential miter.\n" );
2296 return 0;
2297 }
2298 // make sure the miter is isomorphic
2299 if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) )
2300 {
2301 Gia_ManStop( pGia1 );
2302 Gia_ManStop( pGia2 );
2303 Gia_ManStop( pMiter );
2304 Abc_Print( 1, "The number of objects in different.\n" );
2305 return 0;
2306 }
2307 if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
2308 {
2309 Gia_ManStop( pGia1 );
2310 Gia_ManStop( pGia2 );
2311 Gia_ManStop( pMiter );
2312 Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
2313 return 0;
2314 }
2315 // transfer copies
2316 Gia_ManCleanMark0( pGia );
2317 Gia_ManForEachObj( pGia1, pObj1, i )
2318 {
2319 if ( pObj1->Value == ~0 )
2320 continue;
2321 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
2322 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2323 pObj->fMark0 = 1;
2324 }
2325 Gia_ManCleanMark1( pGia );
2326 Gia_ManForEachObj( pGia2, pObj2, i )
2327 {
2328 if ( pObj2->Value == ~0 )
2329 continue;
2330 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
2331 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2332 pObj->fMark1 = 1;
2333 }
2334
2335 // filter equivalences
2336 Gia_ManForEachConst( pGia, i )
2337 {
2338 Gia_ObjUnsetRepr( pGia, i );
2339 assert( pGia->pNexts[i] == 0 );
2340 }
2341 Gia_ManForEachClass( pGia, i )
2342 {
2343 // find the first colorA and colorB
2344 int ClassA = -1, ClassB = -1;
2345 Gia_ClassForEachObj( pGia, i, iObj )
2346 {
2347 pObj = Gia_ManObj( pGia, iObj );
2348 if ( ClassA == -1 && pObj->fMark0 && !pObj->fMark1 )
2349 {
2350 if ( fLatchA && !Gia_ObjIsRo(pGia, pObj) )
2351 continue;
2352 ClassA = iObj;
2353 }
2354 if ( ClassB == -1 && pObj->fMark1 && !pObj->fMark0 )
2355 {
2356 if ( fLatchB && !Gia_ObjIsRo(pGia, pObj) )
2357 continue;
2358 ClassB = iObj;
2359 }
2360 }
2361 // undo equivalence classes
2362 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2363 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2364 {
2365 Gia_ObjUnsetRepr( pGia, iObj );
2366 Gia_ObjSetNext( pGia, iObj, 0 );
2367 }
2368 assert( !Gia_ObjIsHead(pGia, i) );
2369 if ( ClassA > 0 && ClassB > 0 )
2370 {
2371 if ( ClassA > ClassB )
2372 {
2373 ClassA ^= ClassB;
2374 ClassB ^= ClassA;
2375 ClassA ^= ClassB;
2376 }
2377 assert( ClassA < ClassB );
2378 Gia_ObjSetNext( pGia, ClassA, ClassB );
2379 Gia_ObjSetRepr( pGia, ClassB, ClassA );
2380 Counter++;
2381 assert( Gia_ObjIsHead(pGia, ClassA) );
2382 }
2383 }
2384 Abc_Print( 1, "The number of two-node classes after filtering = %d.\n", Counter );
2385//Gia_ManEquivPrintClasses( pGia, 1, 0 );
2386
2387 Gia_ManCleanMark0( pGia );
2388 Gia_ManCleanMark1( pGia );
2389 return 1;
2390}
2391
2392
2404int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName2 )
2405{
2406 Vec_Int_t * vNodes;
2407 Gia_Man_t * pGia1, * pGia2, * pMiter;
2408 Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj = NULL;
2409 int i, k, iObj, iNext, iPrev, iRepr;
2410 int iLitsOld, iLitsNew;
2411 if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
2412 {
2413 Abc_Print( 1, "Equivalences are not defined.\n" );
2414 return 0;
2415 }
2416 pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
2417 if ( pGia1 == NULL )
2418 {
2419 Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
2420 return 0;
2421 }
2422 pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
2423 if ( pGia2 == NULL )
2424 {
2425 Gia_ManStop( pGia2 );
2426 Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
2427 return 0;
2428 }
2429 pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
2430 if ( pMiter == NULL )
2431 {
2432 Gia_ManStop( pGia1 );
2433 Gia_ManStop( pGia2 );
2434 Abc_Print( 1, "Cannot create sequential miter.\n" );
2435 return 0;
2436 }
2437 // make sure the miter is isomorphic
2438 if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) )
2439 {
2440 Gia_ManStop( pGia1 );
2441 Gia_ManStop( pGia2 );
2442 Gia_ManStop( pMiter );
2443 Abc_Print( 1, "The number of objects in different.\n" );
2444 return 0;
2445 }
2446 if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
2447 {
2448 Gia_ManStop( pGia1 );
2449 Gia_ManStop( pGia2 );
2450 Gia_ManStop( pMiter );
2451 Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
2452 return 0;
2453 }
2454 // transfer copies
2455 Gia_ManCleanMark0( pGia );
2456 Gia_ManForEachObj( pGia1, pObj1, i )
2457 {
2458 if ( pObj1->Value == ~0 )
2459 continue;
2460 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
2461 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2462 pObj->fMark0 = 1;
2463 }
2464 Gia_ManCleanMark1( pGia );
2465 Gia_ManForEachObj( pGia2, pObj2, i )
2466 {
2467 if ( pObj2->Value == ~0 )
2468 continue;
2469 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
2470 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2471 pObj->fMark1 = 1;
2472 }
2473
2474 // filter equivalences
2475 iLitsOld = iLitsNew = 0;
2476 Gia_ManForEachConst( pGia, i )
2477 {
2478 iLitsOld++;
2479 pObj = Gia_ManObj( pGia, i );
2480 assert( pGia->pNexts[i] == 0 );
2481 assert( pObj->fMark0 || pObj->fMark1 );
2482 if ( pObj->fMark0 && pObj->fMark1 ) // belongs to both A and B
2483 Gia_ObjUnsetRepr( pGia, i );
2484 else
2485 iLitsNew++;
2486 }
2487 // filter equivalences
2488 vNodes = Vec_IntAlloc( 100 );
2489 Gia_ManForEachClass( pGia, i )
2490 {
2491 int fSeenA = 0, fSeenB = 0;
2492 assert( pObj->fMark0 || pObj->fMark1 );
2493 Vec_IntClear( vNodes );
2494 Gia_ClassForEachObj( pGia, i, iObj )
2495 {
2496 pObj = Gia_ManObj( pGia, iObj );
2497 if ( pObj->fMark0 && !pObj->fMark1 )
2498 {
2499 fSeenA = 1;
2500 Vec_IntPush( vNodes, iObj );
2501 }
2502 if ( !pObj->fMark0 && pObj->fMark1 )
2503 {
2504 fSeenB = 1;
2505 Vec_IntPush( vNodes, iObj );
2506 }
2507 iLitsOld++;
2508 }
2509 iLitsOld--;
2510 // undo equivalence classes
2511 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2512 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2513 {
2514 Gia_ObjUnsetRepr( pGia, iObj );
2515 Gia_ObjSetNext( pGia, iObj, 0 );
2516 }
2517 assert( !Gia_ObjIsHead(pGia, i) );
2518 if ( fSeenA && fSeenB && Vec_IntSize(vNodes) > 1 )
2519 {
2520 // create new class
2521 iPrev = iRepr = Vec_IntEntry( vNodes, 0 );
2522 Vec_IntForEachEntryStart( vNodes, iObj, k, 1 )
2523 {
2524 Gia_ObjSetRepr( pGia, iObj, iRepr );
2525 Gia_ObjSetNext( pGia, iPrev, iObj );
2526 iPrev = iObj;
2527 iLitsNew++;
2528 }
2529 assert( Gia_ObjNext(pGia, iPrev) == 0 );
2530 }
2531 }
2532 Vec_IntFree( vNodes );
2533 Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
2534//Gia_ManEquivPrintClasses( pGia, 1, 0 );
2535
2536 Gia_ManCleanMark0( pGia );
2537 Gia_ManCleanMark1( pGia );
2538 return 1;
2539}
2540
2552void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlopsWith, int fUseRiDrivers )
2553{
2554 Gia_Obj_t * pObjR;
2555 Vec_Int_t * vNodes, * vFfIds;
2556 int i, k, iObj, iNext, iPrev, iRepr;
2557 int iLitsOld = 0, iLitsNew = 0;
2558 assert( fFlopsOnly ^ fFlopsWith );
2559 vNodes = Vec_IntAlloc( 100 );
2560 // select nodes "flop" node IDs
2561 vFfIds = Vec_IntStart( Gia_ManObjNum(pGia) );
2562 if ( fUseRiDrivers )
2563 {
2564 Gia_ManForEachRi( pGia, pObjR, i )
2565 Vec_IntWriteEntry( vFfIds, Gia_ObjFaninId0p(pGia, pObjR), 1 );
2566 }
2567 else
2568 {
2569 Gia_ManForEachRo( pGia, pObjR, i )
2570 Vec_IntWriteEntry( vFfIds, Gia_ObjId(pGia, pObjR), 1 );
2571 }
2572 // remove all non-flop constants
2573 Gia_ManForEachConst( pGia, i )
2574 {
2575 iLitsOld++;
2576 assert( pGia->pNexts[i] == 0 );
2577 if ( !Vec_IntEntry(vFfIds, i) )
2578 Gia_ObjUnsetRepr( pGia, i );
2579 else
2580 iLitsNew++;
2581 }
2582 // clear the classes
2583 if ( fFlopsOnly )
2584 {
2585 Gia_ManForEachClass( pGia, i )
2586 {
2587 Vec_IntClear( vNodes );
2588 Gia_ClassForEachObj( pGia, i, iObj )
2589 {
2590 if ( Vec_IntEntry(vFfIds, iObj) )
2591 Vec_IntPush( vNodes, iObj );
2592 iLitsOld++;
2593 }
2594 iLitsOld--;
2595 // undo equivalence classes
2596 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2597 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2598 {
2599 Gia_ObjUnsetRepr( pGia, iObj );
2600 Gia_ObjSetNext( pGia, iObj, 0 );
2601 }
2602 assert( !Gia_ObjIsHead(pGia, i) );
2603 if ( Vec_IntSize(vNodes) > 1 )
2604 {
2605 // create new class
2606 iPrev = iRepr = Vec_IntEntry( vNodes, 0 );
2607 Vec_IntForEachEntryStart( vNodes, iObj, k, 1 )
2608 {
2609 Gia_ObjSetRepr( pGia, iObj, iRepr );
2610 Gia_ObjSetNext( pGia, iPrev, iObj );
2611 iPrev = iObj;
2612 iLitsNew++;
2613 }
2614 assert( Gia_ObjNext(pGia, iPrev) == 0 );
2615 }
2616 }
2617 }
2618 else
2619 {
2620 Gia_ManForEachClass( pGia, i )
2621 {
2622 int fSeenFlop = 0;
2623 Gia_ClassForEachObj( pGia, i, iObj )
2624 {
2625 if ( Vec_IntEntry(vFfIds, iObj) )
2626 fSeenFlop = 1;
2627 iLitsOld++;
2628 iLitsNew++;
2629 }
2630 iLitsOld--;
2631 iLitsNew--;
2632 if ( fSeenFlop )
2633 continue;
2634 // undo equivalence classes
2635 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2636 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2637 {
2638 Gia_ObjUnsetRepr( pGia, iObj );
2639 Gia_ObjSetNext( pGia, iObj, 0 );
2640 iLitsNew--;
2641 }
2642 iLitsNew++;
2643 assert( !Gia_ObjIsHead(pGia, i) );
2644 }
2645 }
2646 Vec_IntFree( vNodes );
2647 Vec_IntFree( vFfIds );
2648 Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
2649}
2650
2662int Gia_ManChangeOrder_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
2663{
2664 if ( ~pObj->Value )
2665 return pObj->Value;
2666 if ( Gia_ObjIsCi(pObj) )
2667 return pObj->Value = Gia_ManAppendCi(pNew);
2668 Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) );
2669 if ( Gia_ObjIsCo(pObj) )
2670 return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2671 Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin1(pObj) );
2672 return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2673}
2674Gia_Man_t * Gia_ManChangeOrder( Gia_Man_t * p )
2675{
2676 Gia_Man_t * pNew;
2677 Gia_Obj_t * pObj;
2678 int i, k;
2679 Gia_ManFillValue( p );
2680 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2681 pNew->pName = Abc_UtilStrsav( p->pName );
2682 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2683 Gia_ManConst0(p)->Value = 0;
2684 Gia_ManForEachCi( p, pObj, i )
2685 pObj->Value = Gia_ManAppendCi(pNew);
2686 Gia_ManForEachClass( p, i )
2687 Gia_ClassForEachObj( p, i, k )
2688 Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) );
2689 Gia_ManForEachConst( p, k )
2690 Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) );
2691 Gia_ManForEachCo( p, pObj, i )
2692 Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) );
2693 Gia_ManForEachCo( p, pObj, i )
2694 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2695 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2696 assert( Gia_ManObjNum(pNew) == Gia_ManObjNum(p) );
2697 return pNew;
2698}
2699void Gia_ManTransferEquivs( Gia_Man_t * p, Gia_Man_t * pNew )
2700{
2701 Vec_Int_t * vClass;
2702 int i, k, iNode, iRepr;
2703 assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) );
2704 assert( p->pReprs != NULL );
2705 assert( p->pNexts != NULL );
2706 assert( pNew->pReprs == NULL );
2707 assert( pNew->pNexts == NULL );
2708 // start representatives
2709 pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
2710 for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
2711 Gia_ObjSetRepr( pNew, i, GIA_VOID );
2712 // iterate over constant candidates
2713 Gia_ManForEachConst( p, i )
2714 Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
2715 // iterate over class candidates
2716 vClass = Vec_IntAlloc( 100 );
2717 Gia_ManForEachClass( p, i )
2718 {
2719 Vec_IntClear( vClass );
2720 Gia_ClassForEachObj( p, i, k )
2721 Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
2722 assert( Vec_IntSize( vClass ) > 1 );
2723 Vec_IntSort( vClass, 0 );
2724 iRepr = Vec_IntEntry( vClass, 0 );
2725 Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
2726 Gia_ObjSetRepr( pNew, iNode, iRepr );
2727 }
2728 Vec_IntFree( vClass );
2729 pNew->pNexts = Gia_ManDeriveNexts( pNew );
2730}
2731void Gia_ManTransferTest( Gia_Man_t * p )
2732{
2733 Gia_Obj_t * pObj; int i;
2734 Gia_Rpr_t * pReprs = p->pReprs; // representatives (for CIs and ANDs)
2735 int * pNexts = p->pNexts; // next nodes in the equivalence classes
2736 Gia_Man_t * pNew = Gia_ManChangeOrder(p);
2737 //Gia_ManEquivPrintClasses( p, 1, 0 );
2738 assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) );
2739 Gia_ManTransferEquivs( p, pNew );
2740 p->pReprs = NULL;
2741 p->pNexts = NULL;
2742 // make new point to old
2743 Gia_ManForEachObj( p, pObj, i )
2744 {
2745 assert( !Abc_LitIsCompl(pObj->Value) );
2746 Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
2747 }
2748 Gia_ManTransferEquivs( pNew, p );
2749 //Gia_ManEquivPrintClasses( p, 1, 0 );
2750 for ( i = 0; i < Gia_ManObjNum(p); i++ )
2751 pReprs[i].fProved = 0;
2752 //printf( "%5d : %5d %5d %5d %5d\n", i, *(int*)&p->pReprs[i], *(int*)&pReprs[i], (int)p->pNexts[i], (int)pNexts[i] );
2753 if ( memcmp(p->pReprs, pReprs, sizeof(int)*Gia_ManObjNum(p)) )
2754 printf( "Verification of reprs failed.\n" );
2755 else
2756 printf( "Verification of reprs succeeded.\n" );
2757 if ( memcmp(p->pNexts, pNexts, sizeof(int)*Gia_ManObjNum(p)) )
2758 printf( "Verification of nexts failed.\n" );
2759 else
2760 printf( "Verification of nexts succeeded.\n" );
2761 ABC_FREE( pNew->pReprs );
2762 ABC_FREE( pNew->pNexts );
2763 ABC_FREE( pReprs );
2764 ABC_FREE( pNexts );
2765 Gia_ManStop( pNew );
2766}
2767
2779void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pOld )
2780{
2781 Gia_Obj_t * pObj;
2782 Vec_Int_t * vClass;
2783 int i, k, iNode, iRepr;
2784 assert( p->pReprs != NULL );
2785 assert( p->pNexts != NULL );
2786 assert( pOld->pReprs == NULL );
2787 assert( pOld->pNexts == NULL );
2788 // create map
2789 Gia_ManFillValue( p );
2790 Gia_ManForEachObj( pOld, pObj, i )
2791 if ( ~pObj->Value )
2792 Gia_ManObj(p, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
2793 // start representatives
2794 pOld->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pOld) );
2795 for ( i = 0; i < Gia_ManObjNum(pOld); i++ )
2796 Gia_ObjSetRepr( pOld, i, GIA_VOID );
2797 // iterate over constant candidates
2798 Gia_ManForEachConst( p, i )
2799 Gia_ObjSetRepr( pOld, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
2800 // iterate over class candidates
2801 vClass = Vec_IntAlloc( 100 );
2802 Gia_ManForEachClass( p, i )
2803 {
2804 Vec_IntClear( vClass );
2805 Gia_ClassForEachObj( p, i, k )
2806 if ( (int)Gia_ManObj(p, k)->Value >= 0 )
2807 Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
2808 if ( Vec_IntSize( vClass ) <= 1 )
2809 continue;
2810 assert( Vec_IntSize( vClass ) > 1 );
2811 Vec_IntSort( vClass, 0 );
2812 iRepr = Vec_IntEntry( vClass, 0 );
2813 Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
2814 Gia_ObjSetRepr( pOld, iNode, iRepr );
2815 }
2816 Vec_IntFree( vClass );
2817 pOld->pNexts = Gia_ManDeriveNexts( pOld );
2818}
2819
2831int Cec4_ManMarkIndependentClasses_rec( Gia_Man_t * p, int iObj )
2832{
2833 Gia_Obj_t * pObj;
2834 assert( iObj > 0 );
2835 if ( Gia_ObjIsTravIdPreviousId(p, iObj) ) // failed
2836 return 0;
2837 if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) // passed
2838 return 1;
2839 Gia_ObjSetTravIdCurrentId(p, iObj);
2840 pObj = Gia_ManObj( p, iObj );
2841 if ( Gia_ObjIsCi(pObj) )
2842 return 1;
2843 assert( Gia_ObjIsAnd(pObj) );
2844 if ( Cec4_ManMarkIndependentClasses_rec( p, Gia_ObjFaninId0(pObj, iObj) ) &&
2845 Cec4_ManMarkIndependentClasses_rec( p, Gia_ObjFaninId1(pObj, iObj) ) )
2846 return 1;
2847 Gia_ObjSetTravIdPreviousId(p, iObj);
2848 return 0;
2849}
2850int Cec4_ManMarkIndependentClasses( Gia_Man_t * p, Gia_Man_t * pNew )
2851{
2852 int iObjNew, iRepr, iObj, Res, fHaveChoices = 0;
2853 Gia_ManCleanMark01(p);
2854 Gia_ManForEachClass( p, iRepr )
2855 {
2856 Gia_ManIncrementTravId( pNew );
2857 Gia_ManIncrementTravId( pNew );
2858 iObjNew = Abc_Lit2Var( Gia_ManObj(p, iRepr)->Value );
2859 Res = Cec4_ManMarkIndependentClasses_rec( pNew, iObjNew );
2860 assert( Res == 1 );
2861 Gia_ObjSetTravIdPreviousId( pNew, iObjNew );
2862 p->pReprs[iRepr].fColorA = 1;
2863 Gia_ClassForEachObj1( p, iRepr, iObj )
2864 {
2865 assert( p->pReprs[iObj].iRepr == (unsigned)iRepr );
2866 iObjNew = Abc_Lit2Var( Gia_ManObj(p, iObj)->Value );
2867 if ( Cec4_ManMarkIndependentClasses_rec( pNew, iObjNew ) )
2868 {
2869 p->pReprs[iObj].fColorA = 1;
2870 fHaveChoices = 1;
2871 }
2872 Gia_ObjSetTravIdPreviousId( pNew, iObjNew );
2873 }
2874 }
2875 return fHaveChoices;
2876}
2877int Cec4_ManSatSolverAnd_rec( Gia_Man_t * pCho, Gia_Man_t * p, Gia_Man_t * pNew, int iObj )
2878{
2879 return 0;
2880}
2881int Cec4_ManSatSolverChoices_rec( Gia_Man_t * pCho, Gia_Man_t * p, Gia_Man_t * pNew, int iObj )
2882{
2883 if ( !Gia_ObjIsClass(p, iObj) )
2884 return Cec4_ManSatSolverAnd_rec( pCho, p, pNew, iObj );
2885 else
2886 {
2887 Vec_Int_t * vLits = Vec_IntAlloc( 100 );
2888 int i, iHead, iNext, iRepr = Gia_ObjIsHead(p, iObj) ? iObj : Gia_ObjRepr(p, iObj);
2889 Gia_ClassForEachObj( p, iRepr, iObj )
2890 if ( p->pReprs[iObj].fColorA )
2891 Vec_IntPush( vLits, Cec4_ManSatSolverAnd_rec( pCho, p, pNew, iObj ) );
2892 Vec_IntSort( vLits, 1 );
2893 iHead = Abc_Lit2Var( Vec_IntEntry(vLits, 0) );
2894 if ( Vec_IntSize(vLits) > 1 )
2895 {
2896 Vec_IntForEachEntryStart( vLits, iNext, i, 1 )
2897 {
2898 pCho->pSibls[iHead] = Abc_Lit2Var(iNext);
2899 iHead = Abc_Lit2Var(iNext);
2900 }
2901 }
2902 return Abc_LitNotCond( Vec_IntEntry(vLits, 0), Gia_ManObj(p, iHead)->fPhase );
2903 }
2904}
2905Gia_Man_t * Cec4_ManSatSolverChoices( Gia_Man_t * p, Gia_Man_t * pNew )
2906{
2907 Gia_Man_t * pCho;
2908 Gia_Obj_t * pObj;
2909 int i, DriverId;
2910 // mark topologically dependent equivalent nodes
2911 if ( !Cec4_ManMarkIndependentClasses( p, pNew ) )
2912 return Gia_ManDup( pNew );
2913 // rebuild AIG in a different order with choices
2914 pCho = Gia_ManStart( Gia_ManObjNum(pNew) );
2915 pCho->pName = Abc_UtilStrsav( p->pName );
2916 pCho->pSpec = Abc_UtilStrsav( p->pSpec );
2917 pCho->pSibls = ABC_CALLOC( int, Gia_ManObjNum(pNew) );
2918 Gia_ManFillValue(pNew);
2919 Gia_ManConst0(pNew)->Value = 0;
2920 for ( i = 0; i < Gia_ManCiNum(pNew); i++ )
2921 Gia_ManCi(pNew, i)->Value = Gia_ManAppendCi( pCho );
2922 Gia_ManForEachCoDriverId( p, DriverId, i )
2923 Cec4_ManSatSolverChoices_rec( pCho, p, pNew, DriverId );
2924 Gia_ManForEachCo( pNew, pObj, i )
2925 pObj->Value = Gia_ManAppendCo( pCho, Gia_ObjFanin0Copy(pObj) );
2926 Gia_ManSetRegNum( pCho, Gia_ManRegNum(p) );
2927 return pCho;
2928}
2929
2941Gia_Man_t * Gia_ManCombSpecReduce( Gia_Man_t * p )
2942{
2943 Gia_Obj_t * pObj, * pRepr; int i, iLit;
2944 Vec_Int_t * vXors = Vec_IntAlloc( 100 );
2945 Gia_Man_t * pTemp, * pNew = Gia_ManStart( Gia_ManObjNum(p) );
2946 assert( p->pReprs && p->pNexts );
2947 pNew->pName = Abc_UtilStrsav( p->pName );
2948 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2949 Gia_ManLevelNum(p);
2950 Gia_ManSetPhase(p);
2951 Gia_ManFillValue(p);
2952 Gia_ManConst0(p)->Value = 0;
2953 Gia_ManForEachCi( p, pObj, i )
2954 pObj->Value = Gia_ManAppendCi( pNew );
2955 Gia_ManHashAlloc( pNew );
2956 Gia_ManForEachAnd( p, pObj, i )
2957 {
2958 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2959 pRepr = Gia_ObjReprObj( p, i );
2960 if ( pRepr && Abc_Lit2Var(pObj->Value) != Abc_Lit2Var(pRepr->Value) )
2961 {
2962 //if ( Gia_ObjLevel(p, pRepr) > Gia_ObjLevel(p, pObj) + 50 )
2963 //printf( "%d %d ", Gia_ObjLevel(p, pRepr), Gia_ObjLevel(p, pObj) );
2964 iLit = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
2965 Vec_IntPush( vXors, Gia_ManHashXor( pNew, pObj->Value, iLit ) );
2966 pObj->Value = iLit;
2967 }
2968 }
2969 Gia_ManHashStop( pNew );
2970 if ( Vec_IntSize(vXors) == 0 )
2971 Vec_IntPush( vXors, 0 );
2972 Vec_IntForEachEntry( vXors, iLit, i )
2973 Gia_ManAppendCo( pNew, iLit );
2974 Vec_IntFree( vXors );
2975 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2976 pNew = Gia_ManCleanup( pTemp = pNew );
2977 Gia_ManStop( pTemp );
2978 return pNew;
2979}
2980void Gia_ManCombSpecReduceTest( Gia_Man_t * p, char * pFileName )
2981{
2982 Gia_Man_t * pSrm = Gia_ManCombSpecReduce( p );
2983 if ( pFileName == NULL )
2984 pFileName = "test.aig";
2985 Gia_AigerWrite( pSrm, pFileName, 0, 0, 0 );
2986 Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
2987 Gia_ManStop( pSrm );
2988}
2989
2993
2994
2995ABC_NAMESPACE_IMPL_END
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
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
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Saig_BmcPerform
int Saig_BmcPerform(Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent, int fUseSatoko)
Definition bmcBmc2.c:811
Cec_ManSimClassCreate
void Cec_ManSimClassCreate(Gia_Man_t *p, Vec_Int_t *vClass)
Definition cecClass.c:234
Cec_ParFra_t
struct Cec_ParFra_t_ Cec_ParFra_t
Definition cec.h:96
Cec_ManCheckNonTrivialCands
int Cec_ManCheckNonTrivialCands(Gia_Man_t *pAig)
Definition cecSeq.c:295
Cec_ManFraSetDefaultParams
void Cec_ManFraSetDefaultParams(Cec_ParFra_t *p)
Definition cecCore.c:126
Cec_ManSeqResimulateCounter
int Cec_ManSeqResimulateCounter(Gia_Man_t *pAig, Cec_ParSim_t *pPars, Abc_Cex_t *pCex)
Definition cecSeq.c:215
Cec_ManSatSweeping
Gia_Man_t * Cec_ManSatSweeping(Gia_Man_t *pAig, Cec_ParFra_t *pPars, int fSilent)
Definition cecCore.c:344
Cec_ManSimSetDefaultParams
void Cec_ManSimSetDefaultParams(Cec_ParSim_t *p)
Definition cecCore.c:71
Cec_ParSim_t
struct Cec_ParSim_t_ Cec_ParSim_t
Definition cec.h:60
p
Cube * p
Definition exorList.c:222
Gia_ManToAig
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition giaAig.c:318
Cec4_ManSatSolverChoices_rec
int Cec4_ManSatSolverChoices_rec(Gia_Man_t *pCho, Gia_Man_t *p, Gia_Man_t *pNew, int iObj)
Definition giaEquiv.c:2881
Gia_ManEquivImprove
void Gia_ManEquivImprove(Gia_Man_t *p)
Definition giaEquiv.c:1780
Gia_ManEquivFixOutputPairs
void Gia_ManEquivFixOutputPairs(Gia_Man_t *p)
Definition giaEquiv.c:882
Gia_ManCheckTopoOrder
int Gia_ManCheckTopoOrder(Gia_Man_t *p)
Definition giaEquiv.c:236
Gia_ManChangeOrder_rec
int Gia_ManChangeOrder_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaEquiv.c:2662
Gia_ManTransferEquivs
void Gia_ManTransferEquivs(Gia_Man_t *p, Gia_Man_t *pNew)
Definition giaEquiv.c:2699
Gia_ManEquivFilter
void Gia_ManEquivFilter(Gia_Man_t *p, Vec_Int_t *vPoIds, int fVerbose)
Definition giaEquiv.c:1678
Gia_ManSpecReduce
Gia_Man_t * Gia_ManSpecReduce(Gia_Man_t *p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose)
Definition giaEquiv.c:1253
Gia_ManEquivCountLits
int Gia_ManEquivCountLits(Gia_Man_t *p)
Definition giaEquiv.c:450
Gia_CommandSpecI
int Gia_CommandSpecI(Gia_Man_t *pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose)
Definition giaEquiv.c:2168
Gia_ManTransferTest
void Gia_ManTransferTest(Gia_Man_t *p)
Definition giaEquiv.c:2731
Gia_ObjCheckTfi
int Gia_ObjCheckTfi(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
Definition giaEquiv.c:1877
Gia_ManEquivToChoices_rec
void Gia_ManEquivToChoices_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaEquiv.c:1925
Gia_ManEquivCountLitsAll
int Gia_ManEquivCountLitsAll(Gia_Man_t *p)
Definition giaEquiv.c:357
Gia_ManEquivReduce
Gia_Man_t * Gia_ManEquivReduce(Gia_Man_t *p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose)
Definition giaEquiv.c:677
Gia_ManCombSpecReduce
Gia_Man_t * Gia_ManCombSpecReduce(Gia_Man_t *p)
Definition giaEquiv.c:2941
Gia_MakeRandomChoice
Gia_Obj_t * Gia_MakeRandomChoice(Gia_Man_t *p, int iRepr)
Definition giaEquiv.c:762
Gia_ManEquivSetColor_rec
int Gia_ManEquivSetColor_rec(Gia_Man_t *p, Gia_Obj_t *pObj, int fOdds)
Definition giaEquiv.c:1075
Gia_ManCountChoiceNodes
int Gia_ManCountChoiceNodes(Gia_Man_t *p)
Definition giaEquiv.c:2091
Gia_ManOrigIdsStart
void Gia_ManOrigIdsStart(Gia_Man_t *p)
Definition giaEquiv.c:51
Gia_ManDeriveReprsFromSibls
void Gia_ManDeriveReprsFromSibls(Gia_Man_t *p)
Definition giaEquiv.c:325
Gia_ManDeriveReprs
void Gia_ManDeriveReprs(Gia_Man_t *p)
Definition giaEquiv.c:293
Gia_ManTransferEquivs2
void Gia_ManTransferEquivs2(Gia_Man_t *p, Gia_Man_t *pOld)
Definition giaEquiv.c:2779
Gia_ManEquivDeriveReprs
void Gia_ManEquivDeriveReprs(Gia_Man_t *p, Gia_Man_t *pNew, Gia_Man_t *pFinal)
Definition giaEquiv.c:935
Gia_ManDeriveNexts
int * Gia_ManDeriveNexts(Gia_Man_t *p)
Definition giaEquiv.c:260
Gia_ManEquivSetColors
int Gia_ManEquivSetColors(Gia_Man_t *p, int fVerbose)
Definition giaEquiv.c:1097
Cec4_ManMarkIndependentClasses_rec
int Cec4_ManMarkIndependentClasses_rec(Gia_Man_t *p, int iObj)
Definition giaEquiv.c:2831
Gia_ManOrigIdsReduceTest
Gia_Man_t * Gia_ManOrigIdsReduceTest(Gia_Man_t *p, Vec_Int_t *vPairs)
Definition giaEquiv.c:160
Gia_ManChoiceMinLevel_rec
int Gia_ManChoiceMinLevel_rec(Gia_Man_t *p, int iPivot, int fDiveIn, Vec_Int_t *vMap)
Definition giaEquiv.c:560
Cec4_ManSatSolverAnd_rec
int Cec4_ManSatSolverAnd_rec(Gia_Man_t *pCho, Gia_Man_t *p, Gia_Man_t *pNew, int iObj)
Definition giaEquiv.c:2877
Gia_ManRemoveBadChoices
void Gia_ManRemoveBadChoices(Gia_Man_t *p)
Definition giaEquiv.c:1986
Gia_ManEquivReduce2_rec
void Gia_ManEquivReduce2_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vMap, int fDiveIn)
Definition giaEquiv.c:786
Gia_ManEquivFilterTest
void Gia_ManEquivFilterTest(Gia_Man_t *p)
Definition giaEquiv.c:1754
Cec4_ManSatSolverChoices
Gia_Man_t * Cec4_ManSatSolverChoices(Gia_Man_t *p, Gia_Man_t *pNew)
Definition giaEquiv.c:2905
Gia_ManSpecReduceInit_rec
void Gia_ManSpecReduceInit_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vXorLits, int f, int fDualOut)
Definition giaEquiv.c:1368
Gia_ManEquivUpdatePointers
void Gia_ManEquivUpdatePointers(Gia_Man_t *p, Gia_Man_t *pNew)
Definition giaEquiv.c:910
Gia_ManCombSpecReduceTest
void Gia_ManCombSpecReduceTest(Gia_Man_t *p, char *pFileName)
Definition giaEquiv.c:2980
Gia_ManEquivPrintClasses
void Gia_ManEquivPrintClasses(Gia_Man_t *p, int fVerbose, float Mem)
Definition giaEquiv.c:501
Gia_ManPrintStatsClasses
void Gia_ManPrintStatsClasses(Gia_Man_t *p)
Definition giaEquiv.c:416
Gia_ManHasNoEquivs
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START int Gia_ManHasNoEquivs(Gia_Man_t *p)
Definition giaEquiv.c:2145
Gia_ManOrigIdsInit
ABC_NAMESPACE_IMPL_START void Gia_ManOrigIdsInit(Gia_Man_t *p)
DECLARATIONS ///.
Definition giaEquiv.c:46
Gia_ManEquivMark
void Gia_ManEquivMark(Gia_Man_t *p, char *pFileName, int fSkipSome, int fVerbose)
Definition giaEquiv.c:1580
Gia_ManEquivPrintOne
void Gia_ManEquivPrintOne(Gia_Man_t *p, int i, int Counter)
Definition giaEquiv.c:489
Gia_ManSpecReduce_rec
void Gia_ManSpecReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vXorLits, int fDualOut, int fSpeculate, Vec_Int_t *vTrace, Vec_Int_t *vGuide, Vec_Int_t *vMap)
Definition giaEquiv.c:1175
Gia_ManChoiceMinLevel
Vec_Int_t * Gia_ManChoiceMinLevel(Gia_Man_t *p)
Definition giaEquiv.c:593
Gia_ManEquivCountOne
int Gia_ManEquivCountOne(Gia_Man_t *p, int i)
Definition giaEquiv.c:479
Gia_ManSpecBuildInit
void Gia_ManSpecBuildInit(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vXorLits, int f, int fDualOut)
Definition giaEquiv.c:1341
Gia_ManEquivCountClasses
int Gia_ManEquivCountClasses(Gia_Man_t *p)
Definition giaEquiv.c:376
Cec4_ManMarkIndependentClasses
int Cec4_ManMarkIndependentClasses(Gia_Man_t *p, Gia_Man_t *pNew)
Definition giaEquiv.c:2850
Gia_ManEquivRemapDfs
Gia_Man_t * Gia_ManEquivRemapDfs(Gia_Man_t *p)
Definition giaEquiv.c:994
Gia_ManComputeGiaEquivs
Gia_Man_t * Gia_ManComputeGiaEquivs(Gia_Man_t *pGia, int nConfs, int fVerbose)
Definition giaEquiv.c:183
Gia_ManOrigIdsRemapPairsExtract
int Gia_ManOrigIdsRemapPairsExtract(Vec_Int_t *vMap, int One)
Definition giaEquiv.c:81
Gia_ManCountChoices
int Gia_ManCountChoices(Gia_Man_t *p)
Definition giaEquiv.c:2113
Gia_ManCheckTopoOrder_rec
int Gia_ManCheckTopoOrder_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaEquiv.c:209
Gia_ObjCheckTfi_rec
int Gia_ObjCheckTfi_rec(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode, Vec_Ptr_t *vVisited)
Definition giaEquiv.c:1841
Gia_ManOrigIdsRemapPairs
Vec_Int_t * Gia_ManOrigIdsRemapPairs(Vec_Int_t *vEquivPairs, int nObjs)
Definition giaEquiv.c:87
Gia_ManEquivTransform
void Gia_ManEquivTransform(Gia_Man_t *p, int fVerbose)
Definition giaEquiv.c:1519
Gia_ManEquivToChoices
Gia_Man_t * Gia_ManEquivToChoices(Gia_Man_t *p, int nSnapshots)
Definition giaEquiv.c:2034
Gia_ManSpecReduceTrace
Gia_Man_t * Gia_ManSpecReduceTrace(Gia_Man_t *p, Vec_Int_t *vTrace, Vec_Int_t *vMap)
Definition giaEquiv.c:1197
Gia_ManFilterEquivsUsingParts
int Gia_ManFilterEquivsUsingParts(Gia_Man_t *pGia, char *pName1, char *pName2)
Definition giaEquiv.c:2404
Gia_ManEquivReduce2
Gia_Man_t * Gia_ManEquivReduce2(Gia_Man_t *p, int fRandom)
Definition giaEquiv.c:811
Gia_ManEquivReduce_rec
void Gia_ManEquivReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int fUseAll, int fDualOut)
Definition giaEquiv.c:649
Gia_ManEquivCheckLits
int Gia_ManEquivCheckLits(Gia_Man_t *p, int nLits)
Definition giaEquiv.c:397
Gia_ManAddNextEntry_rec
void Gia_ManAddNextEntry_rec(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
Definition giaEquiv.c:1904
Gia_ManFilterEquivsUsingLatches
void Gia_ManFilterEquivsUsingLatches(Gia_Man_t *pGia, int fFlopsOnly, int fFlopsWith, int fUseRiDrivers)
Definition giaEquiv.c:2552
Gia_ManChangeOrder
Gia_Man_t * Gia_ManChangeOrder(Gia_Man_t *p)
Definition giaEquiv.c:2674
Gia_ManFilterEquivsForSpeculation
int Gia_ManFilterEquivsForSpeculation(Gia_Man_t *pGia, char *pName1, char *pName2, int fLatchA, int fLatchB)
Definition giaEquiv.c:2267
Gia_ManOrigIdsRemapPairsInsert
void Gia_ManOrigIdsRemapPairsInsert(Vec_Int_t *vMap, int One, int Two)
Definition giaEquiv.c:71
Gia_ManOrigIdsRemap
void Gia_ManOrigIdsRemap(Gia_Man_t *p, Gia_Man_t *pNew)
Definition giaEquiv.c:56
Gia_ManSpecReduceInitFrames
Gia_Man_t * Gia_ManSpecReduceInitFrames(Gia_Man_t *p, Abc_Cex_t *pInit, int nFramesMax, int *pnFrames, int fDualOut, int nMinOutputs)
Definition giaEquiv.c:1480
Gia_ManOrigIdsReduce
Gia_Man_t * Gia_ManOrigIdsReduce(Gia_Man_t *p, Vec_Int_t *vPairs)
Definition giaEquiv.c:106
Gia_ManEquivReduceAndRemap
Gia_Man_t * Gia_ManEquivReduceAndRemap(Gia_Man_t *p, int fSeq, int fMiterPairs)
Definition giaEquiv.c:1040
Gia_ManSpecReduceInit
Gia_Man_t * Gia_ManSpecReduceInit(Gia_Man_t *p, Abc_Cex_t *pInit, int nFrames, int fDualOut)
Definition giaEquiv.c:1390
Gia_Rpr_t
struct Gia_Rpr_t_ Gia_Rpr_t
Definition gia.h:57
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_ManCombMarkUsed
int Gia_ManCombMarkUsed(Gia_Man_t *p)
Definition giaScl.c:60
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManSeqMarkUsed
int Gia_ManSeqMarkUsed(Gia_Man_t *p)
Definition giaScl.c:156
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_ManForEachConst
#define Gia_ManForEachConst(p, i)
Definition gia.h:1099
Gia_AigerRead
Gia_Man_t * Gia_AigerRead(char *pFileName, int fGiaSimple, int fSkipStrash, int fCheck)
Definition giaAiger.c:1017
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManForEachCoDriverId
#define Gia_ManForEachCoDriverId(p, DriverId, i)
Definition gia.h:1246
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ClassForEachObj1
#define Gia_ClassForEachObj1(p, i, iObj)
Definition gia.h:1109
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManDupMarked
Gia_Man_t * Gia_ManDupMarked(Gia_Man_t *p)
Definition giaDup.c:1444
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:668
Gia_ClassForEachObj
#define Gia_ClassForEachObj(p, i, iObj)
Definition gia.h:1107
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition gia.h:1192
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_NodeMffcSize
int Gia_NodeMffcSize(Gia_Man_t *p, Gia_Obj_t *pNode)
Definition giaUtil.c:1230
Gia_ManForEachClassReverse
#define Gia_ManForEachClassReverse(p, i)
Definition gia.h:1105
Gia_ManForEachClass
#define Gia_ManForEachClass(p, i)
Definition gia.h:1101
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManDupDfs
Gia_Man_t * Gia_ManDupDfs(Gia_Man_t *p)
Definition giaDup.c:1748
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManSeqStructSweep
Gia_Man_t * Gia_ManSeqStructSweep(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition giaScl.c:258
Gia_ManGetDangling
Vec_Int_t * Gia_ManGetDangling(Gia_Man_t *p)
Definition giaUtil.c:1422
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
Gia_ManCleanLevels
void Gia_ManCleanLevels(Gia_Man_t *p, int Size)
Definition giaUtil.c:511
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManMiter
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition giaDup.c:2983
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_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition giaUtil.c:420
GIA_VOID
#define GIA_VOID
Definition gia.h:46
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition giaMan.c:495
Gia_ManCleanMark01
void Gia_ManCleanMark01(Gia_Man_t *p)
Definition giaUtil.c:218
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition giaUtil.c:546
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition giaUtil.c:313
Cec_ParFra_t_::nBTLimit
int nBTLimit
Definition cec.h:103
Cec_ParFra_t_::nItersMax
int nItersMax
Definition cec.h:102
Cec_ParFra_t_::fVerbose
int fVerbose
Definition cec.h:121
Cec_ParFra_t_::fSatSweeping
int fSatSweeping
Definition cec.h:116
Cec_ParFra_t_::fUseOrigIds
int fUseOrigIds
Definition cec.h:119
Cec_ParSim_t_::fCheckMiter
int fCheckMiter
Definition cec.h:69
Gia_Man_t_::pSibls
int * pSibls
Definition gia.h:128
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition gia.h:126
Gia_Man_t_::pNexts
int * pNexts
Definition gia.h:127
Gia_Man_t_::vIdsOrig
Vec_Int_t * vIdsOrig
Definition gia.h:189
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Man_t_::vIdsEquiv
Vec_Int_t * vIdsEquiv
Definition gia.h:190
Gia_Man_t_::pObjs
Gia_Obj_t * pObjs
Definition gia.h:105
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Gia_Obj_t_::fCompl0
unsigned fCompl0
Definition gia.h:80
Gia_Obj_t_::iDiff0
unsigned iDiff0
Definition gia.h:79
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
Gia_Rpr_t_::iRepr
unsigned iRepr
Definition gia.h:60
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
memcmp
int memcmp()
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_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