Add support for bailout lemma

src/math/polysat/clause_builder.cpp

@@ -17,8 +17,13 @@ Author:
 
 namespace polysat {
 
+    static_assert(!std::is_copy_assignable_v<clause_builder>);
+    static_assert(!std::is_copy_constructible_v<clause_builder>);
+    static_assert(std::is_move_assignable_v<clause_builder>);
+    static_assert(std::is_move_constructible_v<clause_builder>);
+
     clause_builder::clause_builder(solver& s):
-        m_solver(s), m_dep(nullptr, s.m_dm)
+        m_solver(&s), m_dep(nullptr, s.m_dm)
     {}
 
     void clause_builder::reset() {
@@ -29,7 +34,6 @@ namespace polysat {
     }
 
     clause_ref clause_builder::build() {
-        // TODO: here we could set all the levels of the new constraints. so we do not have to compute the max at every use site.
         clause_ref cl = clause::from_literals(m_level, std::move(m_dep), std::move(m_literals));
         m_level = 0;
         SASSERT(empty());
@@ -37,11 +41,11 @@ namespace polysat {
     }
 
     void clause_builder::add_dependency(p_dependency* d) {
-        m_dep = m_solver.m_dm.mk_join(m_dep, d);
+        m_dep = m_solver->m_dm.mk_join(m_dep, d);
     }
 
-    void clause_builder::push_literal(sat::literal lit) {
-        push(m_solver.m_constraints.lookup(lit));
+    void clause_builder::push(sat::literal lit) {
+        push(m_solver->m_constraints.lookup(lit));
     }
 
     void clause_builder::push(signed_constraint c) {

src/math/polysat/clause_builder.h

@@ -25,13 +25,17 @@ namespace polysat {
   
     // TODO: this is now incorporated in conflict_core
     class clause_builder {
-        solver&               m_solver;
+        solver*               m_solver;
         sat::literal_vector   m_literals;
         p_dependency_ref      m_dep;
         unsigned              m_level = 0;
 
     public:
         clause_builder(solver& s);
+        clause_builder(clause_builder const& s) = delete;
+        clause_builder(clause_builder&& s) = default;
+        clause_builder& operator=(clause_builder const& s) = delete;
+        clause_builder& operator=(clause_builder&& s) = default;
 
         bool empty() const { return m_literals.empty() && m_dep == nullptr && m_level == 0; }
         void reset();
@@ -43,15 +47,9 @@ namespace polysat {
 
         void add_dependency(p_dependency* d);
 
-        /// Add a literal to the clause.
-        /// Intended to be used for literals representing a constraint that already exists.
-        void push_literal(sat::literal lit);
-
+        void push(sat::literal lit);
         void push(signed_constraint c);
       
-        /// Add a constraint to the clause that does not yet exist in the solver so far.
-        // void push_new_constraint(signed_constraint c);
-
         using const_iterator = decltype(m_literals)::const_iterator;
         const_iterator begin() const { return m_literals.begin(); }
         const_iterator end() const { return m_literals.end(); }

src/math/polysat/conflict_core.cpp

@@ -149,10 +149,10 @@ namespace polysat {
         clause_builder c_lemma(*m_solver);
         for (auto premise : premises) {
             handle_saturation_premises(premise);
-            c_lemma.push_literal(~premise.blit());
+            c_lemma.push(~premise.blit());
             active_level = std::max(active_level, m_solver->m_bvars.level(premise.blit()));
         }
-        c_lemma.push_literal(c.blit());
+        c_lemma.push(c.blit());
         clause* cl = cm().store(c_lemma.build());
         if (cl->size() == 1)
             c->set_unit_clause(cl);
@@ -180,10 +180,10 @@ namespace polysat {
                 pvar v = item.var();
                 auto c = ~cm().eq(0, m_solver->var(v) - m_solver->m_value[v]);
                 cm().ensure_bvar(c.get());
-                lemma.push_literal(c.blit());
+                lemma.push(c.blit());
             } else {
                 sat::literal lit = item.lit();
-                lemma.push_literal(~lit);
+                lemma.push(~lit);
             }
             --todo;
         }
@@ -228,10 +228,12 @@ namespace polysat {
     }
 
     clause_builder conflict_core::build_lemma(unsigned reverted_level) {
-        if (is_bailout())
-            return build_fallback_lemma(reverted_level);
-        else
+        if (!is_bailout())
             return build_core_lemma(reverted_level);
+        else if (m_bailout_lemma)
+            return *std::move(m_bailout_lemma);
+        else
+            return build_fallback_lemma(reverted_level);
     }
 
     bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {

src/math/polysat/conflict_core.h

@@ -14,6 +14,7 @@ Author:
 #pragma once
 #include "math/polysat/constraint.h"
 #include "math/polysat/clause_builder.h"
+#include <optional>
 
 namespace polysat {
 
@@ -38,6 +39,7 @@ namespace polysat {
 
         /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution.  */
         bool m_bailout = false;
+        std::optional<clause_builder> m_bailout_lemma;
 
         solver* m_solver = nullptr;
         constraint_manager& cm();
@@ -69,6 +71,7 @@ namespace polysat {
             m_conflict_var = null_var;
             m_saturation_premises.reset();
             m_bailout = false;
+            m_bailout_lemma.reset();
             SASSERT(empty());
         }
 

src/math/polysat/solver.cpp

@@ -713,7 +713,7 @@ namespace polysat {
             // - drawback: might have to bail out at boolean resolution
             // Also: maybe we can skip ~L in some cases? but in that case it shouldn't be marked.
             //
-            reason_builder.push_literal(~lit);
+            reason_builder.push(~lit);
         }
         clause_ref reason = reason_builder.build();