From 66a41383e80ff3c9c2a92460a8260096df65f291 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 14 Sep 2021 14:42:24 +0200
Subject: [PATCH] remove remove_var

---
 src/math/polysat/conflict_core.cpp | 20 --------------------
 src/math/polysat/conflict_core.h   |  3 ---
 src/math/polysat/explain.cpp       |  7 +++----
 3 files changed, 3 insertions(+), 27 deletions(-)

diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp
index 83b6b82c3..0348e505c 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict_core.cpp
@@ -141,26 +141,6 @@ namespace polysat {
         insert(c_new, c_new_premises);
     }
 
-    void conflict_core::remove_var(pvar v) {
-        LOG("Removing v" << v << " from core");
-        unsigned j = 0;
-        for (unsigned i = 0; i < m_constraints.size(); ++i)
-            if (m_constraints[i]->contains_var(v))
-                unset_mark(m_constraints[i]);
-            else
-                m_constraints[j++] = m_constraints[i];
-        m_constraints.shrink(j);
-        indexed_uint_set literals_copy = m_literals;  // TODO: can avoid copy (e.g., add a filter method for indexed_uint_set)
-        for (unsigned lit_idx : literals_copy) {
-            signed_constraint c = cm().lookup(sat::to_literal(lit_idx));
-            if (c->contains_var(v)) {
-                unset_mark(c);
-                m_literals.remove(lit_idx);
-            }
-        }
-        m_vars.remove(v);
-    }
-
     void conflict_core::set_bailout() {
         SASSERT(!is_bailout());
         m_bailout = true;
diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h
index 9ff94b71d..f306289e9 100644
--- a/src/math/polysat/conflict_core.h
+++ b/src/math/polysat/conflict_core.h
@@ -89,9 +89,6 @@ namespace polysat {
         void remove(signed_constraint c);
         void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises);
 
-        /** remove all constraints that contain the variable v */
-        void remove_var(pvar v);
-
         void keep(signed_constraint c);
 
         /** Perform boolean resolution with the clause upon variable 'var'.
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index b26ce898f..0a6a59567 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -80,10 +80,9 @@ namespace polysat {
                 continue;
 
             if (!c->contains_var(v)) {
-                core.keep(c);
-                // NOTE: more variables than 'v' might have been removed here (see polysat::test_p3), so remove_var(v) isn't enough.
-                //       also, c alone (+ variables) is now enough to represent the conflict.
-                // core.remove_var(v);
+                core.keep(c);  // adds propagation of c to the search stack
+                // NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3).
+                // c alone (+ variables) is now enough to represent the conflict.
                 core.reset();
                 core.set(c);
                 return l_true;