From e9a4a9a3909b0d2307fbcf16dcf028fb3da65232 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Sep 2021 09:23:59 -0700 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/sat/smt/user_solver.cpp | 16 +++++++++++++++- src/sat/smt/user_solver.h | 2 ++ src/smt/user_propagator.cpp | 1 + 3 files changed, 18 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 8190e3bf7..e9d8a54cb 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -44,6 +44,7 @@ namespace user { unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) { m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); + DEBUG_CODE(validate_propagation();); } sat::check_result solver::check() { @@ -95,7 +96,7 @@ namespace user { ctx.push(value_trail(m_qhead)); unsigned np = m_stats.m_num_propagations; for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) { - auto const& prop = m_prop[m_qhead]; + auto const& prop = m_prop[m_qhead]; sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true); if (s().value(lit) != l_true) { s().assign(lit, mk_justification(m_qhead)); @@ -126,6 +127,19 @@ namespace user { ctx.add_antecedent(var2enode(p.first), var2enode(p.second)); } + /* + * All assumptions and equalities have to be true in the current scope. + * A caller could mistakingly supply some assumption that isn't set. + */ + void solver::validate_propagation() { + auto const& prop = m_prop.back(); + for (unsigned id : prop.m_ids) + for (auto lit: m_id2justification[id]) + VERIFY(s().value(lit) == l_true); + for (auto const& p : prop.m_eqs) + VERIFY(var2enode(p.first)->get_root() == var2enode(p.second)->get_root()); + } + std::ostream& solver::display(std::ostream& out) const { for (unsigned i = 0; i < get_num_vars(); ++i) out << i << ": " << mk_pp(var2expr(i), m) << "\n"; diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h index 24f4604d1..e16eb5b5e 100644 --- a/src/sat/smt/user_solver.h +++ b/src/sat/smt/user_solver.h @@ -79,6 +79,8 @@ namespace user { sat::justification mk_justification(unsigned propagation_index); + void validate_propagation(); + public: solver(euf::solver& ctx); diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp index ca99e9768..1bbb6073a 100644 --- a/src/smt/user_propagator.cpp +++ b/src/smt/user_propagator.cpp @@ -128,6 +128,7 @@ void user_propagator::propagate() { DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id));); DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true);); + if (m.is_false(prop.m_conseq)) { js = ctx.mk_justification( ext_theory_conflict_justification(