bailout

src/math/polysat/conflict_core.cpp

@@ -49,12 +49,6 @@ namespace polysat {
         return out;
     }
 
-    void conflict_core::set(std::nullptr_t) {
-        SASSERT(empty());
-        m_constraints.push_back({});
-        m_needs_model = false;
-    }
-
     void conflict_core::set(signed_constraint c) {
         LOG("Conflict: " << c);
         SASSERT(empty());

src/math/polysat/conflict_core.h

@@ -35,6 +35,9 @@ namespace polysat {
         //       The drawback is that we may get weaker lemmas in some cases (but they are still correct).
         //       For example: if we have 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
 
+        /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution.  */
+        bool m_bailout = false;
+
         solver* m_solver = nullptr;
         constraint_manager& cm();
         scoped_ptr_vector<variable_elimination_engine> ve_engines;
@@ -50,7 +53,8 @@ namespace polysat {
         bool needs_model() const { return m_needs_model; }
         pvar conflict_var() const { return m_conflict_var; }
 
-        bool is_bailout() const { return m_constraints.size() == 1 && !m_constraints[0]; }
+        bool is_bailout() const { return m_bailout; }
+        void set_bailout() { m_bailout = true; }
 
         bool empty() const {
             return m_constraints.empty() && !m_needs_model && m_conflict_var == null_var;
@@ -61,11 +65,10 @@ namespace polysat {
             m_needs_model = false;
             m_conflict_var = null_var;
             m_saturation_premises.reset();
+            m_bailout = false;
             SASSERT(empty());
         }
 
-        /** for bailing out with a conflict at the base level */
-        void set(std::nullptr_t);
         /** conflict because the constraint c is false under current variable assignment */
         void set(signed_constraint c);
         /** conflict because there is no viable value for the variable v */

src/math/polysat/solver.cpp

@@ -445,17 +445,13 @@ namespace polysat {
 
         SASSERT(is_conflict());
 
-        if (m_conflict.is_bailout()) {
-            report_unsat();
-            return;
-        }
-
         reset_marks();
         set_marks(m_conflict);
 
         if (m_conflict.conflict_var() != null_var) {
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
             if (!resolve_value(m_conflict.conflict_var())) {
+                m_conflict.set_bailout();
                 resolve_bailout(m_search.size() - 1);
                 return;
             }
@@ -482,6 +478,7 @@ namespace polysat {
                 }
                 SASSERT(j.is_propagation());
                 if (!resolve_value(v)) {
+                    m_conflict.set_bailout();
                     resolve_bailout(i);
                     return;
                 }
@@ -553,6 +550,7 @@ namespace polysat {
     }
 
     void solver::resolve_bailout(unsigned i) {
+        // TODO: add bailout bit to conflict state, then merge this function into resolve_conflict...; check the bailout bit in revert_decision and in resolve_value.
         ++m_stats.m_num_bailouts;
         // TODO: conflict resolution failed or was aborted. what to do with the current conflict core?
         //      (we could still use it as lemma, but it probably doesn't help much)
@@ -570,7 +568,7 @@ namespace polysat {
                 if (j.level() <= base_level())
                     break;
                 if (j.is_decision()) {
-                    revert_decision(v, true);
+                    revert_decision(v);
                     return;
                 }
                 // retrieve constraint used for propagation
@@ -698,14 +696,14 @@ namespace polysat {
      * Revert a decision that caused a conflict.
      * Variable v was assigned by a decision at position i in the search stack.
      */
-    void solver::revert_decision(pvar v, bool bailout) {
+    void solver::revert_decision(pvar v) {
         rational val = m_value[v];
         LOG_H3("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
 
         backjump(m_justification[v].level()-1);
 
-        if (bailout) {
+        if (m_conflict.is_bailout()) {
             m_viable.add_non_viable(v, val);
             return;
         }

src/math/polysat/solver.h

@@ -215,7 +215,7 @@ namespace polysat {
         bool resolve_value(pvar v);
         void resolve_bool(sat::literal lit);
         void resolve_bailout(unsigned i);
-        void revert_decision(pvar v, bool bailout = false);
+        void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);
 
         void report_unsat();