Update search_iterator

src/math/polysat/search_state.h

@@ -75,13 +75,14 @@ namespace polysat {
     inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); }
 
 
-    // Go backwards over the search_state
+    // 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;
+        unsigned first;  // highest index + 1
 
         struct idx_range {
             unsigned current;
@@ -89,22 +90,41 @@ namespace polysat {
         };
         vector<idx_range>     m_index_stack;
 
-    public:
+        void init() {
-        search_iterator(search_state& search):
-            m_search(&search) {
             first = m_search->size();
-            current = first;  // we start one before the beginning, then it also works for empty m_search
+            current = first - 1;
         }
 
-        search_item const& operator*() const {
+        void try_push_block() {
-            return (*m_search)[current];
+            if (first != m_search->size()) {
+                m_index_stack.push_back({current, first});
+                init();
+            }
+        }
+
+        void pop_block() {
+            current = m_index_stack.back().current;
+            first = m_index_stack.back().first;
+            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();
+            current++;  // we start one before the beginning, then it also works for empty m_search
+        }
+
+        search_item const& operator*() const {
+            return (*m_search)[current];
+        }
+
         bool next() {
+            try_push_block();
             if (current > last()) {
                 --current;
                 return true;
@@ -113,21 +133,10 @@ namespace polysat {
                 SASSERT(current == last());
                 if (m_index_stack.empty())
                     return false;
-                current = m_index_stack.back().current;
+                pop_block();
-                first = m_index_stack.back().first;
-                m_index_stack.pop_back();
                 return true;
             }
         }
-
-        // to be called after all saturations for a step are done
-        void push_block() {
-            if (first != m_search->size()) {
-                m_index_stack.push_back({current, first});
-                first = m_search->size();
-                current = first - 1;
-            }
-        }
     };
 
 }

src/math/polysat/solver.cpp

@@ -475,10 +475,10 @@ namespace polysat {
         while (search_it.next()) {
             LOG("Conflict: " << m_conflict);
             auto const& item = *search_it;
+            LOG_H2("Working on " << item);
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
-                LOG_H2("Working on pvar v" << v);
                 if (!is_marked(v))
                     continue;
                 justification& j = m_justification[v];
@@ -498,7 +498,6 @@ namespace polysat {
                 // Resolve over boolean literal
                 SASSERT(item.is_boolean());
                 sat::literal const lit = item.lit();
-                LOG_H2("Working on blit " << lit);
                 sat::bool_var const var = lit.var();
                 if (!m_bvars.is_marked(var))
                     continue;