mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Better search stack printing

Browse source
This commit is contained in:
Jakob Rath 2022-04-12 13:48:06 +02:00
parent 59f2603a3a
commit 00fa4b3320
4 changed files with 106 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/math/polysat/log_helper.h
View file

@ -18,29 +18,51 @@ Author:
#pragma once
#include <iostream>
#include <sstream>
#include <utility>
#include "util/ref.h"
#include "util/util.h"
template <typename T>
struct show_deref_t {
T const* ptr;
T const* ptr;
};
template <typename T>
std::ostream& operator<<(std::ostream& os, show_deref_t<T> s) {
if (s.ptr)
return os << *s.ptr;
else
return os << "<null>";
if (s.ptr)
return os << *s.ptr;
else
return os << "<null>";
}
template <typename T>
show_deref_t<T> show_deref(T* ptr) {
return show_deref_t<T>{ptr};
return show_deref_t<T>{ptr};
}
template <typename Ptr, typename T = typename std::remove_pointer<decltype(std::declval<Ptr>().get())>::type>
show_deref_t<T> show_deref(Ptr const& ptr) {
return show_deref_t<T>{ptr.get()};
return show_deref_t<T>{ptr.get()};
}
/// Fill with spaces to the right:
/// out << rpad(8, "hello")
/// writes "hello ".
template <typename T>
struct rpad {
unsigned width;
T const& obj;
rpad(unsigned width, T const& obj): width(width), obj(obj) {}
};
template <typename T>
std::ostream& operator<<(std::ostream& out, rpad<T> 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;
}

63
src/math/polysat/search_state.cpp
View file

@ -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()) {

16
src/math/polysat/search_state.h
View file

@ -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.

5
src/math/polysat/solver.cpp
View file

@ -562,10 +562,7 @@ 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));
LOG(search_state_pp(m_search, true));
++m_stats.m_num_conflicts;
SASSERT(is_conflict());