mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 20:23:27 +00:00
Code Activity

Add global suppress_platform_verbose parameter (#10319)

Browse source 
## 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
This commit is contained in:
Nikolaj Bjorner 2026-07-30 20:08:25 -07:00 • committed by GitHub
parent bffbe2475f
commit 87551f2bb0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 69 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/sat/sat_solver.cpp
View file

@ -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<size_t> 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<double>(num_lits) / static_cast<double>(total_cls)) << "\n";
out << " :memory " << std::fixed << std::setprecision(2) << mem << ")" << std::endl;
out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast<double>(num_lits) / static_cast<double>(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) {