diff options
Diffstat (limited to 'src/proof/acec/acecOrder.c')
| -rw-r--r-- | src/proof/acec/acecOrder.c | 64 |
1 files changed, 50 insertions, 14 deletions
diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c index fbce0835..9b2242d0 100644 --- a/src/proof/acec/acecOrder.c +++ b/src/proof/acec/acecOrder.c @@ -44,20 +44,41 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose ) { + int fDumpLeftOver = 0; int i, iXor, iMaj, iAnd, Entry, Iter, fFound, fFoundAll = 1; - Vec_Int_t * vRecord = Vec_IntAlloc( 100 ); + Vec_Int_t * vRecord = Vec_IntAlloc( 100 ), * vLeft, * vRecord2; Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) ); Gia_ManForEachCoDriverId( pGia, iAnd, i ) Vec_IntWriteEntry( vMap, iAnd, 1 ); + + // collect the last XOR + Vec_IntFreeP( &pGia->vXors ); + pGia->vXors = Gia_PolynCollectLastXor( pGia, fVerbose ); + printf( "Collected %d topmost XORs\n", Vec_IntSize(pGia->vXors) ); + //Vec_IntPrint( p->vXors ); + Vec_IntForEachEntry( pGia->vXors, iAnd, i ) + { + Gia_Obj_t * pAnd = Gia_ManObj( pGia, iAnd ); + assert( Vec_IntEntry(vMap, iAnd) ); + Vec_IntWriteEntry( vMap, iAnd, 0 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 ); + Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 3) ); + if ( fVeryVerbose ) + printf( "Recognizing %d => XXXOR(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) ); + } + + // detect FAs and HAs for ( Iter = 0; fFoundAll; Iter++ ) { if ( fVeryVerbose ) printf( "Iteration %d\n", Iter ); + // check if we can extract FADDs fFoundAll = 0; do { fFound = 0; - for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + for ( i = Vec_IntSize(vFadds)/5 - 1; i >= 0; i-- ) { iXor = Vec_IntEntry(vFadds, 5*i+3); iMaj = Vec_IntEntry(vFadds, 5*i+4); @@ -68,8 +89,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+0), 1 ); Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+1), 1 ); Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+2), 1 ); - //Vec_IntPush( vRecord, iXor ); - //Vec_IntPush( vRecord, iMaj ); Vec_IntPush( vRecord, Abc_Var2Lit2(i, 2) ); fFound = 1; fFoundAll = 1; @@ -81,7 +100,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t // check if we can extract HADDs do { fFound = 0; - for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) + for ( i = Vec_IntSize(vHadds)/2 - 1; i >= 0; i-- ) { iXor = Vec_IntEntry(vHadds, 2*i+0); iMaj = Vec_IntEntry(vHadds, 2*i+1); @@ -92,8 +111,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, iMaj, 0 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iMaj), 1 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iMaj), 1 ); - //Vec_IntPush( vRecord, iXor ); - //Vec_IntPush( vRecord, iMaj ); Vec_IntPush( vRecord, Abc_Var2Lit2(i, 1) ); fFound = 1; fFoundAll = 1; @@ -105,6 +122,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t } while ( fFound ); if ( fFoundAll ) continue; +/* // find the last one Vec_IntForEachEntryReverse( vMap, Entry, iAnd ) if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, iAnd)) )//&& Vec_IntFind(vFadds, iAnd) == -1 )//&& Vec_IntFind(vHadds, iAnd) == -1 ) @@ -115,7 +133,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, iAnd, 0 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 ); - //Vec_IntPush( vRecord, iAnd ); Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) ); } else @@ -123,7 +140,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, iAnd, 0 ); Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 ); Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 ); - //Vec_IntPush( vRecord, iAnd ); Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) ); Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId0(pAnd, iAnd), 0) ); Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId1(pAnd, iAnd), 0) ); @@ -134,21 +150,39 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t printf( "Recognizing %d => AND(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) ); break; } +*/ } //Vec_IntPrint( vMap ); -/* + // collect remaining ones + vLeft = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vMap, Entry, i ) + if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) ) + Vec_IntPush( vLeft, i ); + Vec_IntFree( vMap ); + + // collect them in the topo order + vRecord2 = Vec_IntAlloc( 100 ); + Gia_ManIncrementTravId( pGia ); + Gia_ManCollectAnds( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), vRecord2, NULL ); + Vec_IntForEachEntry( vRecord2, iAnd, i ) + Vec_IntWriteEntry( vRecord2, i, Abc_Var2Lit2(iAnd, 0) ); + // dump remaining nodes as an AIG if ( fDumpLeftOver ) { - Gia_Man_t * pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), 0 ); + Gia_Man_t * pNew; + pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 ); Gia_AigerWrite( pNew, "leftover.aig", 0, 0 ); + printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" ); Gia_ManStop( pNew ); } -*/ - Vec_IntFree( vMap ); + Vec_IntFree( vLeft ); + Vec_IntReverseOrder( vRecord ); - return vRecord; + Vec_IntAppend( vRecord2, vRecord ); + Vec_IntFree( vRecord ); + return vRecord2; } /**Function************************************************************* @@ -191,7 +225,9 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose ) } else Gia_ManCollectAnds_rec( pGia, Node, vOrder ); + //printf( "Order = %d. Node = %d. Size = %d ", i, Node, Vec_IntSize(vOrder) ); } + //printf( "\n" ); //assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) ); // remap order |