Version abc50908

12 files changed, 134 insertions, 52 deletions

diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index d7f5b104..d7358749 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -119,6 +119,30 @@ void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
     fprintf( pFile, "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * solver_get_model( solver * p, int * pVars, int nVars )
+{
+    int * pModel;
+    int i;
+    pModel = ALLOC( int, nVars );
+    for ( i = 0; i < nVars; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < p->size );
+        pModel[i] = (int)(p->model.ptr[pVars[i]] == (void *)l_True);
+    }
+    return pModel;    
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index c9dadcb4..98024a7f 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdio.h>
 #include <assert.h>
 #include <math.h>
+#include <time.h>
 
 #include "solver.h"
 
@@ -1055,13 +1056,14 @@ bool   solver_simplify(solver* s)
 }
 
 
-bool   solver_solve(solver* s, lit* begin, lit* end)
+int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
 {
     double  nof_conflicts = 100;
     double  nof_learnts   = solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
     lbool*  values        = s->assigns;
     lit*    i;
+    int     timeStart     = clock();
 
     for (i = begin; i < end; i++)
         if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
@@ -1096,12 +1098,15 @@ bool   solver_solve(solver* s, lit* begin, lit* end)
         status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
         nof_conflicts *= 1.5;
         nof_learnts   *= 1.1;
+        // if the runtime limit is exceeded, quit the restart loop
+        if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC )
+            break;
     }
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
     solver_canceluntil(s,0);
-    return status != l_False;
+    return status;
 }
 
 
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index e04d5780..f328fad5 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -69,7 +69,8 @@ extern void    solver_delete(solver* s);
 
 extern bool    solver_addclause(solver* s, lit* begin, lit* end);
 extern bool    solver_simplify(solver* s);
-extern bool    solver_solve(solver* s, lit* begin, lit* end);
+extern int     solver_solve(solver* s, lit* begin, lit* end, int nSeconds);
+extern int *   solver_get_model( solver * p, int * pVars, int nVars );
 
 extern int     solver_nvars(solver* s);
 extern int     solver_nclauses(solver* s);
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index b030caef..4481297a 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_DEFAULT_TIMEOUT     60   // 60 seconds
+
 struct CSAT_ManagerStruct_t
 {
     // information about the problem
@@ -33,7 +35,8 @@ struct CSAT_ManagerStruct_t
     Abc_Ntk_t *           pTarget;       // the AIG representing the target
     char *                pDumpFileName; // the name of the file to dump the target network
     // solving parameters
-    int                   mode;          // 0 = baseline;  1 = resource-aware fraiging
+    int                   mode;          // 0 = brute-force SAT;  1 = resource-aware FRAIG
+    int                   nSeconds;      // time limit for pure SAT solving
     Fraig_Params_t        Params;        // the set of parameters to call FRAIG package
     // information about the target 
     int                   nog;           // the numbers of gates in the target
@@ -44,11 +47,9 @@ struct CSAT_ManagerStruct_t
 };
 
 static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
-static void CSAT_TargetResFree( CSAT_Target_ResultT * p );
 static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode );
 
 // some external procedures
-extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
 extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 
 ////////////////////////////////////////////////////////////////////////
@@ -77,6 +78,7 @@ CSAT_Manager CSAT_InitManager()
     mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
     mng->vNodes     = Vec_PtrAlloc( 100 );
     mng->vValues    = Vec_IntAlloc( 100 );
+    mng->nSeconds   = ABC_DEFAULT_TIMEOUT;
     return mng;
 }
 
@@ -107,7 +109,7 @@ void CSAT_QuitManager( CSAT_Manager mng )
 
   Synopsis    [Sets solver options for learning.]
 
-  Description [0 = baseline; 1 = resource-aware solving.]
+  Description [0 = brute-force SAT;  1 = resource-aware FRAIG.]
                
   SideEffects []
 
