From 4c78f37a5a78ee39957bcb5c793a7203509e642e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 14 Nov 2020 23:57:34 -0800 Subject: Sweeping up to a given level. --- src/proof/cec/cecSatG2.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/proof') diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 80a4b853..b9ea682d 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1273,7 +1273,7 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p ) int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose ) { abctime clk; - int nBTLimit = (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit; + int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit; int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2]; int UnsatConflicts[3] = {0}; if ( iObj1 < iObj0 ) @@ -1494,6 +1494,8 @@ 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_ManRandom( 1 ); Gia_ManSetPhase( p ); + if ( pPars->nLevelMax ) + Gia_ManLevelNum(p); //Gia_ManStaticFanoutStart( p ); if ( pPars->fCheckMiter ) { @@ -1548,6 +1550,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p Gia_Obj_t * pObjNew; pMan->nAndNodes++; pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pPars->nLevelMax && Gia_ObjLevel(p, pObj) > pPars->nLevelMax ) + continue; pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) ); if ( Gia_ObjIsAnd(pObjNew) ) if ( Vec_BitEntry(pMan->vFails, Gia_ObjFaninId0(pObjNew, Abc_Lit2Var(pObj->Value))) || -- cgit v1.2.3