Remove bail_vars

src/math/polysat/conflict.cpp

@@ -153,7 +153,6 @@ namespace polysat {
         if (is_empty) {
             SASSERT(m_literals.empty());
             SASSERT(m_vars.empty());
-            SASSERT(m_bail_vars.empty());
             SASSERT(m_vars_occurring.empty());
             SASSERT(m_lemmas.empty());
             SASSERT(m_narrow_queue.empty());
@@ -164,7 +163,6 @@ namespace polysat {
     void conflict::reset() {
         m_literals.reset();
         m_vars.reset();
-        m_bail_vars.reset();
         m_relevant_vars.reset();
         m_var_occurrences.reset();
         m_vars_occurring.reset();
@@ -372,7 +370,6 @@ namespace polysat {
         SASSERT(!empty());
         m_literals.reset();
         m_vars.reset();
-        m_bail_vars.reset();
         m_relevant_vars.reset();
         m_var_occurrences.reset();
         m_vars_occurring.reset();
@@ -410,9 +407,10 @@ namespace polysat {
 
         // If evaluation depends on a decision,
         // then we rather keep the more general constraint c instead of inserting "x = v"
+        // TODO: the old implementation based on bail_vars is broken because it may skip relevant decisions.
+        //       is there a way to keep the same effect by adding a side lemma at this point?
         bool has_decision = false;
 #if 0
-        // TODO: this is problematic; may skip relevant decisions
         for (pvar v : c->vars())
             if (s.is_assigned(v) && s.m_justification[v].is_decision())
                 m_bail_vars.insert(v), has_decision = true;
@@ -448,9 +446,6 @@ namespace polysat {
         SASSERT(contains_pvar(v));
         auto const& j = s.m_justification[v];
 
-        if (j.is_decision() && m_bail_vars.contains(v))   // TODO: what if also m_vars.contains(v)? might have a chance at elimination
-            return false;
-
         s.inc_activity(v);
         m_vars.remove(v);
 
@@ -566,10 +561,6 @@ namespace polysat {
             out << " vars";
         for (auto v : m_vars)
             out << " v" << v;
-        if (!m_bail_vars.empty())
-            out << " bail vars";
-        for (auto v : m_bail_vars)
-            out << " v" << v;
         if (!m_lemmas.empty())
             out << " side lemmas";
         for (clause const* lemma : m_lemmas)

src/math/polysat/conflict.h

@@ -100,7 +100,6 @@ namespace polysat {
         // current conflict core consists of m_literals and m_vars
         indexed_uint_set m_literals;        // set of boolean literals in the conflict
         uint_set m_vars;                    // variable assignments used as premises, shorthand for literals (x := v)
-        uint_set m_bail_vars;               // decision variables that are only used to evaluate a constraint; see resolve_with_assignment.
         uint_set m_relevant_vars;           // tracked for cone of influence but not directly involved in conflict resolution
 
         unsigned_vector m_var_occurrences;  // for each variable, the number of constraints in m_literals that contain it
@@ -144,7 +143,6 @@ namespace polysat {
         const_iterator end() const;
 
         uint_set const& vars() const { return m_vars; }
-        uint_set const& bail_vars() const { return m_bail_vars; }
 
         unsigned level() const { return m_level; }
 
@@ -171,7 +169,7 @@ namespace polysat {
 
         bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
         bool contains(sat::literal lit) const;
-        bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
+        bool contains_pvar(pvar v) const { return m_vars.contains(v); }
         bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
         uint_set const& vars_occurring_in_constraints() const { return m_vars_occurring; }
 

src/math/polysat/inference_logger.cpp

@@ -73,10 +73,6 @@ namespace polysat {
             out_indent() << assignment_pp(s, v, s.get_value(v)) << "\n";
             m_used_vars.insert(v);
         }
-        for (auto v : core.bail_vars()) {
-            out_indent() << assignment_pp(s, v, s.get_value(v)) << " (bail)\n";
-            m_used_vars.insert(v);
-        }
         switch (core.kind()) {
         case conflict_kind_t::ok:
             break;