Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.

6 files changed, 13 insertions, 6 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index da3a2d96..259c1b14 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23269,7 +23269,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Saig_ParBmcSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdruvzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdurvzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23435,6 +23435,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'u':
             fOrDecomp ^= 1;
             break;
+        case 'r':
+            pPars->fNoRestarts ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -23501,7 +23504,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axduvzh]\n" );
+    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdurvzh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking with dynamic unrolling\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n",      pPars->nFramesMax );
@@ -23521,6 +23524,7 @@ usage:
     Abc_Print( -2, "\t-x     : toggle storing CEXes when solving all outputs [default = %s]\n",   pPars->fStoreCex? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle dropping (replacing by 0) SAT outputs [default = %s]\n",    pPars->fDropSatOuts? "yes": "no" );
     Abc_Print( -2, "\t-u     : toggle performing structural OR-decomposition [default = %s]\n",   fOrDecomp? "yes": "not" );
+    Abc_Print( -2, "\t-r     : toggle disabling periodic restarts [default = %s]\n",              pPars->fNoRestarts? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n",                           pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n",  pPars->fNotVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 8ab043dd..0a8913fe 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -738,7 +738,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
         if ( Smt_EntryIsName(iRoot0) )
         {
             char * pName, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
-            int fSigned = 0, iObj;
+            int iObj;
             if ( pStr0[0] == 'l' && pStr0[1] == 'e' && pStr0[2] == 't' && pStr0[3] == '\0' )
             {
                 // let ((s35550 (bvor s48 s35549)))
@@ -809,8 +809,8 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
                         int iRoot3 = Vec_IntEntry( vRoots, 3 );
                         char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
                         char * pStr3 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot3));
-                        int Num1 = atoi( pStr1 );
-                        int Num2 = atoi( pStr2 );
+                        int Num1 = atoi( pStr2 );
+                        int Num2 = atoi( pStr3 );
                         assert( Num1 >= Num2 );
                         fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
                         Range = (Num1 - Num2 + 1) + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index bdb5905a..30538253 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -60,6 +60,7 @@ struct Saig_ParBmc_t_
     int         fDropSatOuts;   // replace sat outputs by constant 0
     int         nFfToAddMax;    // max number of flops to add during CBA
     int         fSkipRand;      // skip random decisions
+    int         fNoRestarts;    // disables periodic restarts
     int         nLearnedStart;  // starting learned clause limit
     int         nLearnedDelta;  // delta of learned clause limit
     int         nLearnedPerce;  // ratio of learned clause limit
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index fdc7e613..ccd0bb90 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1415,6 +1415,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
     p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
     p->pSat->nLearntMax   = p->pSat->nLearntStart;
+    p->pSat->fNoRestarts  = p->pPars->fNoRestarts;
     if ( pPars->fSolveAll && p->vCexes == NULL )
         p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
     if ( pPars->fVerbose )
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index e8e13ee7..f1f6345e 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1660,7 +1660,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
             int next;
 
             // Reached bound on number of conflicts:
-            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
+            if ( (!s->fNoRestarts && nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
                 s->progress_estimate = sat_solver_progress(s);
                 sat_solver_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index c4888c73..7ef2c9e8 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -179,6 +179,7 @@ struct sat_solver_t
 
     int         fSkipSimplify; // set to one to skip simplification of the clause database
     int         fNotUseRandom; // do not allow random decisions with a fixed probability
+    int         fNoRestarts;   // disables periodic restarts
 
     int *       pGlobalVars;   // for experiments with global vars during interpolation
     // clause store