@@ -118,11 +120,11 @@ void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
 {
     mng->mode = option;
     if ( option == 0 )
-        printf( "CSAT_SetSolveOption: Setting baseline solving mode.\n" );
+        printf( "CSAT_SetSolveOption: Setting brute-force SAT mode.\n" );
     else if ( option == 1 )
-        printf( "CSAT_SetSolveOption: Setting resource-aware solving mode.\n" );
+        printf( "CSAT_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
     else
-        printf( "CSAT_SetSolveOption: Unknown option.\n" );
+        printf( "CSAT_SetSolveOption: Unknown solving mode.\n" );
 }
 
 
@@ -280,7 +282,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
     // make sure everything is okay with the network structure
-    if ( !Abc_NtkCheckRead( pNtk ) )
+    if ( !Abc_NtkDoCheck( pNtk ) )
     {
         printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
         return 0;
@@ -311,7 +313,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
 ***********************************************************************/
 void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
 {
-    printf( "CSAT_SetTimeLimit: The resource limit is not implemented (warning).\n" );
+    mng->nSeconds = runtime;
 }
 
 /**Function*************************************************************
@@ -458,7 +460,8 @@ void CSAT_SolveInit( CSAT_Manager mng )
     memset( pParams, 0, sizeof(Fraig_Params_t) );
     pParams->nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
     pParams->nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
-    pParams->nBTLimit   = 99;             // the max number of backtracks to perform at a node
+    pParams->nBTLimit   = 10;             // the max number of backtracks to perform at a node
+    pParams->nSeconds   = mng->nSeconds;  // the time out for the final proof
     pParams->fFuncRed   = mng->mode;      // performs only one level hashing
     pParams->fFeedBack  = 1;              // enables solver feedback
     pParams->fDist1Pats = 1;              // enables distance-1 patterns
@@ -498,6 +501,7 @@ void CSAT_AnalyzeTargets( CSAT_Manager mng )
 enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
 {
     Fraig_Man_t * pMan;
+    Abc_Ntk_t * pCnf;
     int * pModel;
     int RetValue, i;
 
@@ -505,34 +509,68 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
     if ( mng->pTarget == NULL )
         { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; }
 
-    // transform the target into a fraig
-    pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); 
-    Fraig_ManProveMiter( pMan );
-
-    // analyze the result
-    mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
-    RetValue = Fraig_ManCheckMiter( pMan );
-    if ( RetValue == -1 )
-        mng->pResult->status = UNDETERMINED;
-    else if ( RetValue == 1 )
-        mng->pResult->status = UNSATISFIABLE;
-    else if ( RetValue == 0 )
+    // optimizations of the target go here
+    // for example, to enable one pass of rewriting, uncomment this line
+//    Abc_NtkRewrite( mng->pTarget, 0, 1, 0 );
+
+    if ( mng->mode == 0 ) // brute-force SAT
+    {
+        // transfor the AIG into a logic network for efficient CNF construction
+        pCnf = Abc_NtkRenode( mng->pTarget, 0, 100, 1, 0, 0 );
+        RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 );
+
+        // analyze the result
+        mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+        if ( RetValue == -1 )
+            mng->pResult->status = UNDETERMINED;
+        else if ( RetValue == 1 )
+            mng->pResult->status = UNSATISFIABLE;
+        else if ( RetValue == 0 )
+        {
+            mng->pResult->status = SATISFIABLE;
+            // create the array of PI names and values
+            for ( i = 0; i < mng->pResult->no_sig; i++ )
+            {
+                mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
+                mng->pResult->values[i] = pCnf->pModel[i];
+            }
+            FREE( mng->pTarget->pModel );
+        }
+        else assert( 0 );
+        Abc_NtkDelete( pCnf );
+    }
+    else if ( mng->mode == 1 ) // resource-aware fraiging
     {
-        mng->pResult->status = SATISFIABLE;
-        pModel = Fraig_ManReadModel( pMan );
-        assert( pModel != NULL );
-        // create the array of PI names and values
-        for ( i = 0; i < mng->pResult->no_sig; i++ )
+        // transform the target into a fraig
+        pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); 
+        Fraig_ManProveMiter( pMan );
+        RetValue = Fraig_ManCheckMiter( pMan );
+
+        // analyze the result
+        mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+        if ( RetValue == -1 )
+            mng->pResult->status = UNDETERMINED;
+        else if ( RetValue == 1 )
+            mng->pResult->status = UNSATISFIABLE;
+        else if ( RetValue == 0 )
         {
-            mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
-            mng->pResult->values[i] = pModel[i];
+            mng->pResult->status = SATISFIABLE;
+            pModel = Fraig_ManReadModel( pMan );
+            assert( pModel != NULL );
+            // create the array of PI names and values
+            for ( i = 0; i < mng->pResult->no_sig; i++ )
+            {
+                mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
+                mng->pResult->values[i] = pModel[i];
+            }
         }
+        else assert( 0 );
+        // delete the fraig manager
+        Fraig_ManFree( pMan );
     }
-    else 
+    else
         assert( 0 );
 
-    // delete the fraig manager
-    Fraig_ManFree( pMan );
     // delete the target
     Abc_NtkDelete( mng->pTarget );
     mng->pTarget = NULL;
@@ -558,9 +596,9 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
 
 /**Function*************************************************************
 
-  Synopsis    [Dumps the target AIG into the BENCH file.]
+  Synopsis    [Dumps the original network into the BENCH file.]
 
-  Description []
+  Description [This procedure should be modified to dump the target.]
                
   SideEffects []
 
@@ -569,11 +607,13 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
 ***********************************************************************/
 void CSAT_Dump_Bench_File( CSAT_Manager mng )
 {
-    Abc_Ntk_t * pNtkTemp;
+    Abc_Ntk_t * pNtkTemp, * pNtkAig;
     char * pFileName;
-
+ 
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlistBench( mng->pTarget );
+    pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0 );
+    pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig );
+    Abc_NtkDelete( pNtkAig );
     if ( pNtkTemp == NULL ) 
         { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
     pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index 124ca266..4ac5a6a3 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -167,6 +167,10 @@ extern enum CSAT_StatusT     CSAT_Solve(CSAT_Manager mng);
 extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
 extern void                  CSAT_Dump_Bench_File(CSAT_Manager mng);
 
+// ADDED PROCEDURES:
+extern void                  CSAT_QuitManager( CSAT_Manager mng );
+extern void                  CSAT_TargetResFree( CSAT_Target_ResultT * p );
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 901bbac9..75dfb812 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -43,6 +43,7 @@ struct Fraig_ParamsStruct_t_
     int  nPatsRand;     // the number of words of random simulation info
     int  nPatsDyna;     // the number of words of dynamic simulation info
     int  nBTLimit;      // the max number of backtracks to perform
+    int  nSeconds;      // the timeout for the final proof
     int  fFuncRed;      // performs only one level hashing
     int  fFeedBack;     // enables solver feedback
     int  fDist1Pats;    // enables distance-1 patterns
@@ -162,8 +163,8 @@ extern int                 Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pO
 extern int                 Fraig_CountLevels( Fraig_Man_t * pMan );
 
 /*=== fraigSat.c =============================================================*/
-extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
-extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
+extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit );
+extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
 extern void                Fraig_ManProveMiter( Fraig_Man_t * p );
 extern int                 Fraig_ManCheckMiter( Fraig_Man_t * p );
 
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index 5a7d0563..a8d6c3af 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -167,7 +167,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
     // there is another node which looks the same according to simulation
 
     // use SAT to resolve the ambiguity
-    if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit ) )
+    if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
     {
         // set the node to be equivalent with this node
         // to prevent loops, only set if the old node is not in the TFI of the new node
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 131b750c..f14fb4c1 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -143,6 +143,7 @@ struct Fraig_ManStruct_t_
     int                   nWordsRand;    // the number of words of random simulation info
     int                   nWordsDyna;    // the number of words of dynamic simulation info
     int                   nBTLimit;      // the max number of backtracks to perform
+    int                   nSeconds;      // the runtime limit for the miter proof
     int                   fFuncRed;      // performs only one level hashing
     int                   fFeedBack;     // enables solver feedback
     int                   fDist1Pats;    // enables solver feedback
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index e5979c93..aa7e5999 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -46,6 +46,7 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
     pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
     pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
     pParams->nBTLimit   = 99;                     // the max number of backtracks to perform
+    pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
     pParams->fFuncRed   =  1;                     // performs only one level hashing
     pParams->fFeedBack  =  1;                     // enables solver feedback
     pParams->fDist1Pats =  1;                     // enables distance-1 patterns
@@ -100,6 +101,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand );  // the number of words of random simulation info
     p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna );  // the number of patterns for dynamic simulation info
     p->nBTLimit   = pParams->nBTLimit;    // -1 means infinite backtrack limit
