merge

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

src/ast/sls/sls_arith_base.cpp

@@ -346,6 +346,11 @@ namespace sls {
             SASSERT(dtt(sign(bv), ineq) == 0);
         }
         vi.m_value = new_value;
+        if (vi.m_shared) {
+            sort* s = vi.m_sort == var_sort::INT ? a.mk_int() : a.mk_real();
+            expr_ref num = from_num(s, new_value);
+            ctx.set_value(vi.m_expr, num);
+        }
         for (auto idx : vi.m_muls) {
             auto const& [w, coeff, monomial] = m_muls[idx];
             ctx.new_value_eh(m_vars[w].m_expr);

src/ast/sls/sls_arith_base.h

@@ -151,7 +151,7 @@ namespace sls {
         bool is_num(expr* e, num_t& i);
         expr_ref from_num(sort* s, num_t const& n);
         void check_ineqs();
-        void init_bool_var(sat::bool_var v);
+        void init_bool_var(sat::bool_var bv);
     public:
         arith_base(context& ctx);
         ~arith_base() override {}        

src/ast/sls/sls_bv.cpp

@@ -0,0 +1,93 @@
+
+#include "ast/sls/sls_bv.h"
+
+namespace sls {
+
+    bv_plugin::bv_plugin(context& ctx): 
+        plugin(ctx),
+        bv(m),
+        m_terms(m),
+        m_eval(m)
+    {}
+
+    void bv_plugin::init_bool_var(sat::bool_var v) {
+    }
+    
+    void bv_plugin::register_term(expr* e) {
+    }
+    
+    expr_ref bv_plugin::get_value(expr* e) {
+        return expr_ref(m);
+    }
+    
+    lbool bv_plugin::check() {
+        return l_undef;
+    }
+    
+    bool bv_plugin::is_sat() {
+        return false;
+    }
+    
+    void bv_plugin::reset() {
+    }
+    
+    void bv_plugin::on_rescale() {
+
+    }
+    
+    void bv_plugin::on_restart() {
+    }
+    
+    std::ostream& bv_plugin::display(std::ostream& out) const {
+        return out;
+    }
+    
+    void bv_plugin::mk_model(model& mdl) {
+
+    }
+    
+    void bv_plugin::set_shared(expr* e) {
+
+    }
+    
+    void bv_plugin::set_value(expr* e, expr* v) {
+
+    }
+
+    std::pair<bool, app*> bv_plugin::next_to_repair() {
+        app* e = nullptr;
+        if (m_repair_down != UINT_MAX) {
+            e = m_terms.term(m_repair_down);
+            m_repair_down = UINT_MAX;
+            return { true, e };
+        }
+
+        if (!m_repair_up.empty()) {
+            unsigned index = m_repair_up.elem_at(ctx.rand(m_repair_up.size()));
+            m_repair_up.remove(index);
+            e = m_terms.term(index);
+            return { false, e };
+        }
+
+        while (!m_repair_roots.empty()) {
+            unsigned index = m_repair_roots.elem_at(ctx.rand(m_repair_roots.size()));
+            e = m_terms.term(index);
+            if (m_terms.is_assertion(e) && !m_eval.bval1(e)) {
+                SASSERT(m_eval.bval0(e));
+                return { true, e };
+            }
+            if (!m_eval.re_eval_is_correct(e)) {
+                init_repair_goal(e);
+                return { true, e };
+            }
+            m_repair_roots.remove(index);
+        }
+
+        return { false, nullptr };
+    }
+
+    void bv_plugin::init_repair_goal(app* e) {
+        m_eval.init_eval(e);
+    }
+
+}

src/ast/sls/sls_bv.h

@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sls_bv.h
+
+Abstract:
+
+    Theory plugin for bit-vector local search
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-07-06
+
+--*/
+#pragma once
+
+#include "ast/sls/sls_smt.h"
+#include "ast/bv_decl_plugin.h"
+#include "ast/sls/bv_sls_terms.h"
+#include "ast/sls/bv_sls_eval.h"
+
+namespace sls {
+
+    class bv_plugin : public plugin {
+        bv_util             bv;
+        bv::sls_terms       m_terms;
+        bv::sls_eval        m_eval;
+        bv::sls_stats       m_stats;
+
+        indexed_uint_set    m_repair_up, m_repair_roots;
+        unsigned            m_repair_down = UINT_MAX;
+
+        std::pair<bool, app*> next_to_repair();
+        void init_repair_goal(app* e);
+    public:
+        bv_plugin(context& ctx);
+        ~bv_plugin() override {}
+        void init_bool_var(sat::bool_var v) override;
+        void register_term(expr* e) override;
+        expr_ref get_value(expr* e) override;
+        lbool check() override;
+        bool is_sat() override;
+        void reset() override;
+
+        void on_rescale() override;
+        void on_restart() override;
+        std::ostream& display(std::ostream& out) const override;
+        void mk_model(model& mdl) override;
+        void set_shared(expr* e) override;
+        void set_value(expr* e, expr* v) override;
+    };
+
+}

src/ast/sls/sls_cc.h

@@ -47,6 +47,7 @@ namespace sls {
         std::ostream& display(std::ostream& out) const override;
         void mk_model(model& mdl) override;
         void set_value(expr* e, expr* v) override {}
+
         void repair_up(app* e) override {}
         void repair_down(app* e) override {}
     };

src/ast/sls/sls_context.cpp

@@ -160,6 +160,7 @@ namespace sls {
         return expr_ref(e, m);
     }
 
+
     void context::set_value(expr * e, expr * v) {
         for (auto p : m_plugins)
             if (p)