From 23d1c0a9a8a7167992e6a823ed3affd93d7f2bc1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Aug 2017 11:13:01 -0700
Subject: [PATCH] move pull/push files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/CMakeLists.txt                    | 2 ++
 src/ast/{simplifier => rewriter}/pull_ite_tree.cpp | 2 +-
 src/ast/{simplifier => rewriter}/pull_ite_tree.h   | 0
 src/ast/{simplifier => rewriter}/push_app_ite.cpp  | 2 +-
 src/ast/{simplifier => rewriter}/push_app_ite.h    | 0
 src/ast/simplifier/CMakeLists.txt                  | 2 --
 src/smt/asserted_formulas.cpp                      | 4 ++--
 7 files changed, 6 insertions(+), 6 deletions(-)
 rename src/ast/{simplifier => rewriter}/pull_ite_tree.cpp (99%)
 rename src/ast/{simplifier => rewriter}/pull_ite_tree.h (100%)
 rename src/ast/{simplifier => rewriter}/push_app_ite.cpp (99%)
 rename src/ast/{simplifier => rewriter}/push_app_ite.h (100%)

diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index abf09ff0c..72bca53d4 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/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
diff --git a/src/ast/simplifier/pull_ite_tree.cpp b/src/ast/rewriter/pull_ite_tree.cpp
similarity index 99%
rename from src/ast/simplifier/pull_ite_tree.cpp
rename to src/ast/rewriter/pull_ite_tree.cpp
index c317cafd8..bcb672ea7 100644
--- a/src/ast/simplifier/pull_ite_tree.cpp
+++ b/src/ast/rewriter/pull_ite_tree.cpp
@@ -16,7 +16,7 @@ Author:
 Revision History:
 
 --*/
-#include "ast/simplifier/pull_ite_tree.h"
+#include "ast/rewriter/pull_ite_tree.h"
 #include "ast/recurse_expr_def.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
diff --git a/src/ast/simplifier/pull_ite_tree.h b/src/ast/rewriter/pull_ite_tree.h
similarity index 100%
rename from src/ast/simplifier/pull_ite_tree.h
rename to src/ast/rewriter/pull_ite_tree.h
diff --git a/src/ast/simplifier/push_app_ite.cpp b/src/ast/rewriter/push_app_ite.cpp
similarity index 99%
rename from src/ast/simplifier/push_app_ite.cpp
rename to src/ast/rewriter/push_app_ite.cpp
index 3d118e4ac..fe6f8b408 100644
--- a/src/ast/simplifier/push_app_ite.cpp
+++ b/src/ast/rewriter/push_app_ite.cpp
@@ -17,7 +17,7 @@ Author:
 Revision History:
 
 --*/
-#include "ast/simplifier/push_app_ite.h"
+#include "ast/rewriter/push_app_ite.h"
 #include "ast/ast_pp.h"
 
 push_app_ite::push_app_ite(simplifier & s, bool conservative):
diff --git a/src/ast/simplifier/push_app_ite.h b/src/ast/rewriter/push_app_ite.h
similarity index 100%
rename from src/ast/simplifier/push_app_ite.h
rename to src/ast/rewriter/push_app_ite.h
diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt
index 9575c5c89..c5c310c07 100644
--- a/src/ast/simplifier/CMakeLists.txt
+++ b/src/ast/simplifier/CMakeLists.txt
@@ -15,8 +15,6 @@ z3_add_component(simplifier
     inj_axiom.cpp
     maximise_ac_sharing.cpp
     poly_simplifier_plugin.cpp
-    pull_ite_tree.cpp
-    push_app_ite.cpp
     seq_simplifier_plugin.cpp
     simplifier.cpp
     simplifier_plugin.cpp
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index eac5f7c10..6f1c4cfcc 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -22,14 +22,14 @@ Revision History:
 #include "ast/for_each_expr.h"
 #include "ast/well_sorted.h"
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/pull_ite_tree.h"
+#include "ast/rewriter/push_app_ite.h"
 #include "ast/simplifier/arith_simplifier_plugin.h"
 #include "ast/simplifier/array_simplifier_plugin.h"
 #include "ast/simplifier/datatype_simplifier_plugin.h"
 #include "ast/simplifier/fpa_simplifier_plugin.h"
 #include "ast/simplifier/seq_simplifier_plugin.h"
 #include "ast/simplifier/bv_simplifier_plugin.h"
-#include "ast/simplifier/pull_ite_tree.h"
-#include "ast/simplifier/push_app_ite.h"
 #include "ast/simplifier/bv_elim.h"
 #include "ast/simplifier/inj_axiom.h"
 #include "ast/simplifier/elim_bounds.h"