From 83519c320c1d335675e97f144cff109200141770 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 Nov 2020 20:17:20 -0800 Subject: Experiments with SAT sweeping. --- src/aig/gia/giaEquiv.c | 118 +++++++++++++++++++++++++++++++++++++++++++++++ src/proof/cec/cecSatG2.c | 73 +++++++++++++++++------------ 2 files changed, 161 insertions(+), 30 deletions(-) diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 0e9f5526..f7f873cd 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -269,6 +269,7 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p ) pTails[i] = i; for ( i = 0; i < Gia_ManObjNum(p); i++ ) { + //if ( p->pReprs[i].iRepr == GIA_VOID ) if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID ) continue; pNexts[ pTails[p->pReprs[i].iRepr] ] = i; @@ -2589,6 +2590,123 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew ); } +/**Function************************************************************* + + Synopsis [Changing node order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManChangeOrder_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return pObj->Value; + if ( Gia_ObjIsCi(pObj) ) + return pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjIsCo(pObj) ) + return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin1(pObj) ); + return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +Gia_Man_t * Gia_ManChangeOrder( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, k; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachClass( p, i ) + Gia_ClassForEachObj( p, i, k ) + Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) ); + Gia_ManForEachConst( p, k ) + Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + assert( Gia_ManObjNum(pNew) == Gia_ManObjNum(p) ); + return pNew; +} +void Gia_ManTransferEquivs( Gia_Man_t * p, Gia_Man_t * pNew ) +{ + Vec_Int_t * vClass; + int i, k, iNode, iRepr; + assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) ); + assert( p->pReprs != NULL ); + assert( p->pNexts != NULL ); + assert( pNew->pReprs == NULL ); + assert( pNew->pNexts == NULL ); + // start representatives + pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) ); + for ( i = 0; i < Gia_ManObjNum(pNew); i++ ) + Gia_ObjSetRepr( pNew, i, GIA_VOID ); + // iterate over constant candidates + Gia_ManForEachConst( p, i ) + Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); + // iterate over class candidates + vClass = Vec_IntAlloc( 100 ); + Gia_ManForEachClass( p, i ) + { + Vec_IntClear( vClass ); + Gia_ClassForEachObj( p, i, k ) + Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) ); + assert( Vec_IntSize( vClass ) > 1 ); + Vec_IntSort( vClass, 0 ); + iRepr = Vec_IntEntry( vClass, 0 ); + Vec_IntForEachEntryStart( vClass, iNode, k, 1 ) + Gia_ObjSetRepr( pNew, iNode, iRepr ); + } + Vec_IntFree( vClass ); + pNew->pNexts = Gia_ManDeriveNexts( pNew ); +} +void Gia_ManTransferTest( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; int i; + Gia_Rpr_t * pReprs = p->pReprs; // representatives (for CIs and ANDs) + int * pNexts = p->pNexts; // next nodes in the equivalence classes + Gia_Man_t * pNew = Gia_ManChangeOrder(p); + //Gia_ManEquivPrintClasses( p, 1, 0 ); + assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) ); + Gia_ManTransferEquivs( p, pNew ); + p->pReprs = NULL; + p->pNexts = NULL; + // make new point to old + Gia_ManForEachObj( p, pObj, i ) + { + assert( !Abc_LitIsCompl(pObj->Value) ); + Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0); + } + Gia_ManTransferEquivs( pNew, p ); + //Gia_ManEquivPrintClasses( p, 1, 0 ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + pReprs[i].fProved = 0; + //printf( "%5d : %5d %5d %5d %5d\n", i, *(int*)&p->pReprs[i], *(int*)&pReprs[i], (int)p->pNexts[i], (int)pNexts[i] ); + if ( memcmp(p->pReprs, pReprs, sizeof(int)*Gia_ManObjNum(p)) ) + printf( "Verification of reprs failed.\n" ); + else + printf( "Verification of reprs succeeded.\n" ); + if ( memcmp(p->pNexts, pNexts, sizeof(int)*Gia_ManObjNum(p)) ) + printf( "Verification of nexts failed.\n" ); + else + printf( "Verification of nexts succeeded.\n" ); + ABC_FREE( pNew->pReprs ); + ABC_FREE( pNew->pNexts ); + ABC_FREE( pReprs ); + ABC_FREE( pNexts ); + Gia_ManStop( pNew ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index d01b7bd5..a9332f1d 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -79,6 +79,7 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// + /**Function************************************************************* Synopsis [] @@ -92,24 +93,11 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) ***********************************************************************/ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) { - Cec4_Man_t * p; - Gia_Obj_t * pObj; int i; - //assert( Gia_ManRegNum(pAig) == 0 ); - p = ABC_CALLOC( Cec4_Man_t, 1 ); + Cec4_Man_t * p = ABC_CALLOC( Cec4_Man_t, 1 ); memset( p, 0, sizeof(Cec4_Man_t) ); - p->timeStart = Abc_Clock(); - p->pPars = pPars; - p->pAig = pAig; - pAig->pData = p->pSat; // point AIG manager to the solver - // create new manager - p->pNew = Gia_ManStart( Gia_ManObjNum(pAig) ); - Gia_ManFillValue( pAig ); - Gia_ManConst0(pAig)->Value = 0; - Gia_ManForEachCi( pAig, pObj, i ) - pObj->Value = Gia_ManAppendCi( p->pNew ); - Gia_ManHashAlloc( p->pNew ); - Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(pAig), -1 ); - // SAT solving + p->timeStart = Abc_Clock(); + p->pPars = pPars; + p->pAig = pAig; p->pSat = bmcg_sat_solver_start(); p->vFrontier = Vec_PtrAlloc( 1000 ); p->vFanins = Vec_PtrAlloc( 100 ); @@ -119,6 +107,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) p->vCands = Vec_IntAlloc( 100 ); p->vVisit = Vec_IntAlloc( 100 ); p->vPat = Vec_IntAlloc( 100 ); + //pAig->pData = p->pSat; // point AIG manager to the solver return p; } void Cec4_ManDestroy( Cec4_Man_t * p ) @@ -158,6 +147,21 @@ void Cec4_ManDestroy( Cec4_Man_t * p ) Vec_IntFreeP( &p->vPat ); ABC_FREE( p ); } +Gia_Man_t * Cec4_ManStartNew( Gia_Man_t * pAig ) +{ + Gia_Obj_t * pObj; int i; + Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(pAig) ); + pNew->pName = Abc_UtilStrsav( pAig->pName ); + pNew->pSpec = Abc_UtilStrsav( pAig->pSpec ); + Gia_ManFillValue( pAig ); + Gia_ManConst0(pAig)->Value = 0; + Gia_ManForEachCi( pAig, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManHashAlloc( pNew ); + Vec_IntFill( &pNew->vCopies2, Gia_ManObjNum(pAig), -1 ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pAig) ); + return pNew; +} /**Function************************************************************* @@ -933,16 +937,24 @@ void Cec4_ManGeneratePatterns( Cec4_Man_t * p ) { abctime clk = Abc_Clock(); int i, k, iLit, nPats = 64 * p->pAig->nSimWords; - Gia_Obj_t * pObj; // collect candidate nodes - Vec_IntClear( p->vCands ); - Gia_ManForEachObj( p->pAig, pObj, i ) + if ( p->pPars->nGenIters ) { - pObj->fMark0 = pObj->fMark1 = 0; - if ( !Gia_ObjIsHead(p->pAig, i) ) - continue; - Gia_ClassForEachObj1( p->pAig, i, k ) - Vec_IntPush( p->vCands, k ); + if ( Vec_IntSize(p->vCands) == 0 ) + { + for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) + if ( Gia_ObjRepr(p->pAig, i) != GIA_VOID ) + Vec_IntPush( p->vCands, i ); + } + else + { + int iObj, k = 0; + Vec_IntForEachEntry( p->vCands, iObj, i ) + if ( Gia_ObjRepr(p->pAig, iObj) != GIA_VOID ) + Vec_IntWriteEntry( p->vCands, k++, iObj ); + Vec_IntShrink( p->vCands, k ); + assert( Vec_IntSize(p->vCands) > 0 ); + } } // generate the given number of patterns for ( i = 0, p->pAig->iPatsPi = 1; i < p->pPars->nGenIters * nPats && p->pAig->iPatsPi < nPats; p->pAig->iPatsPi++, i++ ) @@ -969,6 +981,7 @@ void Cec4_ManGeneratePatterns( Cec4_Man_t * p ) p->timeGenPats += Abc_Clock() - clk; } + /**Function************************************************************* Synopsis [Internal simulation APIs.] @@ -1106,7 +1119,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) p->timeSatSat += Abc_Clock() - clk; RetValue = 0; // this is not needed, but we keep it here anyway, because it takes very little time - Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat ); + //Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat ); // resimulated once in a while if ( p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1 ) { @@ -1186,7 +1199,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p // check if any output trivially fails under all-0 pattern Gia_ManRandomW( 1 ); Gia_ManSetPhase( p ); - Gia_ManStaticFanoutStart( p ); + //Gia_ManStaticFanoutStart( p ); if ( pPars->fCheckMiter ) { Gia_ManForEachCo( p, pObj, i ) @@ -1219,7 +1232,9 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( i % (pPars->nRounds / 5) == 0 && pPars->fVerbose ) Cec4_ManPrintStats( p, pPars, pMan ); } + p->iPatsPi = 0; + pMan->pNew = Cec4_ManStartNew( p ); Gia_ManForEachAnd( p, pObj, i ) { //Gia_Obj_t * pObjNew; @@ -1263,8 +1278,6 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) ); *ppNew = Gia_ManCleanup( pMan->pNew ); - (*ppNew)->pName = Abc_UtilStrsav( p->pName ); - (*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec ); } finalize: if ( pPars->fVerbose ) @@ -1275,7 +1288,7 @@ finalize: pMan->nSatUndec, pMan->nSimulates, pMan->nRecycles ); Cec4_ManDestroy( pMan ); - Gia_ManStaticFanoutStop( p ); + //Gia_ManStaticFanoutStop( p ); //Gia_ManEquivPrintClasses( p, 1, 0 ); return p->pCexSeq ? 0 : 1; } -- cgit v1.2.3