na

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Mar 5, 2024 · 9888d87 · 9888d87
1 parent f46c378
commit 9888d87
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 11 deletions.
diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp
@@ -83,16 +83,16 @@ namespace bv {
         }
 
         if (!m_repair_up.empty()) {
-            unsigned index = m_rand(m_repair_up.size());
+            unsigned index = m_repair_up.elem_at(m_rand(m_repair_up.size()));
             m_repair_up.remove(index);
-            e = m_terms.term(m_repair_up.elem_at(index));
+            e = m_terms.term(index);
             return { false, e };
         }
 
         if (!m_repair_roots.empty()) {
-            unsigned index = m_rand(m_repair_up.size());
-            e = m_terms.term(m_repair_up.elem_at(index));
-            m_repair_roots.remove(index);
+            unsigned index = m_repair_roots.elem_at(m_rand(m_repair_roots.size()));
+            e = m_terms.term(index);
+            m_repair_root = index;
             return { true, e };
         }
 
@@ -107,8 +107,6 @@ namespace bv {
             auto [down, e] = next_to_repair();
             if (!e)
                 return l_true;
-            if (eval_is_correct(e))
-                continue;
 
             trace_repair(down, e);
 
@@ -138,10 +136,23 @@ namespace bv {
     }
 
     void sls::try_repair_down(app* e) {
+
+        if (eval_is_correct(e)) {
+            m_repair_roots.remove(m_repair_root);
+            m_repair_root = UINT_MAX;
+            return;
+        }
+
         unsigned n = e->get_num_args();
         if (n == 0) {
-            m_eval.wval(e).commit_eval();
-            m_repair_up.insert(e->get_id());
+            auto& v = m_eval.wval(e);
+            v.commit_eval();
+            verbose_stream() << mk_pp(e, m) << " := " << v << "\n";
+            for (auto p : m_terms.parents(e))
+                m_repair_up.insert(p->get_id());
+            m_repair_roots.remove(m_repair_root);
+            m_repair_root = UINT_MAX;
+            return;
         }        
 
         unsigned s = m_rand(n);
@@ -152,7 +163,6 @@ namespace bv {
                 return;
             }
         }
-
         // search a new root / random walk to repair        
     }
 

diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h
@@ -46,6 +46,7 @@ namespace bv {
         sls_stats           m_stats;
         indexed_uint_set    m_repair_up, m_repair_roots;
         unsigned            m_repair_down = UINT_MAX;
+        unsigned            m_repair_root = UINT_MAX;
         ptr_vector<expr>    m_todo;
         random_gen          m_rand;
         config              m_config;

diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
@@ -297,8 +297,9 @@ namespace bv {
     }
 
     sls_valuation& sls_eval::eval(app* e) const {
-        auto& val = *m_values[e->get_id()];
+        auto& val = *m_values[e->get_id()];        
         eval(e, val);
+        verbose_stream() << "eval " << mk_pp(e, m) << " := " << val << " " << val.eval << "\n";
         return val;        
     }
 
@@ -1020,12 +1021,19 @@ namespace bv {
         unsigned parity_e = b.parity(e);
         unsigned parity_b = b.parity(b.bits());
 
+        verbose_stream() << e << " := " << a << " * " << b << "\n";
         if (b.is_zero(e)) {
             a.get_variant(m_tmp, m_rand);
             for (unsigned i = 0; i < b.bw - parity_b; ++i)
                 m_tmp.set(i, false);
             return a.set_repair(random_bool(), m_tmp);
         }
+
+        if (b.is_zero()) {
+            a.get_variant(m_tmp, m_rand);
+            return a.set_repair(random_bool(), m_tmp);            
+        }
+
 
         auto& x = m_tmp;
         auto& y = m_tmp2;