mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

initial stab at new bv-sls based on repair actions

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-02-13 16:34:26 +07:00
parent 10687082f1
commit f39756c74b
17 changed files with 2278 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/sls/CMakeLists.txt
View file

@ -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

160
src/ast/sls/bv_sls.cpp Normal file
View file

@ -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<bool(expr*, unsigned)>& 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;
}
}

99
src/ast/sls/bv_sls.h Normal file
View file

@ -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<expr> 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<bool(expr*, unsigned)>& 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();
};
}

821
src/ast/sls/bv_sls_eval.cpp Normal file
View file

@ -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<bool(expr*, unsigned)> 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<expr>& 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<bool(int)> 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 <s y <=> x + 2^{bw-1} <u y + 2^{bw-1}
auto scompare = [&](std::function<bool(int)> 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<digit_t>& 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)));
}
}

134
src/ast/sls/bv_sls_eval.h Normal file
View file

@ -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<expr> m_todo;
random_gen m_rand;
scoped_ptr_vector<sls_valuation> 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<digit_t> 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<bool(expr*, unsigned)> const& eval);
void init_fixed(expr_ref_vector const& es) { m_fix.init(es); }
ptr_vector<expr>& 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<digit_t>& 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);
};
}

386
src/ast/sls/bv_sls_fixed.cpp Normal file
View file

@ -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;
}
}
}

52
src/ast/sls/bv_sls_fixed.h Normal file
View file

@ -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);
};
}

138
src/ast/sls/bv_sls_terms.cpp Normal file
View file

@ -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());
}
}

70
src/ast/sls/bv_sls_terms.h Normal file
View file

@ -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<expr> m_todo;
expr_ref_vector m_assertions, m_pinned, m_translated;
app_ref_vector m_terms;
vector<ptr_vector<expr>> 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<expr> 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()); }
};
}

13
src/ast/sls/sls_engine.cpp
View file

@ -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) {

35
src/ast/sls/sls_engine.h
View file

@ -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);

1
src/ast/sls/sls_powers.h
View file

@ -20,6 +20,7 @@ Notes:
#pragma once
#include "util/mpz.h"
#include "util/map.h"
class powers : public u_map<mpz*> {
unsynch_mpz_manager & m;

48
src/ast/sls/sls_stats.h Normal file
View file

@ -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);
}
};
}

127
src/ast/sls/sls_valuation.cpp Normal file
View file

@ -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<digit_t>& bits) const {
for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i)
set(bits, i, false);
}
void sls_valuation::set_value(svector<digit_t>& 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<digit_t> 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<digit_t>& bits) {
for (unsigned i = 0; i < bw; ++i)
set(bits, i, true);
}
bool sls_valuation::can_set(svector<digit_t> 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<digit_t> 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
}
}

116
src/ast/sls/sls_valuation.h Normal file
View file

@ -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<digit_t> lo, hi; // range assignment to bit-vector, as wrap-around interval
svector<digit_t> 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<digit_t>& bits, rational const& r);
void get_value(svector<digit_t> const& bits, rational& r) const;
void add_range(rational lo, rational hi);
void set1(svector<digit_t>& bits);
void clear_overflow_bits(svector<digit_t>& bits) const;
bool can_set(svector<digit_t> const& bits) const;
bool eq(sls_valuation const& other) const;
bool gt(svector<digit_t> const& a, svector<digit_t> const& b) const {
return 0 > memcmp(a.data(), b.data(), num_bytes());
}
unsigned parity(svector<digit_t> const& bits) const {
unsigned i = 0;
for (; i < bw && !get(bits, i); ++i);
return i;
}
bool try_set(svector<digit_t> const& src) {
if (!can_set(src))
return false;
set(src);
return true;
}
void set(svector<digit_t> const& src) {
for (unsigned i = nw; i-- > 0; )
bits[i] = src[i];
clear_overflow_bits(bits);
}
void set_fixed(svector<digit_t> const& src) {
for (unsigned i = nw; i-- > 0; )
fixed[i] = src[i];
}
void set(svector<digit_t>& d, unsigned bit_idx, bool val) const {
auto _val = static_cast<digit_t>(0 - static_cast<digit_t>(val));
get_bit_word(d, bit_idx) ^= (_val ^ get_bit_word(d, bit_idx)) & get_pos_mask(bit_idx);
}
bool get(svector<digit_t> const& d, unsigned bit_idx) const {
return (get_bit_word(d, bit_idx) & get_pos_mask(bit_idx)) != 0;
}
unsigned to_nat(svector<digit_t> 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<digit_t> const& bits, unsigned bit_idx) {
return bits[bit_idx / (8 * sizeof(digit_t))];
}
static digit_t& get_bit_word(svector<digit_t>& 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); }
}

107
src/tactic/sls/sls_tactic.cpp
View file

@ -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<bool(expr*, unsigned)> 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;
}

9
src/tactic/sls/sls_tactic.h
View file

@ -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)")
*/