From 0f03ef4ab08618fca0df2fb4c3436c618c00ddff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Jan 2022 14:38:11 +0100 Subject: [PATCH] for Clemens: ensure fixed values are propagated after registration Also allow to register expressions that the rewriter changes to ensure they get picked up. --- src/smt/smt_context.cpp | 24 +++++++ src/smt/smt_context.h | 2 + src/smt/smt_theory.h | 6 ++ src/smt/theory_bv.cpp | 15 +++++ src/smt/theory_bv.h | 1 + src/smt/theory_user_propagator.cpp | 105 ++++++++++++++++++----------- src/smt/theory_user_propagator.h | 21 ++++-- 7 files changed, 129 insertions(+), 45 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 48eb23b4f..b6843c954 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2906,6 +2906,30 @@ namespace smt { m_user_propagator->new_fixed_eh(v, val, sz, explain); } + bool context::is_fixed(enode* n, expr_ref& val, literal_vector& explain) { + if (m.is_bool(n->get_expr())) { + literal lit = get_literal(n->get_expr()); + switch (get_assignment(lit)) { + case l_true: + val = m.mk_true(); explain.push_back(lit); return true; + case l_false: + val = m.mk_false(); explain.push_back(~lit); return true; + default: + return false; + } + } + theory_var_list * l = n->get_th_var_list(); + while (l) { + theory_id tid = l->get_id(); + auto* p = m_theories.get_plugin(tid); + if (p && p->is_fixed(l->get_var(), val, explain)) + return true; + l = l->get_next(); + } + return false; + } + + void context::push() { pop_to_base_lvl(); setup_context(false); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 4a764e975..fd6c12482 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1747,6 +1747,8 @@ namespace smt { assign_fixed(n, val, 1, &explain); } + bool is_fixed(enode* n, expr_ref& val, literal_vector& explain); + void display(std::ostream & out) const; void display_unsat_core(std::ostream & out) const; diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 500c47f5e..31e74af13 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -615,6 +615,12 @@ namespace smt { bool is_relevant_and_shared(enode * n) const; bool assume_eq(enode * n1, enode * n2); + + + /** + * \brief theory plugin for fixed values. + */ + virtual bool is_fixed(theory_var v, expr_ref& val, literal_vector & explain) { return false; } }; }; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index c714b17f3..73b208197 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -519,6 +519,21 @@ namespace smt { } } + bool theory_bv::is_fixed(theory_var v, expr_ref& val, literal_vector& lits) { + numeral r; + enode* n = get_enode(v); + if (!get_fixed_value(v, r)) + return false; + val = m_util.mk_numeral(r, n->get_sort()); + for (literal b : m_bits[v]) { + if (ctx.get_assignment(b) == l_false) + b.neg(); + lits.push_back(b); + } + return true; + } + + bool theory_bv::get_fixed_value(theory_var v, numeral & result) const { result.reset(); unsigned i = 0; diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 931e3041a..eecc084e1 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -282,6 +282,7 @@ namespace smt { void collect_statistics(::statistics & st) const override; bool get_fixed_value(app* x, numeral & result) const; + bool is_fixed(theory_var v, expr_ref& val, literal_vector& explain) override; bool check_assignment(theory_var v); bool check_invariant(); diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 48e57f5fd..eca5e6e13 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -40,11 +40,24 @@ void theory_user_propagator::force_push() { unsigned theory_user_propagator::add_expr(expr* e) { force_push(); + expr_ref r(m); + ctx.get_rewriter()(e, r); + if (r != e) { + r = m.mk_fresh_const("aux-expr", e->get_sort()); + expr_ref eq(m.mk_eq(r, e), m); + ctx.assert_expr(eq); + ctx.internalize_assertions(); + e = r; + ctx.mark_as_relevant(eq); + } enode* n = ensure_enode(e); if (is_attached_to_var(n)) return n->get_th_var(get_id()); theory_var v = mk_var(n); ctx.attach_th_var(n, this, v); + literal_vector explain; + if (ctx.is_fixed(n, r, explain)) + m_prop.push_back(prop_info(explain, v, r)); return v; } @@ -118,54 +131,66 @@ bool theory_user_propagator::can_propagate() { return m_qhead < m_prop.size(); } +void theory_user_propagator::propagate_consequence(prop_info const& prop) { + justification* js; + m_lits.reset(); + m_eqs.reset(); + for (unsigned id : prop.m_ids) + m_lits.append(m_id2justification[id]); + for (auto const& p : prop.m_eqs) + m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second))); + DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());); + 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);); + + TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n"); + + if (m.is_false(prop.m_conseq)) { + js = ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), 0, nullptr)); + ctx.set_conflict(js); + } + else { + for (auto& lit : m_lits) + lit.neg(); + for (auto const& [a,b] : m_eqs) + m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false)); + + literal lit; + if (has_quantifiers(prop.m_conseq)) { + expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m); + expr_ref eq(m.mk_eq(fn, prop.m_conseq), m); + ctx.assert_expr(eq); + ctx.internalize_assertions(); + lit = mk_literal(fn); + } + else + lit = mk_literal(prop.m_conseq); + ctx.mark_as_relevant(lit); + m_lits.push_back(lit); + ctx.mk_th_lemma(get_id(), m_lits); + TRACE("user_propagate", ctx.display(tout);); + } +} + +void theory_user_propagator::propagate_new_fixed(prop_info const& prop) { + new_fixed_eh(prop.m_var, prop.m_conseq, prop.m_lits.size(), prop.m_lits.data()); +} + + void theory_user_propagator::propagate() { TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n"); if (m_qhead == m_prop.size()) return; force_push(); unsigned qhead = m_qhead; - justification* js; while (qhead < m_prop.size() && !ctx.inconsistent()) { auto const& prop = m_prop[qhead]; - m_lits.reset(); - m_eqs.reset(); - for (unsigned id : prop.m_ids) - m_lits.append(m_id2justification[id]); - for (auto const& p : prop.m_eqs) - m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second))); - DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());); - 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);); - - TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n"); - - if (m.is_false(prop.m_conseq)) { - js = ctx.mk_justification( - ext_theory_conflict_justification( - get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), 0, nullptr)); - ctx.set_conflict(js); - } - else { - for (auto& lit : m_lits) - lit.neg(); - for (auto const& [a,b] : m_eqs) - m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false)); - - literal lit; - if (has_quantifiers(prop.m_conseq)) { - expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m); - expr_ref eq(m.mk_eq(fn, prop.m_conseq), m); - ctx.assert_expr(eq); - ctx.internalize_assertions(); - lit = mk_literal(fn); - } - else - lit = mk_literal(prop.m_conseq); - ctx.mark_as_relevant(lit); - m_lits.push_back(lit); - ctx.mk_th_lemma(get_id(), m_lits); - TRACE("user_propagate", ctx.display(tout);); - } + if (prop.m_var == null_theory_var) + propagate_consequence(prop); + else + propagate_new_fixed(prop); ++m_stats.m_num_propagations; ++qhead; } diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 0589a87a5..f1e558256 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -30,16 +30,24 @@ namespace smt { class theory_user_propagator : public theory, public user_propagator::callback { struct prop_info { - unsigned_vector m_ids; - expr_ref m_conseq; + unsigned_vector m_ids; + expr_ref m_conseq; svector> m_eqs; - prop_info(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c): + literal_vector m_lits; + theory_var m_var = null_theory_var; + prop_info(unsigned num_fixed, unsigned const* fixed_ids, + unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c): m_ids(num_fixed, fixed_ids), - m_conseq(c) - { + m_conseq(c) { for (unsigned i = 0; i < num_eqs; ++i) m_eqs.push_back(std::make_pair(eq_lhs[i], eq_rhs[i])); } + + prop_info(literal_vector const& lits, theory_var v, expr_ref const& val): + m_conseq(val), + m_lits(lits), + m_var(v) {} + }; struct stats { @@ -71,6 +79,9 @@ namespace smt { void force_push(); + void propagate_consequence(prop_info const& prop); + void propagate_new_fixed(prop_info const& prop); + public: theory_user_propagator(context& ctx);