resolve_bool should work normally also in bailout mode

src/math/polysat/conflict_core.cpp

@@ -83,7 +83,6 @@ namespace polysat {
         //       clause: x \/ u \/ v
         //       resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
 
-        SASSERT(!is_bailout());
         SASSERT(var != sat::null_bool_var);
         DEBUG_CODE({
             bool core_has_pos = std::count_if(begin(), end(), [var](auto c){ return c.blit() == sat::literal(var); }) > 0;
@@ -110,6 +109,7 @@ namespace polysat {
     }
 
     clause_ref conflict_core::build_lemma() {
+        LOG_H3("build lemma from core");
         sat::literal_vector literals;
         p_dependency_ref dep = m_solver->mk_dep_ref(null_dependency);
         unsigned lvl = 0;
@@ -120,6 +120,7 @@ namespace polysat {
             if (!c->has_bvar()) {
                 // temporary constraint -> keep it
                 cm().ensure_bvar(c.get());
+                LOG("new constraint: " << c);
                 // Insert the temporary constraint from saturation into \Gamma.
                 auto it = m_saturation_premises.find_iterator(c);
                 if (it != m_saturation_premises.end()) {

src/math/polysat/conflict_core.h

@@ -26,7 +26,6 @@ namespace polysat {
 
         // 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.
-        // TODO: we could always set this to the variable we're currently focusing on.
         pvar m_conflict_var = null_var;
 
         /** True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.) */

src/math/polysat/solver.cpp

@@ -556,17 +556,18 @@ 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);
-        SASSERT(m_bvars.is_propagation(lit.var()));
+        sat::bool_var const var = lit.var();
+        SASSERT(m_bvars.is_propagation(var));
 
-        if (m_conflict.is_bailout()) {
+        clause* other = m_bvars.reason(var);
-            NOT_IMPLEMENTED_YET();
-            // clause* other = m_bvars.reason(var);
-            // set_marks(*other);
-            // m_conflict.push_back(other);
-        }
 
-        clause* other = m_bvars.reason(lit.var());
+        // if (m_conflict.is_bailout()) {
-        m_conflict.resolve(m_constraints, lit.var(), *other);
+        //     for (sat::literal l : *other)
+        //         set_marks(*m_constraints.lookup(l));
+        //     // m_conflict.push_back(other);  // ???
+        // }
+
+        m_conflict.resolve(m_constraints, var, *other);
     }
 
     void solver::report_unsat() {
@@ -682,18 +683,17 @@ namespace polysat {
 
         learn_lemma(v, std::move(lemma));
 
-        // TODO: check if still necessary... won't the next solver iteration do this anyway? (well, it might choose a different variable... so this "unrolls" the next loop iteration to get a stable variable order)
-        /*
         if (is_conflict()) {
             LOG_H1("Conflict during revert_decision/learn_lemma!");
             return;
         }
+
         narrow(v);
+
         if (m_justification[v].is_unassigned()) {
             m_free_vars.del_var_eh(v);
             decide(v);
         }
-        */
     }
 
     bool solver::is_decision(search_item const& item) const {
@@ -887,6 +887,8 @@ namespace polysat {
         if (!lemma)
             return;
         LOG("Lemma: " << show_deref(lemma));
+        for (sat::literal l : *lemma)
+            LOG("   Literal " << l << " is: " << m_constraints.lookup(l));
         SASSERT(lemma->size() > 0);
         clause* cl = m_constraints.store(std::move(lemma));
         m_redundant_clauses.push_back(cl);