diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index aa8f1c053..37b3e8e3b 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,9 +30,12 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -Vec_Int_t* vMarkBmiter; -Vec_Int_t* vIdBI; -Vec_Int_t* vIdBO; +Vec_Ptr_t* vBmiter2Spec; +Vec_Ptr_t* vBmiter2Impl; +Vec_Int_t* vPatch2Impl; +Vec_Bit_t* vImpl2Spec_phase; +Vec_Int_t* vBI_patch; +Vec_Int_t* vBO_patch; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -5702,186 +5705,55 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Gia_ManConst0(p1)->Value = 0; Gia_ManConst0(p2)->Value = 0; - // allocate vMarkBmiter - vMarkBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); - Vec_IntFill( vMarkBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); - printf( "allocated size: %d\n", Vec_IntSize(vMarkBmiter) ); + // allocate vImpl2Spec_phase; + vImpl2Spec_phase = Vec_BitAlloc( Gia_ManObjNum(p2) ); + Vec_BitFill( vImpl2Spec_phase, Gia_ManObjNum(p2), 0 ); + + // allocate vBmiter2Impl and vBmiter2Spec + Vec_Int_t* pVec_Int; + vBmiter2Impl = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); + Vec_PtrFill( vBmiter2Impl, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); + Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Impl, pVec_Int, i) + { + Vec_PtrSetEntry(vBmiter2Impl, i, Vec_IntAlloc(2) ); + } + vBmiter2Spec = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); + Vec_PtrFill( vBmiter2Spec, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); + Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Spec, pVec_Int, i) + { + Vec_PtrSetEntry(vBmiter2Spec, i, Vec_IntAlloc(2) ); + } Gia_ManForEachCi( p1, pObj, i ) { - int id = pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); - Vec_IntSetEntry( vMarkBmiter, id >> 1, 4 ); + pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); + Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); // same pi id in impl and spec } // TODO: record the corresponding impl node of each lit - Gia_ManForEachAnd( p2, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 ); + Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p2, pObj) ); } - // TODO: find nodes in spec - - Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 ); - Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 ); - int n = Gia_ManBufNum(p1) / 2; - if(biNum > 0){ - n = biNum; - } - - Gia_ManStaticFanoutStart( p1 ); - Vec_Ptr_t * vQ = Vec_PtrAlloc(16); - Vec_Ptr_t * vBO = Vec_PtrAlloc(16); - Gia_Obj_t * pObj2; - int c1 = 0; - int c2 = 0; - int count = 0; - - vIdBI = Vec_IntAlloc(16); - vIdBO = Vec_IntAlloc(16); - - Gia_ManForEachBuf( p1, pObj, i ) - { - if ( count < n ) - { - Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 1 ); - c1++; - count ++; - - Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue; - c1 ++; - Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 1 ); - if ( Gia_ObjFaninNum(p1, pObj2) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj2) ); - if ( Gia_ObjFaninNum(p1, pObj2) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj2) ); - } - - } - else - { - Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 ); - Vec_PtrPush( vBO, pObj ); - c2 ++; - - int j; - // pObj = Gia_ObjFanin0(pObj); - Gia_ObjForEachFanoutStatic(p1, pObj, pObj2, j) - { - Vec_PtrPush( vQ, pObj2 ); - } - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue; - Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 2 ); - c2 ++; - for( int j = 0; j < Gia_ObjFanoutNum(p1, pObj2); j++ ) - { - Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj2, j) ); - } - } - - } - } - - Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) ); - Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 ); - int id; - int count_node = 0; - - // count nodes - Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) - { - Vec_PtrPush( vQ, pObj ); - } - while( Vec_PtrSize(vQ) > 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p1, pObj ); - if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 0 ) continue; - Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 1 ); - count_node ++; - - if ( Vec_IntEntry( vTypeSpec, id ) == 1 ) - { - continue; - } - else - { - if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - } - } - printf( "BI: %d, BO: %d, Box Size: %d\n", n, Gia_ManBufNum(p1)-n, count_node ); - - - Gia_ManStaticFanoutStop( p1 ); - - printf( "spec: fanin: %d / fanout: %d / total %d\n", c1, c2, Gia_ManObjNum(p1) ); - - // TODO: record hashed equivalent nodes - - count = 0; Gia_ManForEachAnd( p1, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 ) - { - if ( Vec_IntGetEntry( vMarkBmiter, pObj->Value >> 1 ) == 3 ) // eq node in impl - { - Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); - } - else - { - Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); - } - } - if ( Gia_ObjIsBuf(pObj) ) - { - Vec_IntPush( vLits, pObj->Value ); - if ( count < n ) - { - Vec_IntPush( vIdBI, (pObj->Value) >> 1 ); - } - else - { - Vec_IntPush( vIdBO, (pObj->Value) >> 1 ); - } - count ++; - } + Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); } - - int e, c3=0, c4=0, c5=0; - c1 = 0; c2 = 0; - - Vec_IntForEachEntry( vMarkBmiter, e, i ) - { - switch (e) - { - case 1: c1++; break; - case 2: c2++; break; - case 3: c3++; break; - case 4: c4++; break; - case 5: c5++; break; - default: - break; - } - } - printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); - Gia_ManForEachCo( p2, pObj, i ) { - int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) << 1; - Vec_IntSetEntry( vMarkBmiter, id, 5 ); + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, id), Gia_ObjId(p2, pObj) ); } Gia_ManForEachCo( p1, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + { + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) ); + } Vec_IntForEachEntry( vLits, iLit, i ) Gia_ManAppendCo( pNew, iLit ); Vec_IntFree( vLits ); @@ -6024,6 +5896,538 @@ Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ) return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) +{ + Vec_Int_t * vLits; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, iLit; + if ( Gia_ManBufNum(p1) == 0 ) { + printf( "The first AIG should have a boundary.\n" ); + return NULL; + } + if ( Gia_ManBufNum(p2) == 0 ) { + printf( "The second AIG should have a boundary.\n" ); + return NULL; + } + assert( Gia_ManBufNum(p1) > 0 ); + assert( Gia_ManBufNum(p2) > 0 ); + assert( Gia_ManBufNum(p1) == Gia_ManBufNum(p2) ); + assert( Gia_ManRegNum(p1) == 0 ); + assert( Gia_ManRegNum(p2) == 0 ); + assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); + assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); + if ( fVerbose ) + printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n", + Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); + pNew = Gia_ManStart( Gia_ManObjNum(p2) ); + pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 ); + sprintf( pNew->pName, "%s_patch", p1->pName ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p1)->Value = 0; + Gia_ManConst0(p2)->Value = 0; + + // add patch aig first + // record lit -> patch id + Vec_Int_t* vVar2Patch = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vVar2Patch, Gia_ManObjNum(p2), -1 ); + + Gia_ManForEachCi( p2, pObj, i ) + { + pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew ); + Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) ); + } + Gia_ManForEachAnd( p2, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "\t%d: %d %d\n", Gia_ObjId( p2, pObj), Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) ); + } + + + // alloc vCompl; + Vec_Bit_t * vComplBuf = Vec_BitAlloc(Gia_ManBufNum(p1)); + Vec_Bit_t * vCompl = Vec_BitAlloc(Gia_ManObjNum(p1)); + Vec_BitFill( vCompl, Gia_ManObjNum(p1), 0 ); + Gia_ManForEachBuf( p2, pObj, i ) + { + printf("\tbuf compl %d: %d\n", Gia_ObjId(p2, pObj), Gia_ObjFaninC0(pObj)); + Vec_BitPush( vComplBuf, Gia_ObjFaninC0(pObj) ); + } + int cnt = 0; + Gia_ManForEachBuf( p1, pObj, i ) + { + printf("\tbuf compl %d: %d\n", Gia_ObjId(p1, pObj), Gia_ObjFaninC0(pObj)); + if ( Vec_BitEntry( vComplBuf, cnt ) || Gia_ObjFaninC0(pObj) ) + { + Vec_BitSetEntry( vCompl, Gia_ObjId( p1, pObj ), 1 ); + printf("\tset\n"); + } + cnt++; + } + + + + // mark the box in spec + Vec_Int_t* vFlagSpec = Vec_IntAlloc( Gia_ManObjNum(p1) ); // 1: bi, 2: inside the box, 3: bo + Vec_IntFill( vFlagSpec, Gia_ManObjNum(p1), 0 ); + int cnt_buf = 0; + Gia_ManForEachBuf( p1, pObj, i ) + { + if ( cnt_buf < biNum ) + { + Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 1 ); + } + else + { + Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 3 ); + } + cnt_buf ++; + } + + int fanin0, fanin1; + Gia_ManForEachAnd( p1, pObj, i ) + { + if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) != 0 ) continue ; + fanin0 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) ); + fanin1 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) ); + if ( fanin0 == 1 || fanin0 == 2 || fanin1 == 1 || fanin1 == 2 ) + Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, pObj ), 2 ); + } + + + // compute spec2impl + Vec_Int_t* vSpec2Impl = Vec_IntAlloc( Gia_ManObjNum(p1) ); + Vec_IntFill( vSpec2Impl, Gia_ManObjNum(p1), -1 ); + Vec_Int_t* vSpec, *vImpl; + int j, id; + for ( i = 0; i < Vec_PtrSize( vBmiter2Spec ); i++ ) + { + vSpec = Vec_PtrEntry( vBmiter2Spec, i ); + vImpl = Vec_PtrEntry( vBmiter2Impl, i ); + Vec_IntForEachEntry( vSpec, id, j ) + { + if ( Vec_IntEntry( vSpec2Impl, id ) == -1 && Vec_IntSize( vImpl ) > 0 ) + { + Vec_IntSetEntry( vSpec2Impl, id, Vec_IntEntry( vImpl, 0 ) ); + } + } + } + + // print + // printf("spec 2 impl:\n"); + // Vec_IntForEachEntry( vSpec2Impl, id, i ) + // { + // printf( "\t%d:\t %d\n", i, id ); + // } + + // alloc patch2impl + vPatch2Impl = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vPatch2Impl, Gia_ManObjNum(p2), -1 ); + Vec_IntSetEntry( vPatch2Impl, 0, 0 ); + + Gia_ManForEachCi( p2, pObj, i ) + { + Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, pObj->Value >> 1); + Vec_IntSetEntry( vPatch2Impl, pObj->Value>>1, Vec_IntEntry( vSpec2Impl, pObj->Value>>1) ); + } + + // set the litral on the boundary of spec as in patch and record patch2impl + Vec_Int_t* vBufLit = Vec_IntAlloc( Gia_ManBufNum( p2 ) ); + vBI_patch = Vec_IntAlloc( Gia_ManBufNum(p2) ); + vBO_patch = Vec_IntAlloc( Gia_ManBufNum(p2) ); + cnt_buf = 0; + Gia_ManForEachBuf( p2, pObj, i ) + { + // TODO: check compl + Vec_IntPush( vBufLit, Gia_ObjFanin0( pObj ) -> Value ); + if ( cnt_buf < biNum ) + { + Vec_IntPush( vBI_patch, Gia_ObjFanin0( pObj) -> Value >> 1 ); + } + else + { + Vec_IntPush( vBO_patch, Gia_ObjFanin0( pObj) -> Value >> 1 ); + } + cnt_buf++; + } + Vec_Int_t* vSpec2Patch = Vec_IntAlloc( Gia_ManObjNum(p1) ); + Vec_IntFill( vSpec2Patch, Gia_ManObjNum(p1), -1 ); + + cnt_buf = 0; + Gia_Obj_t * pObj2; + + Gia_ManForEachBuf( p1, pObj, i ) + { + // TODO: compl? + pObj2 = Gia_ObjFanin0(pObj); + pObj2 -> Value = Vec_IntEntry( vBufLit, cnt_buf ); + Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) ); + // printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) ); + + Vec_IntSetEntry( vPatch2Impl, pObj2 -> Value>>1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj2) ) ); + pObj->Value = pObj2->Value; + cnt_buf++; + } + + + // hash the area outside the box in spec and record patch2impl + int lit0, lit1; + Gia_ManForEachAnd( p1, pObj, i ) { + printf( "spec node %d(%d) = %d %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj)), Gia_ObjId( p1, Gia_ObjFanin0(pObj) ), Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) ); + if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) > 1 ) continue; + if ( Gia_ObjIsBuf(pObj) ) continue; + + lit0 = Gia_ObjFanin0Copy(pObj); + lit1 = Gia_ObjFanin1Copy(pObj); + if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) ) ) lit0 ^= 1; + if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) ) ) lit1 ^= 1; + pObj->Value = Gia_ManHashAnd( pNew, lit0, lit1 ); + + + assert( (pObj->Value>>1) < Vec_IntSize( vVar2Patch) ); + assert( Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) != -1 ); + + Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) ); + printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) ); + + Vec_IntSetEntry( vPatch2Impl, pObj->Value >> 1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj) ) ); + } + + + // print + printf("patch 2 impl:\n"); + Vec_IntForEachEntry( vPatch2Impl, id, i ) + { + printf( "\t%d:\t %d\n", i, id ); + } + + // handle co + Gia_ManForEachCo( p2, pObj, i ) + { + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + } + // TODO: also check spec CO + // Gia_ManForEachCo( p1, pObj, i ) + // { + // int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + // Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) ); + // } + + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) +{ + Vec_Int_t * vLits; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, *pObj2; + int i, j, iLit, id, id2; + assert( Gia_ManRegNum(p1) == 0 ); + assert( Gia_ManRegNum(p2) == 0 ); + assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); + assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); + if ( fVerbose ) + printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n", + Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); + pNew = Gia_ManStart( Gia_ManObjNum(p2) ); + pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 ); + sprintf( pNew->pName, "%s_patch", p1->pName ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p1)->Value = 0; + Gia_ManConst0(p2)->Value = 0; + + + // p1: patch + // p2: impl + + // compute extended box + + Gia_ManStaticFanoutStart( p1 ); + Vec_Ptr_t* vBO = Vec_PtrAlloc(16); + Vec_Ptr_t* vBI = Vec_PtrAlloc(16); + Vec_Ptr_t* vAO = Vec_PtrAlloc(16); + Vec_Ptr_t* vAI = Vec_PtrAlloc(16); + + + + Vec_Ptr_t* vQ = Vec_PtrAlloc(16); + Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) ); + Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 ); + Vec_IntForEachEntry( vBO_patch, id, i ) + { + if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary + Vec_PtrPush( vQ, p1->pObjs+id ); + else + Vec_PtrPush( vBO, p1->pObjs+id ); + } + + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag, id, 1 ); + + printf("%d\n", id); + + if ( Vec_IntEntry( vPatch2Impl, id ) != -1 ) // matched + { + Vec_PtrPush( vAO, pObj ); + } + else + { + for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) ); + printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) ); + } + + } + } + + // set flag 2 for FOC + Vec_IntForEachEntry( vBO_patch, id, i ) + { + Vec_PtrPush( vQ, p1->pObjs+id ); + } + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + + if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) == 2 ) continue; + Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 2 ); + + for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) ); + } + } + + // set flag 3 for BO + Vec_IntForEachEntry( vBO_patch, id, i ) + { + Vec_IntSetEntry( vFlag, id, 3 ); + } + + // traverse down from unmated BI and AO + Vec_IntForEachEntry( vBI_patch, id, i ) + { + if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary + Vec_PtrPush( vQ, p1->pObjs+id ); + else + Vec_PtrPush( vBI, p1->pObjs+id ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) + { + Vec_PtrPush( vQ, pObj ); + } + + // traverse down + printf("traverse down\n"); + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + if ( Vec_IntEntry( vFlag, id ) == 4 ) continue; + + printf("%d\n", id); + + if ( Vec_IntEntry( vPatch2Impl, id ) != -1 && Vec_IntEntry( vFlag, id ) < 2 ) // matched + { + Vec_PtrPush( vAI, pObj ); + printf("matched\n"); + } + else if ( Vec_IntEntry( vFlag, id ) < 3 ) + { + if ( Gia_ObjFaninNum(p1, pObj) > 0 ) + { + Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin0(pObj) ) ); + } + + if ( Gia_ObjFaninNum(p1, pObj) > 1 ) + { + Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) ); + } + } + printf("2impl / flag: %d / %d\n", Vec_IntEntry( vPatch2Impl, id ), Vec_IntEntry( vFlag, id ) ); + + Vec_IntSetEntry( vFlag, id, 4 ); + } + + + // print + printf( "matched BI:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\nAI:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\nmateched BO:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\nAO:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\n"); + + // create patched impl + + // mark fanin cone of Extended Input in impl + Vec_Int_t* vFlag_impl = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vFlag_impl, Gia_ManObjNum(p2), 0 ); + + Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) + { + Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) + { + Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) ); + } + + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p2, pObj ); + if ( Vec_IntEntry( vFlag_impl, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag_impl, id, 1 ); + + if ( Gia_ObjFaninNum(p2, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjFaninNum(p2, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + } + + // add pi + Gia_ManForEachCi( p2, pObj, i ) + { + pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew ); + } + // add fanin cone of EI in impl + int cnt = 0; + Gia_ManForEachAnd( p2, pObj, i ) + { + if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) == 0 ) continue; + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "%d\n", pObj->Value>>1 ); + cnt ++; + } + printf( "%d node added in the fanin cone of EI\n", cnt ); + // set literal and flag of EI in patch + // TODO: input phase + Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value; + Vec_IntSetEntry( vFlag, id, 5 ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value; + Vec_IntSetEntry( vFlag, id, 5 ); + } + // mark fanin cone of EO in patch (to flag 5) + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + Vec_PtrPush( vQ, pObj ); + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) + Vec_PtrPush( vQ, pObj ); + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + if ( Vec_IntEntry( vFlag, id ) >= 5 ) continue; + Vec_IntSetEntry( vFlag, id, 6 ); + + if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + } + // add fanin cone of EO to EI in patch + cnt = 0; + Gia_ManForEachAnd( p1, pObj, i ) + { + if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 6 ) continue; + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "%d\n", pObj->Value>>1 ); + cnt ++; + } + printf( "%d node added in the extended boundary\n", cnt ); + + // set literal and flag(1) of EO in impl + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + id2 = Vec_IntEntry( vPatch2Impl, id ); + pObj2 = p2 -> pObjs + id2; + pObj2 -> Value = pObj -> Value; + if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1; + Vec_IntSetEntry( vFlag_impl, id2, 1 ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + id2 = Vec_IntEntry( vPatch2Impl, id ); + pObj2 = p2 -> pObjs + id2; + pObj2 -> Value = pObj -> Value; + printf( "id %d matched to id %d in impl, phase %d\n", id, id2, Vec_BitEntry( vImpl2Spec_phase, id2 ) ); + if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1; + Vec_IntSetEntry( vFlag_impl, id2, 1 ); + } + + // add flag 0 in impl + cnt = 0; + Gia_ManForEachAnd( p2, pObj, i ) + { + if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) != 0 ) continue; + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "%d\n", pObj->Value>>1 ); + cnt++; + } + printf( "%d node added in the fanout cone\n", cnt ); + + // handle co + cnt = 0; + Gia_ManForEachCo( p2, pObj, i ) + { + id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + printf( "%d\n", id ); + cnt ++; + } + + Gia_ManStaticFanoutStop( p1 ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dab809c25..1a837d030 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -598,6 +598,7 @@ static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9RecoverBoundary ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1378,6 +1379,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&rb", Abc_CommandAbc9RecoverBoundary, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -51953,6 +51955,111 @@ usage: return 1; } +int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); + extern Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); + Gia_Man_t * pTemp, * pSecond, *pImpl, *pPatched; + char * FileName = NULL; + char * FileName2 = NULL; + FILE * pFile = NULL; + int c, fVerbose = 0; + int bi = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + bi = atoi(argv[globalUtilOptind++]); + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 2 ) + { + printf("%d\n", argc-globalUtilOptind); + Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" ); + return 0; + } + + // get the input file name + FileName = argv[globalUtilOptind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + + // get the input file name 2 + FileName2 = argv[globalUtilOptind+1]; + if ( (pFile = fopen( FileName2, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName2 ); + if ( (FileName2 = Extra_FileGetSimilarName( FileName2, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName2 ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + + // map spec to patch + pSecond = Gia_AigerRead( FileName, 0, 1, 0 ); + if ( pSecond == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + return 0; + } + pTemp = Gia_ManPatch( pAbc->pGia, pSecond, fVerbose, bi); + // Gia_ManStop( pSecond ); + // Abc_FrameUpdateGia( pAbc, pTemp ); + // return 0; + + // generated patched impl + pImpl = Gia_AigerRead( FileName2, 0, 0, 0 ); + if ( pImpl == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + return 0; + } + pPatched = Gia_ManPatchImpl( pTemp, pImpl, fVerbose, bi); + + Gia_ManStop( pSecond ); + Gia_ManStop( pImpl ); + Gia_ManStop( pTemp ); + Abc_FrameUpdateGia( pAbc, pPatched ); + return 0; + +usage: + Abc_Print( -2, "usage: &str_eco -I [-vh] \n" ); + Abc_Print( -2, "\t creates the boundary miter\n" ); + Abc_Print( -2, "\t-I : number of boundary inputs\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the implementation file\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 7377367e2..0659b3f60 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -147,6 +147,8 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) extern Vec_Int_t* vMarkBmiter; extern Vec_Int_t* vIdBI; extern Vec_Int_t* vIdBO; +extern Vec_Ptr_t* vBmiter2Spec; +extern Vec_Ptr_t* vBmiter2Impl; //////////////////////////////////////////////////////////////////////// @@ -1788,6 +1790,8 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p ) } //Abc_Print( 1, "Removed %d wrong choices.\n", Counter ); } + +extern Vec_Bit_t* vImpl2Spec_phase; int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly ) { Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); @@ -1890,45 +1894,24 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { - // printf( "*node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr) ); if ( pPars->fBMiterInfo ) { - if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 ) + int eId, j; + Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; + vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); + vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); + vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); + vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); + Vec_IntForEachEntry( vIds_spec_obj, eId, j) { - switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) - { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); - break; - default: - break; - } + Vec_IntPush(vIds_spec_repr, eId); } - else + Vec_IntForEachEntry( vIds_impl_obj, eId, j) { - if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) - switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) - { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); - break; - default: - break; - - } + Vec_IntPush(vIds_impl_repr, eId); } - // TODO - Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); + Vec_IntClear(vIds_spec_obj); + Vec_IntClear(vIds_impl_obj); } assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); Gia_ObjSetProved( p, i ); @@ -1939,178 +1922,101 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) { if (pPars->fBMiterInfo){ - // printf( "node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr ) ); - if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 ) + + int eId, j; + Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; + vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); + vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); + vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); + vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); + + Vec_IntForEachEntry( vIds_spec_obj, eId, j) { - switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) + Vec_IntPush(vIds_spec_repr, eId); + } + Vec_IntForEachEntry( vIds_impl_obj, eId, j) + { + Vec_IntPush(vIds_impl_repr, eId); + } + + // handle phase before cleaning + printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase ); + if ( Vec_IntSize(vIds_spec_repr) == 0 ) // no match + { + if ( pObj->fPhase ^ pRepr -> fPhase ) { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); - break; - default: - break; + Vec_IntForEachEntry( vIds_impl_obj, eId, j ) + { + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } } } - else + else if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) && Vec_IntSize( vIds_impl_obj ) == 0 ) // new match { - if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) - switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) + if ( pObj->fPhase ^ pRepr -> fPhase ) + { + Vec_IntForEachEntry( vIds_impl_repr, eId, j ) { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); - break; - default: - break; - + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); } + printf("new match flip\n"); + } } - // TODO - Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); + else if ( Vec_IntSize( vIds_spec_repr ) > 0 && Vec_IntSize( vIds_impl_obj ) > 0 ) // matched, merge impl + { + if ( ( pObj->fPhase ^ pRepr -> fPhase) ^ ( Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_repr, 0)) ^ Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_obj, 0)) ) ) + { + if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) ) // unmatched repr, matched obj, set repr bits + { + Vec_IntForEachEntry( vIds_impl_repr, eId, j ) + { + if ( j >= Vec_IntSize( vIds_impl_repr)-Vec_IntSize(vIds_impl_obj) ) break; + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + } + else // set obj bits + { + Vec_IntForEachEntry( vIds_impl_obj, eId, j ) + { + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + } + } + } + + Vec_IntClear(vIds_spec_obj); + Vec_IntClear(vIds_impl_obj); + } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); + + } } - if ( pPars->fBMiterInfo ) { - - // check bi, bo - Vec_Ptr_t* vAO = Vec_PtrAlloc( 16 ); // additioal output boundary - Vec_Ptr_t* vAI = Vec_PtrAlloc( 16 ); // additional input boundary - Vec_Ptr_t* vMI = Vec_PtrAlloc(16); // missing input boundary - Vec_Ptr_t* vMO = Vec_PtrAlloc(16); // missing input boundary - Vec_Ptr_t* vQ = Vec_PtrAlloc(16); // queue for fanout traversal - int val; - int cnt_TO = 0; - int cnt_TI = 0; - int cnt_SIDE = 0; - int cnt_MI = 0; - int cnt_MO = 0; - Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs ); - Vec_IntFill( vFlag, p->nObjs, 0 ); - - printf("BI:"); - Vec_IntForEachEntry( vIdBI, val, i ) + // print + Vec_Int_t* vIds_spec, *vIds_impl; + int k, id; + for( int j=0; j < Vec_PtrSize(vBmiter2Spec); j++ ) { - printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) ); - if ( Vec_IntEntry( vMarkBmiter, val) <= 3 ) - { - Vec_PtrPush(vMI, &((p->pObjs)[val]) ); - } - else cnt_MI ++; + printf("node %d: ", j); + vIds_spec = Vec_PtrEntry( vBmiter2Spec, j); + vIds_impl = Vec_PtrEntry( vBmiter2Impl, j); + Vec_IntForEachEntry(vIds_spec, id, k) + printf("%d ", id); + printf("| "); + Vec_IntForEachEntry(vIds_impl, id, k) + printf("%d ", id); + printf("\n"); } - printf("\nBO:"); - Vec_IntForEachEntry( vIdBO, val, i ) - { - printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) ); - if ( Vec_IntEntry( vMarkBmiter, val) <= 3 ) - { - Vec_PtrPush(vQ, &((p->pObjs)[val]) ); - Vec_PtrPush(vMO, &((p->pObjs)[val]) ); - Vec_IntSetEntry( vFlag, val, 2 ); - } - else cnt_MO ++; - } - printf("\n"); - - // find extended output boundary - - Gia_ManStaticFanoutStart( p ); - - Gia_Obj_t * pObj2; - cnt_TO -= Vec_PtrSize(vQ); - - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) == 1 ) continue; - Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 ); - cnt_TO ++; - - val = Vec_IntEntry(vMarkBmiter, Gia_ObjId(p, pObj2)); - if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found - { - Vec_PtrPush( vAO, pObj2 ); - continue; - } - - for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ ) - { - Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) ); - } - } - - Gia_ManStaticFanoutStop(p); - - - // find extneded input boundary - - Vec_PtrForEachEntry( Gia_Obj_t*, vMO, pObj, i ) - { - Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj), 2 ); - } - - int id; - Vec_PtrForEachEntry( Gia_Obj_t*, vMI, pObj, i ) Vec_PtrPush( vQ, pObj ); - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) Vec_PtrPush( vQ, pObj ); - cnt_TI -= Vec_PtrSize(vQ); - while ( Vec_PtrSize(vQ) > 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p, pObj ); - if ( Vec_IntEntry( vFlag, id ) == 2 ) continue; - printf( "backtrace to node %d\n", id ); - if ( Vec_IntEntry(vMarkBmiter, id ) != 2 ) cnt_TI ++; - Vec_IntSetEntry( vFlag, id, 2 ); - - - if ( Vec_IntEntry( vMarkBmiter, id ) >= 3 || Gia_ObjIsCi( pObj ) ) // matched - { - if ( Vec_IntEntry( vMarkBmiter, id ) < 5 || Gia_ObjIsCi( pObj ) ) - { - Vec_PtrPush( vAI, pObj ); - } - continue; - } - else - { - if ( Gia_ObjFaninNum(p, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - if ( Gia_ObjFaninNum(p, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - } - } - - - // print result - printf("extended BO with %d extra nodes:", cnt_TO); - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) - { - printf( " %d", Gia_ObjId(p, pObj) ); - } - printf("\n"); - - printf("extended BI with %d extra nodes:", cnt_TI); - Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) - { - printf( " %d", Gia_ObjId(p, pObj) ); - } - printf("\n"); - - printf("matched BI: %d / matched BO: %d / AI: %d / AO: %d / Extra nodes: %d\n", cnt_MI, cnt_MO, Vec_PtrSize(vAI), Vec_PtrSize(vAO), cnt_TO + cnt_TI ); - } - if ( p->iPatsPi > 0 ) { abctime clk2 = Abc_Clock(); @@ -2155,7 +2061,6 @@ finalize: Gia_ManRemoveWrongChoices( p ); return p->pCexSeq ? 0 : 1; } -extern Vec_Int_t * vMarkBmiter; Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; @@ -2163,22 +2068,8 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) // TODO if (pPars -> fBMiterInfo){ - int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; - Vec_IntForEachEntry( vMarkBmiter, e, i ) - { - switch (e) - { - case 1: c1++; break; - case 2: c2++; break; - case 3: c3++; break; - case 4: c4++; break; - case 5: c5++; break; - default: - break; - } - } - printf("(fraig) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); } + return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )