From 08c4f73e32ed6b1f6e9c1009e125c16124f6de31 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Jun 2025 13:02:48 +0200 Subject: [PATCH] add dependencies to fix build --- scripts/mk_project.py | 2 +- src/tactic/portfolio/CMakeLists.txt | 1 + src/util/trace.cpp | 8 ++++++++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index a62cfe7c0..9d2aa653b 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -82,7 +82,7 @@ def init_project_def(): add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz', 'qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter', 'smtlogic_tactics'], 'tactic/ufbv') add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') - add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'fd_solver', 'qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') + add_lib('portfolio', ['simplifiers', 'smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'fd_solver', 'qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h'] add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'euf', 'arith_tactics'], 'cmd_context/extra_cmds') diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index bd927d4fc..997ad946b 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -16,6 +16,7 @@ z3_add_component(portfolio subpaving_tactic ufbv_tactic fd_solver + simplifiers TACTIC_HEADERS euf_completion_tactic.h default_tactic.h diff --git a/src/util/trace.cpp b/src/util/trace.cpp index a4123fe15..9bd46d9e7 100644 --- a/src/util/trace.cpp +++ b/src/util/trace.cpp @@ -105,11 +105,19 @@ static const tag_info* get_tag_infos() { } +static bool has_overlap(char const* s, char const* t) { + if (s[0] == t[0]) + return true; + return false; +} void enable_trace(const char * tag_str) { TraceTag tag = find_trace_tag_by_string(tag_str); if (tag == TraceTag::Count) { warning_msg("trace tag '%s' does not exist", tag_str); +#define X(tag, tag_class, desc) if (has_overlap(#tag, tag_str)) warning_msg("did you mean '%s'?", #tag); +#include "util/trace_tags.def" +#undef X return; }