na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/sls/bv_sls.cpp

@@ -52,6 +52,19 @@ namespace bv {
                 m_repair_roots.insert(e->get_id());
             }
         }
+        for (auto* t : m_terms.terms()) {
+            if (t && !re_eval_is_correct(t)) 
+                m_repair_roots.insert(t->get_id());            
+        }
+    }
+
+    void sls::init_repair_goal(app* t) {
+        if (m.is_bool(t)) 
+            m_eval.set(t, m_eval.bval1(t));        
+        else if (bv.is_bv(t)) {
+            auto& v = m_eval.wval(t);
+            v.bits().copy_to(v.nw, v.eval);
+        }
     }
 
     void sls::reinit_eval() {
@@ -89,11 +102,18 @@ namespace bv {
             return { false, e };
         }
 
-        if (!m_repair_roots.empty()) {
+        while (!m_repair_roots.empty()) {
             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 };
+            if (m_terms.is_assertion(e) && !m_eval.bval1(e)) {
+                SASSERT(m_eval.bval0(e));
+                return { true, e };
+            }
+            if (!re_eval_is_correct(e)) {
+                init_repair_goal(e);
+                return { true, e };
+            }
+            m_repair_roots.remove(index);
         }
 
         return { false, nullptr };
@@ -103,11 +123,12 @@ namespace bv {
         // init and init_eval were invoked
         unsigned n = 0;
         for (; n++ < m_config.m_max_repairs && m.inc(); ) {
-            ++m_stats.m_moves;
             auto [down, e] = next_to_repair();
             if (!e)
                 return l_true;
 
+            ++m_stats.m_moves;
+
             trace_repair(down, e);
 
             if (down)
@@ -137,22 +158,12 @@ namespace bv {
 
     void sls::try_repair_down(app* e) {
 
-        if (eval_is_correct(e)) {
-//            if (bv.is_bv(e))
-//                verbose_stream() << mk_pp(e, m) << " := " << m_eval.wval(e) << "\n";
-            m_repair_roots.remove(m_repair_root);
-            m_repair_root = UINT_MAX;
-            return;
-        }
-
         unsigned n = e->get_num_args();
         if (n == 0) {
             auto& v = m_eval.wval(e);
-            v.commit_eval();
+            VERIFY(v.commit_eval());
             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;
         }        
 

src/ast/sls/bv_sls.h

@@ -46,7 +46,6 @@ 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;
@@ -55,6 +54,7 @@ namespace bv {
 
         bool eval_is_correct(app* e);
         bool re_eval_is_correct(app* e);
+        void init_repair_goal(app* e);
         void try_repair_down(app* e);
         void try_repair_up(app* e);
         void set_repair_down(expr* e) { m_repair_down = e->get_id(); }

src/ast/sls/bv_sls_eval.cpp

@@ -1100,7 +1100,7 @@ namespace bv {
         if (parity_e > 0 && parity_b > 0)
             b.shift_right(m_tmp2, std::min(parity_b, parity_e));
         a.set_mul(m_tmp, tb, m_tmp2);
-        return a.set_repair(random_bool(), m_tmp);       
+        return a.set_repair(random_bool(), m_tmp);      
     }
 
     bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {
@@ -1633,6 +1633,11 @@ namespace bv {
         }
         if (bv.is_bv(e)) {
             auto& v = eval(to_app(e));
+            for (unsigned i = 0; i < v.nw; ++i)
+                if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
+                    v.bits().copy_to(v.nw, v.eval);
+                    return false;
+                }
             v.commit_eval();
             return true;
         }

src/ast/sls/bv_sls_fixed.cpp

@@ -25,7 +25,7 @@ namespace bv {
     {}
 
     void sls_fixed::init(expr_ref_vector const& es) {
-        // init_ranges(es);
+        init_ranges(es);
         ev.sort_assertions(es);
         for (expr* e : ev.m_todo) {
             if (!is_app(e))

src/ast/sls/sls_valuation.cpp

@@ -95,14 +95,14 @@ namespace bv {
             mask = ~(digit_t)0;
     }
 
-    void sls_valuation::commit_eval() { 
-        DEBUG_CODE(
-            for (unsigned i = 0; i < nw; ++i)
-                VERIFY(0 == (fixed[i] & (m_bits[i] ^ eval[i])));
-        );
+    bool sls_valuation::commit_eval() { 
+        for (unsigned i = 0; i < nw; ++i)
+            if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))
+                return false;        
         for (unsigned i = 0; i < nw; ++i) 
             m_bits[i] = eval[i]; 
         SASSERT(well_formed()); 
+        return true;
     }
 
     bool sls_valuation::in_range(bvect const& bits) const {
@@ -446,6 +446,9 @@ namespace bv {
         if (h == l)
             return;
 
+        //verbose_stream() << "[" << l << ", " << h << "[\n";
+        //verbose_stream() << *this << "\n";
+
         SASSERT(is_zero(fixed)); // ranges can only be added before fixed bits are set.
 
         if (m_lo == m_hi) {
@@ -473,10 +476,13 @@ namespace bv {
                     set_value(m_hi, h);
             }
         }
+
+
+
         SASSERT(!has_overflow(m_lo));
         SASSERT(!has_overflow(m_hi));
-        if (!in_range(eval))
-            set(eval, m_lo);
+        if (!in_range(m_bits))
+            set(m_bits, m_lo);
         SASSERT(well_formed());
     }
 

src/ast/sls/sls_valuation.h

@@ -115,7 +115,7 @@ namespace bv {
 
         digit_t bits(unsigned i) const { return m_bits[i]; }
         bvect const& bits() const { return m_bits; }
-        void commit_eval();
+        bool commit_eval();
 
         bool get_bit(unsigned i) const { return m_bits.get(i); }
         bool try_set_bit(unsigned i, bool b) {