From f94a475da386f2dd84a4711b03526648870644b6 Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Fri, 17 Nov 2023 22:48:04 +0530 Subject: [PATCH] Qel fixes (#6999) * dont use qel for sequences. fix #6950 * handle negation of read-write. fix #6991 * handle neg-peq terms produced by distinct. fix #6889 * dbg print --- src/qe/mbp/mbp_arrays_tg.cpp | 46 +++++++++++++++++++++-------------- src/qe/mbp/mbp_basic_tg.cpp | 1 + src/qe/mbp/mbp_term_graph.cpp | 14 +++++++++-- src/qe/qe_mbp.cpp | 13 +++++++++- 4 files changed, 53 insertions(+), 21 deletions(-) diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp index d3ed1a9eb..98224e8df 100644 --- a/src/qe/mbp/mbp_arrays_tg.cpp +++ b/src/qe/mbp/mbp_arrays_tg.cpp @@ -77,8 +77,7 @@ struct mbp_array_tg::impl { } // Returns true if e has a subterm store(v) where v is a variable to be - // eliminated. Assumes that has_store has already been called for - // subexpressions of e + // eliminated. Recurses on subexpressions of ee bool has_stores(expr *e) { if (m_has_stores.is_marked(e)) return true; if (!is_app(e)) return false; @@ -86,8 +85,13 @@ struct mbp_array_tg::impl { m_has_stores.mark(e, true); return true; } - for (auto c : *(to_app(e))) { - if (m_has_stores.is_marked(c)) { + if (any_of(*(to_app(e)), [&](expr* c) { return m_has_stores.is_marked(c); })) { + m_has_stores.mark(e, true); + return true; + } + //recurse + for(auto c : *(to_app(e))) { + if (has_stores(c)) { m_has_stores.mark(e, true); return true; } @@ -110,7 +114,10 @@ struct mbp_array_tg::impl { return m_array_util.is_array(lhs) && m_array_util.is_array(rhs) && (has_var(lhs) || has_var(rhs)); } - + bool is_neg_peq(expr *e) { + expr* ne; + return m.is_not(e, ne) && is_implicit_peq(ne); + } void mark_seen(expr *t) { m_seen.mark(t); } bool is_seen(expr *t) { return m_seen.is_marked(t); } void mark_seen(expr *t1, expr *t2) { m_seenp.insert(expr_pair(t1, t2)); } @@ -151,7 +158,7 @@ struct mbp_array_tg::impl { void elimwreq(peq p, bool is_neg) { SASSERT(is_arr_write(p.lhs())); TRACE("mbp_tg", - tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m);); + tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m) << " is neg: " << is_neg;); vector indices; expr *j = to_app(p.lhs())->get_arg(1); expr *elem = to_app(p.lhs())->get_arg(2); @@ -178,7 +185,7 @@ struct mbp_array_tg::impl { expr_ref p_new_expr(m); p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq(); m_tg.add_lit(p_new_expr); - m_tg.add_eq(p_new_expr, p.mk_peq()); + m_tg.add_eq(p_new.mk_peq(), p.mk_peq()); return; } for (expr *d : deq) { m_tg.add_deq(j, d); } @@ -193,14 +200,13 @@ struct mbp_array_tg::impl { m_tg.add_eq(rd, elem); m_tg.add_eq(p.mk_peq(), p_new.mk_peq()); } else { - SASSERT(m_mdl.is_false(p_new.mk_peq()) || - !m_mdl.are_equal(rd, elem)); - if (m_mdl.is_false(p_new.mk_peq())) { + expr_ref rd_eq(m.mk_eq(rd, elem), m); + if (m_mdl.is_false(rd_eq)) { m_tg.add_deq(rd, elem); } + else { expr_ref npeq(mk_not(p_new.mk_peq()), m); m_tg.add_lit(npeq); m_tg.add_eq(p.mk_peq(), p_new.mk_peq()); } - if (!m_mdl.are_equal(rd, elem)) { m_tg.add_deq(rd, elem); } } } @@ -281,13 +287,16 @@ struct mbp_array_tg::impl { if (m_seen.is_marked(term)) continue; if (m_tg.is_cgr(term)) continue; TRACE("mbp_tg", tout << "processing " << expr_ref(term, m);); - if (is_implicit_peq(term)) { + if (is_implicit_peq(term) || is_neg_peq(term)) { // rewrite array eq as peq mark_seen(term); progress = true; - e = mk_wr_peq(to_app(term)->get_arg(0), - to_app(term)->get_arg(1)) + nt = term; + bool is_not = m.is_not(term, nt); + e = mk_wr_peq(to_app(nt)->get_arg(0), + to_app(nt)->get_arg(1)) .mk_peq(); + e = is_not ? m.mk_not(e) : e; m_tg.add_lit(e); m_tg.add_eq(term, e); continue; @@ -303,9 +312,10 @@ struct mbp_array_tg::impl { elimwreq(p, is_neg); continue; } - if (!m_array_util.is_store(p.lhs()) && has_var(p.lhs())) { + if (!m_array_util.is_store(p.lhs()) && has_var(p.lhs()) && !is_neg) { // TODO: don't apply this rule if vars in p.lhs() also // appear in p.rhs() + mark_seen(p.lhs()); mark_seen(nt); mark_seen(term); @@ -314,7 +324,7 @@ struct mbp_array_tg::impl { continue; } // eliminate eq when the variable is on the rhs - if (!m_array_util.is_store(p.rhs()) && has_var(p.rhs())) { + if (!m_array_util.is_store(p.rhs()) && has_var(p.rhs()) && !is_neg) { mark_seen(p.rhs()); p.get_diff_indices(indices); peq p_new = mk_wr_peq(p.rhs(), p.lhs(), indices); @@ -325,10 +335,10 @@ struct mbp_array_tg::impl { continue; } } - if (m_use_mdl && is_rd_wr(term)) { + if (m_use_mdl && is_rd_wr(nt)) { mark_seen(term); progress = true; - elimrdwr(term); + elimrdwr(nt); continue; } } diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp index fa657d990..ce5e99eb1 100644 --- a/src/qe/mbp/mbp_basic_tg.cpp +++ b/src/qe/mbp/mbp_basic_tg.cpp @@ -69,6 +69,7 @@ struct mbp_basic_tg::impl { m_tg.get_terms(terms, false); for (expr *term : terms) { if (is_seen(term)) continue; + TRACE("mbp_tg", tout << "Processing " << expr_ref(term, m) << "\n";); if (m.is_ite(term, c, th, el) && should_split(c)) { mark_seen(term); progress = true; diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 190acecdf..e8ba29dfd 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -121,6 +121,8 @@ class term { unsigned m_is_peq : 1; // caches whether m_expr is the child of not unsigned m_is_neq_child : 1; + // caches whether m_expr is peq and the child of not + unsigned m_is_npeq_child : 1; // -- the term is a compound term can be rewritten to be ground or it is a // ground constant @@ -170,6 +172,7 @@ class term { : m_expr(v), m_root(this), m_repr(nullptr), m_next(this), m_mark(false), m_mark2(false), m_interpreted(false), m_is_eq(m_expr.get_manager().is_eq(m_expr)), m_is_peq(false), + m_is_npeq_child(false), m_is_neq_child(false), m_cgr(0), m_gr(0) { m_is_neq = m_expr.get_manager().is_not(m_expr) && m_expr.get_manager().is_eq(to_app(m_expr)->get_arg(0)); @@ -244,7 +247,9 @@ class term { bool is_eq_or_peq() const { return m_is_eq || m_is_peq; } bool is_neq() const { return m_is_neq; } void set_neq_child() { m_is_neq_child = true; } + void set_npeq_child() { m_is_npeq_child = true; } bool is_neq_child() const { return m_is_neq_child; } + bool is_npeq_child() const { return m_is_npeq_child; } unsigned get_decl_id() const { return is_app(m_expr) ? to_app(m_expr)->get_decl()->get_id() : m_expr->get_id(); @@ -491,11 +496,11 @@ void term_graph::get_terms(expr_ref_vector &res, bool exclude_cground) { std::function fil = nullptr; if (exclude_cground) { fil = [](term *t) { - return !t->is_neq_child() && (t->is_eq_or_peq() || !t->is_cgr()); + return !t->is_neq_child() && !t->is_npeq_child() && (t->is_eq_or_peq() || !t->is_cgr()); }; } else { - fil = [](term *t) { return !t->is_neq_child(); }; + fil = [](term *t) { return !t->is_neq_child() && !t->is_npeq_child(); }; } auto terms = m_terms.filter_pure(fil); res.resize(terms.size()); @@ -574,6 +579,11 @@ term *term_graph::internalize_term(expr *t) { } merge_flush(); SASSERT(res); + if (m.is_not(t) && is_app(to_app(t)->get_arg(0)) && is_partial_eq(to_app(to_app(t)->get_arg(0)))) { + term* p = get_term(to_app(t)->get_arg(0)); + SASSERT(p); + p->set_npeq_child(); + } return res; } diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index d53684100..861c841a9 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -29,6 +29,7 @@ Revision History: #include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/scoped_proof.h" +#include "ast/seq_decl_plugin.h" #include "util/gparams.h" #include "model/model_evaluator.h" #include "model/model_pp.h" @@ -405,8 +406,18 @@ public: return true; } + bool has_unsupported_th(const expr_ref_vector fmls) { + seq_util seq(m); + expr_ref e(m); + e = mk_and(fmls); + return any_of(subterms::all(e), [&](expr* c) { return seq.is_char(c) || seq.is_seq(c); }); + } void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) { - if (m_use_qel) { + //don't use mbp_qel on some theories where model evaluation is + //incomplete This is not a limitation of qel. Fix this either by + //making mbp choices less dependent on the model evaluation methods + //or fix theory rewriters to make terms evalution complete + if (m_use_qel && !has_unsupported_th(fmls)) { bool dsub = m_dont_sub; m_dont_sub = !force_elim; expr_ref fml(m);