move away from sets and into vectors for data associated with Boolean…

… variables
Z3Prover · Jan 21, 2025 · d944779 · d944779
1 parent 92ad285
commit d944779
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 7 deletions.
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
@@ -2882,6 +2882,8 @@ namespace sls {
         expr_mark visited;
         ptr_buffer<expr> todo;
 
+        m_tmp_set.reset();
+
         todo.push_back(e); 
         while (!todo.empty()) {
             auto e = todo.back();
@@ -2899,23 +2901,23 @@ namespace sls {
                     continue;
                 if (is_uninterp(e)) {
                     if (!i.fixable_atoms.contains(bv)) {
-                        i.fixable_atoms.insert(bv);
+                        i.fixable_atoms.push_back(bv);
                         i.fixable_exprs.push_back(e);
                     }
                     continue;
                 }
                 auto* ineq = get_ineq(bv);
                 if (!ineq)
                     continue;
-                i.fixable_atoms.insert(bv);
+                i.fixable_atoms.push_back(bv);
                 buffer<var_t> vars;
 
                 for (auto& [v, occ] : ineq->m_nonlinear) 
                     vars.push_back(v);
 
                 for (unsigned j = 0; j < vars.size(); ++j) {
                     auto v = vars[j];
-                    if (i.fixable_vars.contains(v))
+                    if (m_tmp_set.contains(v))
                         continue;
 
                     if (is_add(v)) {
@@ -2928,11 +2930,13 @@ namespace sls {
                     }
                     else {
                         i.fixable_exprs.push_back(m_vars[v].m_expr);
-                        i.fixable_vars.insert(v);
+                        m_tmp_set.insert(v);
                     }
                 }
             }
         }
+        for (auto v : m_tmp_set)
+            i.fixable_vars.push_back(v);
         return i.fixable_exprs;
     }
 

diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
@@ -330,9 +330,9 @@ namespace sls {
             double   score = 0;
             unsigned touched = 1;
             lbool    value = l_undef;
-            indexed_uint_set fixable_atoms;
-            uint_set          fixable_vars;
-            ptr_vector<expr>  fixable_exprs;
+            sat::bool_var_vector fixable_atoms;
+            svector<var_t>       fixable_vars;
+            ptr_vector<expr>     fixable_exprs;
             bool_info(unsigned w) : weight(w) {}
         };