na

src/ast/sls/bv_sls.cpp

@@ -21,6 +21,7 @@ Module Name:
 #include "ast/sls/bv_sls.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include "params/sls_params.hpp"
 
 namespace bv {
 
@@ -48,15 +49,17 @@ namespace bv {
 
     void sls::reinit_eval() {
         std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
+            auto should_keep = [&]() {
+                return m_rand() % 100 >= 95;
+            };
             if (m.is_bool(e)) {
-                if (m_eval.is_fixed0(e))
+                if (m_eval.is_fixed0(e) || should_keep())
                     return m_eval.bval0(e);
             }
             else if (bv.is_bv(e)) {
                 auto& w = m_eval.wval0(e);
-                if (w.get(w.fixed, i))
-                    return w.get(w.bits, i);
-
+                if (w.get(w.fixed, i) || should_keep())
+                    return w.get(w.bits, i);                
             }
             return m_rand() % 2 == 0;
         };
@@ -77,51 +80,59 @@ namespace bv {
             unsigned index = m_rand(m_repair_down.size());
             e = m_terms.term(m_repair_down.elem_at(index));
         }
-        else if (m_repair_up.empty()) {
+        else if (!m_repair_up.empty()) {
             unsigned index = m_rand(m_repair_up.size());
             e = m_terms.term(m_repair_up.elem_at(index));
         }
         return { !m_repair_down.empty(), e };
     }
 
     lbool sls::search() {
-        // init and init_eval were invoked.
-        unsigned& n = m_stats.m_moves;
-        n = 0;
-        for (; n < m_config.m_max_repairs && m.inc(); ++n) {
+        // 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;
-            IF_VERBOSE(20, verbose_stream() << (down ? "d " : "u ") << mk_bounded_pp(e, m, 1) << "\n");
+            IF_VERBOSE(20, verbose_stream() << (down ? "d #" : "u #")
+                << e->get_id() << ": "
+                << mk_bounded_pp(e, m, 1) << " ";
+            if (bv.is_bv(e)) verbose_stream() << m_eval.wval0(e);
+            verbose_stream() << "\n");
             if (eval_is_correct(e)) {
                 if (down)
                     m_repair_down.remove(e->get_id());
                 else
                     m_repair_up.remove(e->get_id());
             }
-            else if (down) {
-                try_repair_down(e);
-            }
+            else if (down) 
+                try_repair_down(e);            
             else
                 try_repair_up(e);
         }
         return l_undef;
     }
 
+    void sls::trace() {
+        IF_VERBOSE(2, verbose_stream()
+            << "(bvsls :restarts " << m_stats.m_restarts
+            << " :repair-down " << m_repair_down.size()
+            << " :repair-up " << m_repair_up.size() << ")\n");
+    }
+
     lbool sls::operator()() {
         lbool res = l_undef;
+        m_stats.reset();
+        m_stats.m_restarts = 0;
         do {
-            if (!m.inc())
-                return l_undef;
-
             res = search();
-
             if (res != l_undef)
-                return res;
-
+                break;
+            trace();
             reinit_eval();
         } 
-        while (m_stats.m_restarts++ < m_config.m_max_restarts);
+        while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts);
 
         return res;
     }
@@ -162,6 +173,8 @@ namespace bv {
     }
 
     bool sls::eval_is_correct(app* e) {
+        if (!m_eval.can_eval1(e))
+            return false;
         if (m.is_bool(e))
             return m_eval.bval0(e) == m_eval.bval1(e);
         if (bv.is_bv(e))
@@ -208,4 +221,9 @@ namespace bv {
         terms.reset();
         return out; 
     }
+
+    void sls::updt_params(params_ref const& _p) {
+        sls_params p(_p);
+        m_config.m_max_restarts = p.max_restarts();
+    }
 }

src/ast/sls/bv_sls.h

@@ -36,7 +36,7 @@ namespace bv {
 
         struct config {
             unsigned    m_max_restarts = 1000;
-            unsigned    m_max_repairs = 100000;
+            unsigned    m_max_repairs = 1000;
         };
 
         ast_manager&        m;
@@ -59,6 +59,7 @@ namespace bv {
 
         lbool search();
         void reinit_eval();
+        void trace();
 
     public:
         sls(ast_manager& m);
@@ -85,7 +86,7 @@ namespace bv {
         */
         lbool operator()();
 
-        void updt_params(params_ref const& p) {}
+        void updt_params(params_ref const& p);
         void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); }
         void reset_statistics() { m_stats.reset(); }
 

src/ast/sls/bv_sls_eval.cpp

@@ -171,15 +171,41 @@ namespace bv {
                 auto const& vb = wval0(b);
                 return va.eq(vb);
             }
-            UNREACHABLE();
-            break;
+            return m.are_equal(a, b);
         }
         default:
             UNREACHABLE();
+            break;
         }
         UNREACHABLE();
         return false;
     }
