From b6c43f6143f07de5eae4a76fc62fe26d8d1b41b1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 15 Jun 2018 15:13:55 -0700
Subject: [PATCH] move files for build script

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_project.py                       | 2 +-
 src/ast/CMakeLists.txt                      | 1 -
 src/ast/rewriter/CMakeLists.txt             | 1 +
 src/ast/{ => rewriter}/factor_equivs.cpp    | 3 ++-
 src/ast/{ => rewriter}/factor_equivs.h      | 0
 src/muz/spacer/spacer_generalizers.cpp      | 2 +-
 src/muz/spacer/spacer_legacy_frames.cpp     | 2 +-
 src/muz/spacer/spacer_quant_generalizer.cpp | 2 +-
 src/muz/spacer/spacer_util.cpp              | 2 +-
 9 files changed, 8 insertions(+), 7 deletions(-)
 rename src/ast/{ => rewriter}/factor_equivs.cpp (98%)
 rename src/ast/{ => rewriter}/factor_equivs.h (100%)

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 22b640305..dada93069 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -41,7 +41,6 @@ def init_project_def():
     add_lib('aig_tactic', ['tactic'], 'tactic/aig')
     add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
     add_lib('cmd_context', ['solver', 'rewriter'])
-    add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
@@ -74,6 +73,7 @@ def init_project_def():
     API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h']
     add_lib('api', ['portfolio',  'realclosure', 'opt'],
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
+    add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)
     _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt
index 4dcdd2a35..80543bb05 100644
--- a/src/ast/CMakeLists.txt
+++ b/src/ast/CMakeLists.txt
@@ -24,7 +24,6 @@ z3_add_component(ast
     expr_map.cpp
     expr_stat.cpp
     expr_substitution.cpp
-    factor_equivs.cpp
     for_each_ast.cpp
     for_each_expr.cpp
     format.cpp
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index f030e2704..9d80fd5ac 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -16,6 +16,7 @@ z3_add_component(rewriter
     enum2bv_rewriter.cpp
     expr_replacer.cpp
     expr_safe_replace.cpp
+    factor_equivs.cpp
     factor_rewriter.cpp
     fpa_rewriter.cpp
     inj_axiom.cpp
diff --git a/src/ast/factor_equivs.cpp b/src/ast/rewriter/factor_equivs.cpp
similarity index 98%
rename from src/ast/factor_equivs.cpp
rename to src/ast/rewriter/factor_equivs.cpp
index be402e628..6384ad8ce 100644
--- a/src/ast/factor_equivs.cpp
+++ b/src/ast/rewriter/factor_equivs.cpp
@@ -25,11 +25,12 @@ Revision History:
 
 */
 
-#include "ast/factor_equivs.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include "ast/rewriter/factor_equivs.h"
+
 /**
    Factors input vector v into equivalence classes and the rest
  */
diff --git a/src/ast/factor_equivs.h b/src/ast/rewriter/factor_equivs.h
similarity index 100%
rename from src/ast/factor_equivs.h
rename to src/ast/rewriter/factor_equivs.h
diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index 4e5b60698..b0fb6c2d3 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -25,7 +25,7 @@ Revision History:
 #include "ast/expr_abstract.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/for_each_expr.h"
-#include "ast/factor_equivs.h"
+#include "ast/rewriter/factor_equivs.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/substitution/matcher.h"
 #include "ast/expr_functors.h"
diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp
index 49157a085..a21df5038 100644
--- a/src/muz/spacer/spacer_legacy_frames.cpp
+++ b/src/muz/spacer/spacer_legacy_frames.cpp
@@ -34,7 +34,7 @@
 #include "util/luby.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_abstract.h"
-#include "ast/factor_equivs.h"
+#include "ast/rewriter/factor_equivs.h"
 
 
 namespace spacer {
diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp
index fb2964c40..f66fe7b29 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -26,7 +26,7 @@ Revision History:
 #include "ast/expr_abstract.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/for_each_expr.h"
-#include "ast/factor_equivs.h"
+#include "ast/rewriter/factor_equivs.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/substitution/matcher.h"
 #include "ast/expr_functors.h"
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 29d72fabd..f53577b5b 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -64,7 +64,7 @@ Notes:
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/arith/arith_bounds_tactic.h"
 
-#include "ast/factor_equivs.h"
+#include "ast/rewriter/factor_equivs.h"
 #include "qe/qe_term_graph.h"
 
 namespace spacer {