From ba64d6118b16f4f405b65affb0b04797e5b665e1 Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Mon, 30 Oct 2023 15:09:01 -0700 Subject: [PATCH] out-side box matching --- Makefile | 3 +- src/aig/gia/giaDup.c | 96 ++++++++++++++++++++++++++++++++++++++++ src/proof/cec/cecSatG2.c | 57 ++++++++++++++++++++++++ 3 files changed, 155 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 3976cf7b1..e6c0f4453 100644 --- a/Makefile +++ b/Makefile @@ -33,7 +33,8 @@ MODULES := \ src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \ src/proof/cec src/proof/acec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ - src/aig/miniaig + src/aig/miniaig \ + src/sat/bsat2 all: $(PROG) default: $(PROG) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 665164eb2..4efbe90dc 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +Vec_Int_t* vLitBmiter; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -5699,13 +5701,107 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) Gia_ManConst0(p2)->Value = 0; Gia_ManForEachCi( p1, pObj, i ) pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + + // TODO: record the corresponding impl node of each lit + vLitBmiter = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vLitBmiter, Gia_ManObjNum(p2) + Gia_ManObjNum(p1), 0 ); + Gia_ManForEachAnd( p2, pObj, i ) + { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 ); + } + + // 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; + + Gia_ManStaticFanoutStart( p1 ); + Vec_Ptr_t * vQ = Vec_PtrAlloc(16); + Gia_Obj_t * pObj2; + int c1 = 0; + int c2 = 0; + int count; + 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 ); + 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) ); + } + } + + } + } + + Gia_ManStaticFanoutStop( p1 ); + + printf( "category %d %d %d\n", c1, c2, Gia_ManObjNum(p1) ); + + + // TODO: record hashed equivalent nodes + 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( vLitBmiter, pObj->Value ) == 3 ) // eq node in impl + { + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + } + else + { + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + } + } if ( Gia_ObjIsBuf(pObj) ) Vec_IntPush( vLits, pObj->Value ); } + + // int e; + // Vec_IntForEachEntry( vLitBmiter, e, i ) + // { + // printf( "%d ", e ); + // } + // printf("\n"); + Gia_ManForEachCo( p2, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); //Gia_ManForEachCo( p1, pObj, i ) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 281deb0e9..d641704f7 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -143,6 +143,9 @@ static inline int Cec4_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec4_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); Vec_IntPush(&p->vSuppVars, Gia_ObjId(p, pObj)); if ( Gia_ObjIsCi(pObj) ) Vec_IntPushTwo(&p->vCopiesTwo, Gia_ObjId(p, pObj), Num); assert(Vec_IntSize(&p->vVarMap) == Num); Vec_IntPush(&p->vVarMap, Gia_ObjId(p, pObj)); return 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; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -1887,7 +1890,43 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p continue; } if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) + { + if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 ) + { + switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 ); + break; + default: + break; + } + } + else + { + if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) + switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 ); + break; + default: + break; + + } + } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); + } } if ( p->iPatsPi > 0 ) { @@ -1933,10 +1972,28 @@ finalize: Gia_ManRemoveWrongChoices( p ); return p->pCexSeq ? 0 : 1; } +extern Vec_Int_t * vLitBmiter; Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); + + int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; + Vec_IntForEachEntry( vLitBmiter, e, i ) + { + if ( i%2 ) continue; + 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("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5); return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )