diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index b8f4763a1..1c0cebd54 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -41,11 +41,4 @@ z3_add_component(rewriter params automata polynomial - PYG_FILES - array_rewriter_params.pyg - bool_rewriter_params.pyg - fpa_rewriter_params.pyg - poly_rewriter_params.pyg - rewriter_params.pyg - seq_rewriter_params.pyg ) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 4a37b1e08..22422fcd1 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -17,12 +17,12 @@ Notes: --*/ #include "ast/rewriter/array_rewriter.h" -#include "ast/rewriter/array_rewriter_params.hpp" #include "ast/ast_lt.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/rewriter/var_subst.h" +#include "params/array_rewriter_params.hpp" void array_rewriter::updt_params(params_ref const & _p) { array_rewriter_params p(_p); diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 1e4b3554d..dc512aa56 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/bool_rewriter.h" -#include "ast/rewriter/bool_rewriter_params.hpp" +#include "params/bool_rewriter_params.hpp" #include "ast/rewriter/rewriter_def.h" #include "ast/ast_lt.h" #include diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index f2699915a..fbc1a8e58 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/fpa_rewriter.h" -#include "ast/rewriter/fpa_rewriter_params.hpp" +#include "params/fpa_rewriter_params.hpp" #include "ast/ast_smt2_pp.h" fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) : diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 70caa0674..c7e21a8db 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -19,7 +19,7 @@ Notes: #include "util/container_util.h" #include "ast/rewriter/poly_rewriter.h" -#include "ast/rewriter/poly_rewriter_params.hpp" +#include "params/poly_rewriter_params.hpp" #include "params/arith_rewriter_params.hpp" #include "ast/ast_lt.h" #include "ast/ast_ll_pp.h" diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e627e2343..caa2188cf 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -27,7 +27,7 @@ Author: #include "ast/well_sorted.h" #include "ast/rewriter/var_subst.h" #include "ast/rewriter/expr_safe_replace.h" -#include "ast/rewriter/seq_rewriter_params.hpp" +#include "params/seq_rewriter_params.hpp" #include "math/automata/automaton.h" #include "math/automata/symbolic_automata_def.h" diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 340c76805..8b2df7390 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -16,8 +16,8 @@ Author: Notes: --*/ +#include "params/rewriter_params.hpp" #include "ast/rewriter/th_rewriter.h" -#include "ast/rewriter/rewriter_params.hpp" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/arith_rewriter.h" #include "ast/rewriter/bv_rewriter.h" diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index 241b48ddd..249b25a5d 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -6,9 +6,15 @@ z3_add_component(params util ast PYG_FILES - pattern_inference_params_helper.pyg - bv_rewriter_params.pyg arith_rewriter_params.pyg + array_rewriter_params.pyg + bool_rewriter_params.pyg + bv_rewriter_params.pyg + fpa_rewriter_params.pyg + pattern_inference_params_helper.pyg + poly_rewriter_params.pyg + rewriter_params.pyg + seq_rewriter_params.pyg EXTRA_REGISTER_MODULE_HEADERS context_params.h ) diff --git a/src/ast/rewriter/array_rewriter_params.pyg b/src/params/array_rewriter_params.pyg similarity index 100% rename from src/ast/rewriter/array_rewriter_params.pyg rename to src/params/array_rewriter_params.pyg diff --git a/src/ast/rewriter/bool_rewriter_params.pyg b/src/params/bool_rewriter_params.pyg similarity index 100% rename from src/ast/rewriter/bool_rewriter_params.pyg rename to src/params/bool_rewriter_params.pyg diff --git a/src/ast/rewriter/fpa_rewriter_params.pyg b/src/params/fpa_rewriter_params.pyg similarity index 100% rename from src/ast/rewriter/fpa_rewriter_params.pyg rename to src/params/fpa_rewriter_params.pyg diff --git a/src/ast/rewriter/poly_rewriter_params.pyg b/src/params/poly_rewriter_params.pyg similarity index 100% rename from src/ast/rewriter/poly_rewriter_params.pyg rename to src/params/poly_rewriter_params.pyg diff --git a/src/ast/rewriter/rewriter_params.pyg b/src/params/rewriter_params.pyg similarity index 100% rename from src/ast/rewriter/rewriter_params.pyg rename to src/params/rewriter_params.pyg diff --git a/src/ast/rewriter/seq_rewriter_params.pyg b/src/params/seq_rewriter_params.pyg similarity index 100% rename from src/ast/rewriter/seq_rewriter_params.pyg rename to src/params/seq_rewriter_params.pyg diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index 3cb895c40..baef6c4f2 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -16,10 +16,10 @@ --*/ #include "tactic/bv/bv_bound_chk_tactic.h" #include "ast/ast.h" +#include "params/rewriter_params.hpp" #include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/bv_bounds.h" -#include "ast/rewriter/rewriter_params.hpp" #include "ast/rewriter/bool_rewriter.h" struct bv_bound_chk_stats {