diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-18 14:20:10 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-18 14:20:10 -0800 |
commit | 429f52ce15d1c10e71d98d8c1388b93809a425e1 (patch) | |
tree | 9c9a388ba80ec97abbc2afcfb1c966e50cccfbc7 /src/sat/satoko/solver_api.c | |
parent | bc010af4be920199d7f1e0bfe4a6d70dcbca042b (diff) | |
download | abc-429f52ce15d1c10e71d98d8c1388b93809a425e1.tar.gz abc-429f52ce15d1c10e71d98d8c1388b93809a425e1.tar.bz2 abc-429f52ce15d1c10e71d98d8c1388b93809a425e1.zip |
Experiments with SAT sweeping.
Diffstat (limited to 'src/sat/satoko/solver_api.c')
-rw-r--r-- | src/sat/satoko/solver_api.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 9cad0a14..e03cc084 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -216,7 +216,7 @@ int satoko_simplify(solver_t * s) return SATOKO_OK; } -void satoko_add_variable(solver_t *s, char sign) +int satoko_add_variable(solver_t *s, char sign) { unsigned var = vec_act_size(s->activity); vec_wl_push(s->watches); @@ -231,6 +231,7 @@ void satoko_add_variable(solver_t *s, char sign) heap_insert(s->var_order, var); if (s->marks) vec_char_push_back(s->marks, 0); + return var; } int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) @@ -351,6 +352,7 @@ void satoko_rollback(satoko_t *s) clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i])); cl_to_remove[i]->f_mark = 1; } + satoko_free(cl_to_remove); vec_uint_shrink(s->originals, s->book_cl_orig); vec_uint_shrink(s->learnts, s->book_cl_lrnt); /* Shrink variable related vectors */ |