h

- avoid more platform specific behavior when using m_mk_extract,
- rename mk_eq in bool_rewriter to mk_eq_plain to distinguish it from mk_eq_rw
- rework bv_lookahead to be more closely based on sls_engine, which has much better heuristic behavior than attempt 1.

src/ast/rewriter/bool_rewriter.cpp

@@ -671,24 +671,28 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
     expr* cond2 = nullptr, *t2 = nullptr, *e2 = nullptr;
     if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2) &&
         BR_FAILED != try_ite_value(to_app(t), val, result)) {
-        result = m().mk_ite(cond, result, mk_eq(e, val));
+        result = m().mk_ite(cond, result, mk_eq_plain(e, val));
         return BR_REWRITE2;
     }
     if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2) && 
         BR_FAILED != try_ite_value(to_app(e), val, result)) {
-        result = m().mk_ite(cond, mk_eq(t, val), result);
+        result = m().mk_ite(cond, mk_eq_plain(t, val), result);
         return BR_REWRITE2;
     }
 
     return BR_FAILED;
 }
 
 
-app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
+app* bool_rewriter::mk_eq_plain(expr* lhs, expr* rhs) {
     if (m().are_equal(lhs, rhs))
         return m().mk_true();
     if (m().are_distinct(lhs, rhs))
         return m().mk_false();
+    if (m().is_false(rhs)) {
+        verbose_stream() << "here\n";
+    }
+    VERIFY(!m().is_false(rhs));
     return m().mk_eq(lhs, rhs);
 }
 
@@ -775,7 +779,8 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             std::swap(lhs, rhs);
 
         if (m().is_not(lhs, lhs)) {
-            result = m().mk_not(m().mk_eq(lhs, rhs));
+            mk_eq(lhs, rhs, result);
+            mk_not(result, result);
             return BR_REWRITE2;
         }
 

src/ast/rewriter/bool_rewriter.h

@@ -135,11 +135,11 @@ class bool_rewriter {
     br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
     br_status mk_not_core(expr * t, expr_ref & result);
 
-    app* mk_eq(expr* lhs, expr* rhs);
+    app* mk_eq_plain(expr* lhs, expr* rhs);
 
     void mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
         if (mk_eq_core(lhs, rhs, result) == BR_FAILED)
-            result = mk_eq(lhs, rhs);
+            result = mk_eq_plain(lhs, rhs);
     }
     expr_ref mk_eq_rw(expr* lhs, expr* rhs) {
         expr_ref r(m()), _lhs(lhs, m()), _rhs(rhs, m());

src/ast/rewriter/bv_rewriter.cpp

@@ -640,8 +640,13 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
             // use the equivalence to simplify:
             // #x000f <=_u b <=> b[sz-1:lnz+1] != 0 or #xf <= b[lnz:0])
 
-            result = m.mk_implies(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, b), mk_zero(bv_sz - lnz - 1)),
-                                  m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b)));
+            expr_ref e1(m_mk_extract(bv_sz - 1, lnz + 1, b), m);
+            expr_ref e2(mk_zero(bv_sz - lnz - 1), m);
+            e1 = m.mk_eq(e1, e2);
+            expr_ref e3(m_mk_extract(lnz, 0, a), m);
+            expr_ref e4(m_mk_extract(lnz, 0, b), m);
+            e2 = m_util.mk_ule(e3, e4);
+            result = m.mk_implies(e1, e2);
             return BR_REWRITE_FULL;
         }
     }
@@ -866,6 +871,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
         return BR_REWRITE2;
     }
 
+    // [....][xx] -> [yy][....] hi <= |[....]| then can extract [hi + k:lo + k]
+    // (ashr t k)[hi:0] -> t[hi+k:k]
+    if (low == 0 && m_util.is_bv_ashr(arg, t, c) && m_util.is_numeral(c, v, sz) && high < sz - v) {
+        result = m_mk_extract(high + v.get_unsigned(), low + v.get_unsigned(), t);
+        return BR_REWRITE1;        
+    }
+
     return BR_FAILED;
 }
 
@@ -2498,8 +2510,8 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
     expr* a = nullptr, *b = nullptr, *c = nullptr;
     if (m.is_ite(lhs, a, b, c)) {
         bool_rewriter rw(m);
-        expr_ref e1(rw.mk_eq(b, rhs), m);
-        expr_ref e2(rw.mk_eq(c, rhs), m);
+        expr_ref e1(rw.mk_eq_rw(b, rhs), m);
+        expr_ref e2(rw.mk_eq_rw(c, rhs), m);
         result = rw.mk_ite(a, e1, e2);
         return BR_REWRITE2;
     }

