From 8b2f1654faef0bc2d47d4af3dc49902c600386b9 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 12 Apr 2022 13:48:06 +0200 Subject: [PATCH] Better search stack printing --- src/math/polysat/log_helper.h | 36 ++++++++++++++---- src/math/polysat/search_state.cpp | 63 +++++++++++++++++++++++++++++++ src/math/polysat/search_state.h | 16 ++++++-- src/math/polysat/solver.cpp | 6 +-- 4 files changed, 107 insertions(+), 14 deletions(-) diff --git a/src/math/polysat/log_helper.h b/src/math/polysat/log_helper.h index 10408bb6c..1eb9470da 100644 --- a/src/math/polysat/log_helper.h +++ b/src/math/polysat/log_helper.h @@ -18,29 +18,51 @@ Author: #pragma once #include +#include #include #include "util/ref.h" #include "util/util.h" template struct show_deref_t { - T const* ptr; + T const* ptr; }; template std::ostream& operator<<(std::ostream& os, show_deref_t s) { - if (s.ptr) - return os << *s.ptr; - else - return os << ""; + if (s.ptr) + return os << *s.ptr; + else + return os << ""; } template show_deref_t show_deref(T* ptr) { - return show_deref_t{ptr}; + return show_deref_t{ptr}; } template ().get())>::type> show_deref_t show_deref(Ptr const& ptr) { - return show_deref_t{ptr.get()}; + return show_deref_t{ptr.get()}; +} + +/// Fill with spaces to the right: +/// out << rpad(8, "hello") +/// writes "hello ". +template +struct rpad { + unsigned width; + T const& obj; + rpad(unsigned width, T const& obj): width(width), obj(obj) {} +}; + +template +std::ostream& operator<<(std::ostream& out, rpad const& pad) { + std::stringstream tmp; + tmp << pad.obj; + auto s = tmp.str(); + out << s; + if (s.length() < pad.width) + out << std::string(pad.width - s.length(), ' '); + return out; } diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp index d49a89921..e7d23ce49 100644 --- a/src/math/polysat/search_state.cpp +++ b/src/math/polysat/search_state.cpp @@ -14,9 +14,72 @@ Author: #include "math/polysat/search_state.h" #include "math/polysat/solver.h" +#include "math/polysat/log.h" namespace polysat { + std::ostream& search_state::display_verbose(search_item const& item, std::ostream& out) const { + switch (item.kind()) { + case search_item_k::assignment: { + rational r; + pvar const v = item.var(); + auto const& j = s.m_justification[v]; + out << "v" << std::setw(3) << std::left << v << " := "; + out << std::setw(30) << std::left; + if (value(item.var(), r)) { + SASSERT_EQ(r, s.m_value[v]); + out << r; + } else + out << "*"; + out << " @" << j.level(); + switch (j.kind()) { + case justification_k::decision: + return out << " by decision"; + case justification_k::propagation: + return out << " by " << viable::var_pp(s.m_viable, v); + case justification_k::unassigned: + return out << " unassigned"; + } + } + case search_item_k::boolean: { + sat::literal const lit = item.lit(); + out << rpad(4, lit); + out << ": " << rpad(32, s.lit2cnstr(lit)); + out << " @" << s.m_bvars.level(lit); + if (s.m_bvars.is_assumption(lit)) + out << " assumption"; + else if (s.m_bvars.is_decision(lit)) { + clause* lemma = s.m_bvars.lemma(lit.var()); + out << " decision on lemma: " << show_deref(lemma); + for (auto l2 : *lemma) { + out << "\n\t" << rpad(4, l2) << ": " << rpad(16, s.lit2cnstr(l2)) << " " << bool_justification_pp(s.m_bvars, l2); + } + } + else if (s.m_bvars.is_bool_propagation(lit)) { + clause* reason = s.m_bvars.reason(lit); + out << " bool propagation " << show_deref(reason); + for (auto l2 : *reason) { + out << "\n\t" << rpad(4, l2) << ": " << rpad(16, s.lit2cnstr(l2)) << " " << bool_justification_pp(s.m_bvars, l2); + } + } + else { + SASSERT(s.m_bvars.is_value_propagation(lit)); + out << " evaluated"; + } + return out; + } + } + UNREACHABLE(); + return out; + } + + std::ostream& search_state::display_verbose(std::ostream& out) const { + out << "Search state:\n"; + for (auto const& item : m_items) + display_verbose(item, out) << "\n"; + return out; + } + std::ostream& search_state::display(search_item const& item, std::ostream& out) const { rational r; switch (item.kind()) { diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h index 82e232ed5..0958e7964 100644 --- a/src/math/polysat/search_state.h +++ b/src/math/polysat/search_state.h @@ -83,18 +83,28 @@ namespace polysat { std::ostream& display(std::ostream& out) const; std::ostream& display(search_item const& item, std::ostream& out) const; - + std::ostream& display_verbose(std::ostream& out) const; + std::ostream& display_verbose(search_item const& item, std::ostream& out) const; + }; + + struct search_state_pp { + search_state const& s; + bool verbose; + search_state_pp(search_state const& s, bool verbose = false) : s(s), verbose(verbose) {} }; struct search_item_pp { search_state const& s; search_item const& i; - search_item_pp(search_state const& s, search_item const& i) : s(s), i(i) {} + bool verbose; + search_item_pp(search_state const& s, search_item const& i, bool verbose = false) : s(s), i(i), verbose(verbose) {} }; inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); } - inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.s.display(p.i, out); } + inline std::ostream& operator<<(std::ostream& out, search_state_pp const& p) { return p.verbose ? p.s.display_verbose(out) : p.s.display(out); } + + inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); } // Go backwards over the search_state. // If new entries are added during processing an item, they will be queued for processing next after the current item. diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index b2b8e3591..3a9421fc9 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -562,10 +562,8 @@ namespace polysat { void solver::resolve_conflict() { LOG_H2("Resolve conflict"); LOG("\n" << *this); - LOG("Search state: " << m_search); - LOG("Assignment: " << assignments_pp(*this)); - for (pvar v = 0; v < m_justification.size(); ++v) - LOG("v" << v << " " << viable::var_pp(m_viable, v)); + m_conflict.begin_conflict(); + LOG(search_state_pp(m_search, true)); ++m_stats.m_num_conflicts; SASSERT(is_conflict());