From ea3628e50bb77adf0bc2a8e0e32132282bde6542 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Dec 2023 16:28:43 -0800 Subject: [PATCH] remove hoist functionality Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/CMakeLists.txt | 1 - src/ast/rewriter/bool_rewriter.cpp | 23 --- src/ast/rewriter/bool_rewriter.h | 4 +- src/ast/rewriter/hoist_rewriter.cpp | 256 ---------------------------- src/ast/rewriter/hoist_rewriter.h | 87 ---------- 5 files changed, 1 insertion(+), 370 deletions(-) delete mode 100644 src/ast/rewriter/hoist_rewriter.cpp delete mode 100644 src/ast/rewriter/hoist_rewriter.h diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index df803b0f186..7f351ecb652 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -23,7 +23,6 @@ z3_add_component(rewriter factor_rewriter.cpp fpa_rewriter.cpp func_decl_replace.cpp - hoist_rewriter.cpp inj_axiom.cpp label_rewriter.cpp macro_replacer.cpp diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 7728716fd29..9afab7a2911 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -34,7 +34,6 @@ void bool_rewriter::updt_params(params_ref const & _p) { m_blast_distinct = p.blast_distinct(); m_blast_distinct_threshold = p.blast_distinct_threshold(); m_ite_extra_rules = p.ite_extra_rules(); - m_hoist.set_elim_and(m_elim_and); } void bool_rewriter::get_param_descrs(param_descrs & r) { @@ -270,28 +269,6 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args return BR_DONE; } -#if 0 - br_status st; - expr_ref r(m()); - st = m_hoist.mk_or(buffer.size(), buffer.data(), r); - if (st != BR_FAILED) { - m_counts1.reserve(m().get_num_asts() + 1); - m_counts2.reserve(m().get_num_asts() + 1); - get_num_internal_exprs(m_counts1, m_todo1, r); - for (unsigned i = 0; i < num_args; ++i) - get_num_internal_exprs(m_counts2, m_todo2, args[i]); - unsigned count1 = count_internal_nodes(m_counts1, m_todo1); - unsigned count2 = count_internal_nodes(m_counts2, m_todo2); - if (count1 > count2) - st = BR_FAILED; - } - if (st != BR_FAILED) - result = r; - if (st == BR_DONE) - return BR_REWRITE1; - if (st != BR_FAILED) - return st; -#endif if (s) { if (m_sort_disjunctions) { ast_lt lt; diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 1c1e7c60e42..7c840b6478c 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -20,7 +20,6 @@ Module Name: #include "ast/ast.h" #include "ast/rewriter/rewriter.h" -#include "ast/rewriter/hoist_rewriter.h" #include "util/params.h" /** @@ -51,7 +50,6 @@ Module Name: */ class bool_rewriter { ast_manager & m_manager; - hoist_rewriter m_hoist; bool m_flat_and_or = false; bool m_sort_disjunctions = true; bool m_local_ctx = false; @@ -84,7 +82,7 @@ class bool_rewriter { void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits); public: - bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { + bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); } ast_manager & m() const { return m_manager; } diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp deleted file mode 100644 index 1b99469a190..00000000000 --- a/src/ast/rewriter/hoist_rewriter.cpp +++ /dev/null @@ -1,256 +0,0 @@ -/*++ -Copyright (c) 2019 Microsoft Corporation - -Module Name: - - hoist_rewriter.cpp - -Abstract: - - Hoist predicates over disjunctions - -Author: - - Nikolaj Bjorner (nbjorner) 2019-2-4 - ---*/ - - -#include "ast/rewriter/hoist_rewriter.h" -#include "ast/rewriter/bool_rewriter.h" -#include "ast/ast_util.h" -#include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" - -hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p): - m(m), m_args1(m), m_args2(m), m_refs(m), m_subst(m) { - updt_params(p); -} - -expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) { - if (m_elim_and) { - expr_ref_vector negs(m); - for (expr* a : args) - if (m.is_false(a)) - return expr_ref(m.mk_false(), m); - else if (m.is_true(a)) - continue; - else - negs.push_back(::mk_not(m, a)); - return ::mk_not(mk_or(negs)); - } - else - return ::mk_and(args); -} - -expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) { - return ::mk_or(args); -} - -br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) { - if (num_args < 2) - return BR_FAILED; - - for (unsigned i = 0; i < num_args; ++i) - if (!is_and(es[i], nullptr)) - return BR_FAILED; - - bool turn = false; - m_preds1.reset(); - m_preds2.reset(); - m_uf1.reset(); - m_uf2.reset(); - m_expr2var.reset(); - m_var2expr.reset(); - basic_union_find* uf[2] = { &m_uf1, &m_uf2 }; - obj_hashtable* preds[2] = { &m_preds1, &m_preds2 }; - expr_ref_vector* args[2] = { &m_args1, &m_args2 }; - VERIFY(is_and(es[0], args[turn])); - expr* e1, *e2; - for (expr* e : *(args[turn])) { - if (m.is_eq(e, e1, e2)) - (*uf)[turn].merge(mk_var(e1), mk_var(e2)); - else - (*preds)[turn].insert(e); - } - unsigned round = 0; - for (unsigned j = 1; j < num_args; ++j) { - ++round; - m_es.reset(); - m_mark.reset(); - - bool last = turn; - turn = !turn; - (*preds)[turn].reset(); - reset(m_uf0); - VERIFY(is_and(es[j], args[turn])); - - for (expr* e : *args[turn]) { - if (m.is_eq(e, e1, e2)) { - m_es.push_back(e1); - m_uf0.merge(mk_var(e1), mk_var(e2)); - } - else if ((*preds)[last].contains(e)) - (*preds)[turn].insert(e); - } - - if ((*preds)[turn].empty() && m_es.empty()) - return BR_FAILED; - - m_eqs.reset(); - for (expr* e : m_es) { - if (m_mark.is_marked(e)) - continue; - unsigned u = mk_var(e); - unsigned v = u; - m_roots.reset(); - do { - m_mark.mark(e); - unsigned r = (*uf)[last].find(v); - if (m_roots.find(r, e2)) - m_eqs.push_back({e, e2}); - else - m_roots.insert(r, e); - v = m_uf0.next(v); - e = mk_expr(v); - } - while (u != v); - } - reset((*uf)[turn]); - for (auto const& [e1, e2] : m_eqs) - (*uf)[turn].merge(mk_var(e1), mk_var(e2)); - if ((*preds)[turn].empty() && m_eqs.empty()) - return BR_FAILED; - } - if (m_eqs.empty()) { - result = hoist_predicates((*preds)[turn], num_args, es); - return BR_DONE; - } - // p & eqs & (or fmls) - expr_ref_vector fmls(m); - m_subst.reset(); - for (expr * p : (*preds)[turn]) { - expr* q = nullptr; - if (m.is_not(p, q)) - m_subst.insert(q, m.mk_false()); - else - m_subst.insert(p, m.mk_true()); - fmls.push_back(p); - } - bool new_eq = false; - for (auto& [a, b] : m_eqs) { - if (m.is_value(a)) - std::swap(a, b); - if (m.are_equal(a, b)) - continue; - if (m.are_distinct(a, b)) { - result = m.mk_false(); - return BR_DONE; - } - new_eq = true; - m_subst.insert(a, b); - fmls.push_back(m.mk_eq(a, b)); - } - expr_ref ors(::mk_or(m, num_args, es), m); - m_subst(ors); - fmls.push_back(ors); - result = mk_and(fmls); - TRACE("hoist", tout << ors << " => " << result << "\n";); - return new_eq ? BR_REWRITE3 : BR_DONE; -} - -unsigned hoist_rewriter::mk_var(expr* e) { - unsigned v = 0; - if (m_expr2var.find(e, v)) - return v; - m_uf1.mk_var(); - v = m_uf2.mk_var(); - SASSERT(v == m_var2expr.size()); - m_expr2var.insert(e, v); - m_var2expr.push_back(e); - return v; -} - -expr_ref hoist_rewriter::hoist_predicates(obj_hashtable const& preds, unsigned num_args, expr* const* es) { - expr_ref_vector args(m), args1(m), fmls(m); - for (unsigned i = 0; i < num_args; ++i) { - VERIFY(is_and(es[i], &args1)); - fmls.reset(); - for (expr* e : args1) - if (!preds.contains(e)) - fmls.push_back(e); - args.push_back(mk_and(fmls)); - } - fmls.reset(); - fmls.push_back(mk_or(args)); - for (auto* p : preds) - fmls.push_back(p); - return mk_and(fmls); -} - - -br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - switch (f->get_decl_kind()) { - case OP_OR: - return mk_or(num_args, args, result); - default: - return BR_FAILED; - } -} - -bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) { -#if 0 - if (!args) - return m.is_and(e) || (m.is_not(e, e) && m.is_or(e)); - expr_fast_mark1 visited; - args->reset(); - args->push_back(e); - m_refs.reset(); - for (unsigned i = 0; i < args->size(); ++i) { - e = args->get(i); - if (visited.is_marked(e)) - goto drop; - m_refs.push_back(e); - visited.mark(e, true); - if (m.is_and(e)) - args->append(to_app(e)->get_num_args(), to_app(e)->get_args()); - else if (m.is_not(e, e) && m.is_or(e)) - for (expr* arg : *to_app(e)) - args->push_back(::mk_not(m, arg)); - else - continue; - drop: - (*args)[i] = args->back(); - args->pop_back(); - --i; - } - return args->size() > 1; -#else - if (m.is_and(e)) { - if (args) { - args->reset(); - args->append(to_app(e)->get_num_args(), to_app(e)->get_args()); - } - return true; - } - if (m.is_not(e, e) && m.is_or(e)) { - if (args) { - args->reset(); - for (expr* arg : *to_app(e)) - args->push_back(::mk_not(m, arg)); - TRACE("hoist", tout << args << " " << * args << "\n"); - } - return true; - } -#endif - return false; -} - - -void hoist_rewriter::reset(basic_union_find& uf) { - uf.reset(); - for (expr* e : m_var2expr) { - (void)e; - uf.mk_var(); - } -} diff --git a/src/ast/rewriter/hoist_rewriter.h b/src/ast/rewriter/hoist_rewriter.h deleted file mode 100644 index b64325584a5..00000000000 --- a/src/ast/rewriter/hoist_rewriter.h +++ /dev/null @@ -1,87 +0,0 @@ -/*++ -Copyright (c) 2019 Microsoft Corporation - -Module Name: - - hoist_rewriter.h - -Abstract: - - Hoist predicates over disjunctions - -Author: - - Nikolaj Bjorner (nbjorner) 2019-2-4 - -Notes: - ---*/ -#pragma once - -#include "ast/ast.h" -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/expr_safe_replace.h" -#include "util/params.h" -#include "util/union_find.h" -#include "util/obj_hashtable.h" - -class bool_rewriter; - -class hoist_rewriter { - ast_manager & m; - expr_ref_vector m_args1, m_args2, m_refs; - obj_hashtable m_preds1, m_preds2; - basic_union_find m_uf1, m_uf2, m_uf0; - ptr_vector m_es; - svector> m_eqs; - u_map m_roots; - expr_safe_replace m_subst; - obj_map m_expr2var; - ptr_vector m_var2expr; - expr_mark m_mark; - bool m_elim_and = false; - - bool is_and(expr* e, expr_ref_vector* args); - expr_ref mk_and(expr_ref_vector const& args); - expr_ref mk_or(expr_ref_vector const& args); - - bool is_var(expr* e) { return m_expr2var.contains(e); } - expr* mk_expr(unsigned v) { return m_var2expr[v]; } - unsigned mk_var(expr* e); - - void reset(basic_union_find& uf); - - expr_ref hoist_predicates(obj_hashtable const& p, unsigned num_args, expr* const* args); - - -public: - hoist_rewriter(ast_manager & m, params_ref const & p = params_ref()); - family_id get_fid() const { return m.get_basic_family_id(); } - bool is_eq(expr * t) const { return m.is_eq(t); } - void updt_params(params_ref const & p) {} - static void get_param_descrs(param_descrs & r) {} - br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result); - void set_elim_and(bool b) { m_elim_and = b; } -}; - -struct hoist_rewriter_cfg : public default_rewriter_cfg { - hoist_rewriter m_r; - bool rewrite_patterns() const { return false; } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - result_pr = nullptr; - if (f->get_family_id() != m_r.get_fid()) - return BR_FAILED; - return m_r.mk_app_core(f, num, args, result); - } - hoist_rewriter_cfg(ast_manager & m, params_ref const & p):m_r(m, p) {} -}; - -class hoist_rewriter_star : public rewriter_tpl { - hoist_rewriter_cfg m_cfg; -public: - hoist_rewriter_star(ast_manager & m, params_ref const & p = params_ref()): - rewriter_tpl(m, false, m_cfg), - m_cfg(m, p) {} -}; -