mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 09:50:23 +00:00
Code Activity

fix #3440

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-22 10:43:52 -07:00
parent 8717c7d7ff
commit 945cd3169e
2 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/sat/sat_solver.cpp
View file

@ -1189,7 +1189,8 @@ namespace sat {
m_cleaner(true); m_cleaner(true);
return do_local_search(num_lits, lits); return do_local_search(num_lits, lits);
} }
if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || m_config.m_ddfw_threads > 0 || m_config.m_unit_walk_threads > 0) && !m_par) { if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 ||
m_config.m_ddfw_threads > 0 || m_config.m_unit_walk_threads > 0) && !m_par) {
SASSERT(scope_lvl() == 0); SASSERT(scope_lvl() == 0);
return check_par(num_lits, lits); return check_par(num_lits, lits);
} }
@ -1453,17 +1454,17 @@ namespace sat {
m_stats = par.get_solver(finished_id).m_stats; m_stats = par.get_solver(finished_id).m_stats;
} }
if (result == l_true && IS_AUX_SOLVER(finished_id)) { if (result == l_true && IS_AUX_SOLVER(finished_id)) {
set_model(par.get_solver(finished_id).get_model()); set_model(par.get_solver(finished_id).get_model(), true);
} }
else if (result == l_false && IS_AUX_SOLVER(finished_id)) { else if (result == l_false && IS_AUX_SOLVER(finished_id)) {
m_core.reset(); m_core.reset();
m_core.append(par.get_solver(finished_id).get_core()); m_core.append(par.get_solver(finished_id).get_core());
} }
if (result == l_true && IS_LOCAL_SEARCH(finished_id)) { if (result == l_true && IS_LOCAL_SEARCH(finished_id)) {
set_model(ls[finished_id - local_search_offset]->get_model()); set_model(ls[finished_id - local_search_offset]->get_model(), true);
} }
if (result == l_true && IS_UNIT_WALK(finished_id)) { if (result == l_true && IS_UNIT_WALK(finished_id)) {
set_model(uw[finished_id - unit_walk_offset]->get_model()); set_model(uw[finished_id - unit_walk_offset]->get_model(), true);
} }
if (!canceled) { if (!canceled) {
rlimit().reset_cancel(); rlimit().reset_cancel();
@ -1963,10 +1964,10 @@ namespace sat {
} }
} }
void solver::set_model(model const& mdl) { void solver::set_model(model const& mdl, bool is_current) {
m_model.reset(); m_model.reset();
m_model.append(mdl); m_model.append(mdl);
m_model_is_current = !m_model.empty(); m_model_is_current = is_current;
} }
void solver::mk_model() { void solver::mk_model() {
@ -2956,7 +2957,7 @@ namespace sat {
// apply optional clause minimization by detecting subsumed literals. // apply optional clause minimization by detecting subsumed literals.
// initial experiment suggests it has no effect. // initial experiment suggests it has no effect.
m_mus(); // ignore return value on cancelation. m_mus(); // ignore return value on cancelation.
set_model(m_mus.get_model()); set_model(m_mus.get_model(), !m_mus.get_model().empty());
IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";); IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";);
} }
} }
@ -4488,7 +4489,7 @@ namespace sat {
else { else {
is_sat = get_consequences(asms, lits, conseq); is_sat = get_consequences(asms, lits, conseq);
} }
set_model(mdl); set_model(mdl, !mdl.empty());
return is_sat; return is_sat;
} }

2
src/sat/sat_solver.h
View file

@ -445,7 +445,7 @@ namespace sat {
literal_vector const& get_core() const override { return m_core; } literal_vector const& get_core() const override { return m_core; }
model_converter const & get_model_converter() const { return m_mc; } model_converter const & get_model_converter() const { return m_mc; }
void flush(model_converter& mc) override { mc.flush(m_mc); } void flush(model_converter& mc) override { mc.flush(m_mc); }
void set_model(model const& mdl); void set_model(model const& mdl, bool is_current);
char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); } char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); }
bool check_clauses(model const& m) const; bool check_clauses(model const& m) const;
bool is_assumption(bool_var v) const; bool is_assumption(bool_var v) const;