From aeabdb4aaec7672f676e7d46f49c12a5315bd06e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2017 14:06:35 -0800 Subject: [PATCH 1/2] add checks for flipping externals / assumptions in model converter, fix scc converter bug Signed-off-by: Nikolaj Bjorner --- src/sat/sat_elim_eqs.cpp | 2 +- src/sat/sat_model_converter.cpp | 26 ++++++++++++++++++++++++-- src/sat/sat_model_converter.h | 2 ++ src/sat/sat_solver.cpp | 6 +++--- src/sat/sat_solver.h | 2 +- 5 files changed, 31 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index d0166b64e..6b8d4cba7 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -182,7 +182,7 @@ namespace sat { literal l(v, false); literal r = roots[v]; SASSERT(v != r.var()); - if (m_solver.is_external(v) && !m_solver.set_root(l, r)) { + if (m_solver.is_external(v) || !m_solver.set_root(l, r)) { // cannot really eliminate v, since we have to notify extension of future assignments m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index d46063455..05c89fba7 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -39,6 +39,22 @@ namespace sat { return *this; } + bool model_converter::legal_to_flip(bool_var v) const { + // std::cout << "check " << v << " " << m_solver << "\n"; + if (m_solver && m_solver->is_assumption(v)) { + std::cout << "flipping assumption v" << v << "\n"; + UNREACHABLE(); + throw solver_exception("flipping assumption"); + } + if (m_solver && m_solver->is_external(v)) { + std::cout << "flipping external v" << v << "\n"; + UNREACHABLE(); + throw solver_exception("flipping external"); + } + return !m_solver || !m_solver->is_assumption(v); + } + + void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const { SASSERT(!stack.empty()); unsigned sz = stack.size(); @@ -50,6 +66,7 @@ namespace sat { sat = value_at(c[j], m) == l_true; } if (!sat) { + VERIFY(legal_to_flip(lit.var())); m[lit.var()] = lit.sign() ? l_false : l_true; } } @@ -59,7 +76,7 @@ namespace sat { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); bool first = true; - //VERIFY(!m_solver || m_solver->check_clauses(m)); + //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef); @@ -69,11 +86,13 @@ namespace sat { bool var_sign = false; unsigned index = 0; literal_vector clause; + VERIFY(legal_to_flip(it->var())); for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause elim_stack* st = it->m_elim_stack[index]; - if (!sat) { + if (!sat) { + VERIFY(legal_to_flip(it->var())); m[it->var()] = var_sign ? l_false : l_true; } if (st) { @@ -101,6 +120,7 @@ namespace sat { if (value_at(l, m) == l_true) sat = true; else if (!sat && v != it->var() && m[v] == l_undef) { + VERIFY(legal_to_flip(v)); // clause can be satisfied by assigning v. m[v] = sign ? l_false : l_true; // if (first) std::cout << "set: " << l << "\n"; @@ -170,6 +190,7 @@ namespace sat { entry & e = m_entries.back(); SASSERT(e.var() == v); SASSERT(e.get_kind() == k); + VERIFY(legal_to_flip(v)); return e; } @@ -213,6 +234,7 @@ namespace sat { for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims)); + for (auto const& s : elims) VERIFY(legal_to_flip(s.second.var())); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 8f8b1a41b..28f23c063 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -92,6 +92,8 @@ namespace sat { std::ostream& display(std::ostream & out, entry const& entry) const; + bool legal_to_flip(bool_var v) const; + public: model_converter(); ~model_converter(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0e51c3332..db6f3d356 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -61,7 +61,7 @@ namespace sat { m_num_checkpoints = 0; m_simplifications = 0; m_cuber = nullptr; - m_mc.set_solver(nullptr); + m_mc.set_solver(this); } solver::~solver() { @@ -1544,7 +1544,7 @@ namespace sat { if (m_config.m_drat) m_drat.check_model(m_model); - m_mc.set_solver(nullptr); + // m_mc.set_solver(nullptr); m_mc(m_model); @@ -1601,7 +1601,7 @@ namespace sat { for (literal l : m_assumptions) { if (value_at(l, m) != l_true) { VERIFY(is_external(l.var())); - IF_VERBOSE(0, verbose_stream() << l << " does not model check " << value_at(l, m) << "\n";); + IF_VERBOSE(0, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";); TRACE("sat", tout << l << " does not model check\n"; tout << "trail: " << m_trail << "\n"; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index ec6746763..8f70086ba 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -353,6 +353,7 @@ namespace sat { void set_model(model const& mdl); char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } bool check_clauses(model const& m) const; + bool is_assumption(bool_var v) const; literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level); @@ -389,7 +390,6 @@ namespace sat { void reinit_assumptions(); bool tracking_assumptions() const; bool is_assumption(literal l) const; - bool is_assumption(bool_var v) const; void simplify_problem(); void mk_model(); bool check_model(model const & m) const; From d1854ab4d263abde358699839d65ce44285342ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2017 15:24:40 -0800 Subject: [PATCH 2/2] fix assertion in model converter for incremental mode Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_simplifier.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 05c89fba7..fac4cface 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -46,7 +46,7 @@ namespace sat { UNREACHABLE(); throw solver_exception("flipping assumption"); } - if (m_solver && m_solver->is_external(v)) { + if (m_solver && m_solver->is_external(v) && m_solver->is_incremental()) { std::cout << "flipping external v" << v << "\n"; UNREACHABLE(); throw solver_exception("flipping external"); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 6d578b4f9..c101e3a29 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -970,11 +970,12 @@ namespace sat { } void insert(literal l) { + VERIFY(process_var(l.var())); m_queue.insert(l); } bool process_var(bool_var v) { - return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); + return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); } void operator()() {