updated include directives

src/model/model_evaluator.h

@@ -22,7 +22,9 @@ Revision History:
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "util/params.h"
+
 class model;
+class model_core;
 
 typedef rewriter_exception model_evaluator_exception;
 
@@ -46,7 +48,7 @@ public:
 
     void cleanup(params_ref const & p = params_ref());
     void reset(params_ref const & p = params_ref());
-    
+
     unsigned get_num_steps() const;
 };
 

src/muz/spacer/spacer_context.h

@@ -28,8 +28,10 @@ Notes:
 #undef max
 #endif
 #include <queue>
-#include "spacer_manager.h"
-#include "spacer_prop_solver.h"
+
+#include "muz/spacer/spacer_manager.h"
+#include "muz/spacer/spacer_prop_solver.h"
+
 #include "fixedpoint_params.hpp"
 
 namespace datalog {

src/muz/spacer/spacer_min_cut.cpp

@@ -15,7 +15,7 @@ Revision History:
 
 
 --*/
-#include "spacer_min_cut.h"
+#include "muz/spacer/spacer_min_cut.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_min_cut.h

@@ -19,7 +19,8 @@ Revision History:
 #ifndef _SPACER_MIN_CUT_H_
 #define _SPACER_MIN_CUT_H_
 
-#include "ast.h"
+#include "ast/ast.h"
+#include "util/vector.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_proof_utils.cpp

@@ -16,11 +16,11 @@ Revision History:
 
 --*/
 
-#include "spacer_proof_utils.h"
-#include "ast_util.h"
-#include "ast_pp.h"
+#include "muz/spacer/spacer_proof_utils.h"
+#include "ast/ast_util.h"
+#include "ast/ast_pp.h"
 
-#include "proof_checker.h"
+#include "ast/proof_checker/proof_checker.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_proof_utils.h

@@ -18,7 +18,7 @@ Revision History:
 
 #ifndef _SPACER_PROOF_UTILS_H_
 #define _SPACER_PROOF_UTILS_H_
-#include "ast.h"
+#include "ast/ast.h"
 
 namespace spacer {
 /*

src/muz/spacer/spacer_prop_solver.cpp

@@ -18,19 +18,23 @@ Revision History:
 
 --*/
 
-#include <sstream>
-#include "model.h"
-#include "spacer_util.h"
-#include "spacer_prop_solver.h"
-#include "ast_smt2_pp.h"
-#include "dl_util.h"
-#include "model_pp.h"
-#include "smt_params.h"
-#include "datatype_decl_plugin.h"
-#include "bv_decl_plugin.h"
-#include "spacer_farkas_learner.h"
-#include "ast_smt2_pp.h"
-#include "expr_replacer.h"
+#include "ast/ast_smt2_pp.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
+
+#include "ast/rewriter/expr_replacer.h"
+
+#include "smt/params/smt_params.h"
+
+#include "model/model.h"
+#include "model/model_pp.h"
+
+#include "muz/base/dl_util.h"
+
+#include "muz/spacer/spacer_util.h"
+#include "muz/spacer/spacer_farkas_learner.h"
+#include "muz/spacer/spacer_prop_solver.h"
+
 #include "fixedpoint_params.hpp"
 
 namespace spacer {

src/muz/spacer/spacer_prop_solver.h

@@ -23,14 +23,15 @@ Revision History:
 #include <map>
 #include <string>
 #include <utility>
-#include "ast.h"
-#include "obj_hashtable.h"
-#include "smt_kernel.h"
-#include "util.h"
-#include "vector.h"
-#include "spacer_manager.h"
-#include "spacer_smt_context_manager.h"
-#include "spacer_itp_solver.h"
+
+#include "ast/ast.h"
+#include "util/obj_hashtable.h"
+#include "smt/smt_kernel.h"
+#include "util/util.h"
+#include "util/vector.h"
+#include "muz/spacer/spacer_manager.h"
+#include "muz/spacer/spacer_smt_context_manager.h"
+#include "muz/spacer/spacer_itp_solver.h"
 
 struct fixedpoint_params;
 

src/muz/spacer/spacer_qe_project.cpp

@@ -21,20 +21,24 @@ Revision History:
 
 --*/
 
-#include "spacer_qe_project.h"
-#include "qe_vartest.h"
-#include "qe.h"
-#include "arith_decl_plugin.h"
-#include "ast_pp.h"
-#include "th_rewriter.h"
-#include "expr_functors.h"
-#include "expr_substitution.h"
-#include "expr_replacer.h"
-#include "model_pp.h"
-#include "expr_safe_replace.h"
-#include "model_evaluator.h"
-#include "qe_lite.h"
-#include "spacer_mev_array.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/ast_pp.h"
+#include "ast/expr_functors.h"
+#include "ast/expr_substitution.h"
+
+#include "ast/rewriter/expr_replacer.h"
+#include "ast/rewriter/expr_safe_replace.h"
+#include "ast/rewriter/th_rewriter.h"
+
+#include "model/model_evaluator.h"
+#include "model/model_pp.h"
+
+#include "qe/qe.h"
+#include "qe/qe_vartest.h"
+#include "qe/qe_lite.h"
+
+#include "muz/spacer/spacer_mev_array.h"
+#include "muz/spacer/spacer_qe_project.h"
 
 namespace
 {

src/muz/spacer/spacer_qe_project.h

@@ -20,8 +20,8 @@ Notes:
 #ifndef SPACER_QE_PROJECT_H_
 #define SPACER_QE_PROJECT_H_
 
-#include "model.h"
-#include "expr_map.h"
+#include "model/model.h"
+#include "ast/expr_map.h"
 
 namespace qe {
     /**

src/muz/spacer/spacer_smt_context_manager.cpp

@@ -17,16 +17,16 @@ Revision History:
 
 --*/
 
-#include "spacer_smt_context_manager.h"
-#include "has_free_vars.h"
-#include "ast_pp.h"
-#include "ast_smt_pp.h"
-#include <sstream>
-#include "smt_params.h"
 
-#include "ast_pp_util.h"
-#include "smt_context.h"
-#include "spacer_util.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_pp_util.h"
+#include "ast/ast_smt_pp.h"
+
+#include "smt/smt_context.h"
+#include "smt/params/smt_params.h"
+
+#include "muz/spacer/spacer_util.h"
+#include "muz/spacer/spacer_smt_context_manager.h"
 namespace spacer {
 
 

src/muz/spacer/spacer_smt_context_manager.h

@@ -20,11 +20,11 @@ Revision History:
 #ifndef _SPACER_SMT_CONTEXT_MANAGER_H_
 #define _SPACER_SMT_CONTEXT_MANAGER_H_
 
-#include "smt_kernel.h"
-#include "func_decl_dependencies.h"
-#include "dl_util.h"
-#include "spacer_virtual_solver.h"
-#include "stopwatch.h"
+#include "util/stopwatch.h"
+
+#include "smt/smt_kernel.h"
+#include "muz/base/dl_util.h"
+#include "muz/spacer/spacer_virtual_solver.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_sym_mux.cpp

@@ -17,14 +17,15 @@ Revision History:
 
 --*/
 
-#include <sstream>
-#include "ast_pp.h"
-#include "for_each_expr.h"
-#include "model.h"
-#include "rewriter.h"
-#include "rewriter_def.h"
-#include "spacer_util.h"
-#include "spacer_sym_mux.h"
+#include "ast/ast_pp.h"
+#include "ast/for_each_expr.h"
+#include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/rewriter_def.h"
+
+#include "model/model.h"
+
+#include "muz/spacer/spacer_util.h"
+#include "muz/spacer/spacer_sym_mux.h"
 
 using namespace spacer;
 

src/muz/spacer/spacer_sym_mux.h

@@ -20,9 +20,9 @@ Revision History:
 #ifndef _SYM_MUX_H_
 #define _SYM_MUX_H_
 
-#include "ast.h"
-#include "map.h"
-#include "vector.h"
+#include "ast/ast.h"
+#include "util/map.h"
+#include "util/vector.h"
 #include <vector>
 
 class model_core;

src/muz/spacer/spacer_unsat_core_learner.cpp

@@ -15,13 +15,12 @@ Revision History:
 
 
 --*/
-#include "spacer_unsat_core_learner.h"
-
-#include "spacer_unsat_core_plugin.h"
-
-#include "proof_utils.h"
-#include "for_each_expr.h"
 #include <unordered_map>
+
+#include "muz/spacer/spacer_unsat_core_learner.h"
+#include "muz/spacer/spacer_unsat_core_plugin.h"
+#include "ast/for_each_expr.h"
+
 namespace spacer
 {
 

src/muz/spacer/spacer_unsat_core_learner.h

@@ -18,9 +18,9 @@ Revision History:
 #ifndef _SPACER_UNSAT_CORE_LEARNER_H_
 #define _SPACER_UNSAT_CORE_LEARNER_H_
 
-#include "ast.h"
-#include "spacer_util.h"
-#include "spacer_proof_utils.h"
+#include "ast/ast.h"
+#include "muz/spacer/spacer_util.h"
+#include "muz/spacer/spacer_proof_utils.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_unsat_core_plugin.cpp

@@ -15,19 +15,21 @@ Revision History:
 
 
 --*/
-#include "spacer_unsat_core_plugin.h"
-
-#include "spacer_unsat_core_learner.h"
-
-#include "smt_farkas_util.h"
-#include "bool_rewriter.h"
-#include "arith_decl_plugin.h"
 #include <set>
-#include "smt_solver.h"
-#include "solver.h"
 #include <limits>
-#include "spacer_proof_utils.h"
-#include "spacer_matrix.h"
+
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/arith_decl_plugin.h"
+
+#include "solver/solver.h"
+
+#include "smt/smt_farkas_util.h"
+#include "smt/smt_solver.h"
+
+#include "muz/spacer/spacer_proof_utils.h"
+#include "muz/spacer/spacer_matrix.h"
+#include "muz/spacer/spacer_unsat_core_plugin.h"
+#include "muz/spacer/spacer_unsat_core_learner.h"
 
 namespace spacer
 {

src/muz/spacer/spacer_unsat_core_plugin.h

@@ -18,8 +18,8 @@ Revision History:
 #ifndef _SPACER_UNSAT_CORE_PLUGIN_H_
 #define _SPACER_UNSAT_CORE_PLUGIN_H_
 
-#include "ast.h"
-#include "spacer_min_cut.h"
+#include "ast/ast.h"
+#include "muz/spacer/spacer_min_cut.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_util.cpp

@@ -27,43 +27,43 @@ Notes:
 #include <sstream>
 #include <algorithm>
 
-#include "ast.h"
-#include "occurs.h"
-#include "array_decl_plugin.h"
-#include "ast_pp.h"
-#include "bool_rewriter.h"
-#include "dl_util.h"
-#include "for_each_expr.h"
-#include "smt_params.h"
-#include "model.h"
-#include "model_evaluator.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 "ast/ast.h"
+#include "ast/occurs.h"
+#include "ast/ast_pp.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 "model/model_evaluator.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/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/array_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
 
-#include "spacer_legacy_mev.h"
-#include "qe_mbp.h"
+#include "muz/spacer/spacer_legacy_mev.h"
+#include "qe/qe_mbp.h"
 
-#include "tactical.h"
-#include "propagate_values_tactic.h"
-#include "propagate_ineqs_tactic.h"
-#include "arith_bounds_tactic.h"
+#include "tactic/tactical.h"
+#include "tactic/core/propagate_values_tactic.h"
+#include "tactic/arith/propagate_ineqs_tactic.h"
+#include "tactic/arith/arith_bounds_tactic.h"
 
-#include "obj_equiv_class.h"
+#include "muz/spacer/obj_equiv_class.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_util.h

@@ -22,20 +22,20 @@ Revision History:
 #ifndef _SPACER_UTIL_H_
 #define _SPACER_UTIL_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 "model.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"
+#include "model/model.h"
 
-#include "stopwatch.h"
-#include "spacer_antiunify.h"
+#include "util/stopwatch.h"
+#include "muz/spacer/spacer_antiunify.h"
 
 class model;
 class model_core;

src/muz/spacer/spacer_virtual_solver.cpp

@@ -17,15 +17,15 @@ Notes:
 
 --*/
 
-#include "spacer_virtual_solver.h"
-#include "ast_util.h"
-#include "ast_pp_util.h"
-#include "spacer_util.h"
-#include "bool_rewriter.h"
+#include "muz/spacer/spacer_virtual_solver.h"
+#include "ast/ast_util.h"
+#include "ast/ast_pp_util.h"
+#include "muz/spacer/spacer_util.h"
+#include "ast/rewriter/bool_rewriter.h"
 
-#include "proof_checker.h"
+#include "ast/proof_checker/proof_checker.h"
 
-#include "scoped_proof.h"
+#include "ast/scoped_proof.h"
 
 namespace spacer {
 virtual_solver::virtual_solver(virtual_solver_factory &factory,

src/muz/spacer/spacer_virtual_solver.h

@@ -18,12 +18,12 @@ Notes:
 --*/
 #ifndef SPACER_VIRTUAL_SOLVER_H_
 #define SPACER_VIRTUAL_SOLVER_H_
-#include"ast.h"
-#include"params.h"
-#include"solver_na2as.h"
-#include"smt_kernel.h"
-#include"smt_params.h"
-#include"stopwatch.h"
+#include"ast/ast.h"
+#include"util/params.h"
+#include"solver/solver_na2as.h"
+#include"smt/smt_kernel.h"
+#include"smt/params/smt_params.h"
+#include"util/stopwatch.h"
 namespace spacer {
 class virtual_solver_factory;