move pull/push files

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

src/ast/rewriter/CMakeLists.txt

@@ -19,6 +19,8 @@ z3_add_component(rewriter
     mk_simplified_app.cpp
     pb_rewriter.cpp
     pb2bv_rewriter.cpp
+    push_app_ite.cpp
+    pull_ite_tree.cpp
     quant_hoist.cpp
     rewriter.cpp
     seq_rewriter.cpp

src/ast/rewriter/pull_ite_tree.cpp

@@ -0,0 +1,249 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    pull_ite_tree.cpp
+
+Abstract:
+
+    <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     = 0;
+        proof * t_pr = 0;
+        expr * e     = 0;
+        proof * e_pr = 0;
+        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, 0);
+        }
+        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 = 0; // it will contain a proof for (ite c (m_p ... t_old ...) (m_p ... e_old ...)) = (ite c t e)
+            proof * pr3 = 0; // 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 != 0) {
+                proofs[num_proofs] = t_pr;
+                num_proofs++;
+            }
+            if (e_pr != 0) {
+                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 = 0; // it will contain a proof for (ite c t e) = r
+            proof * pr5 = 0; // 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, 0);
+        }
+        else {
+            expr_ref old(m_manager);
+            proof * p;
+            old = mk_p_arg(n);
+            if (old == r)
+                p = 0;
+            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 = 0;
+    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 = 0;
+        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 = 0;
+    proof * _pr = 0;
+    get_cached(ite, _r, _pr);
+    r  = to_app(_r);
+    pr = _pr;
+    m_cache.reset();
+    m_todo.reset();
+}
+
+pull_ite_tree_star::pull_ite_tree_star(ast_manager & m, simplifier & s):
+    simplifier(m),
+    m_proc(m) {
+    borrow_plugins(s);
+}
+
+bool pull_ite_tree_star::get_subst(expr * n, expr_ref & r, proof_ref & p) {
+    if (is_app(n) && is_target(to_app(n))) {
+        app_ref tmp(m);
+        m_proc(to_app(n), tmp, p);
+        r = tmp;
+        return true;
+    }
+    return false;
+}
+
+bool pull_cheap_ite_tree_star::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;
+}
+
+
+
+
+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/rewriter/pull_ite_tree.h

