Skip to content

Commit

Permalink
Qel fixes (#6999)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@hgvk94
hgvk94 committed Nov 17, 2023
1 parent 1b6c7d6 commit f94a475
Show file tree
Hide file tree
Showing 4 changed files with 53 additions and 21 deletions.
46 changes: 28 additions & 18 deletions src/qe/mbp/mbp_arrays_tg.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,17 +77,21 @@ 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;
if (m_array_util.is_store(e) && is_var(to_app(e)->get_arg(0))) {
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;
}
Expand All @@ -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)); }
Expand Down Expand Up @@ -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<expr_ref_vector> indices;
expr *j = to_app(p.lhs())->get_arg(1);
expr *elem = to_app(p.lhs())->get_arg(2);
Expand All @@ -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); }
Expand All @@ -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); }
}
}

Expand Down Expand Up @@ -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;
Expand All @@ -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);
Expand All @@ -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);
Expand All @@ -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;
}
}
Expand Down
1 change: 1 addition & 0 deletions src/qe/mbp/mbp_basic_tg.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
14 changes: 12 additions & 2 deletions src/qe/mbp/mbp_term_graph.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -491,11 +496,11 @@ void term_graph::get_terms(expr_ref_vector &res, bool exclude_cground) {
std::function<bool(term *)> 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());
Expand Down Expand Up @@ -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;
}

Expand Down
13 changes: 12 additions & 1 deletion src/qe/qe_mbp.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -405,8 +406,18 @@ class mbproj::impl {
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);
Expand Down

0 comments on commit f94a475

Please sign in to comment.