From f9ec6b45c4cbc8b7681dcddd64ca557afef1428f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Sep 2024 16:48:16 -0700 Subject: [PATCH] Add array plugin support and update bv_eval in ast_sls module --- src/ast/sls/CMakeLists.txt | 2 + src/ast/sls/sls_array_plugin.cpp | 104 +++++++++++++++++++++++++++++++ src/ast/sls/sls_array_plugin.h | 56 +++++++++++++++++ src/ast/sls/sls_bv_eval.cpp | 28 ++++++++- 4 files changed, 188 insertions(+), 2 deletions(-) create mode 100644 src/ast/sls/sls_array_plugin.cpp create mode 100644 src/ast/sls/sls_array_plugin.h diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt index cdddc441c..519497e9f 100644 --- a/src/ast/sls/CMakeLists.txt +++ b/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 ) diff --git a/src/ast/sls/sls_array_plugin.cpp b/src/ast/sls/sls_array_plugin.cpp new file mode 100644 index 000000000..749970be5 --- /dev/null +++ b/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()); + 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 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); + } + } + + +} diff --git a/src/ast/sls/sls_array_plugin.h b/src/ast/sls/sls_array_plugin.h new file mode 100644 index 000000000..f19d112fd --- /dev/null +++ b/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> 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 {} + }; + +} diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index 9b1800108..e2447e0f2 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/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; @@ -1190,7 +1212,7 @@ namespace sls { a.set_mul(m_tmp, tb, m_tmp2); if (a.set_repair(random_bool(), m_tmp)) return true; - + return a.set_random(m_rand); } @@ -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;