conflict logging

src/math/polysat/conflict.cpp

@@ -31,18 +31,119 @@ Notes:
 #include "math/polysat/saturation.h"
 #include "math/polysat/variable_elimination.h"
 #include <algorithm>
+#include <fstream>
 
 namespace polysat {
 
-    conflict::conflict(solver& s):s(s) {
+    class inference_logger {
+        uint_set m_used_constraints;
+        uint_set m_used_vars;
+        scoped_ptr<std::ostream> m_out = nullptr;
+        unsigned m_conflicts = 0;
+
+        std::ostream& out() {
+            SASSERT(m_out);
+            return *m_out;
+        }
+
+        std::ostream& out_indent() { return out() << "    "; }
+
+        std::string hline() const { return std::string(70, '-'); }
+
+    public:
+        void begin_conflict() {
+            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" << hline() << "\n" << hline() << "\n" << hline() << "\n\n\n\n\n";
+            out() << "CONFLICT #" << ++m_conflicts << "\n";
+        }
+
+        void log_inference(conflict const& core, inference const* inf) {
+            out() << hline() << "\n";
+            if (inf)
+                out() << *inf << "\n";
+            if (core.conflict_var() != null_var) {
+                out_indent() << "Conflict var: " << core.conflict_var() << "\n";
+                m_used_vars.insert(core.conflict_var());
+            }
+            for (auto const& c : core) {
+                out_indent() << c.blit() << ": " << c << '\n';
+                m_used_constraints.insert(c.blit().index());
+            }
+            for (auto v : core.vars()) {
+                out_indent() << "v" << v << "\n";
+                m_used_vars.insert(v);
+            }
+            for (auto v : core.bail_vars()) {
+                out_indent() << "v" << v << " (bail)\n";
+                m_used_vars.insert(v);
+            }
+            out().flush();
+        }
+
+        void log_lemma(clause_builder const& cb) {
+            out() << hline() << "\nLemma:";
+            for (auto const& lit : cb)
+                out() << " " << lit;
+            out() << "\n";
+            out().flush();
+        }
+
+        void log_gamma(search_state const& m_search) {
+            out() << "\n" << hline() << "\n\n";
+            out() << "Search state (part):\n";
+            for (auto const& item : m_search)
+                if (is_relevant(item))
+                    out_indent() << search_item_pp(m_search, item, true) << "\n";
+            // TODO: log viable
+            out().flush();
+        }
+
+        bool 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;
+        }
+    };
+
+    conflict::conflict(solver& s): s(s) {
         ex_engines.push_back(alloc(ex_polynomial_superposition, s));
         ex_engines.push_back(alloc(eq_explain, s));
         ve_engines.push_back(alloc(ve_reduction));
         inf_engines.push_back(alloc(inf_saturate, s));
+        // TODO: how to set this on the CLI? "polysat.log_conflicts=true" doesn't seem to work although z3 accepts it
+        if (true || s.get_config().m_log_conflicts)
+            m_logger = alloc(inference_logger);
     }
 
     conflict::~conflict() {}
 
+    void conflict::begin_conflict() {
+        if (m_logger) {
+            m_logger->begin_conflict();
+            // log initial conflict state
+            m_logger->log_inference(*this, nullptr);
+        }
+    }
+
+    void conflict::log_inference(inference const& inf) {
+        if (m_logger)
+            m_logger->log_inference(*this, &inf);
+    }
+
+    void conflict::log_gamma() {
+        if (m_logger)
+            m_logger->log_gamma(s.m_search);
+    }
+
     constraint_manager& conflict::cm() const { return s.m_constraints; }
 
     std::ostream& conflict::display(std::ostream& out) const {
@@ -176,6 +277,7 @@ namespace polysat {
      * NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
      * Ensure that c is assigned and justified
      */
+    // TODO: rename this; it pushes onto \Gamma and doesn't insert into the core
     void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
         // keep(c);
         clause_builder c_lemma(s);
@@ -217,6 +319,15 @@ namespace polysat {
         s.m_stats.m_num_bailouts++;
     }
 
+    struct inference_resolve : public inference {
+        sat::literal m_lit;
+        clause const& m_clause;
+        inference_resolve(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {}
+        std::ostream& display(std::ostream& out) const override {
+            return out << "Resolve upon " << m_lit << " with " << m_clause;
+        }
+    };
+
     void conflict::resolve(sat::literal lit, clause const& cl) {
         // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
         //       clause: x \/ u \/ v
@@ -233,8 +344,22 @@ namespace polysat {
         for (sat::literal lit2 : cl)
             if (lit2 != lit)
                 insert(s.lit2cnstr(~lit2));
+        log_inference(inference_resolve(lit, cl));
     }
 
+    struct inference_resolve_with_assignment : public inference {
+        solver& s;
+        sat::literal lit;
+        signed_constraint c;
+        inference_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
+        std::ostream& display(std::ostream& out) const override {
+            out << "Resolve upon " << lit << " with assignment:";
+            for (pvar v : c->vars())
+                out << " " << assignment_pp(s, v, s.get_value(v), true);
+            return out;
+        }
+    };
+
     void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) {
         // The reason for lit is conceptually:
         //    x1 = v1 /\ ... /\ xn = vn ==> lit
@@ -259,6 +384,7 @@ namespace polysat {
                     m_vars.insert(v);            
                 }
         }
+        log_inference(inference_resolve_with_assignment(s, lit, c));
     }
 
     clause_builder conflict::build_lemma() {
@@ -280,6 +406,9 @@ namespace polysat {
         }        
         s.decay_activity();
 
+        if (m_logger)
+            m_logger->log_lemma(lemma);
+
         return lemma;
     }
 
@@ -309,10 +438,20 @@ namespace polysat {
         m_vars.reset();
         for (auto const& [v, val] : a)
             m_vars.insert(v);
+        log_inference("minimize vars");
         LOG("reduced " << m_vars);
     }
 
 
+    struct inference_resolve_value : public inference {
+        solver& s;
+        pvar v;
+        inference_resolve_value(solver& s, pvar v) : s(s), v(v) {}
+        std::ostream& display(std::ostream& out) const override {
+            return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true);
+        }
+    };
+
     bool conflict::resolve_value(pvar v) {
         // NOTE:
         // In the "standard" case where "v = val" is on the stack:
@@ -353,6 +492,7 @@ namespace polysat {
     bailout:
         if (s.is_assigned(v) && j.is_decision())
             m_vars.insert(v);
+        log_inference(inference_resolve_value(s, v));
         return false;
     }
 

src/math/polysat/conflict.h

@@ -81,6 +81,22 @@ namespace polysat {
     class inference_engine;
     class variable_elimination_engine;
     class conflict_iterator;
+    class inference_logger;
+
+    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; }
+    };
 
     /** Conflict state, represented as core (~negation of clause). */
     class conflict {
@@ -90,6 +106,8 @@ namespace polysat {
         uint_set m_vars;                    // variable assignments used as premises
         uint_set m_bail_vars;
 
+        scoped_ptr<inference_logger> m_logger;
+
         // If this is not null_var, the conflict was due to empty viable set for this variable.
         // Can be treated like "v = x" for any value x.
         pvar m_conflict_var = null_var;
@@ -113,6 +131,14 @@ namespace polysat {
         conflict(solver& s);
         ~conflict();
 
+        /// Begin next conflict
+        void begin_conflict();
+        /// Log inference at the current state.
+        void log_inference(inference const& inf);
+        void log_inference(char const* name) { log_inference(inference_named(name)); }
+        /// Log relevant part of search state.
+        void log_gamma();
+
         pvar conflict_var() const { return m_conflict_var; }
 
         bool is_bailout() const { return m_bailout; }
@@ -168,6 +194,9 @@ namespace polysat {
         const_iterator begin() const;
         const_iterator end() const;
 
+        uint_set const& vars() const { return m_vars; }
+        uint_set const& bail_vars() const { return m_bail_vars; }
+
         std::ostream& display(std::ostream& out) const;
     };
 

src/math/polysat/eq_explain.cpp

@@ -25,7 +25,6 @@ namespace polysat {
      * a << (K - az - 1) = 0 or v << az = 0
      * 
      */
-    
     bool eq_explain::explain_zero(pvar v, pdd & a, pdd & b, signed_constraint c, conflict& core) {
         pdd bv = s.subst(b);
         if (!bv.is_zero())
@@ -40,6 +39,7 @@ namespace polysat {
         core.propagate(s.eq(b));
         core.propagate(~s.eq(a.shl(K - az - 1)));
         core.propagate(~s.eq(b.shl(az)));
+        core.log_inference("explain_zero");
         return true;
     }
 

src/math/polysat/explain.cpp

@@ -69,6 +69,7 @@ namespace polysat {
                 core.insert(c1);
                 core.insert(c2);
                 core.insert(~c);
+                core.log_inference("superposition 1");
                 return l_true;
             case l_undef:
                 // Ensure that c is assigned and justified                    
@@ -79,6 +80,7 @@ namespace polysat {
                 // gets created, c is assigned to false by evaluation propagation
                 // It should have been assigned true by unit propagation.
                 core.replace(c2, c, premises);
+                core.log_inference("superposition 2");
                 SASSERT_EQ(l_true, c.bvalue(s));  // TODO: currently violated, check this!
                 SASSERT(c.is_currently_false(s));
                 break;
@@ -90,6 +92,7 @@ namespace polysat {
             // c alone (+ variables) is now enough to represent the conflict.
             core.reset();
             core.set(c);
+            core.log_inference("superposition 3");
             return c->contains_var(v) ? l_undef : l_true;
         }
         return l_false;
@@ -171,7 +174,7 @@ namespace polysat {
                 vector<signed_constraint> premises;
                 premises.push_back(c);
                 premises.push_back(eq);
-                core.insert(c2, premises);
+                core.insert(c2, premises);  // TODO: insert but then we reset? ... (this call does not insert into the core)
             }
             //    core.keep(c2);  // adds propagation of c to the search stack
             core.reset();
@@ -182,9 +185,11 @@ namespace polysat {
                 core.insert(eq);
                 core.insert(c);
                 core.insert(~c2);
+                core.log_inference("superposition 4");
                 return true;
             }
             core.set(c2);
+            core.log_inference("superposition 5");
             return true;
         }
         return false;

src/math/polysat/saturation.cpp

@@ -61,7 +61,7 @@ namespace polysat {
     * Propagate c. It is added to reason and core all other literals in reason are false in current stack.
     * The lemmas outlined in the rules are valid and therefore c is implied.
     */
-    bool inf_saturate::propagate(conflict& core, inequality const& _crit1, inequality const& _crit2, signed_constraint& c) {
+    bool inf_saturate::propagate(char const* inf_name, conflict& core, inequality const& _crit1, inequality const& _crit2, signed_constraint& c) {
 
         auto crit1 = _crit1.as_signed_constraint();
         auto crit2 = _crit2.as_signed_constraint();
@@ -90,13 +90,14 @@ namespace polysat {
         if (c.bvalue(s) != l_false)
             core.insert_vars(c);
         core.insert(~c);       
+        core.log_inference(inf_name);
         LOG("Core " << core);
         return true;        
     }
 
-    bool inf_saturate::propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs) {
+    bool inf_saturate::propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs) {
         signed_constraint c = ineq(is_strict, lhs, rhs);
-        return propagate(core, crit1, crit2, c);
+        return propagate(inf_name, core, crit1, crit2, c);
     }
 
     /// Add premises for Ω*(x, y)
@@ -297,7 +298,7 @@ namespace polysat {
         if (!xy_l_xz.is_strict)
             m_new_constraints.push_back(~s.eq(x));
         push_omega(x, y);
-        return propagate(core, xy_l_xz, xy_l_xz, xy_l_xz.is_strict, y, z);
+        return propagate("ugt_x", core, xy_l_xz, xy_l_xz, xy_l_xz.is_strict, y, z);
     }
 
     /// [y] z' <= y /\ zx > yx  ==>  Ω*(x,y) \/ zx > z'x
@@ -311,7 +312,7 @@ namespace polysat {
         pdd const& z_prime = le_y.lhs;
         m_new_constraints.reset();
         push_omega(x, y);
-        return propagate(core, le_y, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x);
+        return propagate("ugt_y", core, le_y, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x);
     }
 
     bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& yx_l_zx) {
@@ -369,7 +370,7 @@ namespace polysat {
             return false;
         m_new_constraints.reset();       
         push_omega(a, z);
-        return propagate(core, y_l_ax, x_l_z, x_l_z.is_strict || y_l_ax.is_strict, y, a * z);
+        return propagate("y_l_ax_and_x_l_z", core, y_l_ax, x_l_z, x_l_z.is_strict || y_l_ax.is_strict, y, a * z);
     }
 
 
@@ -405,7 +406,7 @@ namespace polysat {
         m_new_constraints.reset();
         push_omega(x, y_prime);
         // yx <= y'x
-        return propagate(core, yx_l_zx, z_l_y, z_l_y.is_strict || yx_l_zx.is_strict, y * x, y_prime * x);
+        return propagate("ugt_z", core, yx_l_zx, z_l_y, z_l_y.is_strict || yx_l_zx.is_strict, y * x, y_prime * x);
     }
 
     // [x] p(x) <= q(x) where value(p) > value(q)
@@ -456,7 +457,7 @@ namespace polysat {
                 return false;
             m_new_constraints.push_back(d);
             auto conseq = s.ult(r_val, c.rhs);
-            return propagate(core, c, c, conseq);
+            return propagate("tangent (strict)", core, c, c, conseq);
         }
         else {
             auto d = s.ule(c.rhs, r_val);
@@ -464,7 +465,7 @@ namespace polysat {
                 return false;
             m_new_constraints.push_back(d);
             auto conseq = s.ule(c.lhs, r_val);
-            return propagate(core, c, c, conseq);
+            return propagate("tangent (non-strict)", core, c, c, conseq);
         }
     }
 

src/math/polysat/saturation.h

@@ -43,8 +43,8 @@ namespace polysat {
         void push_omega(pdd const& x, pdd const& y);
         void push_omega_bisect(pdd const& x, rational x_max, pdd const& y, rational y_max);
         signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
-        bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c);
+        bool propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c);
-        bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs);
+        bool propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs);
 
         bool try_ugt_x(pvar v, conflict& core, inequality const& c);
 

src/math/polysat/search_state.cpp

@@ -25,12 +25,12 @@ namespace polysat {
             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;
+            out << std::setw(30) << std::left << s.m_value[v];
-            if (value(item.var(), r)) {
+            // if (value(item.var(), r)) {
-                SASSERT_EQ(r, s.m_value[v]);
+            //     SASSERT_EQ(r, s.m_value[v]);
-                out << r;
+            //     out << r;
-            } else
+            // } else
-                out << "*";
+            //     out << "*";
             out << " @" << j.level();
             switch (j.kind()) {
             case justification_k::decision:

src/math/polysat/solver.cpp

@@ -566,10 +566,12 @@ namespace polysat {
         ++m_stats.m_num_conflicts;
 
         SASSERT(is_conflict());
-        
+        m_conflict.begin_conflict();
+
         if (m_conflict.conflict_var() != null_var) {
             pvar v = m_conflict.conflict_var();
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
+            // TODO: use unsat core from m_viable_fallback if the conflict is from there
             VERIFY(m_viable.resolve(v, m_conflict));
             // TBD: saturate resulting conflict to get better lemmas.
             LOG("try-eliminate v" << v);
@@ -600,6 +602,7 @@ namespace polysat {
                 inc_activity(v);
                 justification& j = m_justification[v];
                 if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
+                    m_conflict.log_gamma();
                     revert_decision(v);
                     return;
                 }
@@ -620,6 +623,7 @@ namespace polysat {
                 if (m_bvars.is_assumption(var))
                     continue;
                 else if (m_bvars.is_decision(var)) {
+                    m_conflict.log_gamma();
                     revert_bool_decision(lit);
                     return;
                 }
@@ -631,8 +635,7 @@ namespace polysat {
                 }
             }
         }
-        // here we build conflict clause if it has free variables.
+        m_conflict.log_gamma();
-        // the last decision is reverted.
         report_unsat();
     }
 
@@ -1030,9 +1033,12 @@ namespace polysat {
         out << "v" << var << " := ";
         rational const& p = rational::power_of_two(s.size(var));
         if (val > mod(-val, p))
-            return out << -mod(-val, p);
+            out << -mod(-val, p);
         else 
-            return out << val;
+            out << val;
+        if (with_justification)
+            out << " (" << s.m_justification[var] << ")";
+        return out;
     }
     
 

src/math/polysat/solver.h

@@ -421,8 +421,9 @@ namespace polysat {
         solver const& s;
         pvar var;
         rational const& val;
+        bool with_justification;
     public:
-        assignment_pp(solver const& s, pvar var, rational const& val): s(s), var(var), val(val) {}
+        assignment_pp(solver const& s, pvar var, rational const& val, bool with_justification = false): s(s), var(var), val(val), with_justification(with_justification) {}
         std::ostream& display(std::ostream& out) const;
     };
 

src/math/polysat/variable_elimination.cpp

@@ -24,6 +24,7 @@ namespace polysat {
             if (!c->contains_var(v) && c.is_currently_false(s)) {
                 core.reset();
                 core.set(c);
+                core.log_inference("ve_reduction");
                 return true;
             }                
         }

src/math/polysat/viable.cpp

@@ -649,6 +649,7 @@ namespace polysat {
                 break;
             }
         }
+        core.log_inference("forbidden intervals");
         return true;
     }