From 25c6480e6eabab36c766e72f8429991398208071 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 23:16:42 -0400 Subject: [PATCH] updated include directives --- src/model/model_evaluator.h | 4 +- src/muz/spacer/spacer_context.h | 6 +- src/muz/spacer/spacer_min_cut.cpp | 2 +- src/muz/spacer/spacer_min_cut.h | 3 +- src/muz/spacer/spacer_proof_utils.cpp | 8 +-- src/muz/spacer/spacer_proof_utils.h | 2 +- src/muz/spacer/spacer_prop_solver.cpp | 30 +++++---- src/muz/spacer/spacer_prop_solver.h | 17 ++--- src/muz/spacer/spacer_qe_project.cpp | 32 +++++---- src/muz/spacer/spacer_qe_project.h | 4 +- src/muz/spacer/spacer_smt_context_manager.cpp | 18 ++--- src/muz/spacer/spacer_smt_context_manager.h | 10 +-- src/muz/spacer/spacer_sym_mux.cpp | 17 ++--- src/muz/spacer/spacer_sym_mux.h | 6 +- src/muz/spacer/spacer_unsat_core_learner.cpp | 11 ++-- src/muz/spacer/spacer_unsat_core_learner.h | 6 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 24 +++---- src/muz/spacer/spacer_unsat_core_plugin.h | 4 +- src/muz/spacer/spacer_util.cpp | 66 +++++++++---------- src/muz/spacer/spacer_util.h | 26 ++++---- src/muz/spacer/spacer_virtual_solver.cpp | 14 ++-- src/muz/spacer/spacer_virtual_solver.h | 12 ++-- 22 files changed, 169 insertions(+), 153 deletions(-) diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h index 2497ec927..bd2b2d664 100644 --- a/src/model/model_evaluator.h +++ b/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; }; diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 78541130c..b6cfaff0c 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -28,8 +28,10 @@ Notes: #undef max #endif #include -#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 { diff --git a/src/muz/spacer/spacer_min_cut.cpp b/src/muz/spacer/spacer_min_cut.cpp index c56ddbd66..22ff81a80 100644 --- a/src/muz/spacer/spacer_min_cut.cpp +++ b/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 { diff --git a/src/muz/spacer/spacer_min_cut.h b/src/muz/spacer/spacer_min_cut.h index ae285b9bb..c73a8d3d3 100644 --- a/src/muz/spacer/spacer_min_cut.h +++ b/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 { diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index ff020dee4..6edb29881 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/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 { diff --git a/src/muz/spacer/spacer_proof_utils.h b/src/muz/spacer/spacer_proof_utils.h index 7973c673b..f2897f7ec 100644 --- a/src/muz/spacer/spacer_proof_utils.h +++ b/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 { /* diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 29b34b799..27225315c 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -18,19 +18,23 @@ Revision History: --*/ -#include -#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 { diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 4f5df819b..1ddec91c6 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -23,14 +23,15 @@ Revision History: #include #include #include -#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; diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index cfc5d6449..62c9c2643 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/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 { diff --git a/src/muz/spacer/spacer_qe_project.h b/src/muz/spacer/spacer_qe_project.h index 6074f0d91..b923dc3c7 100644 --- a/src/muz/spacer/spacer_qe_project.h +++ b/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 { /** diff --git a/src/muz/spacer/spacer_smt_context_manager.cpp b/src/muz/spacer/spacer_smt_context_manager.cpp index f5e5ba9c1..e6ab2c883 100644 --- a/src/muz/spacer/spacer_smt_context_manager.cpp +++ b/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 -#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 { diff --git a/src/muz/spacer/spacer_smt_context_manager.h b/src/muz/spacer/spacer_smt_context_manager.h index fd04eaf4e..0df9bc77b 100644 --- a/src/muz/spacer/spacer_smt_context_manager.h +++ b/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 { diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp index 659aea2cc..da8f8eeca 100644 --- a/src/muz/spacer/spacer_sym_mux.cpp +++ b/src/muz/spacer/spacer_sym_mux.cpp @@ -17,14 +17,15 @@ Revision History: --*/ -#include -#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; diff --git a/src/muz/spacer/spacer_sym_mux.h b/src/muz/spacer/spacer_sym_mux.h index d9bae95a3..892542557 100644 --- a/src/muz/spacer/spacer_sym_mux.h +++ b/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 class model_core; diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index 557858ca4..222ca146c 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/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 + +#include "muz/spacer/spacer_unsat_core_learner.h" +#include "muz/spacer/spacer_unsat_core_plugin.h" +#include "ast/for_each_expr.h" + namespace spacer { diff --git a/src/muz/spacer/spacer_unsat_core_learner.h b/src/muz/spacer/spacer_unsat_core_learner.h index 91ae01292..6ee7c3b37 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.h +++ b/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 { diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index 58c700dae..a352a2460 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/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 -#include "smt_solver.h" -#include "solver.h" #include -#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 { diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h index 6e1f383c1..388a2bd38 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.h +++ b/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 { diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index a2cf4101f..be6b12cd0 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -27,43 +27,43 @@ Notes: #include #include -#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 { diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index f51df7a7b..5bbb84bfb 100644 --- a/src/muz/spacer/spacer_util.h +++ b/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; diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp index c6b85a3ea..c080fa2c4 100644 --- a/src/muz/spacer/spacer_virtual_solver.cpp +++ b/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, diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h index b5e97dce0..14e05302e 100644 --- a/src/muz/spacer/spacer_virtual_solver.h +++ b/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;