Added restarts to PDR.

6 files changed, 53 insertions, 21 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e2f0200d..70c51d7a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -20783,7 +20783,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, "OMFCTrmsdgvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCRTrmsdgvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20831,6 +20831,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nConfLimit < 0 ) 
                 goto usage;
             break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRestLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRestLimit < 0 ) 
+                goto usage;
+            break;
         case 'T':
             if ( globalUtilOptind >= argc )
             {
@@ -20904,14 +20915,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-OMFCT<num] [-rmsdgvwh]\n" );
-    Abc_Print( -2, "\t         model checking using property directed reachability (aka ic3)\n" );
+    Abc_Print( -2, "usage: pdr [-OMFCRT<num] [-rmsdgvwh]\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" );
     Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" );
-    Abc_Print( -2, "\t-M num : number of unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
-    Abc_Print( -2, "\t-F num : number of timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
-    Abc_Print( -2, "\t-C num : number of conflicts in a SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
+    Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
+    Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
     Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
     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" );
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 4f0f769e..d245b467 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -44,6 +44,7 @@ struct Pdr_Par_t_
     int nRecycle;     // limit on vars for recycling
     int nFrameMax;    // limit on frame count
     int nConfLimit;   // limit on SAT solver conflicts
+    int nRestLimit;   // limit on the number of proof-obligations
     int nTimeOut;     // timeout in seconds
     int fTwoRounds;   // use two rounds for generalization
     int fMonoCnf;     // monolythic CNF
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 025ada06..9ba5dc2d 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -50,6 +50,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->nFrameMax     =    5000;  // limit on number of timeframes
     pPars->nTimeOut      =       0;  // timeout in seconds
     pPars->nConfLimit    =  100000;  // limit on SAT solver conflicts
+    pPars->nRestLimit    =       0;  // limit on the number of proof-obligations
     pPars->fTwoRounds    =       0;  // use two rounds for generalization
     pPars->fMonoCnf      =       0;  // monolythic CNF
     pPars->fDumpInv      =       0;  // dump inductive invariant
@@ -429,6 +430,12 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
         pThis = Pdr_QueueHead( p );
         if ( pThis->iFrame == 0 )
             return 0; // SAT
+        if ( p->nQueLim && p->nQueCur >= p->nQueLim )
+        {
+            p->nQueLim = p->nQueLim * 11 / 10;
+            Pdr_QueueStop( p );
+            return 1; // restart
+        }
         pThis = Pdr_QueuePop( p );
         assert( pThis->iFrame > 0 );
         assert( !Pdr_SetIsInit(pThis->pState, -1) );
@@ -584,12 +591,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 p->pPars->iFrame = k;
                 return 0; // SAT
             }
+            if ( p->pPars->fVerbose ) 
+                Pdr_ManPrintProgress( p, 0, clock() - clkStart );
         }
         else
         {
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
             // open a new timeframe
+            p->nQueLim = p->pPars->nRestLimit;
             assert( pCube == NULL );
             Pdr_ManSetPropertyOutput( p, k );
             Pdr_ManCreateSolver( p, ++k );
@@ -619,7 +629,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             }
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 0, clock() - clkStart );
-            clkStart = clock();
+//            clkStart = clock();
         }
 
         // check the timeout
@@ -696,6 +706,14 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
 ***********************************************************************/
 int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
 {
+//    printf( "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
+    printf( "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", 
+        pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
+    if ( pPars->iOutput >= 0 )
+        printf( "Output = %d. ", pPars->iOutput );
+    printf( "MonoCNF = %s. SkipGen = %s.\n", 
+        pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
+
 /*
     Vec_Int_t * vPrioInit = NULL;
     int RetValue, nTimeOut;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index baf4ca02..0a90f9d1 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -107,6 +107,9 @@ struct Pdr_Man_t_
     int         nCasesSU;
     int         nCasesUS;
     int         nCasesUU;
+    int         nQueCur;
+    int         nQueMax;
+    int         nQueLim;
     // runtime
     int         timeStart;
     int         timeToStop;
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 30d1145d..92bd6d00 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -46,7 +46,6 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
 {
-    static int PastSize;
     Vec_Ptr_t * vVec;
     int i, ThisSize, Length, LengthStart;
     if ( Vec_PtrSize(p->vSolvers) < 2 )
@@ -56,9 +55,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
     Vec_VecForEachLevel( p->vClauses, vVec, i )
         Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
     // determine the starting point
-    LengthStart = Abc_MaxInt( 0, Length - 70 );
+    LengthStart = Abc_MaxInt( 0, Length - 60 );
     printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
-    ThisSize = 6;
+    ThisSize = 5;
     if ( LengthStart > 0 )
     {
         printf( " ..." );
@@ -76,18 +75,13 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
         Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
         ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
     }
+    for ( i = ThisSize; i < 70; i++ )
+        printf( " " );
+    printf( "%6d", p->nQueMax );
+    printf(" %8.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
+    printf("%s", fClose ? "\n":"\r" );
     if ( fClose )
-    {
-        for ( i = 0; i < PastSize - ThisSize; i++ )
-            printf( " " );
-        printf( "\n" );
-    }
-    else
-    {
-        printf( "\r" );
-        PastSize = ThisSize;
-    }
-//    printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
+        p->nQueMax = 0;
 }
 
 /**Function*************************************************************
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 17383425..c0570988 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -500,6 +500,7 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
         return NULL;
     p->pQueue = p->pQueue->pLink;
     Pdr_OblDeref( pRes );
+    p->nQueCur--;
     return pRes;
 }
 
@@ -518,6 +519,8 @@ void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
 {
     Pdr_Obl_t * pTemp, ** ppPrev;
     p->nObligs++;
+    p->nQueCur++;
+    p->nQueMax = Abc_MaxInt( p->nQueMax, p->nQueCur );
     Pdr_OblRef( pObl );
     if ( p->pQueue == NULL )
     {
@@ -569,6 +572,7 @@ void Pdr_QueueStop( Pdr_Man_t * p )
         Pdr_OblDeref( pObl );
     }
     p->pQueue = NULL;
+    p->nQueCur = 0;
 }