diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/satoko/satoko.h | 2 | ||||
-rw-r--r-- | src/sat/satoko/solver.c | 16 | ||||
-rw-r--r-- | src/sat/satoko/solver.h | 23 | ||||
-rw-r--r-- | src/sat/satoko/solver_api.c | 27 |
4 files changed, 64 insertions, 4 deletions
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index e3134b77..8d55a81c 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -89,6 +89,8 @@ extern void satoko_assump_push(satoko_t *s, unsigned); extern void satoko_assump_pop(satoko_t *s); extern int satoko_simplify(satoko_t *); extern int satoko_solve(satoko_t *); +extern void satoko_mark_cone(satoko_t *s, int * pvars, int nvars); +extern void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars); /* If problem is unsatisfiable under assumptions, this function is used to * obtain the final conflict clause expressed in the assumptions. diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index cdd3141e..2abc9833 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -190,14 +190,18 @@ static inline unsigned solver_decide(solver_t *s) if (heap_size(s->var_order) == 0) { next_var = UNDEF; return UNDEF; - } else - next_var = heap_remove_min(s->var_order); + } + next_var = heap_remove_min(s->var_order); + if (solver_has_marks(s) && !var_mark(s, next_var)) + next_var = UNDEF; } return var2lit(next_var, vec_char_at(s->polarity, next_var)); } static inline void solver_new_decision(solver_t *s, unsigned lit) { + if (solver_has_marks(s) && !var_mark(s, lit2var(lit))) + return; assert(var_value(s, lit2var(lit)) == VAR_UNASSING); vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); solver_enqueue(s, lit, UNDEF); @@ -538,6 +542,8 @@ unsigned solver_propagate(solver_t *s) n_propagations++; watch_list_foreach(s->bin_watches, i, p) { + if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) + continue; if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING) solver_enqueue(s, i->blocker, i->cref); else if (lit_value(s, i->blocker) == LIT_FALSE) @@ -551,6 +557,12 @@ unsigned solver_propagate(solver_t *s) struct clause *clause; struct watcher w; + if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) + { + *j++ = *i++; + continue; + } + if (lit_value(s, i->blocker) == LIT_TRUE) { *j++ = *i++; continue; diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 849d738a..01912a6e 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -93,6 +93,9 @@ struct solver_t_ { vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and * clauses minimization with binary resolution */ + /* Temporary data used for solving cones */ + vec_char_t *marks; + struct satoko_stats stats; struct satoko_opts opts; }; @@ -133,6 +136,18 @@ static inline unsigned var_reason(solver_t *s, unsigned var) { return vec_uint_at(s->reasons, var); } +static inline int var_mark(solver_t *s, unsigned var) +{ + return (int)vec_char_at(s->marks, var); +} +static inline void var_set_mark(solver_t *s, unsigned var) +{ + vec_char_assign(s->marks, var, 1); +} +static inline void var_clean_mark(solver_t *s, unsigned var) +{ + vec_char_assign(s->marks, var, 0); +} //===------------------------------------------------------------------------=== // Inline lit functions //===------------------------------------------------------------------------=== @@ -185,6 +200,14 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason) vec_uint_push_back(s->trail, lit); return SATOKO_OK; } +static inline int solver_varnum(solver_t *s) +{ + return vec_char_size(s->assigns); +} +static inline int solver_has_marks(solver_t *s) +{ + return (int)(s->marks != NULL); +} //===------------------------------------------------------------------------=== // Inline clause functions diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index f3f3d781..b446fb05 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -145,11 +145,13 @@ void satoko_destroy(solver_t *s) vec_uint_free(s->stack); vec_uint_free(s->last_dlevel); vec_uint_free(s->stamps); + if (s->marks) vec_char_free(s->marks); satoko_free(s); } void satoko_default_opts(satoko_opts_t *opts) { + memset(opts, 0, sizeof(satoko_opts_t)); opts->verbose = 0; /* Limits */ opts->conf_limit = 0; @@ -232,6 +234,7 @@ void satoko_add_variable(solver_t *s, char sign) vec_uint_push_back(s->stamps, 0); vec_char_push_back(s->seen, 0); heap_insert(s->var_order, var); + if (s->marks) vec_char_push_back(s->marks, 0); } int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) @@ -287,8 +290,8 @@ int satoko_solve(solver_t *s) char status = SATOKO_UNDEC; assert(s); - if (s->opts.verbose) - print_opts(s); + //if (s->opts.verbose) + // print_opts(s); while (status == SATOKO_UNDEC) { status = solver_search(s); @@ -317,4 +320,24 @@ satoko_stats_t satoko_stats(satoko_t *s) return s->stats; } +void satoko_mark_cone(satoko_t *s, int * pvars, int nvars) +{ + int i; + if (!solver_has_marks(s)) + s->marks = vec_char_init(solver_varnum(s), 0); + for (i = 0; i < nvars; i++) + { + var_set_mark(s, pvars[i]); + if (!heap_in_heap(s->var_order, pvars[i])) + heap_insert(s->var_order, pvars[i]); + } +} +void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars) +{ + int i; + assert(solver_has_marks(s)); + for (i = 0; i < nvars; i++) + var_clean_mark(s, pvars[i]); +} + ABC_NAMESPACE_IMPL_END |