From ecd85b314c35652b1277a5f0c4689fe581c44e18 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 31 Jul 2017 17:57:21 -0400
Subject: [PATCH] more includes

---
 src/muz/spacer/spacer_itp_solver.cpp    | 14 +++----
 src/muz/spacer/spacer_itp_solver.h      |  6 +--
 src/muz/spacer/spacer_legacy_frames.cpp | 54 ++++++++++++------------
 src/muz/spacer/spacer_legacy_mbp.cpp    | 55 +++++++++++++------------
 src/muz/spacer/spacer_legacy_mev.cpp    | 52 +++++++++++------------
 src/muz/spacer/spacer_legacy_mev.h      | 20 ++++-----
 src/muz/spacer/spacer_manager.cpp       | 19 +++++----
 src/muz/spacer/spacer_manager.h         | 23 ++++++-----
 src/muz/spacer/spacer_marshal.cpp       | 13 +++---
 src/muz/spacer/spacer_marshal.h         |  3 +-
 src/muz/spacer/spacer_matrix.cpp        |  2 +-
 src/muz/spacer/spacer_matrix.h          |  3 +-
 src/muz/spacer/spacer_mev_array.cpp     | 26 ++++++------
 src/muz/spacer/spacer_mev_array.h       |  8 ++--
 14 files changed, 152 insertions(+), 146 deletions(-)

diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_itp_solver.cpp
index 7571352b3..bcf6b07ae 100644
--- a/src/muz/spacer/spacer_itp_solver.cpp
+++ b/src/muz/spacer/spacer_itp_solver.cpp
@@ -16,13 +16,13 @@ Author:
 Notes:
 
 --*/
