diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-15 17:07:12 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-15 17:07:12 +0700 |
commit | 7747f21fe6f8a026677f748b2855055297ca0d5a (patch) | |
tree | 19cd350368d11aae527bd6123992fe80e21eea02 /src/sat | |
parent | ca87c1a6a09a7357931432e47c0b0edd4cb29c20 (diff) | |
download | abc-7747f21fe6f8a026677f748b2855055297ca0d5a.tar.gz abc-7747f21fe6f8a026677f748b2855055297ca0d5a.tar.bz2 abc-7747f21fe6f8a026677f748b2855055297ca0d5a.zip |
Added several helpful APIs to Satoko.
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/satoko/satoko.h | 1 | ||||
-rw-r--r-- | src/sat/satoko/solver.h | 17 | ||||
-rw-r--r-- | src/sat/satoko/solver_api.c | 15 |
3 files changed, 33 insertions, 0 deletions
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 6634e68e..2095a650 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -92,6 +92,7 @@ extern void satoko_assump_push(satoko_t *s, int); extern void satoko_assump_pop(satoko_t *s); extern int satoko_simplify(satoko_t *); extern int satoko_solve(satoko_t *); +extern int satoko_solve_with_assumptions(satoko_t *s, int * plits, int nlits); extern void satoko_mark_cone(satoko_t *, int *, int); extern void satoko_unmark_cone(satoko_t *, int *, int); diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index cfb7d538..4abf9979 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -222,6 +222,19 @@ 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) { return (int)(s->marks != NULL); @@ -234,6 +247,10 @@ 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; +} //===------------------------------------------------------------------------=== // Inline clause functions diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 62749e88..54987007 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -313,6 +313,21 @@ int satoko_solve(solver_t *s) return status; } +int satoko_solve_with_assumptions(solver_t *s, int * plits, int nlits) +{ + int i, status; + for ( i = 0; i < nlits; i++ ) + satoko_assump_push( s, plits[i] ); + status = satoko_solve( s ); + for ( i = 0; i < nlits; i++ ) + satoko_assump_pop( s ); + if ( status == SATOKO_UNSAT ) + return 1; + if ( status == SATOKO_SAT ) + return 0; + return -1; +} + int satoko_final_conflict(solver_t *s, unsigned *out) { if (vec_uint_size(s->final_conflict) == 0) |