luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Changing how often timeout is checked in the SAT solver and several application packages.

This commit is contained in:
Alan Mishchenko 2013-05-27 12:07:26 -07:00
parent c27556c569
commit 446cfcf8a6
4 changed files with 21 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/proof/pdr/pdrInt.h
View File

@ -135,6 +135,17 @@ struct Pdr_Man_t_
static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
static inline clock_t Pdr_ManTimeLimit( Pdr_Man_t * p )
{
if ( p->timeToStop == 0 )
return p->timeToStopOne;
if ( p->timeToStopOne == 0 )
return p->timeToStop;
if ( p->timeToStop < p->timeToStopOne )
return p->timeToStop;
return p->timeToStopOne;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////

9
src/proof/pdr/pdrSat.c
View File

@ -256,10 +256,13 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
{
sat_solver * pSat;
Vec_Int_t * vLits;
clock_t Limit;
int RetValue;
pSat = Pdr_ManFetchSolver( p, k );
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
sat_solver_set_runtime_limit( pSat, Limit );
if ( RetValue == l_Undef )
return -1;
return (RetValue == l_False);
@ -284,14 +287,16 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
sat_solver * pSat;
Vec_Int_t * vLits;
int Lit, RetValue;
clock_t clk;
clock_t clk, Limit;
p->nCalls++;
pSat = Pdr_ManFetchSolver( p, k );
if ( pCube == NULL ) // solve the property
{
clk = clock();
Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
sat_solver_set_runtime_limit( pSat, Limit );
if ( RetValue == l_Undef )
return -1;
}
@ -320,7 +325,9 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
// solve
clk = clock();
Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
sat_solver_set_runtime_limit( pSat, Limit );
if ( RetValue == l_Undef )
return -1;
/*

2
src/sat/bsat/satSolver.c
View File

@ -1576,7 +1576,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){
if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){
s->progress_estimate = sat_solver_progress(s);
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);

2
src/sat/bsat/satSolver2.c
View File

@ -1037,7 +1037,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
// NO CONFLICT
int next;
if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){
// Reached bound on number of conflicts:
s->progress_estimate = solver2_progress(s);
solver2_canceluntil(s,s->root_level);