mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

tone down verbosity of integrity checking

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-16 20:39:15 -08:00
parent 886c62ef41
commit c1402ad70f
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/sat/sat_solver.cpp
View file

@ -1790,11 +1790,11 @@ namespace sat {
m_mc(m_model); m_mc(m_model);
if (!check_clauses(m_model)) { if (!check_clauses(m_model)) {
IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";);
IF_VERBOSE(10, m_mc.display(verbose_stream())); IF_VERBOSE(10, m_mc.display(verbose_stream()));
//IF_VERBOSE(0, display_units(verbose_stream())); //IF_VERBOSE(0, display_units(verbose_stream()));
//IF_VERBOSE(0, display(verbose_stream())); //IF_VERBOSE(0, display(verbose_stream()));
IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); IF_VERBOSE(1, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";);
throw solver_exception("check model failed"); throw solver_exception("check model failed");
} }
@ -1806,8 +1806,8 @@ namespace sat {
if (!m_clone->check_model(m_model)) { if (!m_clone->check_model(m_model)) {
//IF_VERBOSE(0, display(verbose_stream())); //IF_VERBOSE(0, display(verbose_stream()));
//IF_VERBOSE(0, display_watches(verbose_stream())); //IF_VERBOSE(0, display_watches(verbose_stream()));
IF_VERBOSE(0, m_mc.display(verbose_stream())); IF_VERBOSE(1, m_mc.display(verbose_stream()));
IF_VERBOSE(0, display_units(verbose_stream())); IF_VERBOSE(1, display_units(verbose_stream()));
//IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n")); //IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n"));
throw solver_exception("check model failed (for cloned solver)"); throw solver_exception("check model failed (for cloned solver)");
} }
@ -1819,7 +1819,7 @@ namespace sat {
for (clause const* cp : m_clauses) { for (clause const* cp : m_clauses) {
clause const & c = *cp; clause const & c = *cp;
if (!c.satisfied_by(m)) { if (!c.satisfied_by(m)) {
IF_VERBOSE(0, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";); IF_VERBOSE(1, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";);
TRACE("sat", tout << "failed: " << c << "\n"; TRACE("sat", tout << "failed: " << c << "\n";
tout << "assumptions: " << m_assumptions << "\n"; tout << "assumptions: " << m_assumptions << "\n";
tout << "trail: " << m_trail << "\n"; tout << "trail: " << m_trail << "\n";
@ -1827,7 +1827,7 @@ namespace sat {
m_mc.display(tout); m_mc.display(tout);
); );
for (literal l : c) { for (literal l : c) {
if (was_eliminated(l.var())) IF_VERBOSE(0, verbose_stream() << "eliminated: " << l << "\n";); if (was_eliminated(l.var())) IF_VERBOSE(1, verbose_stream() << "eliminated: " << l << "\n";);
} }
ok = false; ok = false;
} }
@ -1843,8 +1843,8 @@ namespace sat {
if (l.index() > l2.index()) if (l.index() > l2.index())
continue; continue;
if (value_at(l2, m) != l_true) { if (value_at(l2, m) != l_true) {
IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " := " << value_at(l, m) << " " << l2 << " := " << value_at(l2, m) << "\n"); IF_VERBOSE(1, verbose_stream() << "failed binary: " << l << " := " << value_at(l, m) << " " << l2 << " := " << value_at(l2, m) << "\n");
IF_VERBOSE(0, verbose_stream() << "elim l1: " << was_eliminated(l.var()) << " elim l2: " << was_eliminated(l2) << "\n"); IF_VERBOSE(1, verbose_stream() << "elim l1: " << was_eliminated(l.var()) << " elim l2: " << was_eliminated(l2) << "\n");
TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n");); TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n"););
ok = false; ok = false;
} }
@ -1855,7 +1855,7 @@ namespace sat {
for (literal l : m_assumptions) { for (literal l : m_assumptions) {
if (value_at(l, m) != l_true) { if (value_at(l, m) != l_true) {
VERIFY(is_external(l.var())); VERIFY(is_external(l.var()));
IF_VERBOSE(0, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";); IF_VERBOSE(1, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";);
TRACE("sat", TRACE("sat",
tout << l << " does not model check\n"; tout << l << " does not model check\n";
tout << "trail: " << m_trail << "\n"; tout << "trail: " << m_trail << "\n";
@ -1876,8 +1876,8 @@ namespace sat {
if (ok && !m_mc.check_model(m)) { if (ok && !m_mc.check_model(m)) {
ok = false; ok = false;
TRACE("sat", tout << "model: " << m << "\n"; m_mc.display(tout);); TRACE("sat", tout << "model: " << m << "\n"; m_mc.display(tout););
IF_VERBOSE(0, verbose_stream() << "model check failed\n");
} }
IF_VERBOSE(1, verbose_stream() << "model check " << (ok?"OK":"failed") << "\n";);
return ok; return ok;
} }