From a64fd7145c381eed2be11d68c190b65760fb4261 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Mar 2018 03:36:03 -0800 Subject: [PATCH] remove buggy legacy code, rely on pull_cheap_ite option in rewriter, #1511 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/CMakeLists.txt | 1 - src/ast/rewriter/pull_ite_tree.cpp | 221 ------------------------- src/ast/rewriter/pull_ite_tree.h | 113 ------------- src/smt/asserted_formulas.cpp | 4 +- src/smt/asserted_formulas.h | 4 - src/smt/params/preprocessor_params.cpp | 2 +- src/smt/params/preprocessor_params.h | 4 +- src/smt/smt_setup.cpp | 2 +- 8 files changed, 5 insertions(+), 346 deletions(-) delete mode 100644 src/ast/rewriter/pull_ite_tree.cpp delete mode 100644 src/ast/rewriter/pull_ite_tree.h diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 57924b48a..f030e2704 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -25,7 +25,6 @@ z3_add_component(rewriter pb_rewriter.cpp pb2bv_rewriter.cpp push_app_ite.cpp - pull_ite_tree.cpp quant_hoist.cpp rewriter.cpp seq_rewriter.cpp diff --git a/src/ast/rewriter/pull_ite_tree.cpp b/src/ast/rewriter/pull_ite_tree.cpp deleted file mode 100644 index 61114387c..000000000 --- a/src/ast/rewriter/pull_ite_tree.cpp +++ /dev/null @@ -1,221 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - pull_ite_tree.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-22. - -Revision History: - ---*/ -#include "ast/rewriter/pull_ite_tree.h" -#include "ast/recurse_expr_def.h" -#include "ast/for_each_expr.h" -#include "ast/ast_pp.h" - -pull_ite_tree::pull_ite_tree(ast_manager & m): - m_manager(m), - m_rewriter(m), - m_cache(m) { -} - -void pull_ite_tree::cache_result(expr * n, expr * r, proof * pr) { - m_cache.insert(n, r, pr); -} - -void pull_ite_tree::visit(expr * n, bool & visited) { - if (!is_cached(n)) { - m_todo.push_back(n); - visited = false; - } -} - -bool pull_ite_tree::visit_children(expr * n) { - if (m_manager.is_ite(n)) { - bool visited = true; - visit(to_app(n)->get_arg(1), visited); - visit(to_app(n)->get_arg(2), visited); - return visited; - } - else { - return true; - } -} - -void pull_ite_tree::reduce(expr * n) { - // Remark: invoking the simplifier to build the new expression saves a lot of memory. - if (m_manager.is_ite(n)) { - expr * c = to_app(n)->get_arg(0); - expr * t_old = to_app(n)->get_arg(1); - expr * e_old = to_app(n)->get_arg(2); - expr * t = nullptr; - proof * t_pr = nullptr; - expr * e = nullptr; - proof * e_pr = nullptr; - get_cached(t_old, t, t_pr); - get_cached(e_old, e, e_pr); - expr_ref r(m_manager); - expr * args[3] = {c, t, e}; - r = m_rewriter.mk_app(to_app(n)->get_decl(), 3, args); - if (!m_manager.proofs_enabled()) { - // expr * r = m_manager.mk_ite(c, t, e); - cache_result(n, r, nullptr); - } - else { - // t_pr is a proof for (m_p ... t_old ...) == t - // e_pr is a proof for (m_p ... e_old ...) == e - expr_ref old(m_manager); - expr_ref p_t_old(m_manager); - expr_ref p_e_old(m_manager); - old = mk_p_arg(n); // (m_p ... n ...) where n is (ite c t_old e_old) - p_t_old = mk_p_arg(t_old); // (m_p ... t_old ...) - p_e_old = mk_p_arg(e_old); // (m_p ... e_old ...) - expr_ref tmp1(m_manager); - tmp1 = m_manager.mk_ite(c, p_t_old, p_e_old); // (ite c (m_p ... t_old ...) (m_p ... e_old ...)) - proof * pr1 = m_manager.mk_rewrite(old, tmp1); // proof for (m_p ... (ite c t_old e_old) ...) = (ite c (m_p ... t_old ...) (m_p ... e_old ...)) - expr_ref tmp2(m_manager); - tmp2 = m_manager.mk_ite(c, t, e); // (ite c t e) - proof * pr2 = nullptr; // it will contain a proof for (ite c (m_p ... t_old ...) (m_p ... e_old ...)) = (ite c t e) - proof * pr3 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = (ite c t e) - proof * proofs[2]; - unsigned num_proofs = 0; - if (t_pr != nullptr) { - proofs[num_proofs] = t_pr; - num_proofs++; - } - if (e_pr != nullptr) { - proofs[num_proofs] = e_pr; - num_proofs++; - } - if (num_proofs > 0) { - pr2 = m_manager.mk_congruence(to_app(tmp1), to_app(tmp2), num_proofs, proofs); - pr3 = m_manager.mk_transitivity(pr1, pr2); - } - else { - pr3 = pr1; - } - proof * pr4 = nullptr; // it will contain a proof for (ite c t e) = r - proof * pr5 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = r - if (tmp2 != r) { - pr4 = m_manager.mk_rewrite(tmp2, r); - pr5 = m_manager.mk_transitivity(pr3, pr4); - } - else { - pr5 = pr3; - } - cache_result(n, r, pr5); - } - } - else { - expr_ref r(m_manager); - m_args[m_arg_idx] = n; - r = m_rewriter.mk_app(m_p, m_args.size(), m_args.c_ptr()); - if (!m_manager.proofs_enabled()) { - // expr * r = m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr()); - cache_result(n, r, nullptr); - } - else { - expr_ref old(m_manager); - proof * p; - old = mk_p_arg(n); - if (old == r) - p = nullptr; - else - p = m_manager.mk_rewrite(old, r); - cache_result(n, r, p); - } - } -} - -void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) { - unsigned num_args = n->get_num_args(); - m_args.resize(num_args); - m_p = n->get_decl(); - expr * ite = nullptr; - for (unsigned i = 0; i < num_args; i++) { - expr * arg = n->get_arg(i); - if (ite) { - m_args[i] = arg; - } - else if (m_manager.is_ite(arg)) { - m_arg_idx = i; - m_args[i] = 0; - ite = arg; - } - else { - m_args[i] = arg; - } - } - if (!ite) { - r = n; - pr = nullptr; - return; - } - m_todo.push_back(ite); - while (!m_todo.empty()) { - expr * n = m_todo.back(); - if (is_cached(n)) - m_todo.pop_back(); - else if (visit_children(n)) { - m_todo.pop_back(); - reduce(n); - } - } - SASSERT(is_cached(ite)); - expr * _r = nullptr; - proof * _pr = nullptr; - get_cached(ite, _r, _pr); - r = to_app(_r); - pr = _pr; - m_cache.reset(); - m_todo.reset(); -} - - - -pull_ite_tree_cfg::pull_ite_tree_cfg(ast_manager & m): - m(m), - m_trail(m), - m_proc(m) { -} - -bool pull_ite_tree_cfg::get_subst(expr * n, expr* & r, proof* & p) { - if (is_app(n) && is_target(to_app(n))) { - app_ref tmp(m); - proof_ref pr(m); - m_proc(to_app(n), tmp, pr); - if (tmp != n) { - r = tmp; - p = pr; - m_trail.push_back(r); - m_trail.push_back(p); - return true; - } - } - return false; -} - -bool pull_cheap_ite_tree_cfg::is_target(app * n) const { - bool r = - n->get_num_args() == 2 && - n->get_family_id() != null_family_id && - m.is_bool(n) && - (m.is_value(n->get_arg(0)) || m.is_value(n->get_arg(1))) && - (m.is_term_ite(n->get_arg(0)) || m.is_term_ite(n->get_arg(1))); - TRACE("pull_ite_target", tout << mk_pp(n, m) << "\nresult: " << r << "\n";); - return r; -} - - - - - - diff --git a/src/ast/rewriter/pull_ite_tree.h b/src/ast/rewriter/pull_ite_tree.h deleted file mode 100644 index ea462315a..000000000 --- a/src/ast/rewriter/pull_ite_tree.h +++ /dev/null @@ -1,113 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - pull_ite_tree.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-22. - -Revision History: - ---*/ -#ifndef PULL_ITE_TREE_H_ -#define PULL_ITE_TREE_H_ - -#include "ast/ast.h" -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/th_rewriter.h" -#include "ast/expr_map.h" -#include "ast/recurse_expr.h" -#include "util/obj_hashtable.h" - -/** - \brief Functor for applying the following transformation - F[(p (ite c t1 t2) args)] = F'[(ite c t1 t2), p, args] - - F'[(ite c t1 t2), p, args] = (ite c F'[t1, p, args] F'[t2, p, args]) - F'[t, p, args] = (p t args) -*/ -class pull_ite_tree { - ast_manager & m_manager; - th_rewriter m_rewriter; - func_decl * m_p; - ptr_vector m_args; - unsigned m_arg_idx; //!< position of the ite argument - expr_map m_cache; - ptr_vector m_todo; - - bool is_cached(expr * n) const { return m_cache.contains(n); } - void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); } - void cache_result(expr * n, expr * r, proof * pr); - void visit(expr * n, bool & visited); - bool visit_children(expr * n); - void reduce(expr * n); - /** - \brief Creante an application (m_p ... n ...) where n is the argument m_arg_idx and the other arguments - are in m_args. - */ - expr * mk_p_arg(expr * n) { - m_args[m_arg_idx] = n; - return m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr()); - } -public: - pull_ite_tree(ast_manager & m); - /** - \brief Apply the transformation above if n contains an ite-expression. - Store the result in r. If n does not contain an ite-expression, then - store n in r. - - When proof generation is enabled, pr is a proof for n = r. - */ - void operator()(app * n, app_ref & r, proof_ref & pr); -}; - -/** - \brief Functor for applying the pull_ite_tree on subexpressions n that - satisfy the is_target virtual predicate. -*/ -class pull_ite_tree_cfg : public default_rewriter_cfg { -protected: - ast_manager& m; - expr_ref_vector m_trail; - pull_ite_tree m_proc; -public: - pull_ite_tree_cfg(ast_manager & m); - virtual ~pull_ite_tree_cfg() {} - virtual bool is_target(app * n) const = 0; - bool get_subst(expr * n, expr* & r, proof* & p); -}; - -/** - \brief Apply pull_ite_tree on predicates of the form - (p ite v) and (p v ite) - - where: - - p is an interpreted predicate - - ite is an ite-term expression - - v is a value -*/ -class pull_cheap_ite_tree_cfg : public pull_ite_tree_cfg { -public: - pull_cheap_ite_tree_cfg(ast_manager & m):pull_ite_tree_cfg(m) {} - ~pull_cheap_ite_tree_cfg() override {} - bool is_target(app * n) const override; -}; - -class pull_cheap_ite_tree_rw : public rewriter_tpl { - pull_cheap_ite_tree_cfg m_cfg; -public: - pull_cheap_ite_tree_rw(ast_manager& m): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m) - {} -}; - -#endif /* PULL_ITE_TREE_H_ */ - diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 465371434..5903fefcb 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -46,7 +46,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m_refine_inj_axiom(*this), m_max_bv_sharing_fn(*this), m_elim_term_ite(*this), - m_pull_cheap_ite_trees(*this), m_pull_nested_quantifiers(*this), m_elim_bvs_from_quantifiers(*this), m_cheap_quant_fourier_motzkin(*this), @@ -122,7 +121,7 @@ void asserted_formulas::set_eliminate_and(bool flag) { if (flag == m_elim_and) return; m_elim_and = flag; params_ref p; - p.set_bool("pull_cheap_ite", false); + if (m_params.m_pull_cheap_ite) p.set_bool("pull_cheap_ite", true); p.set_bool("elim_and", flag); p.set_bool("arith_ineq_lhs", true); p.set_bool("sort_sums", true); @@ -241,7 +240,6 @@ void asserted_formulas::reduce() { if (!invoke(m_nnf_cnf)) return; set_eliminate_and(true); if (!invoke(m_reduce_asserted_formulas)) return; - if (!invoke(m_pull_cheap_ite_trees)) return; if (!invoke(m_pull_nested_quantifiers)) return; if (!invoke(m_lift_ite)) return; if (!invoke(m_ng_lift_ite)) return; diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index a67b975eb..275687adb 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -26,7 +26,6 @@ Revision History: #include "ast/rewriter/bit2int.h" #include "ast/rewriter/maximize_ac_sharing.h" #include "ast/rewriter/distribute_forall.h" -#include "ast/rewriter/pull_ite_tree.h" #include "ast/rewriter/push_app_ite.h" #include "ast/rewriter/inj_axiom.h" #include "ast/rewriter/bv_elim.h" @@ -172,7 +171,6 @@ class asserted_formulas { #define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE) - MK_SIMPLIFIERF(pull_cheap_ite_trees, pull_cheap_ite_tree_rw, "pull-cheap-ite-trees", af.m_params.m_pull_cheap_ite_trees, false); MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false); MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true); MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true); @@ -187,7 +185,6 @@ class asserted_formulas { refine_inj_axiom_fn m_refine_inj_axiom; max_bv_sharing_fn m_max_bv_sharing_fn; elim_term_ite_fn m_elim_term_ite; - pull_cheap_ite_trees m_pull_cheap_ite_trees; pull_nested_quantifiers m_pull_nested_quantifiers; elim_bvs_from_quantifiers m_elim_bvs_from_quantifiers; cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin; @@ -219,7 +216,6 @@ class asserted_formulas { bool is_gt(expr* lhs, expr* rhs); void compute_depth(expr* e); unsigned depth(expr* e) { return m_expr2depth[e]; } - bool pull_cheap_ite_trees(); void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 93ea794fa..ee4b7c2e4 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -41,7 +41,7 @@ void preprocessor_params::display(std::ostream & out) const { DISPLAY_PARAM(m_lift_ite); DISPLAY_PARAM(m_ng_lift_ite); - DISPLAY_PARAM(m_pull_cheap_ite_trees); + DISPLAY_PARAM(m_pull_cheap_ite); DISPLAY_PARAM(m_pull_nested_quantifiers); DISPLAY_PARAM(m_eliminate_term_ite); DISPLAY_PARAM(m_macro_finder); diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index dc16d6244..be7fd4c01 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -32,7 +32,7 @@ struct preprocessor_params : public pattern_inference_params, public bit_blaster_params { lift_ite_kind m_lift_ite; lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms - bool m_pull_cheap_ite_trees; + bool m_pull_cheap_ite; bool m_pull_nested_quantifiers; bool m_eliminate_term_ite; bool m_macro_finder; @@ -54,7 +54,7 @@ public: preprocessor_params(params_ref const & p = params_ref()): m_lift_ite(LI_NONE), m_ng_lift_ite(LI_NONE), - m_pull_cheap_ite_trees(false), + m_pull_cheap_ite(false), m_pull_nested_quantifiers(false), m_eliminate_term_ite(false), m_macro_finder(false), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index bbc91e4c6..383d98e67 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -507,7 +507,7 @@ namespace smt { m_params.m_nnf_cnf = false; if (st.m_max_ite_tree_depth > 50) { m_params.m_arith_eq2ineq = false; - m_params.m_pull_cheap_ite_trees = true; + m_params.m_pull_cheap_ite = true; m_params.m_arith_propagate_eqs = true; m_params.m_relevancy_lvl = 2; m_params.m_relevancy_lemma = false;