diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2017-08-29 09:40:51 +0200 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-08-29 09:40:51 +0200 |
commit | ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27 (patch) | |
tree | b8575b157b1019275f5f1da040b18d3c36fd6e11 /src/sat/satoko/solver.h | |
parent | d0f81fcf2952b8a46548c0dd74f95fa1cd0a504f (diff) | |
download | abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.gz abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.bz2 abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.zip |
Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages
Diffstat (limited to 'src/sat/satoko/solver.h')
-rw-r--r-- | src/sat/satoko/solver.h | 47 |
1 files changed, 4 insertions, 43 deletions
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index ee7b84e2..1a20632f 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -30,11 +30,7 @@ #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START -enum { - LIT_FALSE = 1, - LIT_TRUE = 0, - VAR_UNASSING = 3 -}; + #define UNDEF 0xFFFFFFFF @@ -145,11 +141,6 @@ static inline char var_value(solver_t *s, unsigned var) return vec_char_at(s->assigns, var); } -static inline char var_polarity(solver_t *s, unsigned var) -{ - return vec_char_at(s->polarity, var); -} - static inline unsigned var_dlevel(solver_t *s, unsigned var) { return vec_uint_at(s->levels, var); @@ -226,45 +217,15 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason) return SATOKO_OK; } -static inline int solver_varnum(solver_t *s) -{ - return vec_char_size(s->assigns); -} -static inline int solver_clausenum(solver_t *s) -{ - return vec_uint_size(s->originals); -} -static inline int solver_learntnum(solver_t *s) -{ - return vec_uint_size(s->learnts); -} -static inline int solver_conflictnum(solver_t *s) -{ - return satoko_stats(s).n_conflicts; -} - -static inline int solver_has_marks(solver_t *s) +static inline int solver_has_marks(satoko_t *s) { return (int)(s->marks != NULL); } -static inline int solver_stop(solver_t *s) + +static inline int solver_stop(satoko_t *s) { return s->pstop && *s->pstop; } -static inline void solver_set_stop(solver_t *s, int * pstop) -{ - s->pstop = pstop; -} -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 |