summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/asat/added.c24
-rw-r--r--src/sat/asat/solver.c9
-rw-r--r--src/sat/asat/solver.h3
-rw-r--r--src/sat/csat/csat_apis.c114
-rw-r--r--src/sat/csat/csat_apis.h4
-rw-r--r--src/sat/fraig/fraig.h5
-rw-r--r--src/sat/fraig/fraigCanon.c2
-rw-r--r--src/sat/fraig/fraigInt.h1
-rw-r--r--src/sat/fraig/fraigMan.c2
-rw-r--r--src/sat/fraig/fraigSat.c14
-rw-r--r--src/sat/msat/msat.h2
-rw-r--r--src/sat/msat/msatSolverCore.c6
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:50:26 +0000