Extract inference_logger

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

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 <fstream>
+
+
+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;
+    }
+
+}

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 <ostream>
+
+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<std::ostream> 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; }
+    };
+
+}

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;