From b9cbb08858d18e71c5e184a1a5ead2cc99f8d2e4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 29 Aug 2020 09:51:39 -0700
Subject: [PATCH] shuffle dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_project.py                                    | 9 +++++----
 src/CMakeLists.txt                                       | 1 +
 src/api/api_config_params.cpp                            | 2 +-
 src/api/api_context.h                                    | 2 +-
 src/ast/pattern/CMakeLists.txt                           | 3 ---
 src/ast/pattern/pattern_inference.h                      | 2 +-
 src/ast/rewriter/arith_rewriter.cpp                      | 2 +-
 src/ast/rewriter/bit_blaster/CMakeLists.txt              | 1 +
 src/ast/rewriter/bit_blaster/bit_blaster.h               | 8 ++++----
 src/cmd_context/CMakeLists.txt                           | 4 +---
 src/cmd_context/cmd_context.h                            | 2 +-
 src/{ast/rewriter => params}/arith_rewriter_params.pyg   | 0
 .../rewriter/bit_blaster => params}/bit_blaster_params.h | 0
 src/{ast/rewriter => params}/bv_rewriter_params.pyg      | 0
 src/{cmd_context => params}/context_params.cpp           | 3 +--
 src/{cmd_context => params}/context_params.h             | 0
 src/{ast/pattern => params}/pattern_inference_params.cpp | 6 +++---
 src/{ast/pattern => params}/pattern_inference_params.h   | 0
 .../pattern_inference_params_helper.pyg                  | 0
 src/smt/params/CMakeLists.txt                            | 2 +-
 src/smt/params/preprocessor_params.h                     | 4 ++--
 src/smt/params/smt_params.h                              | 2 +-
 src/smt/params/theory_arith_params.cpp                   | 2 +-
 src/smt/params/theory_bv_params.cpp                      | 2 +-
 24 files changed, 27 insertions(+), 30 deletions(-)
 rename src/{ast/rewriter => params}/arith_rewriter_params.pyg (100%)
 rename src/{ast/rewriter/bit_blaster => params}/bit_blaster_params.h (100%)
 rename src/{ast/rewriter => params}/bv_rewriter_params.pyg (100%)
 rename src/{cmd_context => params}/context_params.cpp (99%)
 rename src/{cmd_context => params}/context_params.h (100%)
 rename src/{ast/pattern => params}/pattern_inference_params.cpp (92%)
 rename src/{ast/pattern => params}/pattern_inference_params.h (100%)
 rename src/{ast/pattern => params}/pattern_inference_params_helper.pyg (100%)

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index a0ccc6d95..c34cfc455 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -23,12 +23,13 @@ def init_project_def():
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
+    add_lib('params', ['ast', 'util'])
     add_lib('euf', ['ast','util'], 'ast/euf')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    
     add_lib('sat', ['util','dd', 'grobner'])    
     add_lib('nlsat', ['polynomial', 'sat'])
     add_lib('lp', ['util','nlsat','grobner', 'interval'], 'math/lp')
-    add_lib('rewriter', ['ast', 'polynomial', 'automata'], 'ast/rewriter')
+    add_lib('rewriter', ['ast', 'polynomial', 'automata','params'], 'ast/rewriter')
     add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
     add_lib('model', ['rewriter'])
@@ -37,14 +38,14 @@ def init_project_def():
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
     add_lib('solver', ['model', 'tactic', 'proofs'])
-    add_lib('cmd_context', ['solver', 'rewriter'])
+    add_lib('cmd_context', ['solver', 'rewriter', 'params'])
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('aig_tactic', ['tactic'], 'tactic/aig')
     add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
-    add_lib('bit_blaster', ['rewriter', 'rewriter'], 'ast/rewriter/bit_blaster')
+    add_lib('bit_blaster', ['rewriter', 'params'], 'ast/rewriter/bit_blaster')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
-    add_lib('smt_params', ['ast', 'rewriter', 'pattern', 'bit_blaster'], 'smt/params')
+    add_lib('smt_params', ['ast', 'params'], 'smt/params')
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
 
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9cb25ed98..b207a8bfc 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -44,6 +44,7 @@ add_subdirectory(math/interval)
 add_subdirectory(math/realclosure)
 add_subdirectory(math/subpaving)
 add_subdirectory(ast)
+add_subdirectory(params)
 add_subdirectory(ast/rewriter)
 add_subdirectory(ast/normal_forms)
 add_subdirectory(model)
diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 1682fb707..4babf21ad 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -24,7 +24,7 @@ Revision History:
 #include "util/symbol.h"
 #include "util/gparams.h"
 #include "util/env_params.h"
