Add array plugin support and update bv_eval in ast_sls module

src/ast/sls/CMakeLists.txt

@@ -4,6 +4,7 @@ z3_add_component(ast_sls
     sat_ddfw.cpp
     sls_arith_base.cpp
     sls_arith_plugin.cpp
+    sls_array_plugin.cpp
     sls_basic_plugin.cpp
     sls_bv_engine.cpp
     sls_bv_eval.cpp
@@ -16,6 +17,7 @@ z3_add_component(ast_sls
     sls_smt_solver.cpp
   COMPONENT_DEPENDENCIES
     ast
+    euf
     converters
     normal_forms
 )

src/ast/sls/sls_array_plugin.cpp

@@ -0,0 +1,104 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sls_array_plugin.cpp
+
+Abstract:
+
+    Theory plugin for arrays local search
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-07-06
+
+--*/
+
+#include "ast/sls/sls_array_plugin.h"
+
+
+namespace sls {
+
+        
+    array_plugin::array_plugin(context& ctx):
+        plugin(ctx),
+        a(m)
+    {
+        m_fid = a.get_family_id();
+    }
+
+
+    bool array_plugin::is_sat() {
+        euf::egraph g(m);
+        init_egraph(g);
+
+        return false;
+    }
+
+    void array_plugin::init_kv(euf::egraph& g, kv& kv) {
+        for (auto n : g.nodes()) {
+            if (!n->is_root() || !a.is_array(n->get_expr()))
+                continue;
+            kv.insert(n, obj_map<euf::enode, euf::enode*>());
+            for (auto p : euf::enode_parents(n)) {
+                if (!a.is_select(p->get_expr()))
+                    continue;
+                SASSERT(n->num_args() == 2);
+                if (p->get_arg(0)->get_root() != n->get_root())
+                    continue;
+                auto idx = n->get_arg(1)->get_root();
+                auto val = p->get_root();
+                kv[n].insert(idx, val);
+            }
+        }
+    }
+
+    void array_plugin::saturate_store(euf::egraph& g, kv& kv) {
+        for (auto n : g.nodes()) {
+            if (!a.is_store(n->get_expr()))
+                continue;
+            SASSERT(n->num_args() == 3);
+            auto idx = n->get_arg(1)->get_root();
+            auto val = n->get_arg(2)->get_root();
+            auto arr = n->get_arg(0)->get_root();
+#if 0
+            auto it = kv.find(arr);
+            if (it == kv.end())
+                continue;
+            auto it2 = it->get_value().find(idx);
+            if (it2 == nullptr)
+                continue;
+            g.merge(val, it2->get_value(), nullptr);
+#endif
+        }
+    }
+
+    void array_plugin::init_egraph(euf::egraph& g) {
+        ptr_vector<euf::enode> args;
+        for (auto t : ctx.subterms()) {
+            args.reset();
+            if (is_app(t)) {
+                for (auto* arg : *to_app(t)) {
+                    args.push_back(g.find(arg));
+                }
+            }
+            auto n = g.mk(t, 0, args.size(), args.data());
+            if (a.is_array(t))
+                continue;
+            auto v = ctx.get_value(t);
+            auto n2 = g.mk(v, 0, 0, nullptr);
+            g.merge(n, n2, nullptr);
+        }
+        for (auto lit : ctx.root_literals()) {
+            if (!ctx.is_true(lit))
+                continue;
+            auto e = ctx.atom(lit.var());
+            expr* x, * y;
+            if (e && m.is_eq(e, x, y))
+                g.merge(g.find(x), g.find(y), nullptr);
+        }
+    }
+
+
+}

src/ast/sls/sls_array_plugin.h

@@ -0,0 +1,56 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sls_array_plugin.h
+
+Abstract:
+
+    Theory plugin for arrays local search
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-07-06
+
+--*/
+#pragma once
+
+#include "ast/sls/sls_context.h"
+#include "ast/array_decl_plugin.h"
+#include "ast/euf/euf_egraph.h"
+
+namespace sls {
+
+
+    class array_plugin : public plugin {
+        array_util     a;
+
+        typedef obj_map<euf::enode, obj_map<euf::enode, euf::enode*>> kv;
+        void init_egraph(euf::egraph& g);
+        void init_kv(euf::egraph& g, kv& kv);
+        void saturate_store(euf::egraph& g, kv& kv);
+        
+    public:
+        array_plugin(context& ctx);
+        ~array_plugin() override {}
+        void register_term(expr* e) override { }
+        expr_ref get_value(expr* e) override { return expr_ref(m); }
+        void initialize() override {}
+        void propagate_literal(sat::literal lit) override {}
+        bool propagate() override { return false; }
+        bool repair_down(app* e) override { return false; }
+        void repair_up(app* e) override {}
+        void repair_literal(sat::literal lit) override {}
+        bool is_sat() override;
+
+        void on_rescale() override {}
+        void on_restart() override {}
+        std::ostream& display(std::ostream& out) const override { return out; }
+        void mk_model(model& mdl) override {}
+        bool set_value(expr* e, expr* v) override { return false; }
+        void collect_statistics(statistics& st) const override {}
+        void reset_statistics() override {}
+    };
+
+}

src/ast/sls/sls_bv_eval.cpp

@@ -881,6 +881,7 @@ namespace sls {
     }
 
     bool bv_eval::try_repair_eq_lookahead(app* e) {
+        return false;
         auto is_true = bval0(e);
         if (!is_true)
             return false;
@@ -913,6 +914,27 @@ namespace sls {
 
     bool bv_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
         if (is_true) {
+#if 0
+            if (bv.is_bv_add(t)) {
+                bvval tmp(b);
+                unsigned start = m_rand();
+                unsigned sz = to_app(t)->get_num_args();
+                for (unsigned i = 0; i < sz; ++i) {
+                    unsigned j = (start + i) % sz;
+                    for (unsigned k = 0; k < sz; ++k) {
+                        if (k == j)
+                            continue;
+                        auto& c = wval(to_app(t)->get_arg(k));
+                        set_sub(tmp, tmp, c.bits());
+                    }
+                    
+                    auto& c = wval(to_app(t)->get_arg(j));
+                    verbose_stream() << "TRY " << c << " := " << tmp << "\n";
+                    
+
+                }
+            }
+#endif
             if (m_rand(20) != 0) 
                 if (a.try_set(b.bits()))
                     return true;
@@ -1931,8 +1953,10 @@ namespace sls {
             m_tmp.set(i + lo, e.get(i));
         m_tmp.set_bw(a.bw);
         // verbose_stream() << a << " := " << m_tmp << "\n";
-        if (m_rand(5) != 0 && a.try_set(m_tmp))
+        if (m_rand(20) != 0 && 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";
         return ok;