move asserted_formulas to solver scope

scripts/mk_project.py

@@ -38,7 +38,7 @@ def init_project_def():
     add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution')
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
-    add_lib('solver', ['model', 'tactic', 'proofs'])
+    add_lib('solver', ['model', 'tactic', 'proofs', 'smt_params'])
     add_lib('cmd_context', ['solver', 'rewriter', 'params'])
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('aig_tactic', ['tactic'], 'tactic/aig')

src/CMakeLists.txt

@@ -52,6 +52,7 @@ add_subdirectory(model)
 add_subdirectory(tactic)
 add_subdirectory(ast/substitution)
 add_subdirectory(ast/euf)
+add_subdirectory(smt/params)
 add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)
 add_subdirectory(sat)
@@ -66,7 +67,6 @@ add_subdirectory(cmd_context/extra_cmds)
 add_subdirectory(parsers/smt2)
 add_subdirectory(ast/pattern)
 add_subdirectory(ast/rewriter/bit_blaster)
-add_subdirectory(smt/params)
 add_subdirectory(math/lp)
 add_subdirectory(qe/mbp)
 add_subdirectory(sat/smt)

src/smt/CMakeLists.txt

@@ -2,7 +2,6 @@ z3_add_component(smt
   SOURCES
     arith_eq_adapter.cpp
     arith_eq_solver.cpp
-    asserted_formulas.cpp
     dyn_ack.cpp
     expr_context_simplifier.cpp
     fingerprints.cpp

src/smt/smt_context.h

@@ -37,7 +37,6 @@ Revision History:
 #include "smt/smt_case_split_queue.h"
 #include "smt/smt_almost_cg_table.h"
 #include "smt/smt_failure.h"
-#include "smt/asserted_formulas.h"
 #include "smt/smt_types.h"
 #include "smt/dyn_ack.h"
 #include "ast/ast_smt_pp.h"
@@ -51,6 +50,7 @@ Revision History:
 #include "smt/user_propagator.h"
 #include "model/model.h"
 #include "solver/progress_callback.h"
+#include "solver/asserted_formulas.h"
 #include <tuple>
 
 // there is a significant space overhead with allocating 1000+ contexts in

src/solver/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(solver
   SOURCES
+    asserted_formulas.cpp
     check_sat_result.cpp
     check_logic.cpp
     combined_solver.cpp
@@ -14,6 +15,7 @@ z3_add_component(solver
   COMPONENT_DEPENDENCIES
     model
     tactic
+    smt_params
   PYG_FILES
     combined_solver_params.pyg
     parallel_params.pyg

src/solver/asserted_formulas.cpp

@@ -26,7 +26,7 @@ Revision History:
 #include "ast/pattern/pattern_inference.h"
 #include "ast/macros/quasi_macros.h"
 #include "ast/occurs.h"
-#include "smt/asserted_formulas.h"
+#include "solver/asserted_formulas.h"
 
 asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
     m(m),