src/ast/sls/sls_basic_plugin.cpp

@@ -29,7 +29,7 @@ namespace sls {
     bool basic_plugin::is_basic(expr* e) const {
         if (!e || !is_app(e))
             return false;
-        if (m.is_ite(e) && !m.is_bool(e) && false)
+        if (m.is_ite(e) && !m.is_bool(e))
             return true;
         if (m.is_xor(e) && to_app(e)->get_num_args() != 2)
             return true;
@@ -149,7 +149,6 @@ namespace sls {
         if (m.is_value(child))
             return false;
         bool r = ctx.set_value(child, ctx.get_value(e));
-        verbose_stream() << "repair-ite-down " << mk_bounded_pp(e, m) << " @ " << mk_bounded_pp(child, m) << " := " << ctx.get_value(e) << " success " << r << "\n";
         return r;
     }
 
@@ -166,7 +165,6 @@ namespace sls {
             val = eval_distinct(e);           
         else
             return;
-        verbose_stream() << "repair-up " << mk_bounded_pp(e, m) << " " << val << "\n";
         if (!ctx.set_value(e, val))
             ctx.new_value_eh(e);
     }
@@ -176,14 +174,14 @@ namespace sls {
 
     bool basic_plugin::repair_down(app* e) {    
         if (!is_basic(e))
-            return true;        
+            return true;     
+
         if (m.is_xor(e) && eval_xor(e) == ctx.get_value(e))
             return true;
         if (m.is_ite(e) && eval_ite(e) == ctx.get_value(e))
             return true;
         if (m.is_distinct(e) && eval_distinct(e) == ctx.get_value(e))
             return true;
-        verbose_stream() << "basic repair down " << mk_bounded_pp(e, m) << "\n";
         unsigned n = e->get_num_args();
         unsigned s = ctx.rand(n);
         for (unsigned i = 0; i < n; ++i) {

src/ast/sls/sls_bv_engine.cpp

@@ -477,9 +477,7 @@ lbool sls_engine::search() {
             // update assertion weights if a weighting is enabled (sp < 1024)
             if (m_paws)
             {
-                for (unsigned i = 0; i < sz; i++)
-                {
-                    expr * q = m_assertions[i];
+                for (auto q : m_assertions) {
                     // smooth weights with probability sp / 1024
                     if (m_tracker.get_random_uint(10) < m_paws_sp)
                     {

src/ast/sls/sls_bv_eval.cpp

@@ -48,6 +48,10 @@ namespace sls {
         }
     }
 
+    void bv_eval::start_propagation() {
+        m_lookahead.start_propagation();
+    }
+
     void bv_eval::add_bit_vector(app* e) {
         if (!bv.is_bv(e))
             return;
@@ -688,8 +692,6 @@ namespace sls {
         expr* arg = e->get_arg(i);
         if (m.is_value(arg))
             return false;
-        if (m.is_bool(e) && is_lookahead_phase() && m_lookahead.try_repair_down(e))
-            return true;
         if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
             commit_eval(e, to_app(arg));
             IF_VERBOSE(11, verbose_stream() << "repair " << mk_bounded_pp(e, m) << " : " << mk_bounded_pp(arg, m) << " := " << wval(arg) << "\n";);
@@ -702,8 +704,6 @@ namespace sls {
             ctx.new_value_eh(arg);
             return true;
         }
-        if (m.is_bool(e) && m_lookahead.try_repair_down(e))
-            return true;
 
         return false;
     }

src/ast/sls/sls_bv_eval.h

@@ -156,6 +156,8 @@ namespace sls {
 
         void init() { m_fix.init(); }
 
+        void start_propagation();
+
         void register_term(expr* e);
 
         /**

src/ast/sls/sls_bv_evaluator.h

@@ -658,6 +658,7 @@ class sls_evaluator {
     }
 
     void serious_update(func_decl * fd, const mpz & new_value) {
+        TRACE("sls", tout << "set: " << fd->get_name() << " to " << m_mpz_manager.to_string(new_value) << std::endl;);
         m_tracker.set_value(fd, new_value);
         expr * ep = m_tracker.get_entry_point(fd);
         unsigned cur_depth = m_tracker.get_distance(ep);

src/ast/sls/sls_bv_fixed.cpp

@@ -29,6 +29,8 @@ namespace sls {
 
     void bv_fixed::init() {
 
+        return;
+
         for (auto e : ctx.subterms())
             set_fixed(e);