From ab0735fde225fff30a0595fefa2acee39122e2e2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Mar 2021 15:51:38 -0700
Subject: [PATCH] separate component for asserted_formulas to break dependency
cycles
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 5 +++--
src/CMakeLists.txt | 1 +
src/smt/smt_context.h | 2 +-
src/solver/CMakeLists.txt | 2 --
src/solver/{ => assertions}/asserted_formulas.cpp | 3 ++-
src/solver/{ => assertions}/asserted_formulas.h | 0
6 files changed, 7 insertions(+), 6 deletions(-)
rename src/solver/{ => assertions}/asserted_formulas.cpp (99%)
rename src/solver/{ => assertions}/asserted_formulas.h (100%)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 0bf9b30fa..7088862cc 100644
--- a/scripts/mk_project.py
+++ b/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')
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 33a0cf99d..75a12cdd9 100644
--- a/src/CMakeLists.txt
+++ b/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)
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 1058e232e..e7e924036 100644
--- a/src/smt/smt_context.h
+++ b/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
diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt
index 74da214b4..67549c46b 100644
--- a/src/solver/CMakeLists.txt
+++ b/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
diff --git a/src/solver/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
similarity index 99%
rename from src/solver/asserted_formulas.cpp
rename to src/solver/assertions/asserted_formulas.cpp
index 0cb4af10a..e0c7456b9 100644
--- a/src/solver/asserted_formulas.cpp
+++ b/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),
diff --git a/src/solver/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
similarity index 100%
rename from src/solver/asserted_formulas.h
rename to src/solver/assertions/asserted_formulas.h