separate component for asserted_formulas to break dependency cycles

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/mk_project.py

@@ -38,14 +38,15 @@ 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', 'smt_params', 'normal_forms'])
+    add_lib('solver', ['model', 'tactic', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter', 'params'])
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
+    add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
+    add_lib('solver_assertions', ['pattern'], 'solver/assertions')
     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', 'params'], 'ast/rewriter/bit_blaster')
-    add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')

src/CMakeLists.txt

@@ -65,6 +65,7 @@ add_subdirectory(solver)
 add_subdirectory(cmd_context)
 add_subdirectory(cmd_context/extra_cmds)
 add_subdirectory(parsers/smt2)
+add_subdirectory(solver/assertions)
 add_subdirectory(ast/pattern)
 add_subdirectory(ast/rewriter/bit_blaster)
 add_subdirectory(math/lp)

src/smt/smt_context.h

@@ -50,7 +50,7 @@ Revision History:
 #include "smt/user_propagator.h"
 #include "model/model.h"
 #include "solver/progress_callback.h"
-#include "solver/asserted_formulas.h"
+#include "solver/assertions/asserted_formulas.h"
 #include <tuple>
 
 // there is a significant space overhead with allocating 1000+ contexts in

src/solver/CMakeLists.txt

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

src/solver/assertions/asserted_formulas.cpp

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