From c1402ad70fc416b8fc8d814f7b4f85464bb451b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 20:39:15 -0800 Subject: [PATCH] tone down verbosity of integrity checking Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b933b6ddb..541c4f0f5 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1790,11 +1790,11 @@ namespace sat { m_mc(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(0, display_units(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"); } @@ -1806,8 +1806,8 @@ namespace sat { if (!m_clone->check_model(m_model)) { //IF_VERBOSE(0, display(verbose_stream())); //IF_VERBOSE(0, display_watches(verbose_stream())); - IF_VERBOSE(0, m_mc.display(verbose_stream())); - IF_VERBOSE(0, display_units(verbose_stream())); + IF_VERBOSE(1, m_mc.display(verbose_stream())); + IF_VERBOSE(1, display_units(verbose_stream())); //IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n")); throw solver_exception("check model failed (for cloned solver)"); } @@ -1819,7 +1819,7 @@ namespace sat { for (clause const* cp : m_clauses) { clause const & c = *cp; 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"; tout << "assumptions: " << m_assumptions << "\n"; tout << "trail: " << m_trail << "\n"; @@ -1827,7 +1827,7 @@ namespace sat { m_mc.display(tout); ); 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; } @@ -1843,8 +1843,8 @@ namespace sat { if (l.index() > l2.index()) continue; 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(0, verbose_stream() << "elim l1: " << was_eliminated(l.var()) << " elim l2: " << was_eliminated(l2) << "\n"); + IF_VERBOSE(1, verbose_stream() << "failed binary: " << l << " := " << value_at(l, m) << " " << l2 << " := " << value_at(l2, m) << "\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");); ok = false; } @@ -1855,7 +1855,7 @@ namespace sat { for (literal l : m_assumptions) { if (value_at(l, m) != l_true) { 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", tout << l << " does not model check\n"; tout << "trail: " << m_trail << "\n"; @@ -1876,8 +1876,8 @@ namespace sat { if (ok && !m_mc.check_model(m)) { ok = false; 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; }