From 5af6e1a046c803fbae472e84dc1f8e5c341b827d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Nov 2022 11:38:41 +0700 Subject: [PATCH] make max_bv_sharing a simplifier --- src/ast/simplifiers/CMakeLists.txt | 1 + .../simplifiers/max_bv_sharing.cpp} | 98 ++++++------------- src/ast/simplifiers/max_bv_sharing.h | 25 +++++ src/tactic/bv/CMakeLists.txt | 1 - src/tactic/bv/max_bv_sharing_tactic.h | 17 +++- 5 files changed, 68 insertions(+), 74 deletions(-) rename src/{tactic/bv/max_bv_sharing_tactic.cpp => ast/simplifiers/max_bv_sharing.cpp} (79%) create mode 100644 src/ast/simplifiers/max_bv_sharing.h diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index d10bf87e7..d5a8fd2a4 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -6,6 +6,7 @@ z3_add_component(simplifiers eliminate_predicates.cpp euf_completion.cpp extract_eqs.cpp + max_bv_sharing.cpp model_reconstruction_trail.cpp propagate_values.cpp solve_context_eqs.cpp diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/ast/simplifiers/max_bv_sharing.cpp similarity index 79% rename from src/tactic/bv/max_bv_sharing_tactic.cpp rename to src/ast/simplifiers/max_bv_sharing.cpp index 2bc99806e..b28b5ebdb 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/ast/simplifiers/max_bv_sharing.cpp @@ -3,7 +3,7 @@ Copyright (c) 2011 Microsoft Corporation Module Name: - max_bv_sharing_tactic.cpp + max_bv_sharing.cpp Abstract: @@ -12,7 +12,7 @@ Abstract: This rewriter is particularly useful for reducing the number of Adders and Multipliers before "bit-blasting". -Author: +Author Leonardo de Moura (leonardo) 2011-12-29. @@ -23,9 +23,10 @@ Revision History: #include "ast/bv_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" #include "util/obj_pair_hashtable.h" +#include "ast/simplifiers/dependent_expr_state.h" #include "ast/ast_lt.h" -class max_bv_sharing_tactic : public tactic { +class max_bv_sharing : public dependent_expr_simplifier { struct rw_cfg : public default_rewriter_cfg { typedef std::pair expr_pair; @@ -224,64 +225,22 @@ class max_bv_sharing_tactic : public tactic { } }; - struct imp { - rw m_rw; - unsigned m_num_steps; + rw m_rw; + unsigned m_num_steps = 0; - imp(ast_manager & m, params_ref const & p): - m_rw(m, p) { - } - - ast_manager & m() const { return m_rw.m(); } - - void operator()(goal_ref const & g, - goal_ref_buffer & result) { - tactic_report report("max-bv-sharing", *g); - bool produce_proofs = g->proofs_enabled(); - - expr_ref new_curr(m()); - proof_ref new_pr(m()); - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { - if (g->inconsistent()) - break; - expr * curr = g->form(idx); - m_rw(curr, new_curr, new_pr); - m_num_steps += m_rw.get_num_steps(); - - if (produce_proofs) { - proof * pr = g->pr(idx); - new_pr = m().mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - m_rw.cfg().cleanup(); - g->inc_depth(); - result.push_back(g.get()); - } - }; - - imp * m_imp; + params_ref m_params; + public: - max_bv_sharing_tactic(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); - } - - tactic * translate(ast_manager & m) override { - return alloc(max_bv_sharing_tactic, m, m_params); - } - - ~max_bv_sharing_tactic() override { - dealloc(m_imp); - } - - char const* name() const override { return "max_bv_sharing"; } + max_bv_sharing(ast_manager & m, params_ref const & p, dependent_expr_state& fmls): + dependent_expr_simplifier(m, fmls), + m_params(p), + m_rw(m, p) { + } void updt_params(params_ref const & p) override { m_params.append(p); - m_imp->m_rw.cfg().updt_params(m_params); + m_rw.cfg().updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { @@ -290,21 +249,22 @@ public: r.insert("max_args", CPK_UINT, "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic."); } - - void operator()(goal_ref const & in, - goal_ref_buffer & result) override { - (*m_imp)(in, result); - } - - void cleanup() override { - ast_manager & m = m_imp->m(); - params_ref p = std::move(m_params); - m_imp->~imp(); - new (m_imp) imp(m, p); - } + + void reduce() override { + expr_ref new_curr(m); + proof_ref new_pr(m); + for (unsigned idx = 0; idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) { + auto [curr, d] = m_fmls[idx](); + m_rw(curr, new_curr, new_pr); + // Proof reconstruction: new_pr = m.mk_modus_ponens(old_pr, new_pr); + m_num_steps += m_rw.get_num_steps(); + m_fmls.update(idx, dependent_expr(m, new_curr, d)); + } + m_rw.cfg().cleanup(); + } }; -tactic * mk_max_bv_sharing_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(max_bv_sharing_tactic, m, p)); +dependent_expr_simplifier * mk_max_bv_sharing(ast_manager & m, params_ref const & p, dependent_expr_state& fmls) { + return alloc(max_bv_sharing, m, p, fmls); } diff --git a/src/ast/simplifiers/max_bv_sharing.h b/src/ast/simplifiers/max_bv_sharing.h new file mode 100644 index 000000000..bfc8f4472 --- /dev/null +++ b/src/ast/simplifiers/max_bv_sharing.h @@ -0,0 +1,25 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + max_bv_sharing.h + +Abstract: + + Rewriter for "maximing" the number of shared terms. + The idea is to rewrite AC terms to maximize sharing. + This rewriter is particularly useful for reducing + the number of Adders and Multipliers before "bit-blasting". + +Author: + + Leonardo de Moura (leonardo) 2011-12-29. + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" + +dependent_expr_simplifier * mk_max_bv_sharing(ast_manager & m, params_ref const & p, dependent_expr_state& fmls); diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt index 653571265..50dd941e0 100644 --- a/src/tactic/bv/CMakeLists.txt +++ b/src/tactic/bv/CMakeLists.txt @@ -11,7 +11,6 @@ z3_add_component(bv_tactics bv_slice_tactic.cpp dt2bv_tactic.cpp elim_small_bv_tactic.cpp - max_bv_sharing_tactic.cpp COMPONENT_DEPENDENCIES bit_blaster core_tactics diff --git a/src/tactic/bv/max_bv_sharing_tactic.h b/src/tactic/bv/max_bv_sharing_tactic.h index 00de41256..ebd050aa5 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.h +++ b/src/tactic/bv/max_bv_sharing_tactic.h @@ -21,11 +21,20 @@ Revision History: --*/ #pragma once -#include "util/params.h" -class ast_manager; -class tactic; +#include "ast/simplifiers/max_bv_sharing.h" +#include "tactic/dependent_expr_state_tactic.h" + +class max_bv_sharing_tactic_factory : public dependent_expr_simplifier_factory { +public: + dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { + return mk_max_bv_sharing(m, p, s); + } +}; + +inline tactic* mk_max_bv_sharing_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, alloc(max_bv_sharing_tactic_factory), "max-bv-sharing"); +} -tactic * mk_max_bv_sharing_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("max-bv-sharing", "use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers.", "mk_max_bv_sharing_tactic(m, p)") */