fixes

src/math/polysat/boolean.cpp

@@ -11,6 +11,7 @@ Author:
 
 --*/
 #include "math/polysat/boolean.h"
+#include "math/polysat/clause.h"
 #include "math/polysat/log.h"
 
 namespace polysat {
@@ -69,10 +70,10 @@ namespace polysat {
 
     std::ostream& bool_var_manager::display(std::ostream& out) const {
         for (sat::bool_var v = 0; v < size(); ++v) {
-            sat::literal lit{v};
+            sat::literal lit(v);
             if (value(lit) == l_true)
                 out << " " << lit;
-            if (value(lit) == l_false)
+            else if (value(lit) == l_false)
                 out << " " << ~lit;
         }
         return out;

src/math/polysat/conflict_core.cpp

@@ -103,7 +103,7 @@ namespace polysat {
     }
 
     void conflict_core::insert(signed_constraint c) {
-        LOG("inserting: " << c);
+        LOG("inserting: " << c << " " << c.is_always_true() << " " << c->is_marked() << " " << c->has_bvar());
         // Skip trivial constraints
         // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
         if (c.is_always_true())
@@ -164,6 +164,7 @@ namespace polysat {
             remove_literal(sat::literal(var));
         if (core_has_neg)
             remove_literal(~sat::literal(var));
+        unset_bmark(var);
 
         for (sat::literal lit : cl)
             if (lit.var() != var)

src/math/polysat/explain.cpp

@@ -78,18 +78,17 @@ namespace polysat {
             signed_constraint c = find_replacement(c2, v, core);
             if (!c)
                 continue;
-
+            if (c->contains_var(v))
-            if (!c->contains_var(v)) {
+                return l_undef;
+            if (!c->has_bvar() || l_undef == c.bvalue(s()))
                 core.keep(c);  // adds propagation of c to the search stack
+
             // NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3).
             // c alone (+ variables) is now enough to represent the conflict.
             core.reset();
             core.set(c);
             return l_true;
         }
-            else
-                return l_undef;
-        }
         return l_false;
     }
 

src/math/polysat/solver.cpp

@@ -509,11 +509,11 @@ namespace polysat {
 
     /** Conflict resolution case where boolean literal 'lit' is on top of the stack */
     void solver::resolve_bool(sat::literal lit) {       
-        LOG_H3("resolve_bool: " << lit);
         sat::bool_var const var = lit.var();
         SASSERT(m_bvars.is_propagation(var));
         // NOTE: boolean resolution should work normally even in bailout mode.
         clause* other = m_bvars.reason(var);
+        LOG_H3("resolve_bool: " << lit << " " << *other);
         m_conflict.resolve(m_constraints, var, *other);
     }
 
@@ -543,12 +543,11 @@ namespace polysat {
         SASSERT(lemma->size() > 0);
         lemma->set_justified_var(v);
         add_lemma(lemma);
-        sat::literal lit = decide_bool(*lemma);
+        decide_bool(*lemma);
-        SASSERT(lit != sat::null_literal);
     }
 
     // Guess a literal from the given clause; returns the guessed constraint
-    sat::literal solver::decide_bool(clause& lemma) {
+    void solver::decide_bool(clause& lemma) {
         LOG_H3("Guessing literal in lemma: " << lemma);
         IF_LOGGING(m_viable.log());
         LOG("Boolean assignment: " << m_bvars);
@@ -574,20 +573,21 @@ namespace polysat {
             }
         }
         LOG_V("num_choices: " << num_choices);
+        if (choice == sat::null_literal) {
+            // This case may happen when all undefined literals are false under the current variable assignment.
+            // TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case.
+            for (auto lit : lemma) 
+                set_conflict(~m_constraints.lookup(lit));
+            return;
+        }
 
         signed_constraint c = m_constraints.lookup(choice);
         push_cjust(lemma.justified_var(), c);
 
-        if (num_choices == 0) {
+        if (num_choices == 1)
-            // This case may happen when all undefined literals are false under the current variable assignment.
-            // TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case.
-            // set_conflict(lemma);
-            NOT_IMPLEMENTED_YET();
-        } else if (num_choices == 1)
             propagate_bool(choice, &lemma);
         else
             decide_bool(choice, lemma);
-        return choice;
     }
 
     /**
@@ -805,15 +805,23 @@ namespace polysat {
 
     std::ostream& solver::display(std::ostream& out) const {
         out << "Assignment:\n";
-        for (auto [v, val] : assignment()) {
+        for (auto item : m_search) {
+            if (item.is_assignment()) {
+                pvar v = item.var();
                 auto j = m_justification[v];
-            out << "\t" << assignment_pp(*this, v, val) << " @" << j.level();
+                out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level();
                 if (j.is_propagation())
                     out << " " << m_cjust[v];
                 out << "\n";
-            // out << m_viable[v] << "\n";
             }
-        out << "Boolean assignment:\n\t" << m_bvars << "\n";
+            else {
+                sat::bool_var v = item.lit().var();
+                out << "\t" << item.lit() << " @" << m_bvars.level(v);
+                if (m_bvars.reason(v))
+                    out << " " << *m_bvars.reason(v);
+                out << "\n";
+            }
+        }
         out << "Constraints:\n";
         for (auto c : m_constraints)
             out << "\t" << *c << "\n";

src/math/polysat/solver.h

@@ -153,7 +153,7 @@ namespace polysat {
         void assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma);
         void activate_constraint(signed_constraint c);
         void deactivate_constraint(signed_constraint c);
-        sat::literal decide_bool(clause& lemma);
+        void decide_bool(clause& lemma);
         void decide_bool(sat::literal lit, clause& lemma);
         void propagate_bool(sat::literal lit, clause* reason);
         void propagate_bool_at(unsigned level, sat::literal lit, clause* reason);