From 309473edad780df726be0d2ea61cf03666eb888b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 17 Aug 2022 09:30:21 +0200
Subject: [PATCH] remove overcomplicated search_iterator

---
 src/math/polysat/search_state.h | 70 ---------------------------------
 src/math/polysat/solver.cpp     | 14 +++----
 2 files changed, 6 insertions(+), 78 deletions(-)

diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index 0958e7964..0f351afce 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -106,74 +106,4 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); }
 
-    // Go backwards over the search_state.
-    // If new entries are added during processing an item, they will be queued for processing next after the current item.
-    class search_iterator {
-
-        search_state*   m_search;
-
-        unsigned current;
-        unsigned first;  // highest index + 1
-
-        struct idx_range {
-            unsigned current;
-            unsigned first;  // highest index + 1
-        };
-        vector<idx_range>     m_index_stack;
-
-        void init() {
-            first = m_search->size();
-            current = first;  // we start one before the beginning
-        }
-
-        void try_push_block() {
-            if (first != m_search->size()) {
-                m_index_stack.push_back({current, first});
-                init();
-            }
-        }
-
-        void pop_block() {
-            current = m_index_stack.back().current;
-            // We don't restore 'first', otherwise 'next()' will immediately push a new block again.
-            // Instead, the current block is merged with the popped one.
-            m_index_stack.pop_back();
-        }
-
-        unsigned last() {
-            return m_index_stack.empty() ? 0 : m_index_stack.back().first;
-        }
-
-    public:
-        search_iterator(search_state& search):
-            m_search(&search) {
-            init();
-        }
-
-        void set_resolved() {
-            m_search->set_resolved(current);
-        }
-
-        search_item const& operator*() {
-            return (*m_search)[current];
-        }
-
-        bool next() {
-#if 1  // If you want to resolve over constraints that have been added during conflict resolution, enable this.
-            try_push_block();
-#endif
-            if (current > last()) {
-                --current;
-                return true;
-            }
-            else {
-                SASSERT(current == last());
-                if (m_index_stack.empty())
-                    return false;
-                pop_block();
-                return next();
-            }
-        }
-    };
-
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 256f2c1f3..7edf97ab3 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -624,10 +624,9 @@ namespace polysat {
         }
         m_conflict.begin_conflict("resolve_conflict");
         
-        search_iterator search_it(m_search);
-        while (search_it.next()) {
-            auto& item = *search_it;
-            search_it.set_resolved();
+        for (unsigned i = m_search.size(); i-- > 0; ) {
+            auto& item = m_search[i];
+            m_search.set_resolved(i);
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
@@ -722,10 +721,9 @@ namespace polysat {
      */
     void solver::backtrack_fi() {
         uint_set relevant_vars;
-        search_iterator search_it(m_search);
-        while (search_it.next()) {
-            auto& item = *search_it;
-            search_it.set_resolved();
+        for (unsigned i = m_search.size(); i-- > 0; ) {
+            auto& item = m_search[i];
+            m_search.set_resolved(i);
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();