-#include"spacer_itp_solver.h"
-#include"ast.h"
-#include"spacer_util.h"
-#include"spacer_farkas_learner.h"
-#include"expr_replacer.h"
-#include "spacer_unsat_core_learner.h"
-#include "spacer_unsat_core_plugin.h"
+#include"muz/spacer/spacer_itp_solver.h"
+#include"ast/ast.h"
+#include"muz/spacer/spacer_util.h"
+#include"muz/spacer/spacer_farkas_learner.h"
+#include"ast/rewriter/expr_replacer.h"
+#include"muz/spacer/spacer_unsat_core_learner.h"
+#include"muz/spacer/spacer_unsat_core_plugin.h"
 
 namespace spacer {
 void itp_solver::push ()
diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h
index bf5a00751..fce2c4a9c 100644
--- a/src/muz/spacer/spacer_itp_solver.h
+++ b/src/muz/spacer/spacer_itp_solver.h
@@ -19,9 +19,9 @@ Notes:
 #ifndef SPACER_ITP_SOLVER_H_
 #define SPACER_ITP_SOLVER_H_
 
-#include "solver.h"
-#include "expr_substitution.h"
-#include"stopwatch.h"
+#include"solver/solver.h"
+#include"ast/expr_substitution.h"
+#include"util/stopwatch.h"
 namespace spacer {
 class itp_solver : public solver {
 private:
diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp
index c998121c6..77e6f5650 100644
--- a/src/muz/spacer/spacer_legacy_frames.cpp
+++ b/src/muz/spacer/spacer_legacy_frames.cpp
@@ -3,38 +3,38 @@
 
   Legacy implementations of frames. To be removed.
  */
-#include "spacer_context.h"
 #include <sstream>
 #include <iomanip>
 
-#include "dl_util.h"
-#include "rewriter.h"
-#include "rewriter_def.h"
-#include "var_subst.h"
-#include "util.h"
-#include "spacer_prop_solver.h"
-#include "spacer_context.h"
-#include "spacer_generalizers.h"
-#include "for_each_expr.h"
-#include "dl_rule_set.h"
-#include "unit_subsumption_tactic.h"
-#include "model_smt2_pp.h"
+#include "muz/spacer/spacer_context.h"
+#include "muz/base/dl_util.h"
+#include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/var_subst.h"
+#include "util/util.h"
+#include "muz/spacer/spacer_prop_solver.h"
+#include "muz/spacer/spacer_context.h"
+#include "muz/spacer/spacer_generalizers.h"
+#include "ast/for_each_expr.h"
+#include "muz/base/dl_rule_set.h"
+#include "smt/tactic/unit_subsumption_tactic.h"
+#include "model/model_smt2_pp.h"
 #include "dl_mk_rule_inliner.h"
-#include "ast_smt2_pp.h"
-#include "ast_ll_pp.h"
-#include "ast_util.h"
-#include "proof_checker.h"
-#include "smt_value_sort.h"
-#include "proof_utils.h"
-#include "scoped_proof.h"
-#include "spacer_qe_project.h"
-#include "blast_term_ite_tactic.h"
+#include "ast/ast_smt2_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_util.h"
+#include "ast/proof_checker/proof_checker.h"
+#include "smt/smt_value_sort.h"
+#include "muz/base/proof_utils.h"
+#include "ast/scoped_proof.h"
+#include "muz/spacer/spacer_qe_project.h"
+#include "tactic/core/blast_term_ite_tactic.h"
 
-#include "timeit.h"
-#include "luby.h"
-#include "expr_safe_replace.h"
-#include "expr_abstract.h"
-#include "obj_equiv_class.h"
+#include "util/timeit.h"
+#include "util/luby.h"
+#include "ast/rewriter/expr_safe_replace.h"
+#include "ast/expr_abstract.h"
+#include "muz/spacer/obj_equiv_class.h"
 
 
 namespace spacer {
diff --git a/src/muz/spacer/spacer_legacy_mbp.cpp b/src/muz/spacer/spacer_legacy_mbp.cpp
index a9569004c..fc2fd1fdd 100644
--- a/src/muz/spacer/spacer_legacy_mbp.cpp
+++ b/src/muz/spacer/spacer_legacy_mbp.cpp
@@ -17,35 +17,36 @@ Notes:
 
 --*/
 #include <sstream>
-#include "arith_simplifier_plugin.h"
-#include "array_decl_plugin.h"
-#include "ast_pp.h"
-#include "basic_simplifier_plugin.h"
-#include "bv_simplifier_plugin.h"
-#include "bool_rewriter.h"
-#include "dl_util.h"
-#include "for_each_expr.h"
-#include "smt_params.h"
-#include "model.h"
-#include "ref_vector.h"
-#include "rewriter.h"
-#include "rewriter_def.h"
-#include "util.h"
-#include "spacer_manager.h"
-#include "spacer_util.h"
-#include "arith_decl_plugin.h"
-#include "expr_replacer.h"
-#include "model_smt2_pp.h"
-#include "scoped_proof.h"
-#include "qe_lite.h"
-#include "spacer_qe_project.h"
-#include "model_pp.h"
-#include "expr_safe_replace.h"
 
-#include "datatype_decl_plugin.h"
-#include "bv_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
+#include "ast/ast_pp.h"
+#include "ast/simplifier/arith_simplifier_plugin.h"
+#include "ast/simplifier/basic_simplifier_plugin.h"
+#include "ast/simplifier/bv_simplifier_plugin.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "muz/base/dl_util.h"
+#include "ast/for_each_expr.h"
+#include "smt/params/smt_params.h"
+#include "model/model.h"
+#include "util/ref_vector.h"
+#include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "util/util.h"
+#include "muz/spacer/spacer_manager.h"
+#include "muz/spacer/spacer_util.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/rewriter/expr_replacer.h"
+#include "model/model_smt2_pp.h"
+#include "ast/scoped_proof.h"
+#include "qe/qe_lite.h"
+#include "muz/spacer/spacer_qe_project.h"
+#include "model/model_pp.h"
+#include "ast/rewriter/expr_safe_replace.h"
 
-#include "spacer_legacy_mev.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
+
+#include "muz/spacer/spacer_legacy_mev.h"
 
 namespace spacer {
 void qe_project(ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map)
diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp
index 0ab33c693..8b53410b1 100644
--- a/src/muz/spacer/spacer_legacy_mev.cpp
+++ b/src/muz/spacer/spacer_legacy_mev.cpp
@@ -5,34 +5,34 @@ Copyright (c) 2017 Arie Gurfinkel
 */
 
 #include <sstream>
-#include "arith_simplifier_plugin.h"
-#include "array_decl_plugin.h"
-#include "ast_pp.h"
-#include "basic_simplifier_plugin.h"
-#include "bv_simplifier_plugin.h"
-#include "bool_rewriter.h"
-#include "dl_util.h"
-#include "for_each_expr.h"
-#include "smt_params.h"
-#include "model.h"
-#include "ref_vector.h"
-#include "rewriter.h"
-#include "rewriter_def.h"
-#include "util.h"
-#include "spacer_manager.h"
-#include "spacer_legacy_mev.h"
-#include "spacer_util.h"
+#include "ast/simplifier/arith_simplifier_plugin.h"
+#include "ast/array_decl_plugin.h"
+#include "ast/ast_pp.h"
+#include "ast/simplifier/basic_simplifier_plugin.h"
+#include "ast/simplifier/bv_simplifier_plugin.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "muz/base/dl_util.h"
+#include "ast/for_each_expr.h"
+#include "smt/params/smt_params.h"
+#include "model/model.h"
+#include "util/ref_vector.h"
+#include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "util/util.h"
+#include "muz/spacer/spacer_manager.h"
+#include "muz/spacer/spacer_legacy_mev.h"
+#include "muz/spacer/spacer_util.h"
 #include "arith_decl_plugin.h"
-#include "expr_replacer.h"
-#include "model_smt2_pp.h"
-#include "scoped_proof.h"
-#include "qe_lite.h"
-#include "spacer_qe_project.h"
-#include "model_pp.h"
-#include "expr_safe_replace.h"
+#include "ast/rewriter/expr_replacer.h"
+#include "model/model_smt2_pp.h"
+#include "ast/scoped_proof.h"
+#include "qe/qe_lite.h"
+#include "muz/spacer/spacer_qe_project.h"
+#include "model/model_pp.h"
+#include "ast/rewriter/expr_safe_replace.h"
 
-#include "datatype_decl_plugin.h"
-#include "bv_decl_plugin.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
 
 namespace old {
 
diff --git a/src/muz/spacer/spacer_legacy_mev.h b/src/muz/spacer/spacer_legacy_mev.h
index 21790f022..bebf1d0db 100644
--- a/src/muz/spacer/spacer_legacy_mev.h
+++ b/src/muz/spacer/spacer_legacy_mev.h
@@ -6,16 +6,16 @@ Copyright (c) 2017 Arie Gurfinkel
 #ifndef OLD_MEV_H
 #define OLD_MEV_H
 
-#include "ast.h"
-#include "ast_pp.h"
-#include "obj_hashtable.h"
-#include "ref_vector.h"
-#include "simplifier.h"
-#include "trace.h"
-#include "vector.h"
-#include "arith_decl_plugin.h"
-#include "array_decl_plugin.h"
-#include "bv_decl_plugin.h"
+#include "ast/ast.h"
+#include "ast/ast_pp.h"
+#include "util/obj_hashtable.h"
+#include "util/ref_vector.h"
+#include "ast/simplifier/simplifier.h"
+#include "util/trace.h"
+#include "util/vector.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
 
 namespace old {
 class model_evaluator {
diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index 077874488..4ad3e0d7f 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -19,15 +19,16 @@ Revision History:
 --*/
 
 #include <sstream>
-#include "spacer_manager.h"
-#include "ast_smt2_pp.h"
-#include "for_each_expr.h"
-#include "has_free_vars.h"
-#include "expr_replacer.h"
-#include "expr_abstract.h"
-#include "model2expr.h"
-#include "model_smt2_pp.h"
-#include "model_converter.h"
+
+#include "muz/spacer/spacer_manager.h"
+#include "ast/ast_smt2_pp.h"
+#include "ast/for_each_expr.h"
+#include "ast/has_free_vars.h"
+#include "ast/rewriter/expr_replacer.h"
+#include "ast/expr_abstract.h"
+#include "model/model2expr.h"
+#include "model/model_smt2_pp.h"
+#include "tactic/model_converter.h"
 
 namespace spacer {
 
diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h
index 360c4ceb2..f2382c15d 100644
--- a/src/muz/spacer/spacer_manager.h
+++ b/src/muz/spacer/spacer_manager.h
@@ -23,19 +23,20 @@ Revision History:
 
 #include <utility>
 #include <map>
-#include "bool_rewriter.h"
-#include "expr_replacer.h"
-#include "expr_substitution.h"
-#include "map.h"
-#include "ref_vector.h"
-#include "smt_kernel.h"
-#include "spacer_util.h"
-#include "spacer_sym_mux.h"
-#include "spacer_farkas_learner.h"
-#include "spacer_smt_context_manager.h"
-#include "dl_rule.h"
 #include <vector>
 
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/expr_replacer.h"
+#include "ast/expr_substitution.h"
+#include "util/map.h"
+#include "util/ref_vector.h"
+#include "smt/smt_kernel.h"
+#include "muz/spacer/spacer_util.h"
+#include "muz/spacer/spacer_sym_mux.h"
+#include "muz/spacer/spacer_farkas_learner.h"
+#include "muz/spacer/spacer_smt_context_manager.h"
+#include "muz/base/dl_rule.h"
+
 namespace smt {
 class context;
 }
diff --git a/src/muz/spacer/spacer_marshal.cpp b/src/muz/spacer/spacer_marshal.cpp
index fce0d6a34..68c90bd33 100644
--- a/src/muz/spacer/spacer_marshal.cpp
+++ b/src/muz/spacer/spacer_marshal.cpp
@@ -9,14 +9,15 @@ Abstract:
    marshaling and unmarshaling of expressions
 
    --*/
-#include "spacer_marshal.h"
+#include "muz/spacer/spacer_marshal.h"
 
 #include <sstream>
-#include "cmd_context.h"
-#include "smt2parser.h"
-#include "vector.h"
-#include "ast_smt_pp.h"
-#include "ast_pp.h"
+
+#include "cmd_context/cmd_context.h"
+#include "parsers/smt2/smt2parser.h"
+#include "util/vector.h"
+#include "ast/ast_smt_pp.h"
+#include "ast/ast_pp.h"
 
 namespace spacer {
 std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m)
diff --git a/src/muz/spacer/spacer_marshal.h b/src/muz/spacer/spacer_marshal.h
index e4c59628f..95cb8f26a 100644
--- a/src/muz/spacer/spacer_marshal.h
+++ b/src/muz/spacer/spacer_marshal.h
@@ -13,9 +13,10 @@ Abstract:
 #define _SPACER_MARSHAL_H_
 
 #include <string>
-#include "ast.h"
 #include <iostream>
 
+#include "ast/ast.h"
+
 namespace spacer {
 std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m);
 std::string marshal(expr_ref e, ast_manager &m);
diff --git a/src/muz/spacer/spacer_matrix.cpp b/src/muz/spacer/spacer_matrix.cpp
index b7d03d453..3cc83996c 100644
--- a/src/muz/spacer/spacer_matrix.cpp
+++ b/src/muz/spacer/spacer_matrix.cpp
@@ -15,7 +15,7 @@ Revision History:
 
 
 --*/
-#include "spacer_matrix.h"
+#include "muz/spacer/spacer_matrix.h"
 
 namespace spacer
 {
diff --git a/src/muz/spacer/spacer_matrix.h b/src/muz/spacer/spacer_matrix.h
index def194793..4fc418f2b 100644
--- a/src/muz/spacer/spacer_matrix.h
+++ b/src/muz/spacer/spacer_matrix.h
@@ -18,7 +18,8 @@ Revision History:
 #ifndef _SPACER_MATRIX_H_
 #define _SPACER_MATRIX_H_
 
-#include "ast.h"
+#include "util/rational.h"
+#include "util/vector.h"
 
 namespace spacer {
 
diff --git a/src/muz/spacer/spacer_mev_array.cpp b/src/muz/spacer/spacer_mev_array.cpp
index 7a69eeab5..9e04b457e 100644
--- a/src/muz/spacer/spacer_mev_array.cpp
+++ b/src/muz/spacer/spacer_mev_array.cpp
@@ -14,20 +14,20 @@ Author:
 Revision History:
 
 --*/
-#include"model.h"
+#include"model/model.h"
 #include"model_evaluator_params.hpp"
-#include"rewriter_types.h"
-#include"model_evaluator.h"
-#include"spacer_mev_array.h"
-#include"bool_rewriter.h"
-#include"arith_rewriter.h"
-#include"bv_rewriter.h"
-#include"datatype_rewriter.h"
-#include"array_rewriter.h"
-#include"rewriter_def.h"
-#include"cooperate.h"
-#include"ast_pp.h"
-#include"func_interp.h"
+#include"ast/rewriter/rewriter_types.h"
+#include"model/model_evaluator.h"
+#include"muz/spacer/spacer_mev_array.h"
+#include"ast/rewriter/bool_rewriter.h"
+#include"ast/rewriter/arith_rewriter.h"
+#include"ast/rewriter/bv_rewriter.h"
+#include"ast/rewriter/datatype_rewriter.h"
+#include"ast/rewriter/array_rewriter.h"
+#include"ast/rewriter/rewriter_def.h"
+#include"util/cooperate.h"
+#include"ast/ast_pp.h"
+#include"model/func_interp.h"
 
 
 
diff --git a/src/muz/spacer/spacer_mev_array.h b/src/muz/spacer/spacer_mev_array.h
index d7904d677..078925865 100644
--- a/src/muz/spacer/spacer_mev_array.h
+++ b/src/muz/spacer/spacer_mev_array.h
@@ -18,10 +18,10 @@ Revision History:
 #ifndef _SPACER_MEV_ARRAY_H_
 #define _SPACER_MEV_ARRAY_H_
 
-#include"ast.h"
-#include"rewriter_types.h"
-#include"params.h"
-#include "array_decl_plugin.h"
+#include"ast/ast.h"
+#include"ast/rewriter/rewriter_types.h"
+#include"util/params.h"
+#include"ast/array_decl_plugin.h"
 
 /**
  * based on model_evaluator in muz/pdr/pdr_util.h