From 9a2693bb72f8973f891618622fdfd0e78f831f41 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Nov 2022 16:39:20 +0700 Subject: [PATCH] tune euf-completion --- src/ast/rewriter/bool_rewriter.cpp | 4 ++ src/ast/rewriter/bool_rewriter.h | 10 +-- src/ast/rewriter/th_rewriter.cpp | 11 +++- src/ast/rewriter/th_rewriter.h | 1 + src/ast/simplifiers/euf_completion.cpp | 88 ++++++++++++++++++++++++-- src/ast/simplifiers/euf_completion.h | 1 + 6 files changed, 104 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index ffceec277ed..5abfe01a62f 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -780,6 +780,10 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { } } } + if (m_order_eq && lhs->get_id() > rhs->get_id()) { + result = m().mk_eq(rhs, lhs); + return BR_DONE; + } return BR_FAILED; } diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 2cec0b2ce82..8f2221a8cee 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -52,10 +52,11 @@ Module Name: class bool_rewriter { ast_manager & m_manager; hoist_rewriter m_hoist; - bool m_flat_and_or; - bool m_local_ctx; - bool m_elim_and; - bool m_blast_distinct; + bool m_flat_and_or = false; + bool m_local_ctx = false; + bool m_elim_and = false; + bool m_blast_distinct = false; + bool m_order_eq = false; unsigned m_blast_distinct_threshold; bool m_ite_extra_rules; unsigned m_local_ctx_limit; @@ -90,6 +91,7 @@ class bool_rewriter { bool elim_and() const { return m_elim_and; } void set_elim_and(bool f) { m_elim_and = f; } void reset_local_ctx_cost() { m_local_ctx_cost = 0; } + void set_order_eq(bool f) { m_order_eq = f; } void updt_params(params_ref const & p); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 9bc8c22cf6e..456a7afba13 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -707,9 +707,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg { expr_ref mk_eq(expr* a, expr* b) { expr_ref result(m()); - if (a->get_id() > b->get_id()) - std::swap(a, b); - if (BR_FAILED == reduce_eq(a, b, result)) + br_status st = reduce_eq(a, b, result); + if (BR_FAILED == st) + st = m_b_rw.mk_eq_core(a, b, result); + if (BR_FAILED == st) result = m().mk_eq(a, b); return result; } @@ -945,6 +946,10 @@ void th_rewriter::set_flat_and_or(bool f) { m_imp->cfg().m_b_rw.set_flat_and_or(f); } +void th_rewriter::set_order_eq(bool f) { + m_imp->cfg().m_b_rw.set_order_eq(f); +} + th_rewriter::~th_rewriter() { dealloc(m_imp); } diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 2c08c247d35..a3f0037992e 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -40,6 +40,7 @@ class th_rewriter { static void get_param_descrs(param_descrs & r); void set_flat_and_or(bool f); + void set_order_eq(bool f); unsigned get_cache_size() const; unsigned get_num_steps() const; diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 1ca980d0739..2825f3244de 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -43,6 +43,7 @@ Algorithm for extracting canonical form from an E-graph: #include "ast/ast_util.h" #include "ast/euf/euf_egraph.h" #include "ast/simplifiers/euf_completion.h" +#include "ast/shared_occs.h" namespace euf { @@ -55,20 +56,99 @@ namespace euf { m_rewriter(m) { m_tt = m_egraph.mk(m.mk_true(), 0, 0, nullptr); m_ff = m_egraph.mk(m.mk_false(), 0, 0, nullptr); + m_rewriter.set_order_eq(true); + m_rewriter.set_flat_and_or(false); } void completion::reduce() { - unsigned rounds = 0; - do { + + propagate_values(); + if (m_fmls.inconsistent()) + return; + m_has_new_eq = true; + for (unsigned rounds = 0; m_has_new_eq && rounds <= 3 && !m_fmls.inconsistent(); ++rounds) { ++m_epoch; - ++rounds; m_has_new_eq = false; add_egraph(); map_canonical(); read_egraph(); IF_VERBOSE(11, verbose_stream() << "(euf.completion :rounds " << rounds << ")\n"); } - while (m_has_new_eq && rounds <= 3); + } + + /** + * Propagate writes into values first. It is cheaper to propagate values directly than using + * the E-graph. The E-graph suffers from the following overhead: it prefers interpreted nodes + * as roots and therefore the "merge" function ignores the heuristic of choosing the node to appoint root + * as the one with the fewest parents. Merging a constant value with multiple terms then has a compounding + * quadratic time overhead since the parents of the value are removed and re-inserted into the congruence + * table repeatedly and with growing size (exceeding the n*log(n) overhead when choosing the root to + * have the fewest parents). + */ + void completion::propagate_values() { + shared_occs shared(m, true); + expr_substitution subst(m, true, false); + expr* x, * y; + expr_ref_buffer args(m); + auto add_shared = [&]() { + shared_occs_mark visited; + shared.reset(); + for (unsigned i = 0; i < m_fmls.size(); ++i) + shared(m_fmls[i].fml(), visited); + }; + + auto add_sub = [&](dependent_expr const& de) { + auto const& [f, dep] = de(); + if (m.is_not(f, x) && shared.is_shared(x)) + subst.insert(x, m.mk_false(), dep); + else if (shared.is_shared(f)) + subst.insert(f, m.mk_true(), dep); + if (m.is_eq(f, x, y) && m.is_value(x) && shared.is_shared(y)) + subst.insert(y, x, dep); + else if (m.is_eq(f, x, y) && m.is_value(y) && shared.is_shared(x)) + subst.insert(x, y, dep); + }; + + auto process_fml = [&](unsigned i) { + expr* f = m_fmls[i].fml(); + expr_dependency* dep = m_fmls[i].dep(); + expr_ref fml(m); + proof_ref pr(m); + m_rewriter(f, fml, pr); + if (fml != f) { + dep = m.mk_join(dep, m_rewriter.get_used_dependencies()); + m_fmls.update(i, dependent_expr(m, fml, dep)); + ++m_stats.m_num_rewrites; + } + m_rewriter.reset_used_dependencies(); + add_sub(m_fmls[i]); + }; + + unsigned rw = m_stats.m_num_rewrites + 1; + for (unsigned r = 0; r < 4 && rw != m_stats.m_num_rewrites; ++r) { + rw = m_stats.m_num_rewrites; + add_shared(); + subst.reset(); + m_rewriter.reset(); + m_rewriter.set_substitution(&subst); + for (unsigned i = 0; i < m_qhead; ++i) + add_sub(m_fmls[i]); + for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) + process_fml(i); + add_shared(); + subst.reset(); + m_rewriter.reset(); + m_rewriter.set_substitution(&subst); + for (unsigned i = 0; i < m_qhead; ++i) + add_sub(m_fmls[i]); + for (unsigned i = m_fmls.size(); i-- > m_qhead && !m_fmls.inconsistent();) + process_fml(i); + if (subst.empty()) + break; + } + + m_rewriter.set_substitution(nullptr); + m_rewriter.reset(); } void completion::add_egraph() { diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h index f02e3324569..830f8655ef1 100644 --- a/src/ast/simplifiers/euf_completion.h +++ b/src/ast/simplifiers/euf_completion.h @@ -46,6 +46,7 @@ namespace euf { bool is_new_eq(expr* a, expr* b); void update_has_new_eq(expr* g); expr_ref mk_and(expr* a, expr* b); + void propagate_values(); void add_egraph(); void map_canonical(); void read_egraph();