+
+    bool sls_eval::can_eval1(app* e) const {
+        expr* x, * y, * z;
+        if (m.is_eq(e, x, y))
+            return m.is_bool(x) || bv.is_bv(x);
+        if (m.is_ite(e, x, y, z))
+            return m.is_bool(y) || bv.is_bv(y);
+        if (e->get_family_id() == bv.get_fid()) {
+            switch (e->get_decl_kind()) {
+            case OP_BNEG_OVFL:
+            case OP_BSADD_OVFL:
+            case OP_BSDIV_OVFL:
+            case OP_BSMUL_NO_OVFL:
+            case OP_BSMUL_NO_UDFL:
+            case OP_BSMUL_OVFL:
+                return false;
+            default:
+                return true;
+            }
+        }
+        if (e->get_family_id() == basic_family_id)
+            return true;
+        if (is_uninterp_const(e))
+            return m.is_bool(e) || bv.is_bv(e);
+        return false;
+    }
 
     bool sls_eval::bval1_bv(app* e) const {
         SASSERT(m.is_bool(e));
@@ -1182,8 +1208,8 @@ namespace bv {
         if (i == 0) {
             if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones())
                 return false;            
-            if (b.is_zero())
-                return true;
+            if (b.is_zero()) 
+                return false;            
             if (!e.is_ones()) {
                 for (unsigned i = 0; i < a.nw; ++i)
                     m_tmp[i] = ~a.fixed[i] | a.bits[i];
@@ -1215,11 +1241,19 @@ namespace bv {
             a.set_repair(true, m_tmp3);
         }
         else {
+            if (e.is_one() && a.is_zero()) {
+                for (unsigned i = 0; i < a.nw; ++i)
+                    m_tmp[i] = random_bits();
+                a.clear_overflow_bits(m_tmp);
+                b.set_repair(true, m_tmp);
+                return true;
+            }
             if (e.is_one()) {
                 b.set(m_tmp, a.bits);
                 b.set_repair(true, m_tmp);
                 return true;
             }
+
             // e * b + r = a
             // b = (a - r) udiv e 
             // random version of r:

src/ast/sls/bv_sls_eval.h

@@ -134,6 +134,7 @@ namespace bv {
          * Retrieve evaluation based on immediate children.         
          */
         bool bval1(app* e) const;
+        bool can_eval1(app* e) const;
 
         svector<digit_t>& wval1(app* e) const;
 

src/ast/sls/bv_sls_fixed.cpp

@@ -11,6 +11,7 @@ Module Name:
     
 --*/
 
+#include "ast/ast_pp.h"
 #include "ast/sls/bv_sls_fixed.h"
 #include "ast/sls/bv_sls_eval.h"
 
@@ -137,12 +138,12 @@ namespace bv {
                 v.add_range(-b, a - b);
         }
         else if (!y) {
-            if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 1)
+            if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0)
                 return;
             auto& v = wval0(x);
             if (!sign)
                 v.add_range(-a, b - a + 1);
-            else
+            else 
                 v.add_range(b - a + 1, -a);
         }
         else if (x == y) {

src/ast/sls/sls_stats.h

@@ -35,13 +35,16 @@ namespace bv {
             st.update("sls restarts", m_restarts);
             st.update("sls full evals", m_full_evals);
             st.update("sls incr evals", m_incr_evals);
-            st.update("sls incr evals/sec", m_incr_evals / seconds);
+            if (seconds > 0 && m_incr_evals > 0)
+                st.update("sls incr evals/sec", m_incr_evals / seconds);
+            if (seconds > 0 && m_moves > 0)
+                st.update("sls moves/sec", m_moves / seconds);
             st.update("sls FLIP moves", m_flips);
             st.update("sls INC moves", m_incs);
             st.update("sls DEC moves", m_decs);
             st.update("sls INV moves", m_invs);
             st.update("sls moves", m_moves);
-            st.update("sls moves/sec", m_moves / seconds);
+
         }
 
     };

src/ast/sls/sls_valuation.cpp

@@ -296,6 +296,7 @@ namespace bv {
         h = mod(h, rational::power_of_two(bw));
         if (h == l)
             return;
+
         if (eq(lo, hi)) {
             set_value(lo, l);
             set_value(hi, h);

src/ast/sls/sls_valuation.h

@@ -192,19 +192,26 @@ namespace bv {
 
         std::ostream& display(std::ostream& out) const {
             out << std::hex;
-            for (unsigned i = 0; i < nw; ++i)
-                out << bits[i];
+            auto print_bits = [&](svector<digit_t> const& v) {
+                bool nz = false;
+                for (unsigned i = nw; i-- > 0;)
+                    if (nz)
+                        out << std::setw(8) << std::setfill('0') << v[i];
+                    else if (v[i] != 0)
+                        out << v[i], nz = true;
+                if (!nz)
+                    out << "0";
+            };
+
+            print_bits(bits);
             out << " ";
-            for (unsigned i = 0; i < nw; ++i)
-                out << fixed[i];
+            print_bits(fixed);
 
             if (!eq(lo, hi)) {
                 out << " [";
-                for (unsigned i = 0; i < nw; ++i)
-                    out << lo[i];
+                print_bits(lo);
                 out << ", ";
-                for (unsigned i = 0; i < nw; ++i)
-                    out << hi[i];
+                print_bits(hi);
                 out << "[";
             }
             out << std::dec;