mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 14:55:25 +00:00
Code Activity

Update euf_completion.cpp

Browse source 
try out restricting scope of equalities added by instantation
This commit is contained in:
Nikolaj Bjorner 2025-08-03 14:16:33 -07:00
parent d8fafd8731
commit b9b3e0d337
1 changed files with 28 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/ast/simplifiers/euf_completion.cpp
View file

@ -268,7 +268,6 @@ namespace euf {
expr_ref r(f, m); expr_ref r(f, m);
m_rewriter(r); m_rewriter(r);
f = r.get(); f = r.get();
// verbose_stream() << r << "\n";
auto cons = m.mk_app(symbol("consequence"), 1, &f, m.mk_bool_sort()); auto cons = m.mk_app(symbol("consequence"), 1, &f, m.mk_bool_sort());
m_fmls.add(dependent_expr(m, cons, nullptr, nullptr)); m_fmls.add(dependent_expr(m, cons, nullptr, nullptr));
} }
@ -322,30 +321,38 @@ namespace euf {
add_quantifiers(y1); add_quantifiers(y1);
enode* a = mk_enode(x1); enode* a = mk_enode(x1);
enode* b = mk_enode(y1); enode* b = mk_enode(y1);
if (a->get_root() == b->get_root()) if (a->get_root() == b->get_root())
return; return;
m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d)));
m_egraph.propagate(); TRACE(euf, tout << "merge and propagate\n");
add_children(a); add_children(a);
add_children(b); add_children(b);
m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d)));
m_egraph.propagate();
m_should_propagate = true;
#if 0
auto a1 = mk_enode(x); auto a1 = mk_enode(x);
if (a1->get_root() != a->get_root()) { auto b1 = mk_enode(y);
if (a->get_root() != a1->get_root()) {
add_children(a1);;
m_egraph.merge(a, a1, nullptr); m_egraph.merge(a, a1, nullptr);
m_egraph.propagate(); m_egraph.propagate();
add_children(a1);
}
auto b1 = mk_enode(y);
if (b1->get_root() != b->get_root()) {
TRACE(euf, tout << "merge and propagate\n");
m_egraph.merge(b, b1, nullptr);
m_egraph.propagate();
add_children(b1);
} }
m_should_propagate = true; if (b->get_root() != b1->get_root()) {
if (m_side_condition_solver) add_children(b1);
m_egraph.merge(b, b1, nullptr);
m_egraph.propagate();
}
#endif
if (m_side_condition_solver && a->get_root() != b->get_root())
m_side_condition_solver->add_constraint(f, pr, d); m_side_condition_solver->add_constraint(f, pr, d);
IF_VERBOSE(1, verbose_stream() << "eq: " << mk_pp(x1, m) << " == " << mk_pp(y1, m) << "\n"); IF_VERBOSE(1, verbose_stream() << "eq: " << a->get_root_id() << " " << b->get_root_id() << " "
<< x1 << " == " << y1 << "\n");
} }
else if (m.is_not(f, f)) { else if (m.is_not(f, f)) {
enode* n = mk_enode(f); enode* n = mk_enode(f);
@ -689,7 +696,7 @@ namespace euf {
b = new (mem) binding(q, pat, max_generation, min_top, max_top); b = new (mem) binding(q, pat, max_generation, min_top, max_top);
b->init(b); b->init(b);
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
b->m_nodes[i] = _binding[i]; b->m_nodes[i] = _binding[i]->get_root();
m_bindings.insert(b); m_bindings.insert(b);
get_trail().push(insert_map<bindings, binding*>(m_bindings, b)); get_trail().push(insert_map<bindings, binding*>(m_bindings, b));
@ -754,6 +761,7 @@ namespace euf {
if (pr) if (pr)
pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), r), s.size(), s.data()); pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), r), s.size(), s.data());
m_consequences.push_back(r); m_consequences.push_back(r);
TRACE(euf_completion, tout << "new instantiation: " << r << " q: " << mk_pp(q, m) << "\n");
add_constraint(r, pr, d); add_constraint(r, pr, d);
propagate_rules(); propagate_rules();
m_egraph.propagate(); m_egraph.propagate();
@ -1022,7 +1030,7 @@ namespace euf {
} }
enode* n = m_egraph.find(f); enode* n = m_egraph.find(f);
if (!n) n = mk_enode(f);
enode* r = n->get_root(); enode* r = n->get_root();
d = m.mk_join(d, explain_eq(n, r)); d = m.mk_join(d, explain_eq(n, r));
d = m.mk_join(d, m_deps.get(r->get_id(), nullptr)); d = m.mk_join(d, m_deps.get(r->get_id(), nullptr));