rely on is_sat fallback for failed repair-up, add separate file for WIP on lookahead.

src/ast/sls/CMakeLists.txt

@@ -9,6 +9,7 @@ z3_add_component(ast_sls
     sls_bv_engine.cpp
     sls_bv_eval.cpp
     sls_bv_fixed.cpp
+    sls_bv_lookahead.cpp
     sls_bv_plugin.cpp
     sls_bv_terms.cpp
     sls_bv_valuation.cpp

src/ast/sls/sls_bv_eval.cpp

@@ -23,6 +23,7 @@ namespace sls {
         m(ctx.get_manager()),
         ctx(ctx),
         terms(terms),
+        m_lookahead(*this),
         bv(m),
         m_fix(*this, terms, ctx)
     {}   
@@ -121,8 +122,8 @@ namespace sls {
         SASSERT(m.is_bool(e));
         SASSERT(e->get_family_id() == bv.get_fid());
 
-        bool use_current1 = use_current || (e->get_num_args() > 0 && !m_on_restore.is_marked(e->get_arg(0)));
+        bool use_current1 = use_current || (e->get_num_args() > 0 && !m_lookahead.on_restore(e->get_arg(0)));
-        bool use_current2 = use_current || (e->get_num_args() > 1 && !m_on_restore.is_marked(e->get_arg(1)));
+        bool use_current2 = use_current || (e->get_num_args() > 1 && !m_lookahead.on_restore(e->get_arg(1)));
         auto ucompare = [&](std::function<bool(int)> const& f) {
             auto& a = wval(e->get_arg(0)); 
             auto& b = wval(e->get_arg(1)); 
@@ -211,8 +212,8 @@ namespace sls {
             return bval1_bv(e, false);
         expr* x, * y;
         if (m.is_eq(e, x, y) && bv.is_bv(x)) {
-            bool use_current1 = !m_on_restore.is_marked(x);
+            bool use_current1 = !m_lookahead.on_restore(x);
-            bool use_current2 = !m_on_restore.is_marked(y);
+            bool use_current2 = !m_lookahead.on_restore(y);
             return wval(x).tmp_bits(use_current1) == wval(y).tmp_bits(use_current2);
         }
         verbose_stream() << mk_bounded_pp(e, m) << "\n";
@@ -882,35 +883,8 @@ namespace sls {
     }
 
     bool bv_eval::try_repair_eq_lookahead(app* e) {
-        return false;
+        return m_lookahead.try_repair_down(e);
-        auto is_true = bval0(e);
-        if (!is_true)
-            return false;
-        auto const& uninterp = terms.uninterp_occurs(e);
-        if (uninterp.empty())
-            return false;
-//        for (auto e : uninterp)
-//            verbose_stream() << mk_bounded_pp(e, m) << " ";
-//        verbose_stream() << "\n";
 
-        expr* t = uninterp[m_rand() % uninterp.size()];
-
-        auto& v = wval(t);
-        if (v.set_random(m_rand)) {
-            //verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n";
-            ctx.new_value_eh(t);
-            return true;
-        }
-        return false;
-
-
-        for (auto e : uninterp) {
-            auto& v = wval(e);
-            v.get_variant(m_tmp, m_rand);
-            auto d = lookahead(e, m_tmp);
-            //verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n";
-        }
-        return false;
     }
 
     bool bv_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
@@ -936,13 +910,9 @@ namespace sls {
                 }
             }
 #endif
-            if (m_rand(20) != 0) 
+            if (m_rand(20) != 0 && a.try_set(b.bits()))
-                if (a.try_set(b.bits()))
+                return true;
-                    return true;
+            return a.set_random(m_rand);
-
-            if (m_rand(20) == 0)
-                return a.set_random(m_rand);
-            return false; 
         }
         else {
             bool try_above = m_rand(2) == 0;
@@ -1925,7 +1895,20 @@ namespace sls {
         for (unsigned i = 0; i < a.bw; ++i)
             m_tmp.set(i, ve.get(i + bw));
         a.clear_overflow_bits(m_tmp);
-        return a.try_set(m_tmp);
+        bool r = a.try_set(m_tmp);
+        if (!r) {
+            a.add1(m_tmp);
+            r = a.try_set(m_tmp);
+        }
+        if (!r) {
+            r = a.set_repair(random_bool(), m_tmp);
+        }
+        if (!r) {
+            verbose_stream() << "repair concat " << mk_bounded_pp(e, m) << "\n";
+            verbose_stream() << idx << " " << a << "\n" << m_tmp << "\n";
+
+        }
+        return r;
     }
 
     //
@@ -1934,7 +1917,7 @@ namespace sls {
     // set a outside of [hi:lo] to random values with preference to 0 or 1 bits
     // 
     bool bv_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
-        // verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n";
+        // IF_VERBOSE(4, verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n");
         if (false && m_rand(m_config.m_prob_randomize_extract)  <= 100) {
             a.get_variant(m_tmp, m_rand);
             if (0 == (m_rand(2))) {
@@ -1953,13 +1936,11 @@ namespace sls {
         for (unsigned i = 0; i < e.bw; ++i)
             m_tmp.set(i + lo, e.get(i));
         m_tmp.set_bw(a.bw);
-        // verbose_stream() << a << " := " << m_tmp << "\n";
+        //verbose_stream() << a << " := " << m_tmp << "\n";
-        if (m_rand(20) != 0 && a.try_set(m_tmp))
+        if (a.try_set(m_tmp))
             return true;
-        if (m_rand(20) != 0)
-            return false;
         bool ok = a.set_random(m_rand);
-        // verbose_stream() << "set random " << ok << " " << a << "\n";
+        //verbose_stream() << "set random " << ok << " " << a << "\n";
         return ok;
     }
 
@@ -1994,6 +1975,7 @@ namespace sls {
     bool bv_eval::repair_up(expr* e) {
         if (!is_app(e) || !can_eval1(to_app(e)))
             return false;
+
         if (m.is_bool(e)) {
             bool b = bval1(to_app(e));
             auto v = ctx.atom2bool_var(e);
@@ -2006,29 +1988,20 @@ namespace sls {
 
         if (!bv.is_bv(e))
             return false;
+
         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]))) {
-                //verbose_stream() << "Fail to set " << mk_bounded_pp(e, m) << " " << i << " " << v.fixed[i] << " " << v.bits()[i] << " " << v.eval[i] << "\n";
-                v.bits().copy_to(v.nw, v.eval);
-
-                return false;
-            }
-        }
-
         if (v.eval == v.bits())
             return true;
-        //verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
+
-        if (v.commit_eval()) {
+        for (unsigned i = 0; i < v.nw; ++i) 
-            ctx.new_value_eh(e);
+            if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) 
-            return true;
+                return false;
-        }
+
-        //verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
+        if (!v.commit_eval())
-        //for (expr* arg : *to_app(e))
+            return false;
-        //    verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n";
+
-        v.bits().copy_to(v.nw, v.eval);
+        ctx.new_value_eh(e);
-        return false;
+        return true;
     }
 
     sls::bv_valuation& bv_eval::wval(expr* e) const { 
@@ -2097,73 +2070,5 @@ namespace sls {
         return out << "?";
     }
 
-    double bv_eval::lookahead(expr* e, bvect const& new_value) {
+   
-        SASSERT(bv.is_bv(e));
-        SASSERT(is_uninterp(e));
-        SASSERT(m_restore.empty());
-
-        bool has_tabu = false;
-        double break_count = 0, make_count = 0;
-
-        wval(e).eval = new_value;
-        if (!insert_update(e)) {
-            restore_lookahead();
-            return -1000000;
-        }
-        insert_update_stack(e);
-        unsigned max_depth = get_depth(e);
-        for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
-            for (unsigned i = 0; !has_tabu && i < m_update_stack[depth].size(); ++i) {
-                e = m_update_stack[depth][i];
-                if (bv.is_bv(e)) {
-                    auto& v = eval(to_app(e));
-                    if (insert_update(e)) {
-                        for (auto p : ctx.parents(e)) {
-                            insert_update_stack(p);
-                            max_depth = std::max(max_depth, get_depth(p));
-                        }
-                    }
-                    else
-                        has_tabu = true;                
-                }
-                else if (m.is_bool(e) && can_eval1(to_app(e))) {
-                    bool is_true = ctx.is_true(e);
-                    bool is_true_new = bval1(to_app(e));
-                    bool is_true_old = bval1_tmp(to_app(e));
-                    // verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n";
-                    if (is_true == is_true_new && is_true_new != is_true_old)
-                        ++make_count;
-                    if (is_true == is_true_old && is_true_new != is_true_old)
-                        ++break_count;
-                }
-            }
-            m_update_stack[depth].reset();
-        }
-        restore_lookahead();
-        if (has_tabu)
-            return -10000;
-        return make_count - break_count;
-    }
-
-    bool bv_eval::insert_update(expr* e) {
-        m_restore.push_back(e);
-        m_on_restore.mark(e);
-        auto& v = wval(e);
-        v.save_value();
-        return v.commit_eval();
-    }
-
-    void bv_eval::insert_update_stack(expr* e) {
-        unsigned depth = get_depth(e);
-        m_update_stack.reserve(depth + 1);
-        if (!m_update_stack[depth].contains(e))
-            m_update_stack[depth].push_back(e);
-    }
-
-    void bv_eval::restore_lookahead() {
-        for (auto e : m_restore) 
-            wval(e).restore_value();
-        m_restore.reset();
-        m_on_restore.reset();
-    }
 }

src/ast/sls/sls_bv_eval.h

@@ -20,8 +20,10 @@ Author:
 #include "ast/sls/sls_bv_valuation.h"
 #include "ast/sls/sls_bv_fixed.h"
 #include "ast/sls/sls_context.h"
+#include "ast/sls/sls_bv_lookahead.h"
 #include "ast/bv_decl_plugin.h"
 
+
  
 namespace sls {
 
@@ -31,6 +33,8 @@ namespace sls {
     using bvect = sls::bvect;
 
     class bv_eval {
+        friend class bv_lookahead;
+
         struct config {
             unsigned m_prob_randomize_extract = 50;
         };
@@ -40,6 +44,7 @@ namespace sls {
         ast_manager&        m;
         sls::context&       ctx;
         sls::bv_terms&      terms;
+        sls::bv_lookahead   m_lookahead;
         bv_util             bv;
         sls::bv_fixed       m_fix;
         mutable mpn_manager mpn;
@@ -58,13 +63,6 @@ namespace sls {
 
         void init_eval_bv(app* e);
 
-        ptr_vector<expr> m_restore;
-        vector<ptr_vector<expr>> m_update_stack;
-        expr_mark m_on_restore;
-        void insert_update_stack(expr* e);
-        bool insert_update(expr* e);
-        double lookahead(expr* e, bvect const& new_value);
-        void restore_lookahead();
        
         /**
         * Register e as a bit-vector. 

src/ast/sls/sls_bv_lookahead.cpp

@@ -0,0 +1,139 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+    sls_bv_lookahead.h
+
+Abstract:
+
+    Lookahead solver for BV, modeled after sls_engine/sls_tracker/sls_evaluator.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-12-26
+
+--*/
+
+#include "ast/sls/sls_bv_lookahead.h"
+#include "ast/sls/sls_bv_eval.h"
+#include "ast/sls/sls_bv_terms.h"
+
+namespace sls {
+
+    bv_lookahead::bv_lookahead(bv_eval& ev) : 
+        bv(ev.bv), 
+        m_ev(ev), 
+        ctx(ev.ctx), 
+        m(ev.m) {}
+
+    bool bv_lookahead::try_repair_down(expr* e) {
+        return false;
+        auto is_true = m_ev.bval0(e);
+        if (!is_true)
+            return false;
+        auto const& uninterp = m_ev.terms.uninterp_occurs(e);
+        if (uninterp.empty())
+            return false;
+        //        for (auto e : uninterp)
+        //            verbose_stream() << mk_bounded_pp(e, m) << " ";
+        //        verbose_stream() << "\n";
+
+        expr* t = uninterp[m_ev.m_rand() % uninterp.size()];
+
+        auto& v = wval(t);
+        if (v.set_random(m_ev.m_rand)) {
+            //verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n";
+            ctx.new_value_eh(t);
+            return true;
+        }
+        return false;
+
+
+        for (auto e : uninterp) {
+            auto& v = wval(e);
+            v.get_variant(m_ev.m_tmp, m_ev.m_rand);
+            auto d = lookahead(e, m_ev.m_tmp);
+            //verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n";
+        }
+        return false;
+    }
+
+    double bv_lookahead::lookahead(expr* e, bvect const& new_value) {
+        SASSERT(bv.is_bv(e));
+        SASSERT(is_uninterp(e));
+        SASSERT(m_restore.empty());
+
+        bool has_tabu = false;
+        double break_count = 0, make_count = 0;
+
+        wval(e).eval = new_value;
+        if (!insert_update(e)) {
+            restore_lookahead();
+            return -1000000;
+        }
+        insert_update_stack(e);
+        unsigned max_depth = get_depth(e);
+        for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
+            for (unsigned i = 0; !has_tabu && i < m_update_stack[depth].size(); ++i) {
+                e = m_update_stack[depth][i];
+                if (bv.is_bv(e)) {
+                    auto& v = m_ev.eval(to_app(e));
+                    if (insert_update(e)) {
+                        for (auto p : ctx.parents(e)) {
+                            insert_update_stack(p);
+                            max_depth = std::max(max_depth, get_depth(p));
+                        }
+                    }
+                    else
+                        has_tabu = true;
+                }
+                else if (m.is_bool(e) && m_ev.can_eval1(to_app(e))) {
+                    bool is_true = ctx.is_true(e);
+                    bool is_true_new = m_ev.bval1(to_app(e));
+                    bool is_true_old = m_ev.bval1_tmp(to_app(e));
+                    // verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n";
+                    if (is_true == is_true_new && is_true_new != is_true_old)
+                        ++make_count;
+                    if (is_true == is_true_old && is_true_new != is_true_old)
+                        ++break_count;
+                }
+            }
+            m_update_stack[depth].reset();
+        }
+        restore_lookahead();
+        if (has_tabu)
+            return -10000;
+        return make_count - break_count;
+    }
+
+    bool bv_lookahead::insert_update(expr* e) {
+        m_restore.push_back(e);
+        m_on_restore.mark(e);
+        auto& v = wval(e);
+        v.save_value();
+        return v.commit_eval();
+    }
+
+    void bv_lookahead::insert_update_stack(expr* e) {
+        unsigned depth = get_depth(e);
+        m_update_stack.reserve(depth + 1);
+        if (!m_update_stack[depth].contains(e))
+            m_update_stack[depth].push_back(e);
+    }
+
+    void bv_lookahead::restore_lookahead() {
+        for (auto e : m_restore)
+            wval(e).restore_value();
+        m_restore.reset();
+        m_on_restore.reset();
+    }
+
+    sls::bv_valuation& bv_lookahead::wval(expr* e) const {
+        return m_ev.wval(e);
+    }
+
+    bool bv_lookahead::on_restore(expr* e) const {
+        return m_on_restore.is_marked(e);
+    }
+}

src/ast/sls/sls_bv_lookahead.h

@@ -0,0 +1,53 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+    sls_bv_lookahead.h
+
+Abstract:
+
+    Lookahead solver for BV, modeled after sls_engine/sls_tracker/sls_evaluator.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-12-26
+
+--*/
+#pragma once
+
+#include "ast/bv_decl_plugin.h"
+#include "ast/sls/sls_context.h"
+
+namespace sls {
+    class bv_eval;
+    class bv_valuation;
+    class bvect;
+
+    class bv_lookahead {
+        bv_util bv;
+        bv_eval& m_ev;
+        context& ctx;
+        ast_manager& m;
+
+        ptr_vector<expr> m_restore;
+        vector<ptr_vector<expr>> m_update_stack;
+        expr_mark m_on_restore;
+
+        bv_valuation& wval(expr* e) const;
+
+        void insert_update_stack(expr* e);
+        bool insert_update(expr* e);
+        
+        void restore_lookahead();
+
+        double lookahead(expr* e, bvect const& new_value);
+
+    public:
+        bv_lookahead(bv_eval& ev);
+        bool on_restore(expr* e) const;
+
+        bool try_repair_down(expr* e);
+
+    };
+}

src/ast/sls/sls_bv_plugin.cpp

@@ -153,9 +153,10 @@ namespace sls {
 
     void bv_plugin::repair_up(app* e) {
         if (m_eval.repair_up(e)) {
-            if (!m_eval.eval_is_correct(e)) {
+            IF_VERBOSE(0,
-                verbose_stream() << "Incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
+                if (!m_eval.eval_is_correct(e))
-            }
+                    verbose_stream() << "Incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
+                    );
             log(e, true, true);
             SASSERT(m_eval.eval_is_correct(e));
             if (m.is_bool(e)) {
@@ -163,14 +164,7 @@ namespace sls {
                     ctx.flip(ctx.atom2bool_var(e));
             }
         }
-        else if (bv.is_bv(e)) {
+        else 
-            log(e, true, false);
-            IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e)); 
-            auto& v = m_eval.wval(e);
-            m_eval.set_random(e);
-            ctx.new_value_eh(e);
-        }
-        else
             log(e, true, false);
 
     }

src/ast/sls/sls_context.cpp

@@ -198,6 +198,7 @@ namespace sls {
                     ++m_stats.m_num_repair_down;
                     if (p && !p->repair_down(to_app(e)) && !m_repair_up.contains(e->get_id())) {
                         IF_VERBOSE(3, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n");
+                        TRACE("sls", tout << "revert repair: " << mk_bounded_pp(e, m) << "\n");
                         m_repair_up.insert(e->get_id());
                     }
                 }