mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

logging fix

Browse source
This commit is contained in:
Jakob Rath 2023-08-17 17:32:08 +02:00
parent 0da1d9b218
commit 996012adb1
3 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/inference_logger.cpp
View file

@ -23,8 +23,13 @@ Notes:
namespace polysat {
dummy_inference_logger::dummy_inference_logger() {
// LOG("created dummy_inference_logger");
}
file_inference_logger::file_inference_logger(solver& s)
: s(s) {
// LOG("created file_inference_logger");
}
std::ostream& file_inference_logger::out() {
@ -102,7 +107,6 @@ namespace polysat {
}
void file_inference_logger::end_conflict() {
// search_state const& search, viable const& v
out() << "\n" << hline() << "\n\n";
out() << "Search state (part):\n";
for (auto const& item : s.m_search)
@ -110,7 +114,7 @@ namespace polysat {
out_indent() << search_item_pp(s.m_search, item, true) << "\n";
out() << hline() << "\nViable (part):\n";
for (pvar v : m_used_vars)
out_indent() << "v" << std::setw(3) << std::left << v << ": " << viable::var_pp(s.m_viable, v) << "\n";
out_indent() << "v" << rpad(3, v) << ": " << viable::var_pp(s.m_viable, v) << "\n";
out() << "End CONFLICT #" << m_num_conflicts << "\n";
out().flush();
LOG("End CONFLICT #" << m_num_conflicts);

1
src/math/polysat/inference_logger.h
View file

@ -77,6 +77,7 @@ namespace polysat {
class dummy_inference_logger : public inference_logger {
public:
dummy_inference_logger();
virtual void begin_conflict(displayable const& header) override {}
virtual void log(inference const& inf) override {}
virtual void log_var(pvar v) override {}

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

@ -24,8 +24,8 @@ namespace polysat {
pvar const var = item.var();
rational const& val = s.m_value[var];
auto const& j = s.m_justification[var];
out << "v" << std::setw(3) << std::left << var << " := ";
out << std::setw(30) << std::left << num_pp(s, var, val);
out << "v" << rpad(3, var) << " := ";
out << rpad(30, num_pp(s, var, val));
out << " @" << j.level();
switch (j.kind()) {
case justification_k::decision: