Adding switch 'pdr -i' to start push_clauses from an intermediate timeframe.

3 files changed, 11 insertions, 7 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bfe1bd15..73ddcc97 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23650,7 +23650,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTHGaxrmspdgvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTHGaxrmsipdgvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23746,6 +23746,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fShortest ^= 1;
             break;
+        case 'i':
+            pPars->fShiftStart ^= 1;
+            break;
         case 'p':
             pPars->fReuseProofOblig ^= 1;
             break;
@@ -23796,7 +23799,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCRTHG <num>] [-axrmsdgvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCRTHG <num>] [-axrmsipdgvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -23812,7 +23815,8 @@ usage:
     Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n",                 pPars->fTwoRounds? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle using monolythic CNF computation [default = %s]\n",                    pPars->fMonoCnf? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle creating only shortest counter-examples [default = %s]\n",             pPars->fShortest? "yes": "no" );
-    Abc_Print( -2, "\t-p     : toggle using proof-obligations from the last timeframe [default = %s]\n",     pPars->fReuseProofOblig? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle clause pushing from an intermediate timeframe [default = %s]\n",       pPars->fShiftStart? "yes": "no" );
+    Abc_Print( -2, "\t-p     : toggle reusing proof-obligations in the last timeframe [default = %s]\n",     pPars->fReuseProofOblig? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle dumping inductive invariant [default = %s]\n",                         pPars->fDumpInv? "yes": "no" );
     Abc_Print( -2, "\t-g     : toggle skipping expensive generalization step [default = %s]\n",              pPars->fSkipGeneral? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n",                       pPars->fVerbose? "yes": "no" );
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