From f91496f5fff77ad04647ff3c9f350a8e92a3641c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Aug 2017 16:56:55 -0700
Subject: [PATCH] pruning simplifier dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifier/pull_ite_tree.cpp | 10 +++++-----
 src/ast/simplifier/pull_ite_tree.h   |  5 +++--
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/ast/simplifier/pull_ite_tree.cpp b/src/ast/simplifier/pull_ite_tree.cpp
index 072bbd12c..a092f9649 100644
--- a/src/ast/simplifier/pull_ite_tree.cpp
+++ b/src/ast/simplifier/pull_ite_tree.cpp
@@ -21,9 +21,9 @@ Revision History:
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
 
-pull_ite_tree::pull_ite_tree(ast_manager & m, simplifier & s):
+pull_ite_tree::pull_ite_tree(ast_manager & m):
     m_manager(m),
-    m_simplifier(s),
+    m_rewriter(m),
     m_cache(m) {
 }
 
@@ -64,7 +64,7 @@ void pull_ite_tree::reduce(expr * n) {
         get_cached(e_old, e, e_pr);
         expr_ref r(m_manager);
         expr * args[3] = {c, t, e};
-        m_simplifier.mk_app(to_app(n)->get_decl(), 3, args, r);
+        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);
@@ -117,7 +117,7 @@ void pull_ite_tree::reduce(expr * n) {
     else {
         expr_ref r(m_manager);
         m_args[m_arg_idx] = n;
-        m_simplifier.mk_app(m_p, m_args.size(), m_args.c_ptr(), r);
+        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);
@@ -181,7 +181,7 @@ void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
 
 pull_ite_tree_star::pull_ite_tree_star(ast_manager & m, simplifier & s):
     simplifier(m),
-    m_proc(m, s) {
+    m_proc(m) {
     borrow_plugins(s);
 }
 
diff --git a/src/ast/simplifier/pull_ite_tree.h b/src/ast/simplifier/pull_ite_tree.h
index bc4a0bb68..4b35c124a 100644
--- a/src/ast/simplifier/pull_ite_tree.h
+++ b/src/ast/simplifier/pull_ite_tree.h
@@ -20,6 +20,7 @@ Revision History:
 #define PULL_ITE_TREE_H_
 
 #include "ast/ast.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/simplifier/simplifier.h"
 #include "ast/recurse_expr.h"
 #include "util/obj_hashtable.h"
@@ -34,7 +35,7 @@ Revision History:
 */
 class pull_ite_tree {
     ast_manager &         m_manager;
-    simplifier &          m_simplifier;
+    th_rewriter           m_rewriter;
     func_decl *           m_p;
     ptr_vector<expr>      m_args;
     unsigned              m_arg_idx; //!< position of the ite argument
@@ -56,7 +57,7 @@ class pull_ite_tree {
         return m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
     }
 public:
-    pull_ite_tree(ast_manager & m, simplifier & s);
+    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