From 652b2792345978c34ea614800b76996930a21a49 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 8 May 2016 19:01:46 -0700 Subject: Experiments with CEC for arithmetic circuits. --- src/proof/acec/acecOrder.c | 172 ++++++++++++++++++++++++++++----------------- 1 file changed, 106 insertions(+), 66 deletions(-) (limited to 'src/proof/acec/acecOrder.c') diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c index 0cf686c8..fbce0835 100644 --- a/src/proof/acec/acecOrder.c +++ b/src/proof/acec/acecOrder.c @@ -42,44 +42,19 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) +Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose ) { - int fDumpLeftOver = 0; - Vec_Int_t * vOrder, * vOrder2; - Gia_Obj_t * pFan0, * pFan1; - int i, k, iDriver, Iter, iXor, iMaj, Entry, fFound; - Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVerbose ); - Vec_Int_t * vHadds = Gia_ManDetectHalfAdders( pGia, fVerbose ); + int i, iXor, iMaj, iAnd, Entry, Iter, fFound, fFoundAll = 1; Vec_Int_t * vRecord = Vec_IntAlloc( 100 ); - Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) ); - Gia_ManForEachCoDriverId( pGia, iDriver, i ) - Vec_IntWriteEntry( vMap, iDriver, 1 ); - - for ( Iter = 0; ; Iter++ ) + Gia_ManForEachCoDriverId( pGia, iAnd, i ) + Vec_IntWriteEntry( vMap, iAnd, 1 ); + for ( Iter = 0; fFoundAll; Iter++ ) { - int fFoundAll = 0; - printf( "Iteration %d\n", Iter ); - - // find the last one - iDriver = -1; - Vec_IntForEachEntryReverse( vMap, Entry, i ) - if ( Entry ) - { - iDriver = i; - break; - } - - if ( iDriver > 0 && Gia_ObjRecognizeExor(Gia_ManObj(pGia, iDriver), &pFan0, &pFan1) && Vec_IntFind(vFadds, iDriver) == -1 && Vec_IntFind(vHadds, iDriver) == -1 ) - { - Vec_IntWriteEntry( vMap, iDriver, 0 ); - Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 ); - Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 ); - Vec_IntPush( vRecord, iDriver ); - printf( "Recognizing %d => XOR(%d %d)\n", iDriver, Gia_ObjId(pGia, pFan0), Gia_ObjId(pGia, pFan1) ); - } - + 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++ ) @@ -93,19 +68,23 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) 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, iXor ); + //Vec_IntPush( vRecord, iMaj ); + Vec_IntPush( vRecord, Abc_Var2Lit2(i, 2) ); fFound = 1; fFoundAll = 1; - printf( "Recognizing (%d %d) => FA(%d %d %d)\n", iXor, iMaj, Vec_IntEntry(vFadds, 5*i+0), Vec_IntEntry(vFadds, 5*i+1), Vec_IntEntry(vFadds, 5*i+2) ); + if ( fVeryVerbose ) + printf( "Recognizing (%d %d) => FA(%d %d %d)\n", iXor, iMaj, Vec_IntEntry(vFadds, 5*i+0), Vec_IntEntry(vFadds, 5*i+1), Vec_IntEntry(vFadds, 5*i+2) ); } } } while ( fFound ); // check if we can extract HADDs do { - fFound = 0; - Vec_IntForEachEntryDouble( vHadds, iXor, iMaj, i ) + fFound = 0; + for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) { + iXor = Vec_IntEntry(vHadds, 2*i+0); + iMaj = Vec_IntEntry(vHadds, 2*i+1); if ( Vec_IntEntry(vMap, iXor) && Vec_IntEntry(vMap, iMaj) ) { Gia_Obj_t * pAnd = Gia_ManObj( pGia, iMaj ); @@ -113,32 +92,52 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) 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, iXor ); + //Vec_IntPush( vRecord, iMaj ); + Vec_IntPush( vRecord, Abc_Var2Lit2(i, 1) ); fFound = 1; fFoundAll = 1; - printf( "Recognizing (%d %d) => HA(%d %d)\n", iXor, iMaj, Gia_ObjFaninId0(pAnd, iMaj), Gia_ObjFaninId1(pAnd, iMaj) ); + if ( fVeryVerbose ) + printf( "Recognizing (%d %d) => HA(%d %d)\n", iXor, iMaj, Gia_ObjFaninId0(pAnd, iMaj), Gia_ObjFaninId1(pAnd, iMaj) ); } } + break; // only one iter! } while ( fFound ); - if ( fFoundAll == 0 ) - break; + 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 ) + { + Gia_Obj_t * pFan0, * pFan1, * pAnd = Gia_ManObj( pGia, iAnd ); + if ( !Gia_ObjRecognizeExor(pAnd, &pFan0, &pFan1) ) + { + 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 + { + 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) ); + printf( "Recognizing %d => XOR(%d %d)\n", iAnd, Gia_ObjId(pGia, pFan0), Gia_ObjId(pGia, pFan1) ); + } + fFoundAll = 1; + if ( fVeryVerbose ) + printf( "Recognizing %d => AND(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) ); + break; + } } + //Vec_IntPrint( vMap ); - //Vec_IntPrint( vRecord ); - printf( "Remaining: " ); - Vec_IntForEachEntry( vMap, Entry, i ) - if ( Entry ) - printf( "%d ", i ); - printf( "\n" ); - - // collect remaining nodes - k = 0; - Vec_IntForEachEntry( vMap, Entry, i ) - if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) ) - Vec_IntWriteEntry( vMap, k++, i ); - Vec_IntShrink( vMap, k ); - +/* // dump remaining nodes as an AIG if ( fDumpLeftOver ) { @@ -146,25 +145,66 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) Gia_AigerWrite( pNew, "leftover.aig", 0, 0 ); Gia_ManStop( pNew ); } +*/ + Vec_IntFree( vMap ); + Vec_IntReverseOrder( vRecord ); + return vRecord; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose ) +{ + Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVeryVerbose ); + Vec_Int_t * vHadds = Gia_ManDetectHalfAdders( pGia, fVeryVerbose ); + Vec_Int_t * vRecord = Gia_PolynFindOrder( pGia, vFadds, vHadds, fVerbose, fVeryVerbose ); + Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManAndNum(pGia) ); + Vec_Int_t * vOrder2 = Vec_IntStart( Gia_ManObjNum(pGia) ); + int i, k, Entry; // collect nodes - vOrder = Vec_IntAlloc( Gia_ManAndNum(pGia) ); Gia_ManIncrementTravId( pGia ); - Gia_ManCollectAnds( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), vOrder, NULL ); - Vec_IntForEachEntryReverse( vRecord, Entry, i ) - Gia_ManCollectAnds_rec( pGia, Entry, vOrder ); - assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) ); + Vec_IntForEachEntry( vRecord, Entry, i ) + { + int Node = Abc_Lit2Var2(Entry); + int Attr = Abc_Lit2Att2(Entry); + if ( Attr == 2 ) + { + int * pFanins = Vec_IntEntryP( vFadds, 5*Node ); + for ( k = 3; k < 5; k++ ) + Gia_ManCollectAnds_rec( pGia, pFanins[k], vOrder ); + } + else if ( Attr == 1 ) + { + int * pFanins = Vec_IntEntryP( vHadds, 2*Node ); + for ( k = 0; k < 2; k++ ) + Gia_ManCollectAnds_rec( pGia, pFanins[k], vOrder ); + } + else + Gia_ManCollectAnds_rec( pGia, Node, vOrder ); + } + //assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) ); // remap order - vOrder2 = Vec_IntStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachCiId( pGia, Entry, i ) + Vec_IntWriteEntry( vOrder2, Entry, 1+i ); Vec_IntForEachEntry( vOrder, Entry, i ) - Vec_IntWriteEntry( vOrder2, Entry, i+1 ); - Vec_IntFree( vOrder ); + Vec_IntWriteEntry( vOrder2, Entry, 1+Gia_ManCiNum(pGia)+i ); + //Vec_IntPrint( vOrder ); - Vec_IntFree( vMap ); Vec_IntFree( vRecord ); Vec_IntFree( vFadds ); Vec_IntFree( vHadds ); + Vec_IntFree( vOrder ); return vOrder2; } -- cgit v1.2.3