diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 11:54:14 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 11:54:14 +0700 |
| commit | 443776fed7471d4a0840bb67e64eb833a70a46ba (patch) | |
| tree | 4df49414475d02397d26eb1e8a5893c58795a47a /src/sat/satoko/solver.h | |
| parent | 2280c2e8febcca8082ba87564469b8117e449cbd (diff) | |
| download | abc-443776fed7471d4a0840bb67e64eb833a70a46ba.tar.gz abc-443776fed7471d4a0840bb67e64eb833a70a46ba.tar.bz2 abc-443776fed7471d4a0840bb67e64eb833a70a46ba.zip | |
Additional changes to Satoko to enable various integrations.
Diffstat (limited to 'src/sat/satoko/solver.h')
| -rw-r--r-- | src/sat/satoko/solver.h | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 4abf9979..d6f7d75e 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -103,8 +103,11 @@ struct solver_t_ { /* Temporary data used for solving cones */ vec_char_t *marks; - /* Callback to stop the solver */ - int * pstop; + /* Callbacks to stop the solver */ + abctime nRuntimeLimit; + int *pstop; + int RunId; + int (*pFuncStop)(int); struct satoko_stats stats; struct satoko_opts opts; @@ -251,6 +254,12 @@ static inline int solver_read_cex_varvalue(solver_t *s, int ivar) { return var_polarity(s, ivar) == LIT_TRUE; } +static abctime solver_set_runtime_limit(solver_t* s, abctime Limit) +{ + abctime nRuntimeLimit = s->nRuntimeLimit; + s->nRuntimeLimit = Limit; + return nRuntimeLimit; +} //===------------------------------------------------------------------------=== // Inline clause functions |