diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-27 12:07:26 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-27 12:07:26 -0700 |
| commit | 446cfcf8a6f4f15df46a973737a5280dea43cb14 (patch) | |
| tree | c0adbe9a38b27cafbbde041573081e8f1997dd48 /src/proof/pdr | |
| parent | c27556c5692f41d2ac4fb7c1705c574c0337b684 (diff) | |
| download | abc-446cfcf8a6f4f15df46a973737a5280dea43cb14.tar.gz abc-446cfcf8a6f4f15df46a973737a5280dea43cb14.tar.bz2 abc-446cfcf8a6f4f15df46a973737a5280dea43cb14.zip | |
Changing how often timeout is checked in the SAT solver and several application packages.
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 11 | ||||
| -rw-r--r-- | src/proof/pdr/pdrSat.c | 9 |
2 files changed, 19 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 03d522d3..3f74dd5f 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index a68bbee4..c9028c24 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -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; /* |