print more information

src/math/polysat/conflict.cpp

@@ -53,16 +53,16 @@ namespace polysat {
         std::string hline() const { return std::string(70, '-'); }
 
     public:
-        void begin_conflict() {
+        void begin_conflict(char const* text) {
             ++m_conflicts;
-            LOG("Begin CONFLICT #" << m_conflicts);
+            LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")");
             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_conflicts << "\n";
+            out() << "CONFLICT #" << m_conflicts << " (" << text << ")" << "\n";
         }
 
         void log_inference(conflict const& core, inference const* inf) {
@@ -147,9 +147,9 @@ namespace polysat {
 
     conflict::~conflict() {}
 
-    void conflict::begin_conflict() {
+    void conflict::begin_conflict(char const* text) {
         if (m_logger) {
-            m_logger->begin_conflict();
+            m_logger->begin_conflict(text);
             // log initial conflict state
             m_logger->log_inference(*this, nullptr);
         }

src/math/polysat/conflict.h

@@ -133,7 +133,7 @@ namespace polysat {
         ~conflict();
 
         /// Begin next conflict
-        void begin_conflict();
+        void begin_conflict(char const* text);
         /// Log inference at the current state.
         void log_inference(inference const& inf);
         void log_inference(char const* name) { log_inference(inference_named(name)); }

src/math/polysat/explain.cpp

@@ -17,6 +17,34 @@ Author:
 
 namespace polysat {
 
+    struct post_propagate2 : public inference {
+        const char* name;
+        signed_constraint conclusion;
+        signed_constraint premise1;
+        signed_constraint premise2;
+        post_propagate2(const char* name, signed_constraint conclusion, signed_constraint premise1, signed_constraint premise2)
+            : name(name), conclusion(conclusion), premise1(premise1), premise2(premise2) {}
+        std::ostream& display(std::ostream& out) const override {
+            return out << "Post-propagate (by " << name << "), "
+                << "conclusion " << conclusion.blit() << ": " << conclusion
+                << " from " << premise1.blit() << ": " << premise1
+                << " and " << premise2.blit() << ": " << premise2;
+        }
+    };
+
+    struct inference_sup : public inference {
+        const char* name;
+        pvar var;
+        signed_constraint reduced;
+        signed_constraint reducer;
+        inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {}
+        std::ostream& display(std::ostream& out) const override {
+            return out << "Superposition (" << name << "), reduced v" << var
+                << " in " << reduced.blit() << ": " << reduced
+                << " by " << reducer.blit() << ": " << reducer;
+        }
+    };
+
     signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) {
         // c1 is true, c2 is false
         SASSERT(c1.is_currently_true(s));
@@ -62,6 +90,7 @@ namespace polysat {
             if (!c)
                 continue;
 
+            char const* inf_name = "?";
             switch (c.bvalue(s)) {
             case l_false:
                 // new conflict state based on propagation and theory conflict
@@ -69,9 +98,10 @@ namespace polysat {
                 core.insert(c1);
                 core.insert(c2);
                 core.insert(~c);
-                core.log_inference("superposition 1");
+                core.log_inference(inference_sup("1", v, c2, c1));
                 return l_true;
             case l_undef:
+                SASSERT(premises.empty());
                 // Ensure that c is assigned and justified                    
                 premises.push_back(c1);
                 premises.push_back(c2);
@@ -80,8 +110,9 @@ 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");
+                core.log_inference(post_propagate2("superposition", c, c2, c1));
-                SASSERT_EQ(l_true, c.bvalue(s));  // TODO: currently violated, check this!
+                inf_name = "2";
+                SASSERT_EQ(l_true, c.bvalue(s));
                 SASSERT(c.is_currently_false(s));
                 break;
             default:
@@ -92,7 +123,7 @@ namespace polysat {
             // c alone (+ variables) is now enough to represent the conflict.
             core.reset();
             core.set(c);
-            core.log_inference("superposition 3");
+            core.log_inference(inference_sup(inf_name, v, c2, c1));
             return c->contains_var(v) ? l_undef : l_true;
         }
         return l_false;
@@ -143,19 +174,6 @@ namespace polysat {
         }
     }
 
-    struct inference_sup : public inference {
-        const char* name;
-        pvar var;
-        signed_constraint reduced;
-        signed_constraint reducer;
-        inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {}
-        std::ostream& display(std::ostream& out) const override {
-            return out << "Superposition " << name << ", reduced v" << var
-                << " in " << reduced.blit() << ": " << reduced
-                << " by " << reducer.blit() << ": " << reducer;
-        }
-    };
-
     bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict& core) {
         pdd p = eq.eq();
         LOG("using v" << v << " " << eq);

src/math/polysat/op_constraint.cpp

@@ -225,7 +225,7 @@ namespace polysat {
         }
     }
 
-    lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) const {
+    lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) {
         auto& m = p.manager();
 
         if (p.is_val() && q.is_val() && r.is_val())
@@ -289,7 +289,7 @@ namespace polysat {
         }
     }
 
-    lbool op_constraint::eval_and(pdd const& p, pdd const& q, pdd const& r) const {
+    lbool op_constraint::eval_and(pdd const& p, pdd const& q, pdd const& r) {
         if ((p.is_zero() || q.is_zero()) && r.is_zero())
             return l_true;
 

src/math/polysat/op_constraint.h

@@ -43,10 +43,10 @@ namespace polysat {
         lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
 
         void narrow_lshr(solver& s);
-        lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r) const;
+        static lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r);
 
         void narrow_and(solver& s);
-        lbool eval_and(pdd const& p, pdd const& q, pdd const& r) const;
+        static lbool eval_and(pdd const& p, pdd const& q, pdd const& r);
 
     public:        
         ~op_constraint() override {}

src/math/polysat/solver.cpp

@@ -610,9 +610,9 @@ namespace polysat {
         ++m_stats.m_num_conflicts;
 
         SASSERT(is_conflict());
-        m_conflict.begin_conflict();
 
         if (m_conflict.conflict_var() != null_var) {
+            m_conflict.begin_conflict("backtrack_fi");
             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
@@ -620,6 +620,7 @@ namespace polysat {
             backtrack_fi();
             return;
         }
+        m_conflict.begin_conflict("resolve_conflict");
         
         search_iterator search_it(m_search);
         while (search_it.next()) {

src/math/polysat/viable.cpp

@@ -37,7 +37,7 @@ namespace polysat {
             dealloc(e);
     }
 
-    void viable::push_var(unsigned sz) {
+    void viable::push_var(unsigned bit_width) {
         m_units.push_back(nullptr);
         m_equal_lin.push_back(nullptr);
         m_diseq_lin.push_back(nullptr);
@@ -745,9 +745,9 @@ namespace polysat {
         m_usolver_factory = mk_univariate_bitblast_factory();
     }
 
-    void viable_fallback::push_var(unsigned sz) {
+    void viable_fallback::push_var(unsigned bit_width) {
         auto& mk_solver = *m_usolver_factory;
-        m_usolver.push_back(mk_solver(sz));
+        m_usolver.push_back(mk_solver(bit_width));
         m_constraints.push_back({});
     }
 

src/math/polysat/viable.h

@@ -69,7 +69,7 @@ namespace polysat {
         ~viable();
 
         // declare and remove var
-        void push_var(unsigned sz);
+        void push_var(unsigned bit_width);
         void pop_var();
 
         // undo adding/removing of entries
@@ -223,7 +223,7 @@ namespace polysat {
         return v.v.display(out, v.var);
     }
 
-
+    // TODO: don't push on each constraint add/remove; but only when necessary
     class viable_fallback {
         solver& s;
 
@@ -236,7 +236,7 @@ namespace polysat {
         viable_fallback(solver& s);
 
         // declare and remove var
-        void push_var(unsigned sz);
+        void push_var(unsigned bit_width);
         void pop_var();
 
         // add/remove constraints stored in the fallback solver