From ddbcd08d469d0ee8168b1820c1540a06a439c6bc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Mar 2021 15:02:16 -0700
Subject: [PATCH] move asserted_formulas to solver scope

---
 scripts/mk_project.py                     | 2 +-
 src/CMakeLists.txt                        | 2 +-
 src/smt/CMakeLists.txt                    | 1 -
 src/smt/smt_context.h                     | 2 +-
 src/solver/CMakeLists.txt                 | 2 ++
 src/{smt => solver}/asserted_formulas.cpp | 2 +-
 src/{smt => solver}/asserted_formulas.h   | 0
 7 files changed, 6 insertions(+), 5 deletions(-)
 rename src/{smt => solver}/asserted_formulas.cpp (99%)
 rename src/{smt => solver}/asserted_formulas.h (100%)

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 4af2da3e2..a2bc85757 100644
--- a/scripts/mk_project.py
+++ b/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')
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e100a1f77..33a0cf99d 100644
--- a/src/CMakeLists.txt
+++ b/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)
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 427c2c9cf..f24d29d91 100644
--- a/src/smt/CMakeLists.txt
+++ b/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
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 43718f229..1058e232e 100644
--- a/src/smt/smt_context.h
+++ b/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
diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt
index 67549c46b..74da214b4 100644
--- a/src/solver/CMakeLists.txt
+++ b/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
diff --git a/src/smt/asserted_formulas.cpp b/src/solver/asserted_formulas.cpp
similarity index 99%
rename from src/smt/asserted_formulas.cpp
rename to src/solver/asserted_formulas.cpp
index db387bf4c..0cb4af10a 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/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),
diff --git a/src/smt/asserted_formulas.h b/src/solver/asserted_formulas.h
similarity index 100%
rename from src/smt/asserted_formulas.h
rename to src/solver/asserted_formulas.h