From f39756c74b3736a122ae93c72a805f63fb045084 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Feb 2024 16:34:26 +0700 Subject: [PATCH] initial stab at new bv-sls based on repair actions --- src/ast/sls/CMakeLists.txt | 7 +- src/ast/sls/bv_sls.cpp | 160 +++++++ src/ast/sls/bv_sls.h | 99 ++++ src/ast/sls/bv_sls_eval.cpp | 821 ++++++++++++++++++++++++++++++++++ src/ast/sls/bv_sls_eval.h | 134 ++++++ src/ast/sls/bv_sls_fixed.cpp | 386 ++++++++++++++++ src/ast/sls/bv_sls_fixed.h | 52 +++ src/ast/sls/bv_sls_terms.cpp | 138 ++++++ src/ast/sls/bv_sls_terms.h | 70 +++ src/ast/sls/sls_engine.cpp | 13 - src/ast/sls/sls_engine.h | 35 +- src/ast/sls/sls_powers.h | 1 + src/ast/sls/sls_stats.h | 48 ++ src/ast/sls/sls_valuation.cpp | 127 ++++++ src/ast/sls/sls_valuation.h | 116 +++++ src/tactic/sls/sls_tactic.cpp | 107 +++++ src/tactic/sls/sls_tactic.h | 9 + 17 files changed, 2278 insertions(+), 45 deletions(-) create mode 100644 src/ast/sls/bv_sls.cpp create mode 100644 src/ast/sls/bv_sls.h create mode 100644 src/ast/sls/bv_sls_eval.cpp create mode 100644 src/ast/sls/bv_sls_eval.h create mode 100644 src/ast/sls/bv_sls_fixed.cpp create mode 100644 src/ast/sls/bv_sls_fixed.h create mode 100644 src/ast/sls/bv_sls_terms.cpp create mode 100644 src/ast/sls/bv_sls_terms.h create mode 100644 src/ast/sls/sls_stats.h create mode 100644 src/ast/sls/sls_valuation.cpp create mode 100644 src/ast/sls/sls_valuation.h diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt index 17b803cf3..24eaec4dc 100644 --- a/src/ast/sls/CMakeLists.txt +++ b/src/ast/sls/CMakeLists.txt @@ -1,7 +1,12 @@ z3_add_component(ast_sls SOURCES bvsls_opt_engine.cpp - sls_engine.cpp + bv_sls.cpp + bv_sls_eval.cpp + bv_sls_fixed.cpp + bv_sls_terms.cpp + sls_engine.cpp + sls_valuation.cpp COMPONENT_DEPENDENCIES ast converters diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp new file mode 100644 index 000000000..90058607e --- /dev/null +++ b/src/ast/sls/bv_sls.cpp @@ -0,0 +1,160 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls.cpp + +Abstract: + + A Stochastic Local Search (SLS) engine + Uses invertibility conditions, + interval annotations + don't care annotations + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ + +#include "ast/sls/bv_sls.h" +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" + +namespace bv { + + sls::sls(ast_manager& m): + m(m), + bv(m), + m_terms(m), + m_eval(m) + {} + + void sls::init() { + m_terms.init(); + } + + void sls::init_eval(std::function& eval) { + m_eval.init_eval(m_terms.assertions(), eval); + for (auto* e : m_terms.assertions()) { + if (!m_eval.bval0(e)) { + m_eval.set(e, true); + m_repair_down.insert(e->get_id()); + } + } + m_eval.init_fixed(m_terms.assertions()); + } + + lbool sls::operator()() { + // init and init_eval were invoked. + unsigned& n = m_stats.m_moves; + n = 0; + for (; n < m_config.m_max_repairs && m.inc(); ++n) { + if (!m_repair_down.empty()) { + unsigned index = m_rand(m_repair_down.size()); + unsigned expr_id = m_repair_down.elem_at(index); + auto e = m_terms.term(expr_id); + if (eval_is_correct(e)) + m_repair_down.remove(expr_id); + else + try_repair_down(e); + } + else if (!m_repair_up.empty()) { + unsigned index = m_rand(m_repair_up.size()); + unsigned expr_id = m_repair_up.elem_at(index); + auto e = m_terms.term(expr_id); + if (eval_is_correct(e)) + m_repair_up.remove(expr_id); + else + try_repair_up(e); + } + else + return l_true; + } + return l_undef; + } + + bool sls::try_repair_down(app* e) { + IF_VERBOSE(20, verbose_stream() << "d " << mk_bounded_pp(e, m, 1) << "\n"); + unsigned n = e->get_num_args(); + unsigned s = m_rand(n); + for (unsigned i = 0; i < n; ++i) + if (try_repair_down(e, (i + s) % n)) + return true; + return false; + } + + bool sls::try_repair_down(app* e, unsigned i) { + expr* child = e->get_arg(i); + bool was_repaired = m_eval.try_repair(e, i); + if (was_repaired) { + m_repair_down.insert(child->get_id()); + for (auto p : m_terms.parents(child)) + m_repair_up.insert(p->get_id()); + } + return was_repaired; + } + + bool sls::try_repair_up(app* e) { + IF_VERBOSE(20, verbose_stream() << "u " << mk_bounded_pp(e, m, 1) << "\n"); + m_repair_up.remove(e->get_id()); + if (m_terms.is_assertion(e)) { + m_repair_down.insert(e->get_id()); + return false; + } + m_eval.repair_up(e); + for (auto p : m_terms.parents(e)) + m_repair_up.insert(p->get_id()); + + return true; + } + + bool sls::eval_is_correct(app* e) { + if (m.is_bool(e)) + return m_eval.bval0(e) == m_eval.bval1(e); + if (bv.is_bv(e)) + return 0 == memcmp(m_eval.wval0(e).bits.data(), m_eval.wval1(e).data(), m_eval.wval0(e).nw * 8); + UNREACHABLE(); + return false; + } + + model_ref sls::get_model() { + model_ref mdl = alloc(model, m); + m_eval.sort_assertions(m_terms.assertions()); + for (expr* e : m_todo) { + if (!is_uninterp_const(e)) + continue; + auto f = to_app(e)->get_decl(); + if (m.is_bool(e)) + mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e))); + else if (bv.is_bv(e)) { + auto const& v = m_eval.wval0(e); + rational n; + v.get_value(v.bits, n); + mdl->register_decl(f, bv.mk_numeral(n, v.bw)); + } + } + return mdl; + } + + std::ostream& sls::display(std::ostream& out) { + auto& terms = m_eval.sort_assertions(m_terms.assertions()); + for (expr* e : terms) { + out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; + if (m_eval.is_fixed0(e)) + out << "f "; + if (m_repair_down.contains(e->get_id())) + out << "d "; + if (m_repair_up.contains(e->get_id())) + out << "u "; + if (bv.is_bv(e)) + out << m_eval.wval0(e); + else if (m.is_bool(e)) + out << (m_eval.bval0(e)?"T":"F"); + out << "\n"; + } + terms.reset(); + return out; + } +} diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h new file mode 100644 index 000000000..6acaf483c --- /dev/null +++ b/src/ast/sls/bv_sls.h @@ -0,0 +1,99 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls.h + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ +#pragma once + +#include "util/lbool.h" +#include "util/params.h" +#include "util/scoped_ptr_vector.h" +#include "util/uint_set.h" +#include "ast/ast.h" +#include "ast/sls/sls_stats.h" +#include "ast/sls/sls_powers.h" +#include "ast/sls/sls_valuation.h" +#include "ast/sls/bv_sls_terms.h" +#include "ast/sls/bv_sls_eval.h" +#include "ast/bv_decl_plugin.h" +#include "model/model.h" + +namespace bv { + + + class sls { + + struct config { + unsigned m_max_restarts = 1000; + unsigned m_max_repairs = 100000; + }; + + ast_manager& m; + bv_util bv; + sls_terms m_terms; + sls_eval m_eval; + sls_stats m_stats; + indexed_uint_set m_repair_down, m_repair_up; + ptr_vector m_todo; + random_gen m_rand; + config m_config; + + + bool eval_is_correct(app* e); + bool try_repair_down(app* e); + bool try_repair_up(app* e); + + bool try_repair_down(app* e, unsigned i); + + public: + sls(ast_manager& m); + + /** + * Add constraints + */ + void assert_expr(expr* e) { m_terms.assert_expr(e); } + + /* + * Invoke init after all expressions are asserted. + * No other expressions can be asserted after init. + */ + void init(); + + /** + * Invoke init_eval to initialize, or re-initialize, values of + * uninterpreted constants. + */ + void init_eval(std::function& eval); + + /** + * Run (bounded) local search to find feasible assignments. + */ + lbool operator()(); + + void updt_params(params_ref const& p) {} + void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); } + void reset_statistics() { m_stats.reset(); } + + sls_stats const& get_stats() const { return m_stats; } + + std::ostream& display(std::ostream& out); + + /** + * Retrieve valuation + */ + sls_valuation const& wval(expr* e) const { return m_eval.wval0(e); } + + model_ref get_model(); + }; +} diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp new file mode 100644 index 000000000..990d87dbb --- /dev/null +++ b/src/ast/sls/bv_sls_eval.cpp @@ -0,0 +1,821 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls_eval.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ + +#include "ast/ast_pp.h" +#include "ast/sls/bv_sls.h" + +namespace bv { + + sls_eval::sls_eval(ast_manager& m): + m(m), + bv(m), + m_fix(*this) + {} + + void sls_eval::init_eval(expr_ref_vector const& es, std::function const& eval) { + sort_assertions(es); + for (expr* e : m_todo) { + if (!is_app(e)) + continue; + app* a = to_app(e); + if (bv.is_bv(e)) + add_bit_vector(e); + if (a->get_family_id() == basic_family_id) + init_eval_basic(a); + else if (a->get_family_id() == bv.get_family_id()) + init_eval_bv(a); + else if (is_uninterp(e)) { + if (bv.is_bv(e)) { + auto& v = wval0(e); + for (unsigned i = 0; i < v.bw; ++i) + v.set(v.bits, i, eval(e, i)); + } + else if (m.is_bool(e)) + m_eval.setx(e->get_id(), eval(e, 0), false); + } + else { + TRACE("sls", tout << "Unhandled expression " << mk_pp(e, m) << "\n"); + } + } + m_todo.reset(); + } + + /** + * Sort all sub-expressions by depth, smallest first. + */ + ptr_vector& sls_eval::sort_assertions(expr_ref_vector const& es) { + expr_fast_mark1 mark; + for (expr* e : es) { + if (!mark.is_marked(e)) { + mark.mark(e); + m_todo.push_back(e); + } + } + for (unsigned i = 0; i < m_todo.size(); ++i) { + auto e = m_todo[i]; + if (!is_app(e)) + continue; + for (expr* arg : *to_app(e)) { + if (!mark.is_marked(arg)) { + mark.mark(arg); + m_todo.push_back(arg); + } + } + } + std::stable_sort(m_todo.begin(), m_todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); + return m_todo; + } + + bool sls_eval::add_bit_vector(expr* e) { + auto bw = bv.get_bv_size(e); + m_values0.reserve(e->get_id() + 1); + if (m_values0.get(e->get_id())) + return false; + m_values1.reserve(e->get_id() + 1); + m_values0.set(e->get_id(), alloc_valuation(bw)); + m_values1.set(e->get_id(), alloc_valuation(bw)); + return true; + } + + sls_valuation* sls_eval::alloc_valuation(unsigned bit_width) { + auto* r = alloc(sls_valuation, bit_width); + while (m_tmp.size() < r->nw) { + m_tmp.push_back(0); + m_tmp2.push_back(0); + m_tmp2.push_back(0); + m_zero.push_back(0); + } + return r; + } + + void sls_eval::init_eval_basic(app* e) { + auto id = e->get_id(); + if (m.is_bool(e)) + m_eval.setx(id, bval1(e), false); + else if (m.is_ite(e)) { + SASSERT(bv.is_bv(e->get_arg(1))); + auto& val = wval0(e); + auto& val_th = wval0(e->get_arg(1)); + auto& val_el = wval0(e->get_arg(2)); + if (bval0(e->get_arg(0))) + val.set(val_th.bits); + else + val.set(val_el.bits); + } + else { + UNREACHABLE(); + } + } + + void sls_eval::init_eval_bv(app* e) { + if (bv.is_bv(e)) { + auto& v = wval0(e); + v.set(wval1(e)); + } + else if (m.is_bool(e)) + m_eval.setx(e->get_id(), bval1_bv(e), false); + } + + bool sls_eval::bval1_basic(app* e) const { + SASSERT(m.is_bool(e)); + SASSERT(e->get_family_id() == basic_family_id); + + auto id = e->get_id(); + switch (e->get_decl_kind()) { + case OP_TRUE: + return true; + case OP_FALSE: + return false; + case OP_AND: + return all_of(*to_app(e), [&](expr* arg) { return bval0(arg); }); + case OP_OR: + return any_of(*to_app(e), [&](expr* arg) { return bval0(arg); }); + case OP_NOT: + return !bval0(e->get_arg(0)); + case OP_XOR: { + bool r = false; + for (auto* arg : *to_app(e)) + r ^= bval0(arg); + return r; + } + case OP_IMPLIES: { + auto a = e->get_arg(0); + auto b = e->get_arg(1); + return !bval0(a) || bval0(b); + } + case OP_ITE: { + auto c = bval0(e->get_arg(0)); + return bval0(c ? e->get_arg(1) : e->get_arg(2)); + } + case OP_EQ: { + auto a = e->get_arg(0); + auto b = e->get_arg(1); + if (m.is_bool(a)) + return bval0(a) == bval0(b); + else if (bv.is_bv(a)) { + auto const& va = wval0(a); + auto const& vb = wval0(b); + return va.eq(vb); + } + UNREACHABLE(); + break; + } + default: + UNREACHABLE(); + } + UNREACHABLE(); + return false; + } + + bool sls_eval::bval1_bv(app* e) const { + SASSERT(m.is_bool(e)); + SASSERT(e->get_family_id() == bv.get_fid()); + + auto ucompare = [&](std::function const& f) { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + return f(mpn.compare(a.bits.data(), a.nw, b.bits.data(), b.nw)); + }; + + // x x + 2^{bw-1} const& f) { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + unsigned c; + a.set(m_zero, a.bw - 1, true); + mpn.add(a.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp.data(), a.nw, &c); + mpn.add(b.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp2.data(), a.nw, &c); + a.set(m_zero, a.bw - 1, false); + return f(mpn.compare(m_tmp.data(), a.nw, m_tmp2.data(), b.nw)); + }; + + auto umul_overflow = [&]() { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + mpn.mul(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp2.data()); + for (unsigned i = a.nw; i < 2 * a.nw; ++i) + if (m_tmp2[i] != 0) + return true; + for (unsigned i = a.bw; i < sizeof(digit_t) * 8 * a.nw; ++i) + if (a.get(m_tmp2, i)) + return true; + return false; + }; + + switch (e->get_decl_kind()) { + case OP_ULEQ: + return ucompare([](int i) { return i <= 0; }); + case OP_ULT: + return ucompare([](int i) { return i < 0; }); + case OP_UGT: + return ucompare([](int i) { return i > 0; }); + case OP_UGEQ: + return ucompare([](int i) { return i >= 0; }); + case OP_SLEQ: + return scompare([](int i) { return i <= 0; }); + case OP_SLT: + return scompare([](int i) { return i < 0; }); + case OP_SGT: + return scompare([](int i) { return i > 0; }); + case OP_SGEQ: + return scompare([](int i) { return i >= 0; }); + case OP_BIT2BOOL: { + expr* child; + unsigned idx; + VERIFY(bv.is_bit2bool(e, child, idx)); + auto& a = wval0(child); + return a.get(a.bits, idx); + } + case OP_BUMUL_NO_OVFL: + return !umul_overflow(); + case OP_BUMUL_OVFL: + return umul_overflow(); + case OP_BUADD_OVFL: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + digit_t c = 0; + mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp.data(), a.nw, &c); + return c != 0; + } + case OP_BNEG_OVFL: + case OP_BSADD_OVFL: + case OP_BSDIV_OVFL: + case OP_BSMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + case OP_BSMUL_OVFL: + NOT_IMPLEMENTED_YET(); + break; + default: + UNREACHABLE(); + break; + } + return false; + } + + bool sls_eval::bval1(app* e) const { + if (e->get_family_id() == basic_family_id) + return bval1_basic(e); + if (e->get_family_id() == bv.get_fid()) + return bval1_bv(e); + SASSERT(is_uninterp_const(e)); + return bval0(e); + } + + svector& sls_eval::wval1(app* e) const { + auto& val = *m_values1[e->get_id()]; + wval1(e, val); + return val.bits; + } + + void sls_eval::wval1(app* e, sls_valuation& val) const { + SASSERT(bv.is_bv(e)); + if (m.is_ite(e)) { + SASSERT(bv.is_bv(e->get_arg(1))); + auto& val_th = wval0(e->get_arg(1)); + auto& val_el = wval0(e->get_arg(2)); + if (bval0(e->get_arg(0))) + val.set(val_th.bits); + else + val.set(val_el.bits); + return; + } + if (e->get_family_id() == null_family_id) { + val.set(wval0(e).bits); + return; + } + SASSERT(e->get_family_id() == bv.get_fid()); + switch (e->get_decl_kind()) { + case OP_BV_NUM: { + rational n; + VERIFY(bv.is_numeral(e, n)); + val.set_value(val.bits, n); + break; + } + case OP_BAND: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + for (unsigned i = 0; i < a.bw; ++i) + val.bits[i] = a.bits[i] & b.bits[i]; + break; + } + case OP_BOR: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + for (unsigned i = 0; i < a.bw; ++i) + val.bits[i] = a.bits[i] | b.bits[i]; + break; + } + case OP_BXOR: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + for (unsigned i = 0; i < a.bw; ++i) + val.bits[i] = a.bits[i] ^ b.bits[i]; + break; + } + case OP_BNAND: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + for (unsigned i = 0; i < a.bw; ++i) + val.bits[i] = ~(a.bits[i] & b.bits[i]); + break; + } + case OP_BADD: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + digit_t c; + mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), val.nw, &c); + break; + } + case OP_BMUL: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + mpn.mul(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp2.data()); + val.set(m_tmp2); + break; + } + case OP_CONCAT: { + SASSERT(e->get_num_args() == 2); + auto const& a = wval0(e->get_arg(0)); + auto const& b = wval0(e->get_arg(1)); + for (unsigned i = 0; i < b.bw; ++i) + val.set(val.bits, i, b.get(b.bits, i)); + for (unsigned i = 0; i < a.bw; ++i) + val.set(val.bits, i + b.bw, a.get(a.bits, i)); + break; + } + case OP_EXTRACT: { + expr* child; + unsigned lo, hi; + VERIFY(bv.is_extract(e, lo, hi, child)); + auto const& a = wval0(child); + SASSERT(lo <= hi && hi + 1 <= a.bw && hi - lo + 1 == val.bw); + for (unsigned i = lo; i <= hi; ++i) + val.set(val.bits, i - lo, a.get(a.bits, i)); + break; + } + case OP_BNOT: { + auto& a = wval0(e->get_arg(0)); + for (unsigned i = 0; i < a.nw; ++i) + val.bits[i] = ~a.bits[i]; + break; + } + case OP_BNEG: { + auto& a = wval0(e->get_arg(0)); + digit_t c; + mpn.sub(m_zero.data(), a.nw, a.bits.data(), a.nw, val.bits.data(), &c); + break; + } + case OP_BIT0: + val.set(val.bits, 0, false); + break; + case OP_BIT1: + val.set(val.bits, 0, true); + break; + case OP_BSHL: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + auto sh = b.to_nat(b.bits, b.bw); + if (sh == 0) { + for (unsigned i = 0; i < a.nw; ++i) + val.bits[i] = a.bits[i]; + } + else if (sh >= b.bw) { + for (unsigned i = 0; i < a.nw; ++i) + val.bits[i] = 0; + } + else { + for (unsigned i = 0; i < a.bw; ++i) + val.set(val.bits, i, i >= sh && b.get(b.bits, i - sh)); + } + break; + } + case OP_BLSHR: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + auto sh = b.to_nat(b.bits, b.bw); + if (sh == 0) { + for (unsigned i = 0; i < a.nw; ++i) + val.bits[i] = a.bits[i]; + } + else if (sh >= b.bw) { + for (unsigned i = 0; i < a.nw; ++i) + val.bits[i] = 0; + } + else { + for (unsigned i = 0; i < a.bw; ++i) + val.set(val.bits, i, i + sh < a.bw && b.get(b.bits, i + sh)); + } + break; + } + case OP_BASHR: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + auto sh = b.to_nat(b.bits, b.bw); + auto sign = a.get(a.bits, a.bw - 1); + if (sh == 0) { + for (unsigned i = 0; i < a.nw; ++i) + val.bits[i] = a.bits[i]; + } + else if (sh >= b.bw) { + for (unsigned i = 0; i < a.nw; ++i) + val.bits[i] = sign ? ~0 : 0; + } + else { + for (unsigned i = 0; i < a.bw; ++i) + val.set(val.bits, i, i + sh < a.bw && b.get(b.bits, i + sh)); + if (sign) + for (unsigned i = 0; i < sh; ++i) + val.set(val.bits, a.bw - i, true); + } + break; + } + case OP_BSDIV: + case OP_BSDIV_I: + case OP_BSDIV0: + case OP_BUDIV: + case OP_BUDIV_I: + case OP_BUDIV0: + case OP_BUREM: + case OP_BUREM_I: + case OP_BUREM0: + case OP_BSMOD: + case OP_BSMOD_I: + case OP_BSMOD0: + case OP_BREDAND: + case OP_BREDOR: + case OP_BXNOR: + case OP_INT2BV: + case OP_BCOMP: + NOT_IMPLEMENTED_YET(); + break; + case OP_BIT2BOOL: + case OP_BV2INT: + case OP_BNEG_OVFL: + case OP_BSADD_OVFL: + case OP_BUADD_OVFL: + case OP_BSDIV_OVFL: + case OP_BSMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + case OP_BSMUL_OVFL: + case OP_BUMUL_NO_OVFL: + case OP_BUMUL_OVFL: + case OP_ULEQ: + case OP_UGEQ: + case OP_UGT: + case OP_ULT: + case OP_SLEQ: + case OP_SGEQ: + case OP_SGT: + case OP_SLT: + UNREACHABLE(); + break; + default: + UNREACHABLE(); + break; + } + val.clear_overflow_bits(val.bits); + } + + bool sls_eval::try_repair(app* e, unsigned i) { + if (is_fixed0(e->get_arg(i))) + return false; + if (e->get_family_id() == basic_family_id) + return try_repair_basic(e, i); + if (e->get_family_id() == bv.get_family_id()) + return try_repair_bv(e, i); + return false; + } + + bool sls_eval::try_repair_basic(app* e, unsigned i) { + switch (e->get_decl_kind()) { + case OP_AND: + return try_repair_and_or(e, i); + case OP_OR: + return try_repair_and_or(e, i); + case OP_NOT: + return try_repair_not(e); + case OP_FALSE: + return false; + case OP_TRUE: + return false; + case OP_EQ: + return try_repair_eq(e, i); + case OP_IMPLIES: + return try_repair_implies(e, i); + case OP_XOR: + return try_repair_xor(e, i); + case OP_ITE: + return try_repair_ite(e, i); + default: + UNREACHABLE(); + return false; + } + } + + bool sls_eval::try_repair_bv(app* e, unsigned i) { + switch (e->get_decl_kind()) { + case OP_BAND: + return try_repair_band(wval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_BOR: + return try_repair_bor(wval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_BXOR: + return try_repair_bxor(wval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_BADD: + return try_repair_add(wval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_BMUL: + return try_repair_mul(wval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_BNOT: + return try_repair_bnot(wval0(e), wval0(e, i)); + case OP_BNEG: + return try_repair_bneg(wval0(e), wval0(e, i)); + case OP_BIT0: + return false; + case OP_BIT1: + return false; + case OP_BV2INT: + return false; + case OP_INT2BV: + return false; + case OP_ULEQ: + if (i == 0) + return try_repair_ule(bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_uge(bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_UGEQ: + if (i == 0) + return try_repair_uge(bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_ule(bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_UGT: + if (i == 0) + return try_repair_ule(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_uge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_ULT: + if (i == 0) + return try_repair_uge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_ule(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_SLEQ: + if (i == 0) + return try_repair_sle(bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_sge(bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_SGEQ: + if (i == 0) + return try_repair_sge(bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_sle(bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_SGT: + if (i == 0) + return try_repair_sle(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_sge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_SLT: + if (i == 0) + return try_repair_sge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + else + return try_repair_sle(!bval0(e), wval0(e, i), wval0(e, 1 - i)); + case OP_BASHR: + case OP_BLSHR: + case OP_BSHL: + case OP_BCOMP: + case OP_BIT2BOOL: + case OP_BNAND: + case OP_BREDAND: + case OP_BREDOR: + case OP_BSDIV: + case OP_BSDIV_I: + case OP_BSDIV0: + case OP_BUDIV: + case OP_BUDIV_I: + case OP_BUDIV0: + case OP_BUREM: + case OP_BUREM_I: + case OP_BUREM0: + case OP_BSMOD: + case OP_BSMOD_I: + case OP_BSMOD0: + case OP_BXNOR: + case OP_BNEG_OVFL: + case OP_BSADD_OVFL: + case OP_BUADD_OVFL: + case OP_BSDIV_OVFL: + case OP_BSMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + case OP_BSMUL_OVFL: + case OP_BUMUL_NO_OVFL: + case OP_BUMUL_OVFL: + default: + return false; + } + } + + bool sls_eval::try_repair_and_or(app* e, unsigned i) { + auto b = bval0(e); + auto child = e->get_arg(i); + if (b == bval0(child)) + return false; + m_eval[child->get_id()] = b; + return true; + } + + bool sls_eval::try_repair_not(app* e) { + auto child = e->get_arg(0); + m_eval[child->get_id()] = !bval0(e); + return true; + } + + bool sls_eval::try_repair_eq(app* e, unsigned i) { + auto child = e->get_arg(i); + auto ev = bval0(e); + if (m.is_bool(child)) { + auto bv = bval0(e->get_arg(1 - i)); + m_eval[child->get_id()] = ev == bv; + return true; + } + else if (bv.is_bv(child)) { + auto & a = wval0(e->get_arg(i)); + auto & b = wval0(e->get_arg(1 - i)); + if (ev) + return a.try_set(b.bits); + else { + // pick random bit to differ + for (unsigned i = 0; i < a.nw; ++i) + m_tmp[i] = a.bits[i]; + unsigned idx = m_rand(a.bw); + a.set(m_tmp, idx, !b.get(b.bits, idx)); + return a.try_set(m_tmp); + } + } + return false; + } + + bool sls_eval::try_repair_xor(app* e, unsigned i) { + bool ev = bval0(e); + bool bv = bval0(e->get_arg(1 - i)); + auto child = e->get_arg(i); + m_eval[child->get_id()] = ev != bv; + return true; + } + + bool sls_eval::try_repair_ite(app* e, unsigned i) { + auto child = e->get_arg(i); + bool c = bval0(e->get_arg(0)); + if (i == 0) { + m_eval[child->get_id()] = !c; + return true; + } + if (c != (i == 1)) + return false; + if (m.is_bool(e)) { + m_eval[child->get_id()] = bval0(e); + return true; + } + if (bv.is_bv(e)) + return wval0(child).try_set(wval0(e).bits); + return false; + } + + bool sls_eval::try_repair_implies(app* e, unsigned i) { + auto child = e->get_arg(i); + bool ev = bval0(e); + bool av = bval0(child); + bool bv = bval0(e->get_arg(1 - i)); + if (i == 0) { + if (ev == (!av || bv)) + return false; + } + else if (ev != (!bv || av)) + return false; + m_eval[child->get_id()] = ev; + return true; + } + + // + // e = a & b + // e[i] = 1 -> a[i] = 1 + // e[i] = 0 & b[i] = 1 -> a[i] = 0 + // + // a := e[i] | (~b[i] & a[i]) + + bool sls_eval::try_repair_band(bvval const& e, bvval& a, bvval const& b) { + for (unsigned i = 0; i < e.nw; ++i) + m_tmp[i] = e.bits[i] | (~b.bits[i] & a.bits[i]); + return a.try_set(m_tmp); + } + + // + // e = a | b + // set a[i] to 1 where b[i] = 0, e[i] = 1 + // set a[i] to 0 where e[i] = 0, a[i] = 1 + // + bool sls_eval::try_repair_bor(bvval const& e, bvval& a, bvval const& b) { + for (unsigned i = 0; i < e.nw; ++i) + m_tmp[i] = e.bits[i] & (a.bits[i] | ~b.bits[i]); + return a.try_set(m_tmp); + } + + bool sls_eval::try_repair_bxor(bvval const& e, bvval& a, bvval const& b) { + for (unsigned i = 0; i < e.nw; ++i) + m_tmp[i] = e.bits[i] ^ b.bits[i]; + return a.try_set(m_tmp); + } + + bool sls_eval::try_repair_add(bvval const& e, bvval& a, bvval const& b) { + digit_t c; + mpn.sub(e.bits.data(), e.nw, b.bits.data(), e.nw, m_tmp.data(), &c); + return a.try_set(m_tmp); + } + + /** + * e = a*b, then a = e * b^-1 + * 8*e = a*(2b), then a = 4e*b^-1 + */ + bool sls_eval::try_repair_mul(bvval const& e, bvval& a, bvval const& b) { + unsigned parity_e = e.parity(e.bits); + unsigned parity_b = b.parity(b.bits); + if (parity_e < parity_b) + return false; + rational ne, nb; + e.get_value(e.bits, ne); + b.get_value(b.bits, nb); + if (parity_b > 0) + ne /= rational::power_of_two(parity_b); + auto inv_b = nb.pseudo_inverse(b.bw); + rational na = mod(inv_b * ne, rational::power_of_two(a.bw)); + a.set_value(m_tmp, na); + return a.try_set(m_tmp); + } + + bool sls_eval::try_repair_bnot(bvval const& e, bvval& a) { + for (unsigned i = 0; i < e.nw; ++i) + m_tmp[i] = ~e.bits[i]; + return a.try_set(m_tmp); + } + + bool sls_eval::try_repair_bneg(bvval const& e, bvval& a) { + digit_t c; + mpn.sub(m_zero.data(), e.nw, e.bits.data(), e.nw, m_tmp.data(), &c); + return a.try_set(m_tmp); + } + + bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) { + if (e) + return a.try_set(b.bits); + else { + digit_t c; + a.set(m_zero, 0, true); + mpn.add(b.bits.data(), a.nw, m_zero.data(), a.nw, &c, a.nw, m_tmp.data()); + a.set(m_zero, 0, false); + return a.try_set(m_tmp); + } + } + + bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) { + if (e) + return a.try_set(b.bits); + else { + digit_t c; + a.set(m_zero, 0, true); + mpn.sub(b.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp.data(), &c); + a.set(m_zero, 0, false); + return a.try_set(m_tmp); + } + } + + bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) { + return false; + } + + bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) { + return false; + } + + void sls_eval::repair_up(expr* e) { + if (!is_app(e)) + return; + if (m.is_bool(e)) + set(e, bval1(to_app(e))); + else if (bv.is_bv(e)) + wval0(e).try_set(wval1(to_app(e))); + } +} diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h new file mode 100644 index 000000000..a09065735 --- /dev/null +++ b/src/ast/sls/bv_sls_eval.h @@ -0,0 +1,134 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls.h + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ +#pragma once + +#include "ast/ast.h" +#include "ast/sls/sls_valuation.h" +#include "ast/sls/bv_sls_fixed.h" +#include "ast/bv_decl_plugin.h" + +namespace bv { + + class sls_fixed; + + class sls_eval { + friend class sls_fixed; + ast_manager& m; + bv_util bv; + sls_fixed m_fix; + mpn_manager mpn; + ptr_vector m_todo; + random_gen m_rand; + + scoped_ptr_vector m_values0, m_values1; // expr-id -> bv valuation + bool_vector m_eval; // expr-id -> boolean valuation + bool_vector m_fixed; // expr-id -> is Boolean fixed + + mutable svector m_tmp, m_tmp2, m_zero; + + using bvval = sls_valuation; + + + void init_eval_basic(app* e); + void init_eval_bv(app* e); + + /** + * Register e as a bit-vector. + * Return true if not already registered, false if already registered. + */ + bool add_bit_vector(expr* e); + sls_valuation* alloc_valuation(unsigned bit_width); + + bool bval1_basic(app* e) const; + bool bval1_bv(app* e) const; + + /** + * Repair operations + */ + bool try_repair_basic(app* e, unsigned i); + bool try_repair_bv(app * e, unsigned i); + bool try_repair_and_or(app* e, unsigned i); + bool try_repair_not(app* e); + bool try_repair_eq(app* e, unsigned i); + bool try_repair_xor(app* e, unsigned i); + bool try_repair_ite(app* e, unsigned i); + bool try_repair_implies(app* e, unsigned i); + bool try_repair_band(bvval const& e, bvval& a, bvval const& b); + bool try_repair_bor(bvval const& e, bvval& a, bvval const& b); + bool try_repair_add(bvval const& e, bvval& a, bvval const& b); + bool try_repair_mul(bvval const& e, bvval& a, bvval const& b); + bool try_repair_bxor(bvval const& e, bvval& a, bvval const& b); + bool try_repair_bnot(bvval const& e, bvval& a); + bool try_repair_bneg(bvval const& e, bvval& a); + bool try_repair_ule(bool e, bvval& a, bvval const& b); + bool try_repair_uge(bool e, bvval& a, bvval const& b); + bool try_repair_sle(bool e, bvval& a, bvval const& b); + bool try_repair_sge(bool e, bvval& a, bvval const& b); + + sls_valuation& wval0(app* e, unsigned i) { return wval0(e->get_arg(i)); } + + void wval1(app* e, sls_valuation& val) const; + + public: + sls_eval(ast_manager& m); + + void init_eval(expr_ref_vector const& es, std::function const& eval); + + void init_fixed(expr_ref_vector const& es) { m_fix.init(es); } + + ptr_vector& sort_assertions(expr_ref_vector const& es); + + /** + * Retrieve evaluation based on cache. + * bval - Boolean values + * wval - Word (bit-vector) values + */ + + bool bval0(expr* e) const { return m_eval[e->get_id()]; } + + sls_valuation& wval0(expr* e) const { return *m_values0[e->get_id()]; } + + bool is_fixed0(expr* e) const { return m_fixed[e->get_id()]; } + + /** + * Retrieve evaluation based on immediate children. + */ + bool bval1(app* e) const; + + svector& wval1(app* e) const; + + /** + * Override evaluaton. + */ + + void set(expr* e, bool b) { + m_eval[e->get_id()] = b; + } + + + /* + * Try to invert value of child to repair value assignment of parent. + */ + + bool try_repair(app* e, unsigned i); + + /* + * Propagate repair up to parent + */ + void repair_up(expr* e); + }; +} diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp new file mode 100644 index 000000000..4dafb6034 --- /dev/null +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -0,0 +1,386 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls_fixed.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ + +#include "ast/sls/bv_sls_fixed.h" +#include "ast/sls/bv_sls_eval.h" + +namespace bv { + + sls_fixed::sls_fixed(sls_eval& ev): + ev(ev), + m(ev.m), + bv(ev.bv) + {} + + void sls_fixed::init(expr_ref_vector const& es) { + init_ranges(es); + ev.sort_assertions(es); + for (expr* e : ev.m_todo) { + if (!is_app(e)) + continue; + app* a = to_app(e); + ev.m_fixed.setx(a->get_id(), is_fixed1(a), false); + if (a->get_family_id() == basic_family_id) + init_fixed_basic(a); + else if (a->get_family_id() == bv.get_family_id()) + init_fixed_bv(a); + else + ; + } + ev.m_todo.reset(); + } + + + void sls_fixed::init_ranges(expr_ref_vector const& es) { + for (expr* e : es) { + bool sign = m.is_not(e, e); + if (is_app(e)) + init_range(to_app(e), sign); + } + } + + // s <=s t <=> s + K <= t + K, K = 2^{bw-1} + + void sls_fixed::init_range(app* e, bool sign) { + expr* s, * t, * x, * y; + rational a, b; + auto N = [&](expr* s) { + auto b = bv.get_bv_size(s); + return b > 0 ? rational::power_of_two(b - 1) : rational(0); + }; + if (bv.is_ule(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(x, a, y, b, sign); + } + else if (bv.is_ult(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(y, b, x, a, !sign); + } + else if (bv.is_uge(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(y, b, x, a, sign); + } + else if (bv.is_ugt(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(x, a, y, b, !sign); + } + else if (bv.is_sle(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(x, a + N(s), y, b + N(s), sign); + } + else if (bv.is_slt(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(y, b + N(s), x, a + N(s), !sign); + } + else if (bv.is_sge(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(y, b + N(s), x, a + N(s), sign); + } + else if (bv.is_sgt(e, s, t)) { + get_offset(s, x, a); + get_offset(t, y, b); + init_range(x, a + N(s), y, b + N(s), !sign); + } + } + + // + // x + a <= b <=> x in [-a, b - a + 1[ b != -1 + // a <= x + b <=> x in [a - b, -b[ a != 0 + // x + a <= x + b <=> x in [-a, -b[ a != b + // + // x + a < b <=> ! (b <= x + a) <=> x not in [-b, a - b + 1[ <=> x in [a - b + 1, -b [ b != 0 + // a < x + b <=> ! (x + b <= a) <=> x not in [-a, b - a [ <=> x in [b - a, -a [ a != -1 + // x + a < x + b <=> ! (x + b <= x + a) <=> x in [-a, -b [ a != b + // + void sls_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) { + if (!x && !y) + return; + if (!x) { + // a <= y + b + if (a == 0) + return; + auto& v = wval0(y); + if (!sign) + v.add_range(a - b, -b); + else + v.add_range(-b, a - b); + } + else if (!y) { + if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 1) + return; + auto& v = wval0(x); + if (!sign) + v.add_range(-a, b - a + 1); + else + v.add_range(b - a + 1, -a); + } + else if (x == y) { + if (a == b) + return; + auto& v = wval0(x); + if (!sign) + v.add_range(-a, -b); + else + v.add_range(-b, -a); + } + } + + void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) { + expr* s, * t; + x = e; + offset = 0; + if (bv.is_bv_add(e, s, t)) { + if (bv.is_numeral(s, offset)) + x = t; + else if (bv.is_numeral(t, offset)) + x = s; + } + else if (bv.is_numeral(e, offset)) + x = nullptr; + } + + sls_valuation& sls_fixed::wval0(expr* e) { + return ev.wval0(e); + } + + void sls_fixed::init_fixed_basic(app* e) { + if (bv.is_bv(e) && m.is_ite(e)) { + auto& val = wval0(e); + auto& val_th = wval0(e->get_arg(1)); + auto& val_el = wval0(e->get_arg(2)); + for (unsigned i = 0; i < val.nw; ++i) + val.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits[i] ^ val_th.bits[i]); + } + } + + void sls_fixed::init_fixed_bv(app* e) { + if (bv.is_bv(e)) + set_fixed_bw(e); + } + + bool sls_fixed::is_fixed1(app* e) const { + if (is_uninterp(e)) + return false; + if (e->get_family_id() == basic_family_id) + return is_fixed1_basic(e); + return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); }); + } + + bool sls_fixed::is_fixed1_basic(app* e) const { + switch (e->get_decl_kind()) { + case OP_TRUE: + case OP_FALSE: + return true; + case OP_AND: + return any_of(*e, [&](expr* arg) { return ev.is_fixed0(arg) && !ev.bval0(e); }); + case OP_OR: + return any_of(*e, [&](expr* arg) { return ev.is_fixed0(arg) && ev.bval0(e); }); + default: + return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); }); + } + } + + void sls_fixed::set_fixed_bw(app* e) { + SASSERT(bv.is_bv(e)); + SASSERT(e->get_family_id() == bv.get_fid()); + auto& v = ev.wval0(e); + if (all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) { + for (unsigned i = 0; i < v.bw; ++i) + v.set(v.fixed, i, true); + ev.m_fixed.setx(e->get_id(), true, false); + return; + } + switch (e->get_decl_kind()) { + case OP_BAND: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + // (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits) + for (unsigned i = 0; i < a.nw; ++i) + v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits[i]) | (b.fixed[i] & ~b.bits[i]); + break; + } + case OP_BOR: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + // (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits) + for (unsigned i = 0; i < a.nw; ++i) + v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits[i]) | (b.fixed[i] & b.bits[i]); + break; + } + case OP_BNOT: { + auto& a = wval0(e->get_arg(0)); + for (unsigned i = 0; i < a.nw; ++i) + v.fixed[i] = a.fixed[i]; + break; + } + case OP_BADD: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + bool pfixed = true; + for (unsigned i = 0; i < v.bw; ++i) { + if (pfixed && a.get(a.fixed, i) && b.get(b.fixed, i)) + v.set(v.fixed, i, true); + else if (!pfixed && a.get(a.fixed, i) && b.get(b.fixed, i) && + !a.get(a.bits, i) && !b.get(b.bits, i)) { + pfixed = true; + v.set(v.fixed, i, false); + } + else { + pfixed = false; + v.set(v.fixed, i, false); + } + } + break; + } + case OP_BMUL: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + unsigned j = 0, k = 0, zj = 0, zk = 0, hzj = 0, hzk = 0; + // i'th bit depends on bits j + k = i + // if the first j, resp k bits are 0, the bits j + k are 0 + for (; j < v.bw; ++j) + if (!a.get(a.fixed, j)) + break; + for (; k < v.bw; ++k) + if (!b.get(b.fixed, k)) + break; + for (; zj < v.bw; ++zj) + if (!a.get(a.fixed, zj) || a.get(a.bits, zj)) + break; + for (; zk < v.bw; ++zk) + if (!b.get(b.fixed, zk) || b.get(b.bits, zk)) + break; + for (; hzj < v.bw; ++hzj) + if (!a.get(a.fixed, v.bw - hzj - 1) || a.get(a.bits, v.bw - hzj - 1)) + break; + for (; hzk < v.bw; ++hzk) + if (!b.get(b.fixed, v.bw - hzk - 1) || b.get(b.bits, v.bw - hzk - 1)) + break; + + + if (j > 0 && k > 0) { + for (unsigned i = 0; i < std::min(k, j); ++i) + v.set(v.fixed, i, true); + } + // lower zj + jk bits are 0 + if (zk > 0 || zj > 0) { + for (unsigned i = 0; i < zk + zj; ++i) + v.set(v.fixed, i, true); + } + // upper bits are 0, if enough high order bits of a, b are 0. + if (hzj < v.bw && hzk < v.bw && hzj + hzk > v.bw) { + hzj = v.bw - hzj; + hzk = v.bw - hzk; + for (unsigned i = hzj + hzk - 1; i < v.bw; ++i) + v.set(v.fixed, i, true); + } + break; + } + case OP_CONCAT: { + auto& a = wval0(e->get_arg(0)); + auto& b = wval0(e->get_arg(1)); + for (unsigned i = 0; i < b.bw; ++i) + v.set(v.fixed, i, b.get(b.fixed, i)); + for (unsigned i = 0; i < a.bw; ++i) + v.set(v.fixed, i + b.bw, a.get(a.fixed, i)); + break; + } + case OP_EXTRACT: { + expr* child; + unsigned lo, hi; + VERIFY(bv.is_extract(e, lo, hi, child)); + auto& a = wval0(child); + for (unsigned i = lo; i <= hi; ++i) + v.set(v.fixed, i - lo, a.get(a.fixed, i)); + break; + } + case OP_BNEG: { + auto& a = wval0(e->get_arg(0)); + bool pfixed = true; + for (unsigned i = 0; i < v.bw; ++i) { + if (pfixed && a.get(a.fixed, i)) + v.set(v.fixed, i, true); + else { + pfixed = false; + v.set(v.fixed, i, false); + } + } + break; + } + case OP_BSHL: { + // determine range of b. + // if b = 0, then inherit fixed from a + // if b >= v.bw then make e fixed to 0 + // if 0 < b < v.bw is known, then inherit shift of fixed values of a + // if 0 < b < v.bw but not known, then inherit run lengths of equal bits of a + // that are fixed. + NOT_IMPLEMENTED_YET(); + break; + } + case OP_BASHR: + case OP_BLSHR: + case OP_INT2BV: + case OP_BCOMP: + case OP_BNAND: + case OP_BREDAND: + case OP_BREDOR: + case OP_BSDIV: + case OP_BSDIV_I: + case OP_BSDIV0: + case OP_BUDIV: + case OP_BUDIV_I: + case OP_BUDIV0: + case OP_BUREM: + case OP_BUREM_I: + case OP_BUREM0: + case OP_BSMOD: + case OP_BSMOD_I: + case OP_BSMOD0: + case OP_BXOR: + case OP_BXNOR: + NOT_IMPLEMENTED_YET(); + break; + case OP_BV_NUM: + case OP_BIT0: + case OP_BIT1: + case OP_BV2INT: + case OP_BNEG_OVFL: + case OP_BSADD_OVFL: + case OP_BUADD_OVFL: + case OP_BSDIV_OVFL: + case OP_BSMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + case OP_BSMUL_OVFL: + case OP_BUMUL_NO_OVFL: + case OP_BUMUL_OVFL: + case OP_BIT2BOOL: + case OP_ULEQ: + case OP_UGEQ: + case OP_UGT: + case OP_ULT: + case OP_SLEQ: + case OP_SGEQ: + case OP_SGT: + case OP_SLT: + UNREACHABLE(); + break; + } + } +} diff --git a/src/ast/sls/bv_sls_fixed.h b/src/ast/sls/bv_sls_fixed.h new file mode 100644 index 000000000..2dfedca19 --- /dev/null +++ b/src/ast/sls/bv_sls_fixed.h @@ -0,0 +1,52 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls_fixed.h + +Abstract: + + Initialize fixed information. + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ +#pragma once + +#include "ast/ast.h" +#include "ast/sls/sls_valuation.h" +#include "ast/bv_decl_plugin.h" + +namespace bv { + + class sls_eval; + + class sls_fixed { + sls_eval& ev; + ast_manager& m; + bv_util& bv; + + void init_ranges(expr_ref_vector const& es); + void init_range(app* e, bool sign); + void init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign); + void get_offset(expr* e, expr*& x, rational& offset); + + void init_fixed_basic(app* e); + void init_fixed_bv(app* e); + + bool is_fixed1(app* e) const; + bool is_fixed1_basic(app* e) const; + void set_fixed_bw(app* e); + + sls_valuation& wval0(expr* e); + + public: + sls_fixed(sls_eval& ev); + + void init(expr_ref_vector const& es); + + }; +} diff --git a/src/ast/sls/bv_sls_terms.cpp b/src/ast/sls/bv_sls_terms.cpp new file mode 100644 index 000000000..422b2017e --- /dev/null +++ b/src/ast/sls/bv_sls_terms.cpp @@ -0,0 +1,138 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls.cpp + +Abstract: + + A Stochastic Local Search (SLS) engine + Uses invertibility conditions, + interval annotations + don't care annotations + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ + +#include "ast/sls/bv_sls.h" + +namespace bv { + + sls_terms::sls_terms(ast_manager& m): + m(m), + bv(m), + m_assertions(m), + m_pinned(m), + m_translated(m), + m_terms(m){} + + + void sls_terms::assert_expr(expr* e) { + m_assertions.push_back(ensure_binary(e)); + } + + expr* sls_terms::ensure_binary(expr* e) { + expr* top = e; + m_pinned.push_back(e); + m_todo.push_back(e); + expr_fast_mark1 mark; + for (unsigned i = 0; i < m_todo.size(); ++i) { + expr* e = m_todo[i]; + if (!is_app(e)) + continue; + if (m_translated.get(e->get_id(), nullptr)) + continue; + if (mark.is_marked(e)) + continue; + mark.mark(e); + for (auto arg : *to_app(e)) + m_todo.push_back(arg); + } + std::stable_sort(m_todo.begin(), m_todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); + for (expr* e : m_todo) + ensure_binary_core(e); + m_todo.reset(); + return m_translated.get(top->get_id()); + } + + void sls_terms::ensure_binary_core(expr* e) { + app* a = to_app(e); + auto arg = [&](unsigned i) { + return m_translated.get(a->get_arg(i)->get_id()); + }; + unsigned num_args = a->get_num_args(); + expr_ref r(m); +#define FOLD_OP(oper) \ + r = arg(0); \ + for (unsigned i = 1; i < num_args; ++i)\ + r = oper(r, arg(i)); \ + + if (m.is_and(e)) { + FOLD_OP(m.mk_and); + } + else if (m.is_or(e)) { + FOLD_OP(m.mk_or); + } + else if (m.is_xor(e)) { + FOLD_OP(m.mk_xor); + } + else if (bv.is_bv_and(e)) { + FOLD_OP(bv.mk_bv_and); + } + else if (bv.is_bv_or(e)) { + FOLD_OP(bv.mk_bv_or); + } + else if (bv.is_bv_xor(e)) { + FOLD_OP(bv.mk_bv_xor); + } + else if (bv.is_bv_add(e)) { + FOLD_OP(bv.mk_bv_add); + } + else if (bv.is_bv_mul(e)) { + FOLD_OP(bv.mk_bv_mul); + } + else if (bv.is_concat(e)) { + FOLD_OP(bv.mk_concat); + } + else { + for (unsigned i = 0; i < num_args; ++i) + m_todo.push_back(arg(i)); + r = m.mk_app(a->get_decl(), num_args, m_todo.data()); + m_todo.reset(); + } + m_translated.setx(e->get_id(), r); + } + + + void sls_terms::init() { + // populate terms + expr_fast_mark1 mark; + for (expr* e : m_assertions) + m_todo.push_back(e); + while (!m_todo.empty()) { + expr* e = m_todo.back(); + m_todo.pop_back(); + if (mark.is_marked(e) || !is_app(e)) + continue; + mark.mark(e); + m_terms.setx(e->get_id(), to_app(e)); + for (expr* arg : *to_app(e)) + m_todo.push_back(arg); + } + // populate parents + m_parents.reserve(m_terms.size()); + for (expr* e : m_terms) { + if (!e || !is_app(e)) + continue; + for (expr* arg : *to_app(e)) + m_parents[arg->get_id()].push_back(e); + } + for (auto a : m_assertions) + m_assertion_set.insert(a->get_id()); + } + +} diff --git a/src/ast/sls/bv_sls_terms.h b/src/ast/sls/bv_sls_terms.h new file mode 100644 index 000000000..688047846 --- /dev/null +++ b/src/ast/sls/bv_sls_terms.h @@ -0,0 +1,70 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + bv_sls_terms.h + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ +#pragma once + +#include "util/lbool.h" +#include "util/params.h" +#include "util/scoped_ptr_vector.h" +#include "util/uint_set.h" +#include "ast/ast.h" +#include "ast/sls/sls_stats.h" +#include "ast/sls/sls_powers.h" +#include "ast/sls/sls_valuation.h" +#include "ast/bv_decl_plugin.h" + +namespace bv { + + class sls_terms { + ast_manager& m; + bv_util bv; + ptr_vector m_todo; + expr_ref_vector m_assertions, m_pinned, m_translated; + app_ref_vector m_terms; + vector> m_parents; + tracked_uint_set m_assertion_set; + + expr* ensure_binary(expr* e); + void ensure_binary_core(expr* e); + + public: + sls_terms(ast_manager& m); + + /** + * Add constraints + */ + void assert_expr(expr* e); + + /** + * Initialize structures: assertions, parents, terms + */ + void init(); + + /** + * Accessors. + */ + + ptr_vector const& parents(expr* e) const { return m_parents[e->get_id()]; } + + expr_ref_vector const& assertions() const { return m_assertions; } + + app* term(unsigned id) const { return m_terms.get(id); } + + bool is_assertion(expr* e) const { return m_assertion_set.contains(e->get_id()); } + + + }; +} diff --git a/src/ast/sls/sls_engine.cpp b/src/ast/sls/sls_engine.cpp index 8bf70f3dd..249c771ed 100644 --- a/src/ast/sls/sls_engine.cpp +++ b/src/ast/sls/sls_engine.cpp @@ -76,19 +76,6 @@ void sls_engine::updt_params(params_ref const & _p) { NOT_IMPLEMENTED_YET(); } -void sls_engine::collect_statistics(statistics& st) const { - double seconds = m_stats.m_stopwatch.get_current_seconds(); - st.update("sls restarts", m_stats.m_restarts); - st.update("sls full evals", m_stats.m_full_evals); - st.update("sls incr evals", m_stats.m_incr_evals); - st.update("sls incr evals/sec", m_stats.m_incr_evals / seconds); - st.update("sls FLIP moves", m_stats.m_flips); - st.update("sls INC moves", m_stats.m_incs); - st.update("sls DEC moves", m_stats.m_decs); - st.update("sls INV moves", m_stats.m_invs); - st.update("sls moves", m_stats.m_moves); - st.update("sls moves/sec", m_stats.m_moves / seconds); -} bool sls_engine::full_eval(model & mdl) { diff --git a/src/ast/sls/sls_engine.h b/src/ast/sls/sls_engine.h index 32338b8ae..614534f1a 100644 --- a/src/ast/sls/sls_engine.h +++ b/src/ast/sls/sls_engine.h @@ -22,42 +22,15 @@ Notes: #include "util/lbool.h" #include "ast/converters/model_converter.h" +#include "ast/sls/sls_stats.h" #include "ast/sls/sls_tracker.h" #include "ast/sls/sls_evaluator.h" -#include "util/statistics.h" class sls_engine { -public: - class stats { - public: - unsigned m_restarts; - stopwatch m_stopwatch; - unsigned m_full_evals; - unsigned m_incr_evals; - unsigned m_moves, m_flips, m_incs, m_decs, m_invs; - - stats() : - m_restarts(0), - m_full_evals(0), - m_incr_evals(0), - m_moves(0), - m_flips(0), - m_incs(0), - m_decs(0), - m_invs(0) { - m_stopwatch.reset(); - m_stopwatch.start(); - } - void reset() { - m_full_evals = m_flips = m_incr_evals = 0; - m_stopwatch.reset(); - m_stopwatch.start(); - } - }; protected: ast_manager & m_manager; - stats m_stats; + bv::sls_stats m_stats; unsynch_mpz_manager m_mpz_manager; powers m_powers; mpz m_zero, m_one, m_two; @@ -94,8 +67,8 @@ public: void assert_expr(expr * e) { m_assertions.push_back(e); } - stats const & get_stats(void) { return m_stats; } - void collect_statistics(statistics & st) const; + bv::sls_stats const & get_stats(void) { return m_stats; } + void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); } void reset_statistics() { m_stats.reset(); } bool full_eval(model & mdl); diff --git a/src/ast/sls/sls_powers.h b/src/ast/sls/sls_powers.h index 9616c43ab..80ccbe04f 100644 --- a/src/ast/sls/sls_powers.h +++ b/src/ast/sls/sls_powers.h @@ -20,6 +20,7 @@ Notes: #pragma once #include "util/mpz.h" +#include "util/map.h" class powers : public u_map { unsynch_mpz_manager & m; diff --git a/src/ast/sls/sls_stats.h b/src/ast/sls/sls_stats.h new file mode 100644 index 000000000..8599a1f64 --- /dev/null +++ b/src/ast/sls/sls_stats.h @@ -0,0 +1,48 @@ +#pragma once +#include "util/statistics.h" +#include "util/stopwatch.h" + + +namespace bv { + class sls_stats { + public: + unsigned m_restarts; + stopwatch m_stopwatch; + unsigned m_full_evals; + unsigned m_incr_evals; + unsigned m_moves, m_flips, m_incs, m_decs, m_invs; + + sls_stats() : + m_restarts(0), + m_full_evals(0), + m_incr_evals(0), + m_moves(0), + m_flips(0), + m_incs(0), + m_decs(0), + m_invs(0) { + m_stopwatch.reset(); + m_stopwatch.start(); + } + void reset() { + m_full_evals = m_flips = m_incr_evals = 0; + m_stopwatch.reset(); + m_stopwatch.start(); + } + + void collect_statistics(statistics& st) const { + double seconds = m_stopwatch.get_current_seconds(); + st.update("sls restarts", m_restarts); + st.update("sls full evals", m_full_evals); + st.update("sls incr evals", m_incr_evals); + st.update("sls incr evals/sec", m_incr_evals / seconds); + st.update("sls FLIP moves", m_flips); + st.update("sls INC moves", m_incs); + st.update("sls DEC moves", m_decs); + st.update("sls INV moves", m_invs); + st.update("sls moves", m_moves); + st.update("sls moves/sec", m_moves / seconds); + } + + }; +} diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp new file mode 100644 index 000000000..bb15c8da3 --- /dev/null +++ b/src/ast/sls/sls_valuation.cpp @@ -0,0 +1,127 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + sls_valuation.cpp + +Abstract: + + A Stochastic Local Search (SLS) engine + Uses invertibility conditions, + interval annotations + don't care annotations + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ + +#include "ast/sls/sls_valuation.h" + +namespace bv { + + sls_valuation::sls_valuation(unsigned bw): bw(bw) { + nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t)); + unsigned num_bytes = nw * sizeof(digit_t); + lo.reserve(nw); + hi.reserve(nw); + bits.reserve(nw); + fixed.reserve(nw); + // have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated + for (unsigned i = 0; i < nw; ++i) + lo[i] = 0, hi[i] = 0, bits[i] = 0, fixed[i] = 0; + for (unsigned i = bw; i < 8 * sizeof(digit_t) * nw; ++i) + set(fixed, i, true); + } + + sls_valuation::~sls_valuation() { + } + + bool sls_valuation::is_feasible() const { + return true; + mpn_manager m; + unsigned nb = (bw + 7) / 8; + auto c = m.compare(lo.data(), nb, hi.data(), nb); + if (c == 0) + return true; + if (c < 0) + return + m.compare(lo.data(), nb, bits.data(), nb) <= 0 && + m.compare(bits.data(), nb, hi.data(), nb) < 0; + return + m.compare(lo.data(), nb, bits.data(), nb) <= 0 || + m.compare(bits.data(), nb, hi.data(), nb) < 0; + } + + bool sls_valuation::eq(sls_valuation const& other) const { + SASSERT(bw == other.bw); + auto c = 0 == memcmp(bits.data(), other.bits.data(), bw / 8); + if (bw % 8 == 0 || !c) + return c; + NOT_IMPLEMENTED_YET(); + return false; + } + + void sls_valuation::clear_overflow_bits(svector& bits) const { + for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i) + set(bits, i, false); + } + + void sls_valuation::set_value(svector& bits, rational const& n) { + for (unsigned i = 0; i < bw; ++i) + set(bits, i, n.get_bit(i)); + clear_overflow_bits(bits); + } + + void sls_valuation::get_value(svector const& bits, rational& r) const { + rational p(1); + for (unsigned i = 0; i < nw; ++i) { + r += p * rational(bits[i]); + p *= rational::power_of_two(bw); + } + } + + void sls_valuation::set1(svector& bits) { + for (unsigned i = 0; i < bw; ++i) + set(bits, i, true); + } + + bool sls_valuation::can_set(svector const& new_bits) const { + for (unsigned i = 0; i < nw; ++i) + if (bits[i] != ((new_bits[i] & ~fixed[i]) | (bits[i] & fixed[i]))) + return true; + return false; + } + + unsigned sls_valuation::to_nat(svector const& d, unsigned max_n) { + SASSERT(max_n < UINT_MAX / 2); + unsigned p = 1; + unsigned value = 0; + for (unsigned i = 0; i < bw; ++i) { + if (p >= max_n) { + for (unsigned j = i; j < bw; ++j) + if (get(d, j)) + return max_n; + return value; + } + if (get(d, i)) + value += p; + p <<= 1; + } + return value; + } + + void sls_valuation::add_range(rational l, rational h) { + l = mod(l, rational::power_of_two(bw)); + h = mod(h, rational::power_of_two(bw)); + if (h == l) + return; + set_value(this->lo, l); + set_value(this->hi, h); + // TODO: intersect with previous range, if any + + } + +} diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h new file mode 100644 index 000000000..bdc731bfd --- /dev/null +++ b/src/ast/sls/sls_valuation.h @@ -0,0 +1,116 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + sls_valuation.h + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-07 + +--*/ +#pragma once + +#include "util/lbool.h" +#include "util/params.h" +#include "util/scoped_ptr_vector.h" +#include "util/uint_set.h" +#include "ast/ast.h" +#include "ast/sls/sls_stats.h" +#include "ast/sls/sls_powers.h" +#include "ast/bv_decl_plugin.h" + +namespace bv { + + struct sls_valuation { + unsigned bw; // bit-width + unsigned nw; // num words + svector lo, hi; // range assignment to bit-vector, as wrap-around interval + svector bits, fixed; // bit assignment and don't care bit + bool is_feasible() const; // the current bit-evaluation is between lo and hi. + sls_valuation(unsigned bw); + ~sls_valuation(); + + unsigned num_bytes() const { return (bw + 7) / 8; } + + void set_value(svector& bits, rational const& r); + void get_value(svector const& bits, rational& r) const; + void add_range(rational lo, rational hi); + void set1(svector& bits); + + void clear_overflow_bits(svector& bits) const; + bool can_set(svector const& bits) const; + + bool eq(sls_valuation const& other) const; + + bool gt(svector const& a, svector const& b) const { + return 0 > memcmp(a.data(), b.data(), num_bytes()); + } + + unsigned parity(svector const& bits) const { + unsigned i = 0; + for (; i < bw && !get(bits, i); ++i); + return i; + } + + bool try_set(svector const& src) { + if (!can_set(src)) + return false; + set(src); + return true; + } + + void set(svector const& src) { + for (unsigned i = nw; i-- > 0; ) + bits[i] = src[i]; + clear_overflow_bits(bits); + } + + void set_fixed(svector const& src) { + for (unsigned i = nw; i-- > 0; ) + fixed[i] = src[i]; + } + + void set(svector& d, unsigned bit_idx, bool val) const { + auto _val = static_cast(0 - static_cast(val)); + get_bit_word(d, bit_idx) ^= (_val ^ get_bit_word(d, bit_idx)) & get_pos_mask(bit_idx); + } + + bool get(svector const& d, unsigned bit_idx) const { + return (get_bit_word(d, bit_idx) & get_pos_mask(bit_idx)) != 0; + } + + unsigned to_nat(svector const& d, unsigned max_n); + + static digit_t get_pos_mask(unsigned bit_idx) { + return (digit_t)1 << (digit_t)(bit_idx % (8 * sizeof(digit_t))); + } + + static digit_t get_bit_word(svector const& bits, unsigned bit_idx) { + return bits[bit_idx / (8 * sizeof(digit_t))]; + } + + static digit_t& get_bit_word(svector& bits, unsigned bit_idx) { + return bits[bit_idx / (8 * sizeof(digit_t))]; + } + + std::ostream& display(std::ostream& out) const { + out << std::hex; + for (unsigned i = 0; i < nw; ++i) + out << bits[i]; + out << " "; + for (unsigned i = 0; i < nw; ++i) + out << fixed[i]; + out << std::dec; + return out; + } + }; + + inline std::ostream& operator<<(std::ostream& out, sls_valuation const& v) { return v.display(out); } + +} diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 6daadc83b..ca3f46bc0 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -29,6 +29,7 @@ Notes: #include "tactic/sls/sls_tactic.h" #include "params/sls_params.hpp" #include "ast/sls/sls_engine.h" +#include "ast/sls/bv_sls.h" class sls_tactic : public tactic { ast_manager & m; @@ -123,11 +124,111 @@ public: }; +class bv_sls_tactic : public tactic { + ast_manager& m; + params_ref m_params; + bv::sls* m_engine; + +public: + bv_sls_tactic(ast_manager& _m, params_ref const& p) : + m(_m), + m_params(p) { + m_engine = alloc(bv::sls, m); + } + + tactic* translate(ast_manager& m) override { + return alloc(bv_sls_tactic, m, m_params); + } + + ~bv_sls_tactic() override { + dealloc(m_engine); + } + + char const* name() const override { return "bv-sls"; } + + void updt_params(params_ref const& p) override { + m_params.append(p); + m_engine->updt_params(m_params); + } + + void collect_param_descrs(param_descrs& r) override { + sls_params::collect_param_descrs(r); + } + + void run(goal_ref const& g, model_converter_ref& mc) { + if (g->inconsistent()) { + mc = nullptr; + return; + } + + for (unsigned i = 0; i < g->size(); i++) + m_engine->assert_expr(g->form(i)); + + m_engine->init(); + std::function false_eval = [&](expr* e, unsigned idx) { + return false; + }; + m_engine->init_eval(false_eval); + + lbool res = m_engine->operator()(); + auto const& stats = m_engine->get_stats(); + report_tactic_progress("Number of flips:", stats.m_moves); + IF_VERBOSE(0, verbose_stream() << res << "\n"); + IF_VERBOSE(0, m_engine->display(verbose_stream())); + if (res == l_true) { + + if (g->models_enabled()) { + model_ref mdl = m_engine->get_model(); + mc = model2model_converter(mdl.get()); + TRACE("sls_model", mc->display(tout);); + } + g->reset(); + } + else + mc = nullptr; + + } + + void operator()(goal_ref const& g, + goal_ref_buffer& result) override { + result.reset(); + + TRACE("sls", g->display(tout);); + tactic_report report("sls", *g); + + model_converter_ref mc; + run(g, mc); + g->add(mc.get()); + g->inc_depth(); + result.push_back(g.get()); + } + + void cleanup() override { + auto* d = alloc(bv::sls, m); + std::swap(d, m_engine); + dealloc(d); + } + + void collect_statistics(statistics& st) const override { + m_engine->collect_statistics(st); + } + + void reset_statistics() override { + m_engine->reset_statistics(); + } + +}; + static tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) { return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported. clean(alloc(sls_tactic, m, p))); } +tactic* mk_bv_sls_tactic(ast_manager& m, params_ref const& p) { + return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported. + clean(alloc(bv_sls_tactic, m, p))); +} + static tactic * mk_preamble(ast_manager & m, params_ref const & p) { params_ref main_p; @@ -171,3 +272,9 @@ tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { t->updt_params(p); return t; } + +tactic* mk_qfbv_new_sls_tactic(ast_manager& m, params_ref const& p) { + tactic* t = and_then(mk_preamble(m, p), mk_bv_sls_tactic(m, p)); + t->updt_params(p); + return t; +} diff --git a/src/tactic/sls/sls_tactic.h b/src/tactic/sls/sls_tactic.h index 3c0612e6e..d58d310e3 100644 --- a/src/tactic/sls/sls_tactic.h +++ b/src/tactic/sls/sls_tactic.h @@ -24,7 +24,16 @@ class tactic; tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p = params_ref()); +tactic* mk_qfbv_new_sls_tactic(ast_manager& m, params_ref const& p = params_ref()); + +tactic* mk_bv_sls_tactic(ast_manager& m, params_ref const& p = params_ref()); + /* ADD_TACTIC("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_sls_tactic(m, p)") + + ADD_TACTIC("qfbv-new-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_new_sls_tactic(m, p)") + + ADD_TACTIC("qfbv-new-sls-core", "(try to) solve using stochastic local search for QF_BV.", "mk_bv_sls_tactic(m, p)") + */