+    p->nSeconds   = pParams->nSeconds;    // the timeout for the final miter
     p->fFuncRed   = pParams->fFuncRed;    // enables functional reduction (otherwise, only one-level hashing is performed)
     p->fFeedBack  = pParams->fFeedBack;   // enables solver feedback (the use of counter-examples in simulation)
     p->fDist1Pats = pParams->fDist1Pats;  // enables solver feedback (the use of counter-examples in simulation)
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 17201e58..fcb1018f 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -56,13 +56,13 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i );
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
+int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit )
 {
     if ( pNode1 == pNode2 )
         return 1;
     if ( pNode1 == Fraig_Not(pNode2) )
         return 0;
-    return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit );
+    return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
 }
 
 /**Function*************************************************************
@@ -95,7 +95,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
         // skip nodes that are different according to simulation
         if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
             continue;
-        if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1 ) )
+        if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
         {
             if ( Fraig_IsComplement(p->vOutputs->pArray[i]) )
                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
@@ -160,7 +160,7 @@ int Fraig_ManCheckMiter( Fraig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
+int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit )
 {
     int RetValue, RetValue1, i, fComp, clk;
     int fVerbose = 0;
@@ -227,7 +227,7 @@ if ( fVerbose )
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
     // run the solver
 clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
@@ -286,7 +286,7 @@ p->time3 += clock() - clk;
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
     // run the solver
 clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += clock() - clk;
     if ( RetValue1 == MSAT_FALSE )
     {
@@ -411,7 +411,7 @@ if ( fVerbose )
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
     // run the solver
 clk = clock();
-    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit );
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
 p->timeSat += clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 21ddcb81..8cbbea97 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -79,7 +79,7 @@ extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p
 extern bool             Msat_SolverAddVar( Msat_Solver_t * p );
 extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
 extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
-extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit );
+extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
 // printing stats, assignments, and clauses
 extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
 extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index b8d9f328..6a1a1ae7 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -131,11 +131,12 @@ void Msat_SolverPrintStats( Msat_Solver_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit )
+bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
 {
     Msat_SearchParams_t Params = { 0.95, 0.999 };
     double nConflictsLimit, nLearnedLimit;
     Msat_Type_t Status;
+    int timeStart = clock();
     int64 nConflictsOld = p->Stats.nConflicts;
     int64 nDecisionsOld = p->Stats.nDecisions;
 
@@ -174,6 +175,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
         // if the limit on the number of backtracks is given, quit the restart loop
         if ( nBackTrackLimit > 0 )
             break;
+        // if the runtime limit is exceeded, quit the restart loop
+        if ( clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
+            break;
     }
     Msat_SolverCancelUntil( p, 0 );
     p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;