From 8b2d60e3caceb6c6803d653c7e8a48b3b6e587b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Aug 2017 17:57:03 -0700 Subject: [PATCH] using rewrite in push_app_ite Signed-off-by: Nikolaj Bjorner --- src/ast/simplifier/pull_ite_tree.cpp | 36 +++++++++++++++ src/ast/simplifier/pull_ite_tree.h | 44 ++++++++++++++++++- src/ast/simplifier/push_app_ite.cpp | 65 +++++++++++++++++++++++++++- src/ast/simplifier/push_app_ite.h | 43 +++++++++++++++++- src/smt/asserted_formulas.cpp | 6 +-- 5 files changed, 187 insertions(+), 7 deletions(-) diff --git a/src/ast/simplifier/pull_ite_tree.cpp b/src/ast/simplifier/pull_ite_tree.cpp index a092f9649..c317cafd8 100644 --- a/src/ast/simplifier/pull_ite_tree.cpp +++ b/src/ast/simplifier/pull_ite_tree.cpp @@ -209,5 +209,41 @@ bool pull_cheap_ite_tree_star::is_target(app * n) const { +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/simplifier/pull_ite_tree.h b/src/ast/simplifier/pull_ite_tree.h index 4b35c124a..37837a3cf 100644 --- a/src/ast/simplifier/pull_ite_tree.h +++ b/src/ast/simplifier/pull_ite_tree.h @@ -20,11 +20,12 @@ Revision History: #define PULL_ITE_TREE_H_ #include "ast/ast.h" +#include "ast/rewriter/rewriter.h" #include "ast/rewriter/th_rewriter.h" #include "ast/simplifier/simplifier.h" +#include "ast/expr_map.h" #include "ast/recurse_expr.h" #include "util/obj_hashtable.h" -#include "ast/expr_map.h" /** \brief Functor for applying the following transformation @@ -98,5 +99,46 @@ public: virtual bool is_target(app * n) const; }; +/** + \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) {} + virtual ~pull_cheap_ite_tree_cfg() {} + virtual bool is_target(app * n) const; +}; + +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/ast/simplifier/push_app_ite.cpp b/src/ast/simplifier/push_app_ite.cpp index 8b56dcd85..3d118e4ac 100644 --- a/src/ast/simplifier/push_app_ite.cpp +++ b/src/ast/simplifier/push_app_ite.cpp @@ -32,7 +32,7 @@ push_app_ite::~push_app_ite() { m_plugins.release(); } -int push_app_ite::has_ite_arg(unsigned num_args, expr * const * args) { +static int has_ite_arg(ast_manager& m, unsigned num_args, expr * const * args) { for (unsigned i = 0; i < num_args; i++) if (m.is_ite(args[i])) return i; @@ -41,7 +41,7 @@ int push_app_ite::has_ite_arg(unsigned num_args, expr * const * args) { void push_app_ite::apply(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & r) { TRACE("push_app_ite", tout << "pushing app...\n";); - int ite_arg_idx = has_ite_arg(num_args, args); + int ite_arg_idx = has_ite_arg(m, num_args, args); if (ite_arg_idx < 0) { mk_app(decl, num_args, args, r); return; @@ -218,3 +218,64 @@ bool ng_push_app_ite::is_target(func_decl * decl, unsigned num_args, expr * cons ng_push_app_ite::ng_push_app_ite(simplifier & s, bool conservative): push_app_ite(s, conservative) { } + + +/** + \brief Default (conservative) implementation. Return true if there one and only one ite-term argument. +*/ +bool push_app_ite_cfg::is_target(func_decl * decl, unsigned num_args, expr * const * args) { + if (m.is_ite(decl)) + return false; + bool found_ite = false; + for (unsigned i = 0; i < num_args; i++) { + if (m.is_ite(args[i]) && !m.is_bool(args[i])) { + if (found_ite) { + if (m_conservative) + return false; + } + else { + found_ite = true; + } + } + } + CTRACE("push_app_ite", found_ite, tout << "found target for push app ite:\n"; + tout << decl->get_name(); + for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m); + tout << "\n";); + return found_ite; +} + +br_status push_app_ite_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if (!is_target(f, num, args)) { + return BR_FAILED; + } + int ite_arg_idx = has_ite_arg(m, num, args); + if (ite_arg_idx < 0) { + return BR_FAILED; + } + app * ite = to_app(args[ite_arg_idx]); + expr * c = 0, * t = 0, * e = 0; + VERIFY(m.is_ite(ite, c, t, e)); + expr ** args_prime = const_cast(args); + expr * old = args_prime[ite_arg_idx]; + args_prime[ite_arg_idx] = t; + expr_ref t_new(m.mk_app(f, num, args_prime), m); + args_prime[ite_arg_idx] = e; + expr_ref e_new(m.mk_app(f, num, args_prime), m); + args_prime[ite_arg_idx] = old; + result = m.mk_ite(c, t_new, e_new); + if (m.proofs_enabled()) { + result_pr = m.mk_rewrite(m.mk_app(f, num, args), result); + } + return BR_REWRITE2; +} + +bool ng_push_app_ite_cfg::is_target(func_decl * decl, unsigned num_args, expr * const * args) { + bool r = push_app_ite_cfg::is_target(decl, num_args, args); + if (!r) + return false; + for (unsigned i = 0; i < num_args; i++) + if (!is_ground(args[i])) + return true; + return false; +} diff --git a/src/ast/simplifier/push_app_ite.h b/src/ast/simplifier/push_app_ite.h index 96400b1af..4faf853ea 100644 --- a/src/ast/simplifier/push_app_ite.h +++ b/src/ast/simplifier/push_app_ite.h @@ -21,6 +21,7 @@ Revision History: #include "ast/ast.h" #include "ast/simplifier/simplifier.h" +#include "ast/rewriter/rewriter.h" /** \brief Functor for applying the following transformation: @@ -30,7 +31,6 @@ Revision History: class push_app_ite : public simplifier { protected: bool m_conservative; - int has_ite_arg(unsigned num_args, expr * const * args); void apply(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result); virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args); void reduce_core(expr * n); @@ -59,5 +59,46 @@ public: virtual ~ng_push_app_ite() {} }; +struct push_app_ite_cfg : public default_rewriter_cfg { + ast_manager& m; + bool m_conservative; + virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args); + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr); + push_app_ite_cfg(ast_manager& m, bool conservative = true): m(m), m_conservative(conservative) {} +}; + +/** + \brief Variation of push_app_ite that applies the transformation on nonground terms only. + + \remark This functor uses the app::is_ground method. This method is not + completly precise, for instance, any term containing a quantifier is marked as non ground. +*/ +class ng_push_app_ite_cfg : public push_app_ite_cfg { +protected: + virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args); +public: + ng_push_app_ite_cfg(ast_manager& m, bool conservative = true): push_app_ite_cfg(m, conservative) {} + virtual ~ng_push_app_ite_cfg() {} +}; + +struct push_app_ite_rw : public rewriter_tpl { + push_app_ite_cfg m_cfg; +public: + push_app_ite_rw(ast_manager& m, bool conservative = true): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, conservative) + {} +}; + +struct ng_push_app_ite_rw : public rewriter_tpl { + ng_push_app_ite_cfg m_cfg; +public: + ng_push_app_ite_rw(ast_manager& m, bool conservative = true): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, conservative) + {} +}; + + #endif /* PUSH_APP_ITE_H_ */ diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 26265a6f8..b475ee778 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -755,7 +755,7 @@ void asserted_formulas::propagate_booleans() { return changed; \ } -MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); +MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_rw functor(m), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m), "pull_nested_quantifiers", "pull-nested-quantifiers", false); @@ -830,8 +830,8 @@ MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "el reduce_and_solve(); \ } -LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite"); -LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite"); +LIFT_ITE(lift_ite, push_app_ite_rw functor(m, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite"); +LIFT_ITE(ng_lift_ite, ng_push_app_ite_rw functor(m, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite"); unsigned asserted_formulas::get_total_size() const { expr_mark visited;