From 87551f2bb0a46e793c81855b777f3f79d6ba387d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jul 2026 20:08:25 -0700 Subject: [PATCH] Add global suppress_platform_verbose parameter (#10319) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Adds a global configuration parameter **`suppress_platform_verbose`** (bool, default `false`). When set to `true`, memory and time information is suppressed from verbose output — the same behavior as the `-V` flag proposed in #10301, but driven by a global parameter instead of a dedicated command-line switch. This yields deterministic, platform-independent verbose output that is useful for testing and diffing. Usage: ``` z3 -v:2 suppress_platform_verbose=true problem.smt2 ``` ## Approach Instead of introducing a `-V` command-line flag (#10301), this registers `suppress_platform_verbose` as a global parameter via `env_params`, wired to a lightweight `get_suppress_platform_verbose()` flag in `util`. Verbose output sites guard only their **memory** (`mem_stat`) and **time** (`m_watch` / `:time` / `:before-memory` / `:after-memory`) fields on this flag. Platform-independent counters (e.g. `:cost`, `:threshold`, `:elim-vars`) are always emitted. Affected sites: - SAT: asymm-branch, probing, scc, simplifier (subsumer / blocked-clauses / resolution), solver stats (`sat.stats`, `:memory`, `mk_stat`) - SMT: context stats (`smt.stats`) - Tactic report (`:time`, `:before-memory`, `:after-memory`) ## Validation - Release build succeeds. - `suppress_platform_verbose` appears in `z3 -pd` with the correct type/default, and is accepted on the command line. - All 93 `test-z3 /a` unit tests pass. Closes the need for the `-V` switch in #10301. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 --- src/sat/sat_asymm_branch.cpp | 7 +++++-- src/sat/sat_probing.cpp | 5 ++++- src/sat/sat_scc.cpp | 3 ++- src/sat/sat_simplifier.cpp | 27 ++++++++++++++++++--------- src/sat/sat_solver.cpp | 19 ++++++++++++++----- src/smt/smt_context_pp.cpp | 7 +++++-- src/tactic/tactic.cpp | 12 +++++++----- src/util/env_params.cpp | 2 ++ src/util/util.cpp | 10 ++++++++++ src/util/util.h | 2 ++ 10 files changed, 69 insertions(+), 25 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 4c7aeca916..f4b1e27f5d 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -69,8 +69,11 @@ namespace sat { if (num_units > 0) verbose_stream() << " :units " << num_units; if (tr > 0) verbose_stream() << " :hte " << tr; verbose_stream() << " :cost " << m_asymm_branch.m_counter; - verbose_stream() << mem_stat(); - verbose_stream() << m_watch << ")\n";); + if (!get_suppress_platform_verbose()) { + verbose_stream() << mem_stat(); + verbose_stream() << m_watch; + } + verbose_stream() << ")\n";); } }; diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index b29e9513b1..1e4421a144 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -219,7 +219,10 @@ namespace sat { if (!p.m_equivs.empty()) verbose_stream() << " :equivs " << p.m_equivs.size(); verbose_stream() << " :cost " << p.m_counter; if (p.m_stopped_at != 0) verbose_stream() << " :stopped-at " << p.m_stopped_at; - verbose_stream() << mem_stat() << m_watch << ")\n";); + if (!get_suppress_platform_verbose()) { + verbose_stream() << mem_stat() << m_watch; + } + verbose_stream() << ")\n";); } }; diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 21ceb3c6c5..f31be48325 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -63,7 +63,8 @@ namespace sat { verbose_stream() << " (sat-scc :elim-vars " << (m_scc.m_num_elim - m_num_elim); if (elim_bin > 0) verbose_stream() << " :elim-bin " << elim_bin; if (num_units > 0) verbose_stream() << " :units " << num_units; - verbose_stream() << m_watch << ")\n";); + if (!get_suppress_platform_verbose()) verbose_stream() << m_watch; + verbose_stream() << ")\n";); } }; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 79c8a723c6..1b4a1df90c 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -840,9 +840,11 @@ namespace sat { verbose_stream() << " (sat-subsumer :subsumed " << (m_simplifier.m_num_subsumed - m_num_subsumed) << " :subsumption-resolution " << (m_simplifier.m_num_sub_res - m_num_sub_res) - << " :threshold " << m_simplifier.m_sub_counter - << mem_stat() - << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); + << " :threshold " << m_simplifier.m_sub_counter; + if (!get_suppress_platform_verbose()) + verbose_stream() << mem_stat() << " :time " + << std::fixed << std::setprecision(2) << m_watch.get_seconds(); + verbose_stream() << ")\n";); } }; @@ -1706,8 +1708,11 @@ namespace sat { report(m_simplifier.m_num_cce, m_num_cce, " :cce "); report(m_simplifier.m_num_bca, m_num_bca, " :bca "); report(m_simplifier.m_num_acce, m_num_acce, " :acce "); - verbose_stream() << mem_stat() - << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); + if (!get_suppress_platform_verbose()) { + verbose_stream() << mem_stat() + << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds(); + } + verbose_stream() << ")\n";); } void report(unsigned n, unsigned m, char const* s) { @@ -2063,11 +2068,15 @@ namespace sat { ~elim_var_report() { m_watch.stop(); IF_VERBOSE(SAT_VB_LVL, - verbose_stream() << " (sat-resolution :elim-vars " + verbose_stream() + << " (sat-resolution :elim-vars " << (m_simplifier.m_num_elim_vars - m_num_elim_vars) - << " :threshold " << m_simplifier.m_elim_counter - << mem_stat() - << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); + << " :threshold " << m_simplifier.m_elim_counter; + if (!get_suppress_platform_verbose()) + verbose_stream() + << mem_stat() + << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds(); + verbose_stream() << ")\n";); } }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 634b09830e..b4c436ec37 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2327,8 +2327,11 @@ namespace sat { strm << "(sat.stats " << std::setw(6) << m_stats.m_conflicts << " " << std::setw(6) << m_stats.m_decision << " " << std::setw(4) << m_stats.m_restart - << mk_stat(*this) - << " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n"; + << mk_stat(*this); + if (!get_suppress_platform_verbose()) { + strm << " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds(); + } + strm << ")\n"; std::string str = std::move(strm).str(); svector nums; for (size_t i = 0; i < str.size(); ++i) { @@ -4797,8 +4800,12 @@ namespace sat { out << " :ternary-clauses " << num_ter << "\n"; out << " :clauses " << num_cls << "\n"; out << " :del-clause " << m_stats.m_del_clause << "\n"; - out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast(num_lits) / static_cast(total_cls)) << "\n"; - out << " :memory " << std::fixed << std::setprecision(2) << mem << ")" << std::endl; + out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast(num_lits) / static_cast(total_cls)); + if (!get_suppress_platform_verbose()) { + out << "\n"; + out << " :memory " << std::fixed << std::setprecision(2) << mem; + } + out << ")" << std::endl; } void stats::collect_statistics(statistics & st) const { @@ -4835,7 +4842,9 @@ namespace sat { out << " " << std::setw(5) << (m_solver.m_learned.size() + redundant - m_solver.m_num_frozen) << "/" << redundant; out << " " << std::setw(3) << m_solver.init_trail_size(); out << " " << std::setw(7) << m_solver.m_stats.m_gc_clause << " "; - out << " " << std::setw(7) << mem_stat(); + if (!get_suppress_platform_verbose()) { + out << " " << std::setw(7) << mem_stat(); + } } std::ostream & operator<<(std::ostream & out, mk_stat const & stat) { diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 10d6f624b8..022656bd53 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -726,8 +726,11 @@ namespace smt { << std::setw(5) << (m_aux_clauses.size() + bin_clauses) << '/' << bin_clauses << '/' << num_units() << ' ' << std::setw(7) << m_lemmas.size() << '/' << bin_lemmas << ' ' << std::setw(5) << m_stats.m_num_simplifications << ' ' - << std::setw(4) << m_stats.m_num_del_clauses << ' ' - << std::setw(7) << mem_stat() << ")\n"; + << std::setw(4) << m_stats.m_num_del_clauses; + if (!get_suppress_platform_verbose()) { + strm << ' ' << std::setw(7) << mem_stat(); + } + strm << ")\n"; std::string str = std::move(strm).str(); svector offsets; diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 71faa912de..cc63664ad4 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -47,11 +47,13 @@ struct tactic_report::imp { IF_VERBOSE(0, verbose_stream() << "(" << m_id << " :num-exprs " << m_goal.num_exprs() - << " :num-asts " << m_goal.m().get_num_asts() - << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() - << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory - << " :after-memory " << std::fixed << std::setprecision(2) << end_memory - << ")\n"); + << " :num-asts " << m_goal.m().get_num_asts(); + if (!get_suppress_platform_verbose()) + verbose_stream() + << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() + << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory + << " :after-memory " << std::fixed << std::setprecision(2) << end_memory; + verbose_stream() << ")\n"); IF_VERBOSE(20, m_goal.display(verbose_stream() << m_id << "\n")); SASSERT(m_goal.is_well_formed()); } diff --git a/src/util/env_params.cpp b/src/util/env_params.cpp index 80a1195aa5..616290df9a 100644 --- a/src/util/env_params.cpp +++ b/src/util/env_params.cpp @@ -25,6 +25,7 @@ Notes: void env_params::updt_params() { params_ref const& p = gparams::get_ref(); set_verbosity_level(p.get_uint("verbose", get_verbosity_level())); + set_suppress_platform_verbose(p.get_bool("suppress_platform_verbose", get_suppress_platform_verbose())); enable_warning_messages(p.get_bool("warning", true)); memory::set_max_size(megabytes_to_bytes(p.get_uint("memory_max_size", 0))); memory::set_max_alloc_count(p.get_uint("memory_max_alloc_count", 0)); @@ -36,6 +37,7 @@ void env_params::updt_params() { void env_params::collect_param_descrs(param_descrs & d) { d.insert("verbose", CPK_UINT, "be verbose, where the value is the verbosity level", "0"); + d.insert("suppress_platform_verbose", CPK_BOOL, "suppress memory and time information from verbose output", "false"); d.insert("warning", CPK_BOOL, "enable/disable warning messages", "true"); d.insert("memory_max_size", CPK_UINT, "set hard upper limit for memory consumption (in megabytes), if 0 then there is no limit", "0"); d.insert("memory_max_alloc_count", CPK_UINT, "set hard upper limit for memory allocations, if 0 then there is no limit", "0"); diff --git a/src/util/util.cpp b/src/util/util.cpp index d60f8467a6..b158cf9508 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -30,6 +30,16 @@ unsigned get_verbosity_level() { return g_verbosity_level; } +static bool g_suppress_platform_verbose = false; + +void set_suppress_platform_verbose(bool suppress) { + g_suppress_platform_verbose = suppress; +} + +bool get_suppress_platform_verbose() { + return g_suppress_platform_verbose; +} + static std::ostream* g_verbose_stream = &std::cerr; void set_verbose_stream(std::ostream& str) { diff --git a/src/util/util.h b/src/util/util.h index b4e8078d40..b1415671d2 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -197,6 +197,8 @@ struct delete_proc { void set_verbosity_level(unsigned lvl); unsigned get_verbosity_level(); +void set_suppress_platform_verbose(bool suppress); +bool get_suppress_platform_verbose(); std::ostream& verbose_stream(); void set_verbose_stream(std::ostream& str);