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/proof/cec/cecSatG2.c | 73 ++++++++++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 30 deletions(-) (limited to 'src/proof') 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