mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

Print less output in non-verbose mode

Browse source
This commit is contained in:
Jakob Rath 2023-03-18 08:04:03 +01:00
parent ee64bf27d1
commit 707a5b78f7
4 changed files with 18 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/polysat/conflict.cpp
View file

@ -320,12 +320,14 @@ namespace polysat {
LOG_H3("Lemma: " << ": " << show_deref(lemma));
VERIFY(lemma);
for (auto lit : *lemma)
if (s.m_bvars.is_true(lit)) {
verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
// for (sat::literal lit : *lemma)
// verbose_stream() << " " << lit_pp(s, lit) << "\n";
}
IF_VERBOSE(1, {
for (auto lit : *lemma)
if (s.m_bvars.is_true(lit)) {
verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
for (sat::literal lit : *lemma)
verbose_stream() << " " << lit_pp(s, lit) << "\n";
}
});
s.m_simplify_clause.apply(*lemma);
lemma->set_redundant(true);

2
src/math/polysat/restart.cpp
View file

@ -40,7 +40,7 @@ namespace polysat {
s.pop_levels(s.m_level - s.base_level());
m_conflicts_at_restart = s.m_stats.m_num_conflicts;
m_restart_threshold = m_restart_init * get_luby(++m_luby_idx);
verbose_stream() << "Restart with Conflict #" << s.m_stats.m_num_conflicts << "\n";
IF_VERBOSE(10, verbose_stream() << "Restart with Conflict #" << s.m_stats.m_num_conflicts << "\n";);
s.randomize_activity();
}

6
src/math/polysat/solver.h
View file

@ -470,12 +470,12 @@ namespace polysat {
// <=> p * 2^(N - k) == 0
if (k > N) {
// parity(p) > N is never true
verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";
IF_VERBOSE(1, verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";);
return ~eq(p.manager().zero());
}
else if (k == 0) {
// parity(p) >= 0 is a tautology
verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";
IF_VERBOSE(1, verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";);
return eq(p.manager().zero());
}
else if (k == N)
@ -491,7 +491,7 @@ namespace polysat {
// <=> ~(parity(p) >= k+1)
if (k >= N) {
// parity(p) <= N is a tautology
verbose_stream() << "REDUNDANT parity constraint: parity_at_most(" << p << ", " << k << ")\n";
IF_VERBOSE(1, verbose_stream() << "REDUNDANT parity constraint: parity_at_most(" << p << ", " << k << ")\n";);
return eq(p.manager().zero());
}
else

11
src/math/polysat/viable.cpp
View file

@ -1572,12 +1572,14 @@ namespace {
else {
UNREACHABLE();
}
if (refinements % 100 == 0)
verbose_stream() << "Refinements " << refinements << "\n";
IF_VERBOSE(10, {
if (refinements % 100 == 0)
verbose_stream() << "Refinements " << refinements << "\n";
});
if (res != l_undef)
return res;
}
verbose_stream() << "Fallback\n";
IF_VERBOSE(10, verbose_stream() << "Fallback\n";);
LOG("Refinement budget exhausted! Fall back to univariate solver.");
return query_fallback<mode>(v, result);
}
@ -1730,7 +1732,6 @@ namespace {
added.insert(lit);
LOG("Adding " << lit_pp(s, lit));
IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
verbose_stream() << ";; " << lit_pp(s, lit) << "\n";
src.add_to_univariate_solver(v, s, *us, lit.to_uint());
}
}
@ -1825,7 +1826,7 @@ namespace {
}
SASSERT(!core.vars().contains(v));
core.add_lemma("viable unsat core", core.build_lemma());
verbose_stream() << "unsat core " << core << "\n";
IF_VERBOSE(10, verbose_stream() << "unsat core " << core << "\n";);
return true;
}