Adding switch to enable reuse of proof-obligations in the last timeframe.

src/base/abci/abc.c

@@ -23622,7 +23622,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, "MFCRTHGaxrmsdgvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTHGaxrmspdgvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23718,6 +23718,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fShortest ^= 1;
             break;
+        case 'p':
+            pPars->fReuseProofOblig ^= 1;
+            break;
         case 'd':
             pPars->fDumpInv ^= 1;
             break;
@@ -23781,6 +23784,7 @@ 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-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" );

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 fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
     int fSkipGeneral;     // skips expensive generalization step
     int fVerbose;         // verbose output`
     int fVeryVerbose;     // very verbose output

src/proof/pdr/pdrCore.c

@@ -525,7 +525,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             for ( i = 1; i <= k; i++ )
                 Pdr_ManSolverAddClause( p, i, pCubeMin );
             // schedule proof obligation
-            if ( !p->pPars->fShortest )
+            if ( (k < kMax || p->pPars->fReuseProofOblig) && !p->pPars->fShortest )
             {
                 pThis->iFrame = k+1;
                 pThis->prio   = Prio--;