diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-03 07:28:04 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-03 07:28:04 -0700 |
| commit | 1d44f420392d40a71c907a0ad7636983f2441f30 (patch) | |
| tree | befcd781e41c12f993896bf04ad9c988de39825e /src/sat/satoko | |
| parent | f99149889037a439460e06f5e1e089d0c914f9a8 (diff) | |
| download | abc-1d44f420392d40a71c907a0ad7636983f2441f30.tar.gz abc-1d44f420392d40a71c907a0ad7636983f2441f30.tar.bz2 abc-1d44f420392d40a71c907a0ad7636983f2441f30.zip | |
Change in Satoko to make assumption var values appear in satisfiable assignments produced.
Diffstat (limited to 'src/sat/satoko')
| -rw-r--r-- | src/sat/satoko/solver_api.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 837d64e7..20217e54 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -290,6 +290,7 @@ void satoko_assump_push(solver_t *s, int lit) assert(lit2var(lit) < satoko_varnum(s)); // printf("[Satoko] Push assumption: %d\n", lit); vec_uint_push_back(s->assumptions, lit); + vec_char_assign(s->polarity, lit2var(lit), lit_polarity(lit)); } void satoko_assump_pop(solver_t *s) |