diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 7 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index dcf5b534..adbdafca 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -52,6 +52,7 @@ struct Pdr_Par_t_ int fMonoCnf; // monolythic CNF int fDumpInv; // dump inductive invariant int fShortest; // forces bug traces to be shortest + int fShiftStart; // allows clause pushing to start from an intermediate frame int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe int fSkipGeneral; // skips expensive generalization step int fVerbose; // verbose output` diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index fe023617..55c40c1e 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -137,10 +137,11 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) Pdr_Set_t * pTemp, * pCubeK, * pCubeK1; Vec_Ptr_t * vArrayK, * vArrayK1; int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1; + int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1; int Counter = 0; abctime clk = Abc_Clock(); assert( p->iUseFrame > 0 ); - Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax ) + Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) { Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare ); vArrayK1 = Vec_VecEntry( p->vClauses, k+1 ); @@ -441,9 +442,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) pThis = Pdr_QueueHead( p ); if ( pThis->iFrame == 0 ) return 0; // SAT - if ( pThis->iFrame > kMax ) // finished this level - return 1; if ( p->nQueLim && p->nQueCur >= p->nQueLim ) { @@ -586,7 +585,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { p->nFrames = k; assert( k == Vec_PtrSize(p->vSolvers)-1 ); - p->iUseFrame = ABC_INFINITY; + p->iUseFrame = Abc_MaxInt(k, 1); Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) { // skip disproved outputs |