From db74e23de1efe92170f3e6e9083516e6af652bc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Nov 2022 11:07:31 +0700 Subject: [PATCH] make card2bv a simplifier --- src/ast/simplifiers/CMakeLists.txt | 1 + src/ast/simplifiers/card2bv.cpp | 61 ++++++++++ src/ast/simplifiers/card2bv.h | 42 +++++++ src/ast/simplifiers/elim_unconstrained.cpp | 2 +- src/ast/simplifiers/eliminate_predicates.cpp | 2 +- .../simplifiers/model_reconstruction_trail.h | 2 +- src/tactic/arith/CMakeLists.txt | 1 - src/tactic/arith/card2bv_tactic.cpp | 105 ------------------ src/tactic/arith/card2bv_tactic.h | 95 +++------------- 9 files changed, 120 insertions(+), 191 deletions(-) create mode 100644 src/ast/simplifiers/card2bv.cpp create mode 100644 src/ast/simplifiers/card2bv.h delete mode 100644 src/tactic/arith/card2bv_tactic.cpp diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index 9361937f7..d10bf87e7 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(simplifiers SOURCES bv_slice.cpp + card2bv.cpp elim_unconstrained.cpp eliminate_predicates.cpp euf_completion.cpp diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp new file mode 100644 index 000000000..d9c387c5a --- /dev/null +++ b/src/ast/simplifiers/card2bv.cpp @@ -0,0 +1,61 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + card2bv.cpp + +Abstract: + + convert cardinality constraints to bit-vectors + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-24 + +--*/ + + +#include "ast/simplifiers/card2bv.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/rewriter/pb2bv_rewriter.h" + +card2bv::card2bv(ast_manager& m, params_ref const& p, dependent_expr_state& fmls) : + dependent_expr_simplifier(m, fmls), m_params(p) {} + +void card2bv::reduce() { + th_rewriter rw1(m, m_params); + pb2bv_rewriter rw2(m, m_params); + + expr_ref new_f1(m), new_f2(m); + proof_ref new_pr(m); + for (unsigned idx = 0; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) { + auto [f, d] = m_fmls[idx](); + rw1(f, new_f1); + rw2(false, new_f1, new_f2, new_pr); + if (new_f2 != f) { + TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_f2 << "\n"); + m_fmls.update(idx, dependent_expr(m, new_f2, d)); + ++m_stats.m_num_rewrites; + } + } + + expr_ref_vector fmls(m); + rw2.flush_side_constraints(fmls); + for (expr* e : fmls) + m_fmls.add(dependent_expr(m, e, nullptr)); + + func_decl_ref_vector const& fns = rw2.fresh_constants(); + for (func_decl* f : fns) + m_fmls.model_trail().hide(f); +} + +void card2bv::collect_statistics(statistics& st) const { + st.update("card2bv-rewrites", m_stats.m_num_rewrites); +} + +void card2bv::collect_param_descrs(param_descrs& r) { + r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver"); + pb2bv_rewriter rw(m, m_params); + rw.collect_param_descrs(r); +} diff --git a/src/ast/simplifiers/card2bv.h b/src/ast/simplifiers/card2bv.h new file mode 100644 index 000000000..e089fa84c --- /dev/null +++ b/src/ast/simplifiers/card2bv.h @@ -0,0 +1,42 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + card2bv.h + +Abstract: + + convert cardinality constraints to bit-vectors + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-24 + + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/th_rewriter.h" + + +class card2bv : public dependent_expr_simplifier { + + struct stats { + unsigned m_num_rewrites = 0; + void reset() { memset(this, 0, sizeof(*this)); } + }; + + stats m_stats; + params_ref m_params; + +public: + card2bv(ast_manager& m, params_ref const& p, dependent_expr_state& fmls); + void reduce() override; + void collect_statistics(statistics& st) const override; + void reset_statistics() override { m_stats.reset(); } + void updt_params(params_ref const& p) override { m_params.append(p); } + void collect_param_descrs(param_descrs& r) override; +}; diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index d590f3e59..52dc95f05 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -285,7 +285,7 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector< for (auto const& entry : mc.entries()) { switch (entry.m_instruction) { case generic_model_converter::instruction::HIDE: - trail.push(entry.m_f); + trail.hide(entry.m_f); break; case generic_model_converter::instruction::ADD: break; diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index afa07a3a3..6d1288c5d 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -327,7 +327,7 @@ void eliminate_predicates::try_find_macro(clause& cl) { app_ref def(m), k(m), fml(m); func_decl_ref fn(m); fn = m.mk_fresh_func_decl(df->get_arity(), df->get_domain(), df->get_range()); - m_fmls.model_trail().push(fn); // hide definition of fn + m_fmls.model_trail().hide(fn); // hide definition of fn k = m.mk_app(fn, f->get_num_args(), f->get_args()); def = m.mk_ite(cond, t, k); insert_macro(f, def, cl.m_dep); diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index 40db7dfba..906aaa738 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -102,7 +102,7 @@ public: /** * add declaration to hide */ - void push(func_decl* f) { + void hide(func_decl* f) { m_trail.push_back(alloc(entry, m, f)); m_trail_stack.push(push_back_vector(m_trail)); } diff --git a/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt index cb025b206..d5c7557e6 100644 --- a/src/tactic/arith/CMakeLists.txt +++ b/src/tactic/arith/CMakeLists.txt @@ -6,7 +6,6 @@ z3_add_component(arith_tactics bound_propagator.cpp bv2int_rewriter.cpp bv2real_rewriter.cpp - card2bv_tactic.cpp degree_shift_tactic.cpp diff_neq_tactic.cpp eq2bv_tactic.cpp diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp deleted file mode 100644 index 4f79a887d..000000000 --- a/src/tactic/arith/card2bv_tactic.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - card2bv_tactic.cpp - -Abstract: - - Tactic for converting Pseudo-Boolean constraints to BV - -Author: - - Nikolaj Bjorner (nbjorner) 2014-03-20 - -Notes: - ---*/ -#include "tactic/tactical.h" -#include "ast/ast_smt2_pp.h" -#include "tactic/arith/card2bv_tactic.h" -#include "ast/rewriter/pb2bv_rewriter.h" -#include "ast/ast_util.h" -#include "ast/ast_pp.h" -#include "ast/converters/generic_model_converter.h" - -class card2bv_tactic : public tactic { - ast_manager & m; - params_ref m_params; - -public: - - card2bv_tactic(ast_manager & m, params_ref const & p): - m(m), - m_params(p) { - } - - tactic * translate(ast_manager & m) override { - return alloc(card2bv_tactic, m, m_params); - } - - char const* name() const override { return "card2bv"; } - - void updt_params(params_ref const & p) override { - m_params.append(p); - } - - void collect_param_descrs(param_descrs & r) override { - r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver"); - pb2bv_rewriter rw(m, m_params); - rw.collect_param_descrs(r); - } - - - void operator()(goal_ref const & g, - goal_ref_buffer & result) override { - TRACE("card2bv-before", g->display(tout);); - result.reset(); - tactic_report report("card2bv", *g); - th_rewriter rw1(m, m_params); - pb2bv_rewriter rw2(m, m_params); - - if (g->inconsistent()) { - result.push_back(g.get()); - return; - } - - expr_ref new_f1(m), new_f2(m); - for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) { - proof_ref new_pr1(m), new_pr2(m); - rw1(g->form(idx), new_f1, new_pr1); - TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_pr1 << std::endl;); - rw2(false, new_f1, new_f2, new_pr2); - TRACE("card2bv", tout << "Rewriting " << new_f2 << "\n" << new_pr2 << std::endl;); - if (m.proofs_enabled()) { - new_pr1 = m.mk_transitivity(new_pr1, new_pr2); - new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1); - } - g->update(idx, new_f2, new_pr1, g->dep(idx)); - } - expr_ref_vector fmls(m); - rw2.flush_side_constraints(fmls); - for (expr* e : fmls) { - g->assert_expr(e); - } - - func_decl_ref_vector const& fns = rw2.fresh_constants(); - if (!fns.empty()) { - generic_model_converter* filter = alloc(generic_model_converter, m, "card2bv"); - for (func_decl* f : fns) filter->hide(f); - g->add(filter); - } - - g->inc_depth(); - result.push_back(g.get()); - } - - void cleanup() override { - } -}; - -tactic * mk_card2bv_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(card2bv_tactic, m, p)); -} - diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h index 81296f18d..95282d93c 100644 --- a/src/tactic/arith/card2bv_tactic.h +++ b/src/tactic/arith/card2bv_tactic.h @@ -13,95 +13,26 @@ Author: Nikolaj Bjorner (nbjorner) 2014-03-20 -Notes: - --*/ #pragma once + #include "util/params.h" -#include "ast/pb_decl_plugin.h" -#include "ast/rewriter/th_rewriter.h" -#include "ast/rewriter/rewriter.h" -#include -#include "util/sorting_network.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/card2bv.h" - -class ast_manager; -class tactic; - -namespace pb { - - class card2bv_rewriter { - public: - typedef expr* pliteral; - typedef ptr_vector pliteral_vector; - private: - ast_manager& m; - arith_util au; - pb_util pb; - bv_util bv; - psort_nw m_sort; - expr_ref_vector m_lemmas; - expr_ref_vector m_trail; - - unsigned get_num_bits(func_decl* f); - void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result); - br_status mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result); - expr* negate(expr* e); - expr* mk_ite(expr* c, expr* hi, expr* lo); - bool is_or(func_decl* f); - bool is_and(func_decl* f); - bool is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result); - expr_ref mk_atmost1(unsigned sz, expr * const* args); - void mk_at_most_1_small(bool last, unsigned n, pliteral const* xs, expr_ref_vector& result, expr_ref_vector& ors); - - public: - card2bv_rewriter(ast_manager& m); - br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result); - void mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas); - - // definitions used for sorting network - pliteral mk_false() { return m.mk_false(); } - pliteral mk_true() { return m.mk_true(); } - pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); } - pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); } - pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } - std::ostream& pp(std::ostream& out, pliteral lit); - pliteral fresh(); - pliteral trail(pliteral l); - void mk_clause(unsigned n, pliteral const* lits); - - }; - - struct card2bv_rewriter_cfg : public default_rewriter_cfg { - card2bv_rewriter m_r; - bool rewrite_patterns() const { return false; } - bool flat_assoc(func_decl * f) 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; - return m_r.mk_app_core(f, num, args, result); - } - card2bv_rewriter_cfg(ast_manager & m):m_r(m) {} - }; - - class card_pb_rewriter : public rewriter_tpl { - card2bv_rewriter_cfg m_cfg; - pb_util pb; - expr_ref_vector m_lemmas; - public: - card_pb_rewriter(ast_manager & m): - rewriter_tpl(m, false, m_cfg), - m_cfg(m), - pb(m), - m_lemmas(m) {} - - void rewrite(expr* e, expr_ref& result); - - expr_ref_vector& lemmas() { return m_lemmas; } - }; +class card2bv_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 alloc(card2bv, m, p, s); + } }; -tactic * mk_card2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); +inline tactic* mk_card2bv_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, alloc(card2bv_tactic_factory), "card2bv"); +} + /* ADD_TACTIC("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_card2bv_tactic(m, p)") */