diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 23:57:34 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 23:57:34 -0800 |
| commit | 4c78f37a5a78ee39957bcb5c793a7203509e642e (patch) | |
| tree | 99aa27d295b846f1b916a25bbd6f5e71e3abe388 /src/proof | |
| parent | 581f2e59721498880d20c85444c2358e6c7c97e9 (diff) | |
| download | abc-4c78f37a5a78ee39957bcb5c793a7203509e642e.tar.gz abc-4c78f37a5a78ee39957bcb5c793a7203509e642e.tar.bz2 abc-4c78f37a5a78ee39957bcb5c793a7203509e642e.zip | |
Sweeping up to a given level.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cecSatG2.c | 6 |
1 files changed, 5 insertions, 1 deletions
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))) || |