From 284b9d6a9c01c7df0636a696fc35a47d10f10f0a Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Sun, 10 Dec 2023 21:30:46 +0800 Subject: [PATCH] extended box report; --- src/aig/gia/giaDup.c | 68 ++++++++++++++---- src/base/abci/abc.c | 14 +--- src/proof/cec/cecSatG2.c | 150 +++++++++++++++++++++++++++------------ 3 files changed, 160 insertions(+), 72 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index ffd776cc4..aa8f1c053 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -Vec_Int_t* vLitBmiter; +Vec_Int_t* vMarkBmiter; Vec_Int_t* vIdBI; Vec_Int_t* vIdBO; @@ -5701,18 +5701,24 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Gia_ManHashStart( pNew ); 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) ); + Gia_ManForEachCi( p1, pObj, i ) - pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + { + int id = pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + Vec_IntSetEntry( vMarkBmiter, id >> 1, 4 ); + } // TODO: record the corresponding impl node of each lit - vLitBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2 ); - Vec_IntFill( vLitBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2, 0 ); - printf( "allocated size: %d\n", Vec_IntSize(vLitBmiter) ); Gia_ManForEachAnd( p2, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 ); + Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 ); } // TODO: find nodes in spec @@ -5726,11 +5732,11 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, 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; - int val; + int count = 0; vIdBI = Vec_IntAlloc(16); vIdBO = Vec_IntAlloc(16); @@ -5759,6 +5765,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, else { Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 ); + Vec_PtrPush( vBO, pObj ); c2 ++; int j; @@ -5782,6 +5789,37 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, } } + 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) ); @@ -5794,13 +5832,13 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 ) { - if ( Vec_IntGetEntry( vLitBmiter, pObj->Value ) == 3 ) // eq node in impl + if ( Vec_IntGetEntry( vMarkBmiter, pObj->Value >> 1 ) == 3 ) // eq node in impl { - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); } else { - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); } } if ( Gia_ObjIsBuf(pObj) ) @@ -5822,9 +5860,8 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int e, c3=0, c4=0, c5=0; c1 = 0; c2 = 0; - Vec_IntForEachEntry( vLitBmiter, e, i ) + Vec_IntForEachEntry( vMarkBmiter, e, i ) { - if ( i%2 ) continue; switch (e) { case 1: c1++; break; @@ -5839,7 +5876,10 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); Gia_ManForEachCo( p2, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + { + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) << 1; + Vec_IntSetEntry( vMarkBmiter, id, 5 ); + } Gia_ManForEachCo( p1, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Vec_IntForEachEntry( vLits, iLit, i ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 755aeaea0..dab809c25 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37921,7 +37921,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "OJWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) { switch ( c ) { @@ -37969,18 +37969,6 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nItersMax < 0 ) goto usage; break; - case 'O': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nPO = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nPO < 1 ) - goto usage; - break; - case 'L': if ( globalUtilOptind >= argc ) { diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index a01cc7445..7377367e2 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -144,7 +144,7 @@ static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); } -extern Vec_Int_t* vLitBmiter; +extern Vec_Int_t* vMarkBmiter; extern Vec_Int_t* vIdBI; extern Vec_Int_t* vIdBO; @@ -1885,25 +1885,25 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( pRepr == NULL ) continue; } - int lit_obj = Gia_ObjId( p, pObj ) << 1; - int lit_repr = Gia_ObjId( p, pRepr ) << 1; + int id_obj = Gia_ObjId( p, pObj ); + int id_repr = Gia_ObjId( p, pRepr ); if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { - printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) ); + // 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( vLitBmiter, lit_repr ) == 3 ) + if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 ) { - switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) + switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); break; default: break; @@ -1911,16 +1911,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } else { - if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) + if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) + switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); break; default: break; @@ -1928,7 +1928,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } } // TODO - Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) ); + Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); } assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); Gia_ObjSetProved( p, i ); @@ -1939,18 +1939,18 @@ 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", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr ) ); - if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) + // 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 ) { - switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) + switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); break; default: break; @@ -1958,16 +1958,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } else { - if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) + if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) + switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); break; default: break; @@ -1975,7 +1975,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } } // TODO - Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) ); + Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); } @@ -1986,67 +1986,128 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p { // check bi, bo - Vec_Ptr_t* vBO = Vec_PtrAlloc( 16 ); - Vec_Ptr_t * vQ = Vec_PtrAlloc(16); - + 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 ) { - printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) ); + printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) ); + if ( Vec_IntEntry( vMarkBmiter, val) <= 3 ) + { + Vec_PtrPush(vMI, &((p->pObjs)[val]) ); + } + else cnt_MI ++; } printf("\nBO:"); Vec_IntForEachEntry( vIdBO, val, i ) { - printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) ); - if ( Vec_IntEntry( vLitBmiter, val << 1) != 5 ) + 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 bound + // find extended output boundary Gia_ManStaticFanoutStart( p ); - Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs ); - Vec_IntFill( vFlag, p->nObjs, 0 ); Gia_Obj_t * pObj2; - int cnt_node = 0; - int cnt_newBo = 0; + cnt_TO -= Vec_PtrSize(vQ); while ( Vec_PtrSize(vQ) != 0 ) { pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) != 0 ) continue; - cnt_node ++; + if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) == 1 ) continue; Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 ); + cnt_TO ++; - val = Vec_IntEntry(vLitBmiter, Gia_ObjId(p, pObj2) << 1); + val = Vec_IntEntry(vMarkBmiter, Gia_ObjId(p, pObj2)); if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found { - cnt_newBo ++; - Vec_PtrPush( vBO, pObj2 ); + Vec_PtrPush( vAO, pObj2 ); continue; } for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ ) { Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) ); - printf( "add fanout\n"); } } Gia_ManStaticFanoutStop(p); - printf("extended BO with %d extra nodes:", cnt_node); - Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + // 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 ); + } @@ -2094,7 +2155,7 @@ finalize: Gia_ManRemoveWrongChoices( p ); return p->pCexSeq ? 0 : 1; } -extern Vec_Int_t * vLitBmiter; +extern Vec_Int_t * vMarkBmiter; Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; @@ -2103,9 +2164,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( vLitBmiter, e, i ) + Vec_IntForEachEntry( vMarkBmiter, e, i ) { - if ( i%2 ) continue; switch (e) { case 1: c1++; break;