From 873d975c77abeeb58fc170e8c8e03e671ff39bd4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Jan 2017 13:41:15 -0800 Subject: [PATCH 1/2] fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences) Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 28 +++++++++++++++++++++++----- src/sat/sat_solver.h | 6 ++++-- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index eec94879a..37fb971fd 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3227,20 +3227,32 @@ namespace sat { SASSERT(!inconsistent()); unsigned sz = m_trail.size(); for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) { - extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq); + if (!extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)) { + for (i = 0; i < sz && lvl(m_trail[i]) <= 1; ++i) { + VERIFY(extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)); + } + break; + } } start = sz; } - void solver::extract_assumptions(literal lit, index_set& s) { + bool solver::check_domain(literal lit, literal lit2) { + return m_antecedents.contains(lit2.var()); + } + + bool solver::extract_assumptions(literal lit, index_set& s) { justification js = m_justification[lit.var()]; switch (js.get_kind()) { case justification::NONE: break; case justification::BINARY: + if (!check_domain(lit, js.get_literal())) return false; s |= m_antecedents.find(js.get_literal().var()); break; case justification::TERNARY: + if (!check_domain(lit, js.get_literal1())) return false; + if (!check_domain(lit, js.get_literal2())) return false; s |= m_antecedents.find(js.get_literal1().var()); s |= m_antecedents.find(js.get_literal2().var()); break; @@ -3248,6 +3260,7 @@ namespace sat { clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset())); for (unsigned i = 0; i < c.size(); ++i) { if (c[i] != lit) { + if (!check_domain(lit, c[i])) return false; s |= m_antecedents.find(c[i].var()); } } @@ -3258,6 +3271,7 @@ namespace sat { literal_vector::iterator it = m_ext_antecedents.begin(); literal_vector::iterator end = m_ext_antecedents.end(); for (; it != end; ++it) { + if (!check_domain(lit, *it)) return false; s |= m_antecedents.find(it->var()); } break; @@ -3267,6 +3281,7 @@ namespace sat { break; } TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";); + return true; } std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const { @@ -3279,17 +3294,19 @@ namespace sat { } - void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { + bool solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { index_set s; if (m_antecedents.contains(lit.var())) { - return; + return true; } if (assumptions.contains(lit)) { s.insert(lit.index()); } else { + if (!extract_assumptions(lit, s)) { + return false; + } add_assumption(lit); - extract_assumptions(lit, s); } m_antecedents.insert(lit.var(), s); if (unfixed.contains(lit.var())) { @@ -3302,6 +3319,7 @@ namespace sat { unfixed.remove(lit.var()); conseq.push_back(cons); } + return true; } void solver::asymmetric_branching() { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index f28d0aa5b..dcf7e2acb 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -439,7 +439,9 @@ namespace sat { u_map m_antecedents; vector m_binary_clause_graph; - void extract_assumptions(literal lit, index_set& s); + bool extract_assumptions(literal lit, index_set& s); + + bool check_domain(literal lit, literal lit2); std::ostream& display_index_set(std::ostream& out, index_set const& s) const; @@ -451,7 +453,7 @@ namespace sat { void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); - void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); + bool extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars); From 0aa912371b3ea5ca92aa10b34b7fb25bc6372536 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Jan 2017 14:19:24 -0800 Subject: [PATCH 2/2] Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 15 +++++++++++---- src/opt/opt_solver.cpp | 7 +------ src/opt/opt_solver.h | 1 - src/opt/wmax.cpp | 1 + src/smt/smt_context.cpp | 1 + 5 files changed, 14 insertions(+), 11 deletions(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 97b6a5293..f93291599 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -55,15 +55,18 @@ namespace opt { void maxsmt_solver_base::commit_assignment() { expr_ref tmp(m); - rational k(0); + rational k(0), cost(0); for (unsigned i = 0; i < m_soft.size(); ++i) { if (get_assignment(i)) { k += m_weights[i]; } + else { + cost += m_weights[i]; + } } pb_util pb(m); tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k); - TRACE("opt", tout << tmp << "\n";); + TRACE("opt", tout << "cost: " << cost << "\n" << tmp << "\n";); s().assert_expr(tmp); } @@ -140,7 +143,9 @@ namespace opt { m_wth = s.ensure_wmax_theory(); } maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() { - //m_wth->reset_local(); + if (m_wth) { + m_wth->reset_local(); + } } smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; } @@ -226,7 +231,9 @@ namespace opt { m_msolver = 0; symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); - TRACE("opt", tout << "maxsmt\n";); + TRACE("opt", tout << "maxsmt\n"; + s().display(tout); tout << "\n"; + ); if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 42129be70..351141a3f 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -327,12 +327,7 @@ namespace opt { SASSERT(idx < get_num_assertions()); return m_context.get_formulas()[idx]; } - - std::ostream& opt_solver::display(std::ostream & out) const { - m_context.display(out); - return out; - } - + smt::theory_var opt_solver::add_objective(app* term) { smt::theory_var v = get_optimizer().add_objective(term); m_objective_vars.push_back(v); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index cdaad3cf2..27168e2ca 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -104,7 +104,6 @@ namespace opt { virtual void set_progress_callback(progress_callback * callback); virtual unsigned get_num_assertions() const; virtual expr * get_assertion(unsigned idx) const; - virtual std::ostream& display(std::ostream & out) const; virtual ast_manager& get_manager() const { return m; } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 690e2000b..9708bdc8f 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -64,6 +64,7 @@ namespace opt { bool was_sat = false; expr_ref_vector asms(m); vector cores; + obj_map::iterator it = soft.begin(), end = soft.end(); for (; it != end; ++it) { expr* c = assert_weighted(wth(), it->m_key, it->m_value); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ea97d1a64..c7aecca88 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1795,6 +1795,7 @@ namespace smt { void context::set_conflict(b_justification js, literal not_l) { if (!inconsistent()) { + TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); ); m_conflict = js; m_not_l = not_l; }