summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-10-15 09:04:27 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-10-15 09:04:27 -0700
commitf9900a4c3b69ecae26306f567cd85c9cefebf244 (patch)
treeabc84e31e2a3c1b0832ed3c793e2041d7fe12279 /src/proof
parent1692c1a57a74938a396812375f29f0065b5337b7 (diff)
downloadabc-f9900a4c3b69ecae26306f567cd85c9cefebf244.tar.gz
abc-f9900a4c3b69ecae26306f567cd85c9cefebf244.tar.bz2
abc-f9900a4c3b69ecae26306f567cd85c9cefebf244.zip
Adding switch 'pdr -i' to start push_clauses from an intermediate timeframe.
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/pdr/pdr.h1
-rw-r--r--src/proof/pdr/pdrCore.c7
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