From 08294d62e5cd7898d3876038264765bcc0c9d8e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Jan 2022 03:26:22 -0800 Subject: [PATCH] separate dependencies for qe_lite --- scripts/mk_project.py | 5 +++-- src/CMakeLists.txt | 3 ++- src/api/api_qe.cpp | 2 +- src/muz/base/dl_rule.h | 2 +- src/muz/spacer/spacer_legacy_mbp.cpp | 2 +- src/muz/spacer/spacer_legacy_mev.cpp | 2 +- src/muz/spacer/spacer_qe_project.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 2 +- src/muz/tab/tab_context.cpp | 2 +- src/qe/CMakeLists.txt | 3 +-- src/qe/lite/CMakeLists.txt | 9 +++++++++ src/qe/{ => lite}/qe_lite.cpp | 2 +- src/qe/{ => lite}/qe_lite.h | 0 src/qe/qe_mbp.cpp | 2 +- src/tactic/smtlogics/nra_tactic.cpp | 2 +- src/tactic/smtlogics/quant_tactics.cpp | 2 +- 16 files changed, 26 insertions(+), 16 deletions(-) create mode 100644 src/qe/lite/CMakeLists.txt rename src/qe/{ => lite}/qe_lite.cpp (99%) rename src/qe/{ => lite}/qe_lite.h (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 17a76060a..12604d079 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -42,7 +42,6 @@ def init_project_def(): 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','smt_params','cmd_context'], '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') @@ -50,6 +49,8 @@ def init_project_def(): 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') + add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite') + add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions') add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern'], 'sat/smt') add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') @@ -62,7 +63,7 @@ def init_project_def(): add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - add_lib('qe', ['smt', 'mbp', 'nlsat', 'tactic', 'nlsat_tactic'], 'qe') + add_lib('qe', ['smt', 'mbp', 'qe_lite', 'nlsat', 'tactic', 'nlsat_tactic'], 'qe') add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') add_lib('fd_solver', ['core_tactics', 'arith_tactics', 'sat_solver', 'smt'], 'tactic/fd_solver') add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 75a12cdd9..51fafb42f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -65,11 +65,12 @@ add_subdirectory(solver) add_subdirectory(cmd_context) add_subdirectory(cmd_context/extra_cmds) add_subdirectory(parsers/smt2) +add_subdirectory(qe/mbp) +add_subdirectory(qe/lite) add_subdirectory(solver/assertions) add_subdirectory(ast/pattern) add_subdirectory(ast/rewriter/bit_blaster) add_subdirectory(math/lp) -add_subdirectory(qe/mbp) add_subdirectory(sat/smt) add_subdirectory(sat/tactic) add_subdirectory(nlsat/tactic) diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index e3c51c7b5..d1e5d195b 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -26,7 +26,7 @@ Notes: #include "api/api_model.h" #include "api/api_ast_map.h" #include "api/api_ast_vector.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "muz/spacer/spacer_util.h" extern "C" diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 02d13c1ca..c9fa2f6b3 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -28,7 +28,7 @@ Revision History: #include "ast/rewriter/ast_counter.h" #include "ast/rewriter/rewriter.h" #include "muz/base/hnf.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "ast/rewriter/var_subst.h" #include "ast/datatype_decl_plugin.h" #include "ast/rewriter/label_rewriter.h" diff --git a/src/muz/spacer/spacer_legacy_mbp.cpp b/src/muz/spacer/spacer_legacy_mbp.cpp index 76b543f04..324368cec 100644 --- a/src/muz/spacer/spacer_legacy_mbp.cpp +++ b/src/muz/spacer/spacer_legacy_mbp.cpp @@ -35,7 +35,7 @@ Notes: #include "ast/rewriter/expr_replacer.h" #include "model/model_smt2_pp.h" #include "ast/scoped_proof.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "muz/spacer/spacer_qe_project.h" #include "model/model_pp.h" #include "ast/rewriter/expr_safe_replace.h" diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp index 26752beda..e6da53e32 100644 --- a/src/muz/spacer/spacer_legacy_mev.cpp +++ b/src/muz/spacer/spacer_legacy_mev.cpp @@ -23,7 +23,7 @@ Copyright (c) 2017 Arie Gurfinkel #include "ast/rewriter/expr_replacer.h" #include "model/model_smt2_pp.h" #include "ast/scoped_proof.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "muz/spacer/spacer_qe_project.h" #include "model/model_pp.h" #include "ast/rewriter/expr_safe_replace.h" diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 5acbab9aa..b170a59d0 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -36,7 +36,7 @@ Revision History: #include "model/model_pp.h" #include "qe/qe.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "muz/spacer/spacer_mev_array.h" #include "muz/spacer/spacer_qe_project.h" diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index e284d6424..d16b37972 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -52,7 +52,7 @@ Notes: #include "model/model_smt2_pp.h" #include "model/model_pp.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "qe/qe_mbp.h" #include "qe/mbp/mbp_term_graph.h" #include "qe/mbp/mbp_plugin.h" diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 847110beb..b8ca9babb 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -23,7 +23,7 @@ Revision History: #include "muz/base/dl_context.h" #include "muz/transforms/dl_mk_rule_inliner.h" #include "smt/smt_kernel.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/th_rewriter.h" #include "ast/datatype_decl_plugin.h" diff --git a/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt index 49a9f73b4..8539db7a2 100644 --- a/src/qe/CMakeLists.txt +++ b/src/qe/CMakeLists.txt @@ -10,7 +10,6 @@ z3_add_component(qe qe.cpp qe_datatype_plugin.cpp qe_dl_plugin.cpp - qe_lite.cpp qe_mbi.cpp qe_mbp.cpp qe_tactic.cpp @@ -21,9 +20,9 @@ z3_add_component(qe smt tactic mbp + qe_lite TACTIC_HEADERS nlqsat.h - qe_lite.h qe_tactic.h qsat.h ) diff --git a/src/qe/lite/CMakeLists.txt b/src/qe/lite/CMakeLists.txt new file mode 100644 index 000000000..27f9bb09d --- /dev/null +++ b/src/qe/lite/CMakeLists.txt @@ -0,0 +1,9 @@ +z3_add_component(qe_lite + SOURCES + qe_lite.cpp + COMPONENT_DEPENDENCIES + tactic + mbp + TACTIC_HEADERS + qe_lite.h +) diff --git a/src/qe/qe_lite.cpp b/src/qe/lite/qe_lite.cpp similarity index 99% rename from src/qe/qe_lite.cpp rename to src/qe/lite/qe_lite.cpp index 68ab215a2..6d337c12f 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/lite/qe_lite.cpp @@ -34,7 +34,7 @@ Revision History: #include "ast/datatype_decl_plugin.h" #include "tactic/tactical.h" #include "qe/mbp/mbp_solve_plugin.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" namespace qel { diff --git a/src/qe/qe_lite.h b/src/qe/lite/qe_lite.h similarity index 100% rename from src/qe/qe_lite.h rename to src/qe/lite/qe_lite.h diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 42c382542..efadc59e6 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -30,7 +30,7 @@ Revision History: #include "qe/mbp/mbp_arith.h" #include "qe/mbp/mbp_arrays.h" #include "qe/mbp/mbp_datatypes.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "model/model_pp.h" #include "model/model_evaluator.h" diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index c139321f9..e29694bc2 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -24,7 +24,7 @@ Notes: #include "tactic/smtlogics/smt_tactic.h" #include "qe/qe_tactic.h" #include "qe/nlqsat.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "nlsat/tactic/qfnra_nlsat_tactic.h" tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index eef9ae77a..daf020a14 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -21,7 +21,7 @@ Revision History: #include "tactic/core/propagate_values_tactic.h" #include "tactic/core/solve_eqs_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" -#include "qe/qe_lite.h" +#include "qe/lite/qe_lite.h" #include "qe/qsat.h" #include "tactic/core/ctx_simplify_tactic.h" #include "tactic/core/elim_term_ite_tactic.h"