From 9766ad00b1d6038a78c8ef970c3bcf2bcf9c29ca Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 19 Aug 2022 14:12:57 +0200
Subject: [PATCH] Revert "remove overcomplicated search_iterator"

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

diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index 0f351afce..0958e7964 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -106,4 +106,74 @@ 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 7edf97ab3..256f2c1f3 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -624,9 +624,10 @@ namespace polysat {
         }
         m_conflict.begin_conflict("resolve_conflict");
         
-        for (unsigned i = m_search.size(); i-- > 0; ) {
-            auto& item = m_search[i];
-            m_search.set_resolved(i);
+        search_iterator search_it(m_search);
+        while (search_it.next()) {
+            auto& item = *search_it;
+            search_it.set_resolved();
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
@@ -721,9 +722,10 @@ namespace polysat {
      */
     void solver::backtrack_fi() {
         uint_set relevant_vars;
-        for (unsigned i = m_search.size(); i-- > 0; ) {
-            auto& item = m_search[i];
-            m_search.set_resolved(i);
+        search_iterator search_it(m_search);
+        while (search_it.next()) {
+            auto& item = *search_it;
+            search_it.set_resolved();
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();