@@ -0,0 +1,144 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    pull_ite_tree.h
+
+Abstract:
+
+    <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/simplifier/simplifier.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<expr>      m_args;
+    unsigned              m_arg_idx; //!< position of the ite argument
+    expr_map              m_cache;
+    ptr_vector<expr>      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_star : public simplifier {
+protected:
+    pull_ite_tree m_proc;
+    virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
+public:
+    pull_ite_tree_star(ast_manager & m, simplifier & s);
+    virtual ~pull_ite_tree_star() { release_plugins(); }
+    virtual bool is_target(app * n) const = 0;
+};
+
+/**
+   \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_star : public pull_ite_tree_star {
+public:
+    pull_cheap_ite_tree_star(ast_manager & m, simplifier & s):pull_ite_tree_star(m, s) {}
+    virtual ~pull_cheap_ite_tree_star() {}
+    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/rewriter/push_app_ite.cpp

@@ -0,0 +1,281 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    push_app_ite.cpp
+
+Abstract:
+
+    TODO: Write a better ite lifter
+
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-05-14.
+
+Revision History:
+
+--*/
+#include "ast/rewriter/push_app_ite.h"
+#include "ast/ast_pp.h"
+
+push_app_ite::push_app_ite(simplifier & s, bool conservative):
+    simplifier(s.get_manager()),
+    m_conservative(conservative) {
+
+    borrow_plugins(s);
+}
+
+push_app_ite::~push_app_ite() {
+    // the plugins were borrowed. So, release ownership.
+    m_plugins.release();
+}
+
+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;
+    return -1;
+}
+
+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(m, num_args, args);
+    if (ite_arg_idx < 0) {
+        mk_app(decl, num_args, args, r);
+        return;
+    }
+    app * ite               = to_app(args[ite_arg_idx]);
+    expr * c                = ite->get_arg(0);
+    expr * t                = ite->get_arg(1);
+    expr * e                = ite->get_arg(2);
+    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);
+    apply(decl, num_args, args_prime, t_new);
+    args_prime[ite_arg_idx] = e;
+    expr_ref e_new(m);
+    apply(decl, num_args, args_prime, e_new);
+    args_prime[ite_arg_idx] = old;
+    expr * new_args[3] = { c, t_new, e_new };
+    mk_app(ite->get_decl(), 3, new_args, r);
+}
+
+/**
+   \brief Default (conservative) implementation. Return true if there one and only one ite-term argument.
+*/
+bool push_app_ite::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;
+}
+
+void push_app_ite::operator()(expr * s, expr_ref & r, proof_ref & p) {
+    expr  * result;
+    proof * result_proof;
+    reduce_core(s);
+    get_cached(s, result, result_proof);
+    r = result;
+    switch (m.proof_mode()) {
+    case PGM_DISABLED:
+        p = m.mk_undef_proof();
+        break;
+    case PGM_COARSE:
+        if (result == s)
+            p = m.mk_reflexivity(s);
+        else
+            p = m.mk_rewrite_star(s, result, 0, 0);
+        break;
+    case PGM_FINE:
+        if (result == s)
+            p = m.mk_reflexivity(s);
+        else
+            p = result_proof;
+        break;
+    }
+}
+
+void push_app_ite::reduce_core(expr * n) {
+    if (!is_cached(n)) {
+        unsigned sz = m_todo.size();
+        m_todo.push_back(n);
+        while (m_todo.size() != sz) {
+            expr * n = m_todo.back();
+            if (is_cached(n))
+                m_todo.pop_back();
+            else if (visit_children(n)) {
+                m_todo.pop_back();
+                reduce1(n);
+            }
+        }
+    }
+}
+
+bool push_app_ite::visit_children(expr * n) {
+    bool visited = true;
+    unsigned j;
+    switch(n->get_kind()) {
+    case AST_VAR:
+        return true;
+    case AST_APP:
+        j = to_app(n)->get_num_args();
+        while (j > 0) {
+            --j;
+            visit(to_app(n)->get_arg(j), visited);
+        }
+        return visited;
+    case AST_QUANTIFIER: 
+        visit(to_quantifier(n)->get_expr(), visited);
+        return visited;
+    default:
+        UNREACHABLE();
+        return true;
+    }
+}
+
+void push_app_ite::reduce1(expr * n) {
+    switch (n->get_kind()) {
+    case AST_VAR:
+        cache_result(n, n, 0);
+        break;
+    case AST_APP:
+        reduce1_app(to_app(n));
+        break;
+    case AST_QUANTIFIER:
+        reduce1_quantifier(to_quantifier(n));
+        break;
+    default:
+        UNREACHABLE();
+    }
+}
+
+void push_app_ite::reduce1_app(app * n) {
+    m_args.reset();
+    
+    func_decl * decl = n->get_decl();
+    proof_ref p1(m);
+    get_args(n, m_args, p1);
+
+    expr_ref r(m);
+    if (is_target(decl, m_args.size(), m_args.c_ptr()))
+        apply(decl, m_args.size(), m_args.c_ptr(), r);
+    else
+        mk_app(decl, m_args.size(), m_args.c_ptr(), r);
+    
+    if (!m.fine_grain_proofs())
+        cache_result(n, r, 0);
+    else {
+        expr * s = m.mk_app(decl, m_args.size(), m_args.c_ptr());
+        proof * p;
+        if (n == r)
+            p = 0;
+        else if (r != s) 
+            p = m.mk_transitivity(p1, m.mk_rewrite(s, r));
+        else
+            p = p1;
+        cache_result(n, r, p);
+    }
+}
+
+void push_app_ite::reduce1_quantifier(quantifier * q) {
+    expr *  new_body;
+    proof * new_body_pr;
+    get_cached(q->get_expr(), new_body, new_body_pr);
+    
+    quantifier * new_q = m.update_quantifier(q, new_body);
+    proof *      p     = q == new_q ? 0 : m.mk_quant_intro(q, new_q, new_body_pr);   
+    cache_result(q, new_q, p);
+}
+
+bool ng_push_app_ite::is_target(func_decl * decl, unsigned num_args, expr * const * args) {
+    bool r = push_app_ite::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;
+}
+
+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/rewriter/push_app_ite.h

@@ -0,0 +1,104 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    push_app_ite.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-05-14.
+
+Revision History:
+
+--*/
+#ifndef PUSH_APP_ITE_H_
+#define PUSH_APP_ITE_H_
+
+#include "ast/ast.h"
+#include "ast/simplifier/simplifier.h"
+#include "ast/rewriter/rewriter.h"
+
+/**
+   \brief Functor for applying the following transformation:
+
+   (f s (ite c t1 t2)) ==> (ite c (f s t1) (f s t2))
+*/
+class push_app_ite : public simplifier {
+protected:
+    bool          m_conservative;
+    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);
+    bool visit_children(expr * n);
+    void reduce1(expr * n);
+    void reduce1_app(app * n);
+    void reduce1_quantifier(quantifier * q);
+
+public:
+    push_app_ite(simplifier & s, bool conservative = true);
+    virtual ~push_app_ite();
+    void operator()(expr * s, expr_ref & r, proof_ref & p);
+};
+
+/**
+   \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 : public push_app_ite {
+protected:
+    virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
+public:
+    ng_push_app_ite(simplifier & s, bool conservative = true);
+    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_ */
+