From d3a65211852ca13c97bde36ce4e424db3be19df2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Dec 2024 13:06:28 -0800 Subject: [PATCH] rely on is_sat fallback for failed repair-up, add separate file for WIP on lookahead. --- src/ast/sls/CMakeLists.txt | 1 + src/ast/sls/sls_bv_eval.cpp | 175 +++++++------------------------ src/ast/sls/sls_bv_eval.h | 12 +-- src/ast/sls/sls_bv_lookahead.cpp | 139 ++++++++++++++++++++++++ src/ast/sls/sls_bv_lookahead.h | 53 ++++++++++ src/ast/sls/sls_bv_plugin.cpp | 16 +-- src/ast/sls/sls_context.cpp | 1 + 7 files changed, 244 insertions(+), 153 deletions(-) create mode 100644 src/ast/sls/sls_bv_lookahead.cpp create mode 100644 src/ast/sls/sls_bv_lookahead.h diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt index b393d90ed..77e39ce55 100644 --- a/src/ast/sls/CMakeLists.txt +++ b/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 diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index e6f8f8ab5..a9e16797b 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/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_current2 = use_current || (e->get_num_args() > 1 && !m_on_restore.is_marked(e->get_arg(1))); + 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_lookahead.on_restore(e->get_arg(1))); auto ucompare = [&](std::function 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_current2 = !m_on_restore.is_marked(y); + bool use_current1 = !m_lookahead.on_restore(x); + 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; - 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"; + return m_lookahead.try_repair_down(e); - 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 (a.try_set(b.bits())) - return true; - - if (m_rand(20) == 0) - return a.set_random(m_rand); - return false; + if (m_rand(20) != 0 && a.try_set(b.bits())) + return true; + return a.set_random(m_rand); } 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"; - if (m_rand(20) != 0 && a.try_set(m_tmp)) + //verbose_stream() << a << " := " << m_tmp << "\n"; + 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()) { - ctx.new_value_eh(e); - return true; - } - //verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n"; - //for (expr* arg : *to_app(e)) - // verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n"; - v.bits().copy_to(v.nw, v.eval); - return false; + + for (unsigned i = 0; i < v.nw; ++i) + if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) + return false; + + if (!v.commit_eval()) + return false; + + ctx.new_value_eh(e); + 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(); - } + } diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index a4587b987..9964b5a33 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/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 m_restore; - vector> 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. diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp new file mode 100644 index 000000000..dec7c24a3 --- /dev/null +++ b/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); + } +} \ No newline at end of file diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h new file mode 100644 index 000000000..d43359698 --- /dev/null +++ b/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 m_restore; + vector> 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); + + }; +} \ No newline at end of file diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 8b4b29be7..4973bfaee 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/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)) { - verbose_stream() << "Incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; - } + IF_VERBOSE(0, + 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)) { - 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 + else log(e, true, false); } diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index b610e76ed..b177bfb0c 100644 --- a/src/ast/sls/sls_context.cpp +++ b/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()); } }