From da34de340d582784e0068eb6f287faa56b74a243 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 15 Jul 2017 20:25:13 +0100 Subject: [PATCH] Fixed bug in sat model converter. Fixes #1148. --- src/sat/sat_model_converter.cpp | 27 +++++++++++++++++++++++---- src/sat/sat_model_converter.h | 7 ++++--- src/sat/sat_solver.cpp | 17 +++++++++-------- src/sat/sat_solver/inc_sat_solver.cpp | 18 +++++++++--------- 4 files changed, 45 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 8901c276f..525d084dc 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -32,7 +32,7 @@ namespace sat { void model_converter::reset() { m_entries.finalize(); } - + void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); @@ -46,7 +46,7 @@ namespace sat { literal_vector::const_iterator it2 = it->m_clauses.begin(); literal_vector::const_iterator end2 = it->m_clauses.end(); for (; it2 != end2; ++it2) { - literal l = *it2; + literal l = *it2; if (l == null_literal) { // end of clause if (!sat) { @@ -56,6 +56,7 @@ namespace sat { sat = false; continue; } + if (sat) continue; bool sign = l.sign(); @@ -125,7 +126,7 @@ namespace sat { } return ok; } - + model_converter::entry & model_converter::mk(kind k, bool_var v) { m_entries.push_back(entry(k, v)); entry & e = m_entries.back(); @@ -218,7 +219,7 @@ namespace sat { out << *it2; } out << ")"; - } + } out << ")\n"; } @@ -237,4 +238,22 @@ namespace sat { } } + unsigned model_converter::max_var(unsigned min) const { + unsigned result = min; + vector::const_iterator it = m_entries.begin(); + vector::const_iterator end = m_entries.end(); + for (; it != end; ++it) { + literal_vector::const_iterator lvit = it->m_clauses.begin(); + literal_vector::const_iterator lvend = it->m_clauses.end(); + for (; lvit != lvend; ++lvit) { + literal l = *lvit; + if (l != null_literal) { + if (l.var() > result) + result = l.var(); + } + } + } + return result; + } + }; diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index b89e6e784..eb2237707 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -26,7 +26,7 @@ namespace sat { \brief Stores eliminated variables and Blocked clauses. It uses these clauses to extend/patch the model produced for the simplified CNF formula. - + This information may also be used to support incremental solving. If new clauses are asserted into the SAT engine, then we can restore the state by re-asserting all clauses in the model @@ -50,7 +50,7 @@ namespace sat { m_kind(src.m_kind), m_clauses(src.m_clauses) { } - bool_var var() const { return m_var; } + bool_var var() const { return m_var; } kind get_kind() const { return static_cast(m_kind); } }; private: @@ -74,8 +74,9 @@ namespace sat { void copy(model_converter const & src); void collect_vars(bool_var_set & s) const; + unsigned max_var(unsigned min) const; }; - + }; #endif diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7f2b75830..fbfa0ec6b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2628,7 +2628,7 @@ namespace sat { unsigned j = 0; for (unsigned i = 0; i < clauses.size(); ++i) { clause & c = *(clauses[i]); - if (c.contains(lit)) { + if (c.contains(lit) || c.contains(~lit)) { detach_clause(c); del_clause(c); } @@ -2684,6 +2684,7 @@ namespace sat { w = max_var(m_clauses, w); w = max_var(true, w); w = max_var(false, w); + v = m_mc.max_var(w); for (unsigned i = 0; i < m_trail.size(); ++i) { if (m_trail[i].var() > w) w = m_trail[i].var(); } @@ -3150,9 +3151,9 @@ namespace sat { } } } - + // Algorithm 7: Corebased Algorithm with Chunking - + static void back_remove(sat::literal_vector& lits, sat::literal l) { for (unsigned i = lits.size(); i > 0; ) { --i; @@ -3176,7 +3177,7 @@ namespace sat { } } } - + static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { sat::literal_vector lambda; for (unsigned i = 0; i < vars.size(); i++) { @@ -3375,7 +3376,7 @@ namespace sat { if (check_inconsistent()) return l_false; unsigned num_iterations = 0; - extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); + extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); update_unfixed_literals(unfixed_lits, unfixed_vars); while (!unfixed_lits.empty()) { if (scope_lvl() > 1) { @@ -3390,7 +3391,7 @@ namespace sat { unsigned num_assigned = 0; lbool is_sat = l_true; for (; it != end; ++it) { - literal lit = *it; + literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; if (lvl(lit) <= 1 && value(lit) == l_true) { @@ -3445,8 +3446,8 @@ namespace sat { << " iterations: " << num_iterations << " variables: " << unfixed_lits.size() << " fixed: " << conseq.size() - << " status: " << is_sat - << " pre-assigned: " << num_fixed + << " status: " << is_sat + << " pre-assigned: " << num_fixed << " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size() << ")\n";); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b6904ef02..baac9f37b 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -131,7 +131,7 @@ public: } bool is_literal(expr* e) const { - return + return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); } @@ -153,7 +153,7 @@ public: asm2fml.insert(assumptions[i], assumptions[i]); } } - + TRACE("sat", tout << _assumptions << "\n";); dep2asm_t dep2asm; m_model = 0; @@ -163,7 +163,7 @@ public: if (r != l_true) return r; r = m_solver.check(m_asms.size(), m_asms.c_ptr()); - + switch (r) { case l_true: if (sz > 0) { @@ -280,14 +280,14 @@ public: return r; } - // build map from bound variables to + // build map from bound variables to // the consequences that cover them. u_map bool_var2conseq; for (unsigned i = 0; i < lconseq.size(); ++i) { TRACE("sat", tout << lconseq[i] << "\n";); bool_var2conseq.insert(lconseq[i][0].var(), i); } - + // extract original fixed variables u_map asm2dep; extract_asm2dep(dep2asm, asm2dep); @@ -441,7 +441,7 @@ private: lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) { for (unsigned i = 0; i < vars.size(); ++i) { - internalize_var(vars[i], bvars); + internalize_var(vars[i], bvars); } return l_true; } @@ -453,7 +453,7 @@ private: bool internalized = false; if (is_uninterp_const(v) && m.is_bool(v)) { sat::bool_var b = m_map.to_bool_var(v); - + if (b != sat::null_bool_var) { bvars.push_back(b); internalized = true; @@ -479,7 +479,7 @@ private: else if (is_uninterp_const(v) && bvutil.is_bv(v)) { // variable does not occur in assertions, so is unconstrained. } - CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";); + CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";); return internalized; } @@ -506,7 +506,7 @@ private: } expr_ref val(m); expr_ref_vector conj(m); - internalize_value(value, v, val); + internalize_value(value, v, val); while (!premises.empty()) { expr* e = 0; VERIFY(asm2dep.find(premises.pop().index(), e));