-#include "cmd_context/context_params.h"
+#include "params/context_params.h"
 
 extern "C" {
     void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) {
diff --git a/src/api/api_context.h b/src/api/api_context.h
index c83471594..760b0c1b0 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -36,7 +36,7 @@ Revision History:
 #include "smt/smt_kernel.h"
 #include "smt/smt_solver.h"
 #include "cmd_context/tactic_manager.h"
-#include "cmd_context/context_params.h"
+#include "params/context_params.h"
 #include "cmd_context/cmd_context.h"
 #include "solver/solver.h"
 #include "api/z3.h"
diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt
index 0bbb670c3..8d0cf0cb4 100644
--- a/src/ast/pattern/CMakeLists.txt
+++ b/src/ast/pattern/CMakeLists.txt
@@ -23,7 +23,6 @@ z3_add_component(pattern
   SOURCES
     expr_pattern_match.cpp
     pattern_inference.cpp
-    pattern_inference_params.cpp
     # Let CMake know this target depends on this generated
     # header file
     ${CMAKE_CURRENT_BINARY_DIR}/database.h
@@ -31,6 +30,4 @@ z3_add_component(pattern
     normal_forms
     rewriter
     smt2parser
-  PYG_FILES
-    pattern_inference_params_helper.pyg
 )
diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h
index 96e4c379d..af95bcb6c 100644
--- a/src/ast/pattern/pattern_inference.h
+++ b/src/ast/pattern/pattern_inference.h
@@ -20,7 +20,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter.h"
-#include "ast/pattern/pattern_inference_params.h"
+#include "params/pattern_inference_params.h"
 #include "util/vector.h"
 #include "util/uint_set.h"
 #include "util/nat_set.h"
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 1a8648156..26033c2f4 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -16,8 +16,8 @@ Author:
 Notes:
 
 --*/
+#include "params/arith_rewriter_params.hpp"
 #include "ast/rewriter/arith_rewriter.h"
-#include "ast/rewriter/arith_rewriter_params.hpp"
 #include "ast/rewriter/poly_rewriter_def.h"
 #include "math/polynomial/algebraic_numbers.h"
 #include "ast/ast_pp.h"
diff --git a/src/ast/rewriter/bit_blaster/CMakeLists.txt b/src/ast/rewriter/bit_blaster/CMakeLists.txt
index c8985a051..a6d7790fd 100644
--- a/src/ast/rewriter/bit_blaster/CMakeLists.txt
+++ b/src/ast/rewriter/bit_blaster/CMakeLists.txt
@@ -4,4 +4,5 @@ z3_add_component(bit_blaster
     bit_blaster_rewriter.cpp
   COMPONENT_DEPENDENCIES
     rewriter
+    params
 )
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h
index 241d4c97d..8f2e7e50f 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster.h
@@ -18,11 +18,11 @@ Revision History:
 --*/
 #pragma once
 
-#include "ast/rewriter/bool_rewriter.h"
-#include "ast/rewriter/bit_blaster/bit_blaster_params.h"
-#include "ast/rewriter/bit_blaster/bit_blaster_tpl.h"
-#include "ast/bv_decl_plugin.h"
 #include "util/rational.h"
+#include "ast/bv_decl_plugin.h"
+#include "params/bit_blaster_params.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/bit_blaster/bit_blaster_tpl.h"
 
 class bit_blaster_cfg {
 public:
diff --git a/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt
index 8da871f9a..3f869966c 100644
--- a/src/cmd_context/CMakeLists.txt
+++ b/src/cmd_context/CMakeLists.txt
@@ -5,7 +5,6 @@ z3_add_component(cmd_context
     cmd_context.cpp
     cmd_context_to_goal.cpp
     cmd_util.cpp
-    context_params.cpp
     echo_tactic.cpp
     eval_cmd.cpp
     parametric_cmd.cpp
@@ -16,6 +15,5 @@ z3_add_component(cmd_context
   COMPONENT_DEPENDENCIES
     rewriter
     solver
-  EXTRA_REGISTER_MODULE_HEADERS
-    context_params.h
+    params
 )
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index c5e7b88e2..b7beb2625 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -39,7 +39,7 @@ Notes:
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
 #include "cmd_context/check_logic.h"
-#include "cmd_context/context_params.h"
+#include "params/context_params.h"
 
 
 class func_decls {
diff --git a/src/ast/rewriter/arith_rewriter_params.pyg b/src/params/arith_rewriter_params.pyg
similarity index 100%
rename from src/ast/rewriter/arith_rewriter_params.pyg
rename to src/params/arith_rewriter_params.pyg
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_params.h b/src/params/bit_blaster_params.h
similarity index 100%
rename from src/ast/rewriter/bit_blaster/bit_blaster_params.h
rename to src/params/bit_blaster_params.h
diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/params/bv_rewriter_params.pyg
similarity index 100%
rename from src/ast/rewriter/bv_rewriter_params.pyg
rename to src/params/bv_rewriter_params.pyg
diff --git a/src/cmd_context/context_params.cpp b/src/params/context_params.cpp
similarity index 99%
rename from src/cmd_context/context_params.cpp
rename to src/params/context_params.cpp
index 7f022f533..51881ae09 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/params/context_params.cpp
@@ -17,11 +17,10 @@ Author:
 Notes:
 
 --*/
-#include "cmd_context/context_params.h"
 #include "util/gparams.h"
 #include "util/params.h"
 #include "ast/ast.h"
-#include "solver/solver.h"
+#include "params/context_params.h"
 
 context_params::context_params() {
     updt_params();
diff --git a/src/cmd_context/context_params.h b/src/params/context_params.h
similarity index 100%
rename from src/cmd_context/context_params.h
rename to src/params/context_params.h
diff --git a/src/ast/pattern/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp
similarity index 92%
rename from src/ast/pattern/pattern_inference_params.cpp
rename to src/params/pattern_inference_params.cpp
index 1f1118a02..bb9b481ca 100644
--- a/src/ast/pattern/pattern_inference_params.cpp
+++ b/src/params/pattern_inference_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "ast/pattern/pattern_inference_params.h"
-#include "ast/pattern/pattern_inference_params_helper.hpp"
+#include "params/pattern_inference_params.h"
+#include "params/pattern_inference_params_helper.hpp"
 
 void pattern_inference_params::updt_params(params_ref const & _p) {
     pattern_inference_params_helper p(_p);
@@ -44,4 +44,4 @@ void pattern_inference_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_pi_nopat_weight);
     DISPLAY_PARAM(m_pi_avoid_skolems);
     DISPLAY_PARAM(m_pi_warnings);
-}
\ No newline at end of file
+}
diff --git a/src/ast/pattern/pattern_inference_params.h b/src/params/pattern_inference_params.h
similarity index 100%
rename from src/ast/pattern/pattern_inference_params.h
rename to src/params/pattern_inference_params.h
diff --git a/src/ast/pattern/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg
similarity index 100%
rename from src/ast/pattern/pattern_inference_params_helper.pyg
rename to src/params/pattern_inference_params_helper.pyg
diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt
index 31b9b203d..0be62f820 100644
--- a/src/smt/params/CMakeLists.txt
+++ b/src/smt/params/CMakeLists.txt
@@ -11,7 +11,7 @@ z3_add_component(smt_params
     theory_seq_params.cpp
     theory_str_params.cpp
   COMPONENT_DEPENDENCIES
-    pattern
+    params
   PYG_FILES
     smt_params_helper.pyg
 )
diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h
index 886c60c94..a0d56182a 100644
--- a/src/smt/params/preprocessor_params.h
+++ b/src/smt/params/preprocessor_params.h
@@ -18,8 +18,8 @@ Revision History:
 --*/
 #pragma once
 
-#include "ast/pattern/pattern_inference_params.h"
-#include "ast/rewriter/bit_blaster/bit_blaster_params.h"
+#include "params/pattern_inference_params.h"
+#include "params/bit_blaster_params.h"
 
 enum lift_ite_kind {
     LI_NONE,
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 844a9a9b6..dc3b4c0d7 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -28,7 +28,7 @@ Revision History:
 #include "smt/params/theory_pb_params.h"
 #include "smt/params/theory_datatype_params.h"
 #include "smt/params/preprocessor_params.h"
-#include "cmd_context/context_params.h"
+#include "params/context_params.h"
 
 enum phase_selection {
     PS_ALWAYS_FALSE,
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index 70285b681..a2a497731 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #include "smt/params/theory_arith_params.h"
 #include "smt/params/smt_params_helper.hpp"
-#include "ast/rewriter/arith_rewriter_params.hpp"
+#include "params/arith_rewriter_params.hpp"
 
 void theory_arith_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp
index fbd7647a4..7afa00589 100644
--- a/src/smt/params/theory_bv_params.cpp
+++ b/src/smt/params/theory_bv_params.cpp
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #include "smt/params/theory_bv_params.h"
 #include "smt/params/smt_params_helper.hpp"
-#include "ast/rewriter/bv_rewriter_params.hpp"
+#include "params/bv_rewriter_params.hpp"
 
 void theory_bv_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);