Remove bailout state from conflict

src/math/polysat/conflict.cpp

@@ -24,10 +24,6 @@ TODO:
     - bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something)
     - force a restart if we get a bailout lemma or non-asserting conflict?
 
-- store the side lemmas as well (but only those that justify a constraint in the final lemma, recursively)
-
-- consider case if v is both in vars and bail_vars (do we need to keep it in bail_vars even if we can eliminate it from vars?)
-
 - Find a way to use resolve_value with forbidden interval lemmas.
   Then get rid of conflict_kind_t::backtrack and m_relevant_vars.
   Maybe:
@@ -173,12 +169,6 @@ namespace polysat {
         SASSERT(empty());
     }
 
-    void conflict::set_bailout() {
-        SASSERT(m_kind == conflict_kind_t::ok);
-        m_kind = conflict_kind_t::bailout;
-        s.m_stats.m_num_bailouts++;
-    }
-
     void conflict::set_backtrack() {
         SASSERT(m_kind == conflict_kind_t::ok);
         SASSERT(m_relevant_vars.empty());
@@ -190,8 +180,6 @@ namespace polysat {
         switch (m_kind) {
         case conflict_kind_t::ok:
             return contains_pvar(v);
-        case conflict_kind_t::bailout:
-            return true;
         case conflict_kind_t::backtrack:
             return pvar_occurs_in_constraints(v) || m_relevant_vars.contains(v);
         }
@@ -431,9 +419,6 @@ namespace polysat {
 
     bool conflict::resolve_value(pvar v) {
 
-        if (is_bailout())
-            return false;
-
         if (is_backtracking()) {
             for (auto const& c : s.m_viable.get_constraints(v))
                 for (pvar v : c->vars()) {
@@ -462,12 +447,9 @@ namespace polysat {
         if (m_resolver->try_resolve_value(v, *this))
             return true;
 
-        // No conflict resolution plugin succeeded => give up and bail out
-        set_bailout();
         // Need to keep the variable in case of decision
         if (s.is_assigned(v) && j.is_decision())
             m_vars.insert(v);
-        logger().log("Bailout");
         return false;
     }
 

src/math/polysat/conflict.h

@@ -82,8 +82,6 @@ namespace polysat {
     enum class conflict_kind_t {
         // standard conflict resolution
         ok,
-        // bailout lemma because no appropriate conflict resolution method applies
-        bailout,
         // conflict contains the final lemma;
         // backtrack to and revert the last relevant decision
         // NOTE: this is currently used for the forbidden intervals lemmas.
@@ -147,9 +145,7 @@ namespace polysat {
         unsigned level() const { return m_level; }
 
         conflict_kind_t kind() const { return m_kind; }
-        bool is_bailout() const { return m_kind == conflict_kind_t::bailout; }
         bool is_backtracking() const { return m_kind == conflict_kind_t::backtrack; }
-        void set_bailout();
         void set_backtrack();
 
         bool is_relevant_pvar(pvar v) const;

src/math/polysat/inference_logger.cpp

@@ -76,9 +76,6 @@ namespace polysat {
         switch (core.kind()) {
         case conflict_kind_t::ok:
             break;
-        case conflict_kind_t::bailout:
-            out_indent() << "(bailout)\n";
-            break;
         case conflict_kind_t::backtrack:
             out_indent() << "(backtrack)\n";
             break;

src/math/polysat/solver.cpp

@@ -694,7 +694,6 @@ namespace polysat {
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
-                // if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) {
                 if (!m_conflict.is_relevant_pvar(v)) {
                     m_search.pop_assignment();
                     continue;
@@ -1217,7 +1216,6 @@ namespace polysat {
         st.update("polysat iterations",      m_stats.m_num_iterations);
         st.update("polysat decisions",       m_stats.m_num_decisions);
         st.update("polysat conflicts",       m_stats.m_num_conflicts);
-        st.update("polysat bailouts",        m_stats.m_num_bailouts);
         st.update("polysat propagations",    m_stats.m_num_propagations);
         st.update("polysat restarts",        m_stats.m_num_restarts);
         st.update("polysat viable fallback", m_stats.m_num_viable_fallback);

src/math/polysat/solver.h

@@ -52,7 +52,6 @@ namespace polysat {
             unsigned m_num_decisions;
             unsigned m_num_propagations;
             unsigned m_num_conflicts;
-            unsigned m_num_bailouts;
             unsigned m_num_restarts;
             unsigned m_num_viable_fallback;  ///< how often did we query the univariate solver
             void reset() { memset(this, 0, sizeof(*this)); }