mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

bugfix to ac-plugin

Browse source 
use list for "shared" should be indices into an array of shared expressions, not the monomial index.
This commit is contained in:
Nikolaj Bjorner 2025-07-12 17:51:19 -07:00
parent fd5455422e
commit 47a2376172
3 changed files with 31 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/ast/euf/euf_ac_plugin.cpp
View file

@ -80,12 +80,13 @@ TODOs:
namespace euf { namespace euf {
ac_plugin::ac_plugin(egraph& g, unsigned fid, unsigned op) : ac_plugin::ac_plugin(egraph& g, char const* name, unsigned fid, unsigned op) :
plugin(g), m_fid(fid), m_op(op), plugin(g), m_fid(fid), m_op(op),
m_dep_manager(get_region()), m_dep_manager(get_region()),
m_hash(*this), m_eq(*this), m_monomial_table(m_hash, m_eq) m_hash(*this), m_eq(*this), m_monomial_table(m_hash, m_eq)
{ {
g.set_th_propagates_diseqs(m_fid); g.set_th_propagates_diseqs(m_fid);
m_name = symbol(name);
} }
ac_plugin::ac_plugin(egraph& g, func_decl* f) : ac_plugin::ac_plugin(egraph& g, func_decl* f) :
@ -93,6 +94,7 @@ namespace euf {
m_dep_manager(get_region()), m_dep_manager(get_region()),
m_hash(*this), m_eq(*this), m_monomial_table(m_hash, m_eq) m_hash(*this), m_eq(*this), m_monomial_table(m_hash, m_eq)
{ {
m_name = f->get_name();
if (m_fid != null_family_id) if (m_fid != null_family_id)
g.set_th_propagates_diseqs(m_fid); g.set_th_propagates_diseqs(m_fid);
} }
@ -110,14 +112,15 @@ namespace euf {
return; return;
auto m = to_monomial(n); auto m = to_monomial(n);
auto const& ns = monomial(m); auto const& ns = monomial(m);
auto idx = m_shared.size();
for (auto arg : ns) { for (auto arg : ns) {
arg->shared.push_back(m); arg->shared.push_back(idx);
m_node_trail.push_back(arg); m_node_trail.push_back(arg);
push_undo(is_add_shared_index); push_undo(is_add_shared_index);
} }
m_shared_nodes.setx(n->get_id(), true, false); m_shared_nodes.setx(n->get_id(), true, false);
sort(monomial(m)); sort(monomial(m));
m_shared_todo.insert(m_shared.size()); m_shared_todo.insert(idx);
m_shared.push_back({ n, m, justification::axiom(get_id()) }); m_shared.push_back({ n, m, justification::axiom(get_id()) });
push_undo(is_register_shared); push_undo(is_register_shared);
} }
@ -228,12 +231,20 @@ namespace euf {
} }
std::ostream& ac_plugin::display(std::ostream& out) const { std::ostream& ac_plugin::display(std::ostream& out) const {
out << m_name << "\n";
unsigned i = 0; unsigned i = 0;
for (auto const& eq : m_eqs) { for (auto const& eq : m_eqs) {
if (eq.status != eq_status::is_dead) if (eq.status != eq_status::is_dead)
out << i << ": " << eq_pp_ll(*this, eq) << "\n"; out << i << ": " << eq_pp_ll(*this, eq) << "\n";
++i; ++i;
} }
if (!m_shared.empty())
out << "shared monomials:\n";
for (auto const& s : m_shared) {
out << g.bpp(s.n) << ": " << s.m << "\n";
}
#if 0
i = 0; i = 0;
for (auto m : m_monomials) { for (auto m : m_monomials) {
out << i << ": "; out << i << ": ";
@ -241,12 +252,13 @@ namespace euf {
out << "\n"; out << "\n";
++i; ++i;
} }
#endif
for (auto n : m_nodes) { for (auto n : m_nodes) {
if (!n) if (!n)
continue; continue;
if (n->eqs.empty() && n->shared.empty()) if (n->eqs.empty() && n->shared.empty())
continue; continue;
out << g.bpp(n->n) << " r: " << n->id() << " "; out << g.bpp(n->n) << " ";
if (!n->eqs.empty()) { if (!n->eqs.empty()) {
out << "eqs "; out << "eqs ";
for (auto l : n->eqs) for (auto l : n->eqs)
@ -266,7 +278,7 @@ namespace euf {
if (l == r) if (l == r)
return; return;
auto j = justification::equality(l, r); auto j = justification::equality(l, r);
TRACE(plugin, tout << g.bpp(l) << " == " << g.bpp(r) << " " << is_op(l) << " " << is_op(r) << "\n"); TRACE(plugin, tout << "merge: " << m_name << " " << g.bpp(l) << " == " << g.bpp(r) << " " << is_op(l) << " " << is_op(r) << "\n");
if (!is_op(l) && !is_op(r)) if (!is_op(l) && !is_op(r))
merge(mk_node(l), mk_node(r), j); merge(mk_node(l), mk_node(r), j);
init_equation(eq(to_monomial(l), to_monomial(r), j)); init_equation(eq(to_monomial(l), to_monomial(r), j));
@ -285,9 +297,7 @@ namespace euf {
void ac_plugin::init_equation(eq const& e) { void ac_plugin::init_equation(eq const& e) {
m_eqs.push_back(e); m_eqs.push_back(e);
auto& eq = m_eqs.back(); auto& eq = m_eqs.back();
TRACE(plugin, display_equation_ll(tout, e) << "\n");
deduplicate(monomial(eq.l).m_nodes, monomial(eq.r).m_nodes); deduplicate(monomial(eq.l).m_nodes, monomial(eq.r).m_nodes);
TRACE(plugin, display_equation_ll(tout << "dedup ", e) << "\n");
if (orient_equation(eq)) { if (orient_equation(eq)) {
auto& ml = monomial(eq.l); auto& ml = monomial(eq.l);
@ -326,7 +336,7 @@ namespace euf {
for (auto n : mr) for (auto n : mr)
n->root->n->unmark1(); n->root->n->unmark1();
TRACE(plugin, display_equation_ll(tout, e) << "\n"); TRACE(plugin, display_equation_ll(tout, e) << " shared: " << m_shared_todo << "\n");
m_to_simplify_todo.insert(eq_id); m_to_simplify_todo.insert(eq_id);
} }
else else
@ -427,7 +437,7 @@ namespace euf {
} }
void ac_plugin::merge(node* a, node* b, justification j) { void ac_plugin::merge(node* a, node* b, justification j) {
TRACE(plugin, tout << a << " == " << b << " num shared " << b->shared.size() << "\n"); TRACE(plugin, tout << g.bpp(a->n) << " == " << g.bpp(b->n) << " num shared " << b->shared.size() << "\n");
if (a == b) if (a == b)
return; return;
if (a->id() < b->id()) if (a->id() < b->id())
@ -482,8 +492,9 @@ namespace euf {
nodes.push_back(arg->root->n); nodes.push_back(arg->root->n);
args.push_back(arg->root->n->get_expr()); args.push_back(arg->root->n->get_expr());
} }
auto n = m.mk_app(m_fid, m_op, args.size(), args.data()); auto n = args.size() == 1 ? args[0] : m.mk_app(m_fid, m_op, args.size(), args.data());
return g.find(n) ? g.find(n) : g.mk(n, 0, nodes.size(), nodes.data()); auto r = g.find(n);
return r ? r : g.mk(n, 0, nodes.size(), nodes.data());
} }
ac_plugin::node* ac_plugin::node::mk(region& r, enode* n) { ac_plugin::node* ac_plugin::node::mk(region& r, enode* n) {
@ -728,7 +739,6 @@ namespace euf {
TRACE(plugin, tout << "forward simplify " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << "\n"); TRACE(plugin, tout << "forward simplify " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << "\n");
if (forward_subsumes(src_eq, dst_eq)) { if (forward_subsumes(src_eq, dst_eq)) {
TRACE(plugin, tout << "forward subsumed\n"); TRACE(plugin, tout << "forward subsumed\n");
set_status(dst_eq, eq_status::is_dead); set_status(dst_eq, eq_status::is_dead);
@ -738,7 +748,6 @@ namespace euf {
if (!can_be_subset(monomial(src.l), monomial(dst.r))) if (!can_be_subset(monomial(src.l), monomial(dst.r)))
return; return;
m_dst_r_counts.reset(); m_dst_r_counts.reset();
unsigned src_l_size = monomial(src.l).size(); unsigned src_l_size = monomial(src.l).size();
@ -1147,7 +1156,7 @@ namespace euf {
m_monomial_table.reset(); m_monomial_table.reset();
for (auto const& s1 : m_shared) { for (auto const& s1 : m_shared) {
shared s2; shared s2;
TRACE(plugin, tout << "shared " << m_pp(*this, monomial(s1.m)) << "\n"); TRACE(plugin, tout << "shared " << s1.m << ": " << m_pp_ll(*this, monomial(s1.m)) << "\n");
if (!m_monomial_table.find(s1.m, s2)) if (!m_monomial_table.find(s1.m, s2))
m_monomial_table.insert(s1.m, s1); m_monomial_table.insert(s1.m, s1);
else if (s2.n->get_root() != s1.n->get_root()) { else if (s2.n->get_root() != s1.n->get_root()) {
@ -1162,23 +1171,23 @@ namespace euf {
auto old_m = s.m; auto old_m = s.m;
auto old_n = monomial(old_m).m_src; auto old_n = monomial(old_m).m_src;
ptr_vector<node> m1(monomial(old_m).m_nodes); ptr_vector<node> m1(monomial(old_m).m_nodes);
TRACE(plugin, tout << "simplify " << g.bpp(old_n) << ": " << m_pp(*this, monomial(old_m)) << "\n"); TRACE(plugin, tout << "simplify shared: " << g.bpp(old_n) << ": " << m_pp_ll(*this, monomial(old_m)) << "\n");
if (!reduce(m1, j)) if (!reduce(m1, j))
return; return;
auto new_n = from_monomial(m1); auto new_n = from_monomial(m1);
auto new_m = to_monomial(new_n, m1); auto new_m = to_monomial(new_n, m1);
// update shared occurrences for members of the new monomial that are not already in the old monomial. // update shared occurrences for members of the new monomial that are not already in the old monomial.
for (auto n : monomial(old_m)) for (auto n : monomial(old_m))
n->root->n->mark1(); n->root->n->mark1();
for (auto n : m1) for (auto n : m1) {
if (!n->root->n->is_marked1()) { if (!n->root->n->is_marked1()) {
n->root->shared.push_back(idx); n->root->shared.push_back(idx);
m_shared_todo.insert(idx); m_shared_todo.insert(idx);
m_node_trail.push_back(n->root); m_node_trail.push_back(n->root);
push_undo(is_add_shared_index); push_undo(is_add_shared_index);
} }
}
for (auto n : monomial(old_m)) for (auto n : monomial(old_m))
n->root->n->unmark1(); n->root->n->unmark1();
m_update_shared_trail.push_back({ idx, s }); m_update_shared_trail.push_back({ idx, s });
@ -1186,7 +1195,7 @@ namespace euf {
m_shared[idx].m = new_m; m_shared[idx].m = new_m;
m_shared[idx].j = j; m_shared[idx].j = j;
TRACE(plugin, tout << "shared simplified to " << m_pp(*this, monomial(new_m)) << "\n"); TRACE(plugin, tout << "shared simplified to " << m_pp_ll(*this, monomial(new_m)) << "\n");
push_merge(old_n, new_n, j); push_merge(old_n, new_n, j);
} }

3
src/ast/euf/euf_ac_plugin.h
View file

@ -149,6 +149,7 @@ namespace euf {
tracked_uint_set m_to_simplify_todo; tracked_uint_set m_to_simplify_todo;
tracked_uint_set m_shared_todo; tracked_uint_set m_shared_todo;
uint64_t m_tick = 1; uint64_t m_tick = 1;
symbol m_name;
@ -273,7 +274,7 @@ namespace euf {
public: public:
ac_plugin(egraph& g, unsigned fid, unsigned op); ac_plugin(egraph& g, char const* name, unsigned fid, unsigned op);
ac_plugin(egraph& g, func_decl* f); ac_plugin(egraph& g, func_decl* f);

6
src/ast/euf/euf_arith_plugin.cpp
View file

@ -24,8 +24,8 @@ namespace euf {
arith_plugin::arith_plugin(egraph& g) : arith_plugin::arith_plugin(egraph& g) :
plugin(g), plugin(g),
a(g.get_manager()), a(g.get_manager()),
m_add(g, get_id(), OP_ADD), m_add(g, "add", get_id(), OP_ADD),
m_mul(g, get_id(), OP_MUL) { m_mul(g, "mul", get_id(), OP_MUL) {
std::function<void(void)> uadd = [&]() { m_undo.push_back(undo_t::undo_add); }; std::function<void(void)> uadd = [&]() { m_undo.push_back(undo_t::undo_add); };
m_add.set_undo(uadd); m_add.set_undo(uadd);
std::function<void(void)> umul = [&]() { m_undo.push_back(undo_t::undo_mul); }; std::function<void(void)> umul = [&]() { m_undo.push_back(undo_t::undo_mul); };
@ -66,9 +66,7 @@ namespace euf {
} }
std::ostream& arith_plugin::display(std::ostream& out) const { std::ostream& arith_plugin::display(std::ostream& out) const {
out << "add\n";
m_add.display(out); m_add.display(out);
out << "mul\n";
m_mul.display(out); m_mul.display(out);
return out; return out;
} }