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 | |
| 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')
| -rw-r--r-- | src/sat/satoko/satoko.h | 2 | ||||
| -rw-r--r-- | src/sat/satoko/solver_api.c | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 88070eac..7c2f3720 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -83,7 +83,7 @@ extern void satoko_destroy(satoko_t *); extern void satoko_default_opts(satoko_opts_t *); extern void satoko_configure(satoko_t *, satoko_opts_t *); extern int satoko_parse_dimacs(char *, satoko_t **); -extern void satoko_add_variable(satoko_t *, char); +extern int satoko_add_variable(satoko_t *, char); extern int satoko_add_clause(satoko_t *, unsigned *, unsigned); extern void satoko_assump_push(satoko_t *s, unsigned); extern void satoko_assump_pop(satoko_t *s); 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 */ |