diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index 89d42bf43..1d5347bc7 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/src/ast/euf/euf_ac_plugin.cpp @@ -41,16 +41,20 @@ More notes: Shared occurrences are rewritten modulo completion. When equal to a different shared occurrence, propagate equality. -TODOs: -- Establish / fix formal termination properties in the presence of union-find. - The formal interactions between union find and orienting the equations need to be established. - - Union-find merges can change the orientation of an equation and break termination. - - For example, rules are currently not re-oriented if there is a merge. The rules could be re-oriented during propagation. -- Elimination of redundant rules. - - superposition uses a stop-gap to avoid some steps. It should be revisited. + - Elimination of redundant rules. -> forward and backward subsumption - apply forward subsumption when simplifying equality using processed - apply backward subsumption when simplifying processed and to_simplify + + Rewrite rules are reoriented after a merge of enodes. + It simulates creating a critical pair: + n -> n' + n + k = j + k + after merge + n' + k = j + k, could be that n' + k < j + k < n + k in term ordering because n' < j, m < n + + TODOs: + - Efficiency of handling shared terms. - The shared terms hash table is not incremental. It could be made incremental by updating it on every merge similar to how the egraph handles it. @@ -350,10 +354,10 @@ namespace euf { while (true) { loop_start: unsigned eq_id = pick_next_eq(); - TRACE("plugin", tout << "propagate " << eq_id << "\n"); if (eq_id == UINT_MAX) break; - eq& eq = m_eqs[eq_id]; + + TRACE("plugin", tout << "propagate " << eq_id << ": " << eq_pp(*this, m_eqs[eq_id]) << "\n"); // simplify eq using processed for (auto other_eq : backward_iterator(eq_id)) @@ -390,6 +394,7 @@ namespace euf { return UINT_MAX; } + // reorient equations when the status of equations are set to to_simplify. void ac_plugin::set_status(unsigned id, eq_status s) { auto& eq = m_eqs[id]; if (eq.status == eq_status::is_dead) @@ -434,7 +439,7 @@ namespace euf { auto const& eq = m_eqs[eq_id]; init_ref_counts(monomial(eq.r), m_dst_r_counts); init_ref_counts(monomial(eq.l), m_dst_l_counts); - init_overlap_iterator(eq_id, monomial(eq.r)); + init_subset_iterator(eq_id, monomial(eq.r)); return m_eq_occurs; } @@ -442,12 +447,37 @@ namespace euf { m_eq_occurs.reset(); for (auto n : m) m_eq_occurs.append(n->root->eqs); + compress_eq_occurs(eq_id); + } - // prune m_eq_occurs to single occurrences + // + // add all but one of the use lists. Identify the largest use list and skip it. + // The rationale is that [a, b] is a subset of [a, b, c, d, e] if + // it has at least two elements (otherwise it would not apply as a rewrite over AC). + // then one of the two elements has to be in the set of [a, b, c, d, e] \ { x } + // where x is an arbitrary value from a, b, c, d, e. Not a two-element watch list, but still. + // + void ac_plugin::init_subset_iterator(unsigned eq_id, monomial_t const& m) { + unsigned max_use = 0; + node* max_n = nullptr; + for (auto n : m) + if (n->root->eqs.size() >= max_use) + max_n = n, max_use = n->root->eqs.size(); + // found node that occurs in fewest rhs + VERIFY(max_n); + m_eq_occurs.reset(); + for (auto n : m) + if (n != max_n) + m_eq_occurs.append(n->root->eqs); + compress_eq_occurs(eq_id); + } + + // prune m_eq_occurs to single occurrences + void ac_plugin::compress_eq_occurs(unsigned eq_id) { unsigned j = 0; + m_eq_seen.reserve(m_eqs.size() + 1, false); for (unsigned i = 0; i < m_eq_occurs.size(); ++i) { - unsigned id = m_eq_occurs[i]; - m_eq_seen.reserve(id + 1, false); + unsigned id = m_eq_occurs[i]; if (m_eq_seen[id]) continue; if (id == eq_id) @@ -497,6 +527,8 @@ namespace euf { auto& src = m_eqs[src_eq]; auto& dst = m_eqs[dst_eq]; + TRACE("plugin", tout << "forward simplify " << eq_pp(*this, src) << " " << eq_pp(*this, dst) << "\n"); + if (!can_be_subset(monomial(src.l), monomial(dst.r))) return; @@ -530,6 +562,7 @@ namespace euf { m_eqs[dst_eq].r = new_r; m_eqs[dst_eq].j = justify_rewrite(src_eq, dst_eq); push_undo(is_update_eq); + TRACE("plugin", tout << "rewritten to " << m_pp(*this, monomial(new_r)) << "\n"); } m_src_r.shrink(src_r_size); } @@ -543,13 +576,14 @@ namespace euf { // // dst_ids, dst_count contain rhs of dst_eq // - + TRACE("plugin", tout << "backward simplify " << eq_pp(*this, src) << " " << eq_pp(*this, dst) << "\n"); // check that src.l is a subset of dst.r if (!can_be_subset(monomial(src.l), monomial(dst.r))) return false; if (!is_subset(m_dst_l_counts, m_src_l_counts, monomial(src.l))) return false; if (backward_subsumes(src_eq, dst_eq)) { + set_status(dst_eq, eq_status::is_dead); return true; } @@ -558,6 +592,7 @@ namespace euf { m_update_eq_trail.push_back({ dst_eq, m_eqs[dst_eq] }); m_eqs[dst_eq].r = new_r; m_eqs[dst_eq].j = justify_rewrite(src_eq, dst_eq); + TRACE("plugin", tout << "rewritten to " << m_pp(*this, monomial(new_r)) << "\n"); push_undo(is_update_eq); return true; } @@ -769,7 +804,7 @@ namespace euf { change = false; auto & m = monomial(s.m); init_ref_counts(m, m_dst_l_counts); - init_overlap_iterator(UINT_MAX, m); + init_subset_iterator(UINT_MAX, m); for (auto eq : m_eq_occurs) { auto& src = m_eqs[eq]; if (!can_be_subset(monomial(src.l), m)) diff --git a/src/ast/euf/euf_ac_plugin.h b/src/ast/euf/euf_ac_plugin.h index ca8f047ae..5c1b1f775 100644 --- a/src/ast/euf/euf_ac_plugin.h +++ b/src/ast/euf/euf_ac_plugin.h @@ -29,6 +29,7 @@ for p in parents(xyzz): #pragma once +#include #include "ast/euf/euf_plugin.h" namespace euf { @@ -223,6 +224,8 @@ namespace euf { unsigned_vector const& backward_iterator(unsigned eq); void init_ref_counts(monomial_t const& monomial, ref_counts& counts); void init_overlap_iterator(unsigned eq, monomial_t const& m); + void init_subset_iterator(unsigned eq, monomial_t const& m); + void compress_eq_occurs(unsigned eq_id); // check that src is a subset of dst, where dst_counts are precomputed bool is_subset(ref_counts const& dst_counts, ref_counts& src_counts, monomial_t const& src); @@ -244,6 +247,7 @@ namespace euf { std::ostream& display_monomial(std::ostream& out, monomial_t const& m) const; std::ostream& display_equation(std::ostream& out, eq const& e) const; + public: ac_plugin(egraph& g, unsigned fid, unsigned op); @@ -267,5 +271,20 @@ namespace euf { std::ostream& display(std::ostream& out) const override; void set_undo(std::function u) { m_undo_notify = u; } + + struct eq_pp { + ac_plugin& p; eq const& e; + eq_pp(ac_plugin& p, eq const& e) : p(p), e(e) {}; + std::ostream& display(std::ostream& out) const { return p.display_equation(out, e); } + }; + + struct m_pp { + ac_plugin& p; monomial_t const& m; + m_pp(ac_plugin& p, monomial_t const& m) : p(p), m(m) {} + std::ostream& display(std::ostream& out) const { return p.display_monomial(out, m); } + }; }; + + inline std::ostream& operator<<(std::ostream& out, ac_plugin::eq_pp const& d) { return d.display(out); } + inline std::ostream& operator<<(std::ostream& out, ac_plugin::m_pp const& d) { return d.display(out); } }