mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Qel fixes (#6999)

Browse source 
* 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
This commit is contained in:
Hari Govind V K 2023-11-17 22:48:04 +05:30 • committed by GitHub
parent 1b6c7d6541
commit f94a475da3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 53 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/qe/mbp/mbp_arrays_tg.cpp
View file

@ -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<expr_ref_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;
}
}

1
src/qe/mbp/mbp_basic_tg.cpp
View file

@ -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;

14
src/qe/mbp/mbp_term_graph.cpp
View file

@ -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<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());
@ -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;
}

13
src/qe/qe_mbp.cpp
View file

@ -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);