From e39e1dcc4949ec7dd665e680b2c1eb5693f2f0da Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 25 Aug 2022 16:03:17 +0200 Subject: [PATCH] Extract inference_logger --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/inference_logger.cpp | 134 ++++++++++++++++++++++++++ src/math/polysat/inference_logger.h | 108 +++++++++++++++++++++ src/math/polysat/solver.h | 1 + 4 files changed, 244 insertions(+) create mode 100644 src/math/polysat/inference_logger.cpp create mode 100644 src/math/polysat/inference_logger.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 6bc17c650..353dd4a22 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -8,6 +8,7 @@ z3_add_component(polysat eq_explain.cpp explain.cpp forbidden_intervals.cpp + inference_logger.cpp justification.cpp linear_solver.cpp log.cpp diff --git a/src/math/polysat/inference_logger.cpp b/src/math/polysat/inference_logger.cpp new file mode 100644 index 000000000..547aadca6 --- /dev/null +++ b/src/math/polysat/inference_logger.cpp @@ -0,0 +1,134 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat inference logging + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +Notes: + +--*/ + +#include "math/polysat/inference_logger.h" +#include "math/polysat/solver.h" +#include "math/polysat/log.h" +#include "math/polysat/log_helper.h" +#include + + +namespace polysat { + + file_inference_logger::file_inference_logger(solver& s) + : s(s) { + } + + std::ostream& file_inference_logger::out() { + SASSERT(m_out); + return *m_out; + } + + std::ostream& file_inference_logger::out_indent() { + return out() << " "; + } + + std::string file_inference_logger::hline() const { + return std::string(70, '-'); + } + + void file_inference_logger::begin_conflict(char const* text) { + ++m_num_conflicts; + if (text) + LOG("Begin CONFLICT #" << m_num_conflicts << " (" << text << ")"); + else + LOG("Begin CONFLICT #" << m_num_conflicts); + m_used_constraints.reset(); + m_used_vars.reset(); + if (!m_out) + m_out = alloc(std::ofstream, "conflicts.txt"); + else + out() << "\n\n\n\n\n\n\n\n\n\n\n\n"; + out() << "CONFLICT #" << m_num_conflicts; + if (text) + out() << " (" << text << ")"; + out() << "\n"; + // log initial conflict state + out() << hline() << "\n"; + log_conflict_state(); + } + + void file_inference_logger::log_conflict_state() { + out() << "TODO"; + /* TODO: update for new conflict + conflict2 const& core = s.m_conflict2; + for (auto const& c : core) { + out_indent() << c.blit() << ": " << c << '\n'; + m_used_constraints.insert(c.blit().index()); + for (pvar v : c->vars()) + m_used_vars.insert(v); + } + for (auto v : core.vars()) { + out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << "\n"; + m_used_vars.insert(v); + } + for (auto v : core.bail_vars()) { + out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << " (bail)\n"; + m_used_vars.insert(v); + } + if (core.is_bailout()) + out_indent() << "(bailout)\n"; + */ + out().flush(); + } + + void file_inference_logger::log_inference(inference const& inf) { + out() << hline() << "\n"; + out() << inf << "\n"; + log_conflict_state(); + } + + void file_inference_logger::log_var(pvar v) { + m_used_vars.insert(v); + } + + void file_inference_logger::log_lemma(clause_builder const& cb) { + out() << hline() << "\nLemma:"; + for (auto const& lit : cb) + out() << " " << lit; + out() << "\n"; + for (auto const& lit : cb) + out_indent() << lit_pp(s, lit) << "\n"; + // out_indent() << lit << ": " << s.lit2cnstr(lit) << "\n"; + out().flush(); + } + + 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) + if (is_relevant(item)) + 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().flush(); + LOG("End CONFLICT #" << m_num_conflicts); + } + + bool file_inference_logger::is_relevant(search_item const& item) const { + switch (item.kind()) { + case search_item_k::assignment: + return m_used_vars.contains(item.var()); + case search_item_k::boolean: + return m_used_constraints.contains(item.lit().index()); + } + UNREACHABLE(); + return false; + } + +} diff --git a/src/math/polysat/inference_logger.h b/src/math/polysat/inference_logger.h new file mode 100644 index 000000000..3c0623e24 --- /dev/null +++ b/src/math/polysat/inference_logger.h @@ -0,0 +1,108 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat inference logging + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +Notes: + + Log derivations during conflict resolution for easier debugging + +--*/ +#pragma once +#include "math/polysat/constraint.h" +#include "util/util.h" +#include + +namespace polysat { + + class clause_builder; + class search_item; + class inference; + class solver; + + class inference_logger { + public: + virtual ~inference_logger() {} + + /// Begin next conflict + virtual void begin_conflict(char const* text = nullptr) = 0; + /// Log inference and the current state. + virtual void log_inference(inference const& inf) = 0; + virtual void log_inference(char const* name) { log_inference(inference_named(name)); } + virtual void log_var(pvar v) = 0; + /// Log relevant part of search state and viable. + virtual void end_conflict() = 0; + + /// Log current conflict state (implicitly done by log_inference) + virtual void log_conflict_state() = 0; + + virtual void log_lemma(clause_builder const& cb) = 0; + }; + + class dummy_inference_logger : public inference_logger { + public: + virtual void begin_conflict(char const* text) override {} + virtual void log_inference(inference const& inf) override {} + virtual void log_var(pvar v) override {} + virtual void end_conflict() override {} + virtual void log_conflict_state() override {} + virtual void log_lemma(clause_builder const& cb) override {} + }; + + class file_inference_logger : public inference_logger { + solver& s; + uint_set m_used_constraints; + uint_set m_used_vars; + scoped_ptr m_out = nullptr; + unsigned m_num_conflicts = 0; + + std::ostream& out(); + std::ostream& out_indent(); + std::string hline() const; + + bool is_relevant(search_item const& item) const; + + public: + file_inference_logger(solver& s); + + /// Begin next conflict + void begin_conflict(char const* text) override; + /// Log inference and the current state. + void log_inference(inference const& inf) override; + void log_var(pvar v) override; + /// Log relevant part of search state and viable. + void end_conflict() override; + + /// Log current conflict state (implicitly done by log_inference) + void log_conflict_state() override; + + void log_lemma(clause_builder const& cb) override; + }; + + + + class inference { + public: + virtual ~inference() {} + virtual std::ostream& display(std::ostream& out) const = 0; + }; + + inline std::ostream& operator<<(std::ostream& out, inference const& i) { return i.display(out); } + + + + class inference_named : public inference { + char const* m_name; + public: + inference_named(char const* name) : m_name(name) { SASSERT(name); } + std::ostream& display(std::ostream& out) const override { return out << m_name; } + }; + +} diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 98bda894f..ba940d7d5 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -76,6 +76,7 @@ namespace polysat { friend class explainer; friend class inference_engine; friend class inference_logger; + friend class file_inference_logger; friend class forbidden_intervals; friend class linear_solver; friend class viable;