using rewrite in push_app_ite

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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;
+}
+
+
+
+
 
 

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> {
+    pull_cheap_ite_tree_cfg m_cfg;
+public:
+    pull_cheap_ite_tree_rw(ast_manager& m):
+        rewriter_tpl<pull_cheap_ite_tree_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m)
+    {}
+};
+
 #endif /* PULL_ITE_TREE_H_ */
 

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<expr**>(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;
+}

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> {
+    push_app_ite_cfg m_cfg;
+public:
+    push_app_ite_rw(ast_manager& m, bool conservative = true):
+        rewriter_tpl<push_app_ite_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m, conservative)
+    {}
+};
+
+struct ng_push_app_ite_rw : public rewriter_tpl<ng_push_app_ite_cfg> {
+    ng_push_app_ite_cfg m_cfg;
+public:
+    ng_push_app_ite_rw(ast_manager& m, bool conservative = true):
+        rewriter_tpl<ng_push_app_ite_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m, conservative)
+    {}
+};
+
+
 #endif /* PUSH_APP_ITE_H_ */
 

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;