mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity

add intblast to legacy SMT solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-27 12:28:36 -07:00
parent aa67c3655f
commit 7e2acad030
10 changed files with 1047 additions and 704 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/CMakeLists.txt
View file

@ -4,6 +4,7 @@ z3_add_component(rewriter
array_rewriter.cpp
ast_counter.cpp
bit2int.cpp
bv2int_translator.cpp
bool_rewriter.cpp
bv_bounds.cpp
bv_elim.cpp

680
src/ast/rewriter/bv2int_translator.cpp Normal file
View file

@ -0,0 +1,680 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
bv2int_translator
Author:
Nikolaj Bjorner (nbjorner) 2024-10-27
--*/
#include "ast/ast.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/bv2int_translator.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
bv2int_translator::bv2int_translator(ast_manager& m, bv2int_translator_trail& ctx) :
m(m),
ctx(ctx),
bv(m),
a(m),
m_translate(m),
m_args(m),
m_pinned(m),
m_vars(m),
m_preds(m)
{}
void bv2int_translator::reset(bool is_plugin) {
m_vars.reset();
m_preds.reset();
for (unsigned i = m_translate.size(); i-- > 0; )
m_translate[i] = nullptr;
m_is_plugin = is_plugin;
}
void bv2int_translator::set_translated(expr* e, expr* r) {
SASSERT(r);
SASSERT(!is_translated(e));
m_translate.setx(e->get_id(), r);
ctx.push_idx(set_vector_idx_trail(m_translate, e->get_id()));
}
void bv2int_translator::internalize_bv(app* e) {
ensure_translated(e);
if (m.is_bool(e)) {
m_preds.push_back(e);
ctx.push(push_back_vector(m_preds));
}
}
void bv2int_translator::ensure_translated(expr* e) {
if (m_translate.get(e->get_id(), nullptr))
return;
ptr_vector<expr> todo;
ast_fast_mark1 visited;
todo.push_back(e);
visited.mark(e);
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];
if (!is_app(e))
continue;
app* a = to_app(e);
if (m.is_bool(e) && a->get_family_id() != bv.get_family_id())
continue;
for (auto arg : *a)
if (!visited.is_marked(arg) && !m_translate.get(arg->get_id(), nullptr)) {
visited.mark(arg);
todo.push_back(arg);
}
}
std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
for (expr* e : todo)
translate_expr(e);
}
rational bv2int_translator::bv_size(expr* bv_expr) {
return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort()));
}
void bv2int_translator::translate_expr(expr* e) {
if (is_quantifier(e))
translate_quantifier(to_quantifier(e));
else if (is_var(e))
translate_var(to_var(e));
else {
app* ap = to_app(e);
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
set_translated(e, e);
return;
}
m_args.reset();
for (auto arg : *ap)
m_args.push_back(translated(arg));
if (ap->get_family_id() == basic_family_id)
translate_basic(ap);
else if (ap->get_family_id() == bv.get_family_id())
translate_bv(ap);
else
translate_app(ap);
}
}
void bv2int_translator::translate_quantifier(quantifier* q) {
if (m_is_plugin) {
set_translated(q, q);
return;
}
if (is_lambda(q))
throw default_exception("lambdas are not supported in intblaster");
expr* b = q->get_expr();
unsigned nd = q->get_num_decls();
ptr_vector<sort> sorts;
for (unsigned i = 0; i < nd; ++i) {
auto s = q->get_decl_sort(i);
if (bv.is_bv_sort(s)) {
NOT_IMPLEMENTED_YET();
sorts.push_back(a.mk_int());
}
else
sorts.push_back(s);
}
b = translated(b);
// TODO if sorts contain integer, then created bounds variables.
set_translated(q, m.update_quantifier(q, b));
}
void bv2int_translator::translate_var(var* v) {
if (bv.is_bv_sort(v->get_sort()))
set_translated(v, m.mk_var(v->get_idx(), a.mk_int()));
else
set_translated(v, v);
}
// Translate functions that are not built-in or bit-vectors.
// Base method uses fresh functions.
// Other method could use bv2int, int2bv axioms and coercions.
// f(args) = bv2int(f(int2bv(args'))
//
void bv2int_translator::translate_app(app* e) {
if (m_is_plugin && m.is_bool(e)) {
set_translated(e, e);
return;
}
bool has_bv_sort = bv.is_bv(e);
func_decl* f = e->get_decl();
for (unsigned i = 0; i < m_args.size(); ++i)
if (bv.is_bv(e->get_arg(i)))
m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i));
if (has_bv_sort)
m_vars.push_back(e);
if (m_is_plugin) {
expr* r = m.mk_app(f, m_args);
if (has_bv_sort) {
ctx.push(push_back_vector(m_vars));
r = bv.mk_bv2int(r);
}
set_translated(e, r);
return;
}
else if (has_bv_sort) {
if (f->get_family_id() != null_family_id)
throw default_exception("conversion for interpreted functions is not supported by intblast solver");
func_decl* g = nullptr;
if (!m_new_funs.find(f, g)) {
g = m.mk_fresh_func_decl(e->get_decl()->get_name(), symbol("bv"), f->get_arity(), f->get_domain(), a.mk_int());
m_new_funs.insert(f, g);
}
f = g;
m_pinned.push_back(f);
}
set_translated(e, m.mk_app(f, m_args));
}
void bv2int_translator::translate_bv(app* e) {
auto bnot = [&](expr* e) {
return a.mk_sub(a.mk_int(-1), e);
};
auto band = [&](expr_ref_vector const& args) {
expr* r = arg(0);
for (unsigned i = 1; i < args.size(); ++i)
r = a.mk_band(bv.get_bv_size(e), r, arg(i));
return r;
};
auto rotate_left = [&](unsigned n) {
auto sz = bv.get_bv_size(e);
n = n % sz;
expr* r = arg(0);
if (n != 0 && sz != 1) {
// r[sz - n - 1 : 0] ++ r[sz - 1 : sz - n]
// r * 2^(sz - n) + (r div 2^n) mod 2^(sz - n)???
// r * A + (r div B) mod A
auto N = bv_size(e);
auto A = rational::power_of_two(sz - n);
auto B = rational::power_of_two(n);
auto hi = mul(r, a.mk_int(A));
auto lo = amod(e, a.mk_idiv(umod(e, 0), a.mk_int(B)), A);
r = add(hi, lo);
}
return r;
};
expr* bv_expr = e;
expr_ref r(m);
auto const& args = m_args;
switch (e->get_decl_kind()) {
case OP_BADD:
r = a.mk_add(args);
break;
case OP_BSUB:
r = a.mk_sub(args.size(), args.data());
break;
case OP_BMUL:
r = a.mk_mul(args);
break;
case OP_ULEQ:
bv_expr = e->get_arg(0);
r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_UGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_ULT:
bv_expr = e->get_arg(0);
r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_UGT:
bv_expr = e->get_arg(0);
r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_SLEQ:
bv_expr = e->get_arg(0);
r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SLT:
bv_expr = e->get_arg(0);
r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SGT:
bv_expr = e->get_arg(0);
r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_BNEG:
r = a.mk_uminus(arg(0));
break;
case OP_CONCAT: {
unsigned sz = 0;
expr_ref new_arg(m);
for (unsigned i = args.size(); i-- > 0;) {
expr* old_arg = e->get_arg(i);
new_arg = umod(old_arg, i);
if (sz > 0) {
new_arg = mul(new_arg, a.mk_int(rational::power_of_two(sz)));
r = add(r, new_arg);
}
else
r = new_arg;
sz += bv.get_bv_size(old_arg->get_sort());
}
break;
}
case OP_EXTRACT: {
unsigned lo, hi;
expr* old_arg;
VERIFY(bv.is_extract(e, lo, hi, old_arg));
r = arg(0);
if (lo > 0)
r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
break;
}
case OP_BV_NUM: {
rational val;
unsigned sz;
VERIFY(bv.is_numeral(e, val, sz));
r = a.mk_int(val);
break;
}
case OP_BUREM:
case OP_BUREM_I: {
expr* x = umod(e, 0), * y = umod(e, 1);
r = if_eq(y, 0, x, a.mk_mod(x, y));
break;
}
case OP_BUDIV:
case OP_BUDIV_I: {
expr* x = umod(e, 0), * y = umod(e, 1);
r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y));
break;
}
case OP_BUMUL_NO_OVFL: {
bv_expr = e->get_arg(0);
r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
break;
}
case OP_BSHL: {
if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
r = a.mk_shl(bv.get_bv_size(e), arg(0), arg(1));
else {
expr* x = arg(0), * y = umod(e, 1);
r = a.mk_int(0);
IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r);
}
break;
}
case OP_BNOT:
r = bnot(arg(0));
break;
case OP_BLSHR:
if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1));
else {
expr* x = arg(0), * y = umod(e, 1);
r = a.mk_int(0);
IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
}
break;
case OP_BASHR:
if (!a.is_numeral(arg(1)))
r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1));
else {
//
// ashr(x, y)
// if y = k & x >= 0 -> x / 2^k
// if y = k & x < 0 -> (x / 2^k) - 2^{N-k}
//
unsigned sz = bv.get_bv_size(e);
rational N = bv_size(e);
expr* x = umod(e, 0), * y = umod(e, 1);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0));
IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < sz; ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
r = if_eq(y, i,
m.mk_ite(signx, add(d, a.mk_int(-rational::power_of_two(sz - i))), d),
r);
}
}
break;
case OP_BOR:
// p | q := (p + q) - band(p, q)
IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
r = arg(0);
for (unsigned i = 1; i < args.size(); ++i)
r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
break;
case OP_BNAND:
r = bnot(band(args));
break;
case OP_BAND:
IF_VERBOSE(2, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
r = band(args);
break;
case OP_BXNOR:
case OP_BXOR: {
// p ^ q := (p + q) - 2*band(p, q);
unsigned sz = bv.get_bv_size(e);
IF_VERBOSE(2, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
r = arg(0);
for (unsigned i = 1; i < args.size(); ++i) {
expr* q = arg(i);
r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q)));
}
if (e->get_decl_kind() == OP_BXNOR)
r = bnot(r);
break;
}
case OP_ZERO_EXT:
bv_expr = e->get_arg(0);
r = umod(bv_expr, 0);
SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
break;
case OP_SIGN_EXT: {
bv_expr = e->get_arg(0);
r = umod(bv_expr, 0);
SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
unsigned arg_sz = bv.get_bv_size(bv_expr);
//unsigned sz = bv.get_bv_size(e);
// rational N = rational::power_of_two(sz);
rational M = rational::power_of_two(arg_sz);
expr* signbit = a.mk_ge(r, a.mk_int(M / 2));
r = m.mk_ite(signbit, a.mk_sub(r, a.mk_int(M)), r);
break;
}
case OP_INT2BV:
m_int2bv.push_back(e);
ctx.push(push_back_vector(m_int2bv));
r = arg(0);
break;
case OP_BV2INT:
m_bv2int.push_back(e);
ctx.push(push_back_vector(m_bv2int));
r = umod(e->get_arg(0), 0);
break;
case OP_BCOMP:
bv_expr = e->get_arg(0);
r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
break;
case OP_BSMOD_I:
case OP_BSMOD: {
expr* x = umod(e, 0), * y = umod(e, 1);
rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2));
expr* u = a.mk_mod(x, y);
// u = 0 -> 0
// y = 0 -> x
// x < 0, y < 0 -> -u
// x < 0, y >= 0 -> y - u
// x >= 0, y < 0 -> y + u
// x >= 0, y >= 0 -> u
r = a.mk_uminus(u);
r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
r = if_eq(u, 0, a.mk_int(0), r);
r = if_eq(y, 0, x, r);
break;
}
case OP_BSDIV_I:
case OP_BSDIV: {
// d = udiv(abs(x), abs(y))
// y = 0, x > 0 -> 1
// y = 0, x <= 0 -> -1
// x = 0, y != 0 -> 0
// x > 0, y < 0 -> -d
// x < 0, y > 0 -> -d
// x > 0, y > 0 -> d
// x < 0, y < 0 -> d
expr* x = umod(e, 0), * y = umod(e, 1);
rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2));
x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(x, y);
r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
break;
}
case OP_BSREM_I:
case OP_BSREM: {
// y = 0 -> x
// else x - sdiv(x, y) * y
expr* x = umod(e, 0), * y = umod(e, 1);
rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2));
expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(absx, absy);
d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = a.mk_sub(x, mul(d, y));
r = if_eq(y, 0, x, r);
break;
}
case OP_ROTATE_LEFT: {
auto n = e->get_parameter(0).get_int();
r = rotate_left(n);
break;
}
case OP_ROTATE_RIGHT: {
unsigned sz = bv.get_bv_size(e);
auto n = e->get_parameter(0).get_int();
r = rotate_left(sz - n);
break;
}
case OP_EXT_ROTATE_LEFT: {
unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1);
r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i)
r = if_eq(y, i, rotate_left(i), r);
break;
}
case OP_EXT_ROTATE_RIGHT: {
unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1);
r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i)
r = if_eq(y, i, rotate_left(sz - i), r);
break;
}
case OP_REPEAT: {
unsigned n = e->get_parameter(0).get_int();
expr* x = umod(e->get_arg(0), 0);
r = x;
rational N = bv_size(e->get_arg(0));
rational N0 = N;
for (unsigned i = 1; i < n; ++i)
r = add(mul(a.mk_int(N), x), r), N *= N0;
break;
}
case OP_BREDOR: {
r = umod(e->get_arg(0), 0);
r = m.mk_not(m.mk_eq(r, a.mk_int(0)));
break;
}
case OP_BREDAND: {
rational N = bv_size(e->get_arg(0));
r = umod(e->get_arg(0), 0);
r = m.mk_not(m.mk_eq(r, a.mk_int(N - 1)));
break;
}
default:
verbose_stream() << mk_pp(e, m) << "\n";
NOT_IMPLEMENTED_YET();
}
set_translated(e, r);
}
expr_ref bv2int_translator::if_eq(expr* n, unsigned k, expr* th, expr* el) {
rational r;
expr_ref _th(th, m), _el(el, m);
if (bv.is_numeral(n, r)) {
if (r == k)
return expr_ref(th, m);
else
return expr_ref(el, m);
}
return expr_ref(m.mk_ite(m.mk_eq(n, a.mk_int(k)), th, el), m);
}
void bv2int_translator::translate_basic(app* e) {
if (m.is_eq(e)) {
bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
if (has_bv_arg) {
expr* bv_expr = e->get_arg(0);
rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
if (a.is_numeral(arg(0)) || a.is_numeral(arg(1)) ||
is_bounded(arg(0), N) || is_bounded(arg(1), N)) {
set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)));
}
else {
m_args[0] = a.mk_sub(arg(0), arg(1));
set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0)));
}
}
else
set_translated(e, m.mk_eq(arg(0), arg(1)));
}
else if (m.is_ite(e))
set_translated(e, m.mk_ite(arg(0), arg(1), arg(2)));
else if (m_is_plugin)
set_translated(e, e);
else
set_translated(e, m.mk_app(e->get_decl(), m_args));
}
bool bv2int_translator::is_bounded(expr* x, rational const& N) {
return any_of(m_vars, [&](expr* v) {
return is_translated(v) && translated(v) == x && bv_size(v) <= N;
});
}
bool bv2int_translator::is_non_negative(expr* bv_expr, expr* e) {
auto N = rational::power_of_two(bv.get_bv_size(bv_expr));
rational r;
if (a.is_numeral(e, r))
return r >= 0;
if (is_bounded(e, N))
return true;
expr* x = nullptr, * y = nullptr;
if (a.is_mul(e, x, y))
return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
if (a.is_add(e, x, y))
return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
return false;
}
expr* bv2int_translator::umod(expr* bv_expr, unsigned i) {
expr* x = arg(i);
rational N = bv_size(bv_expr);
return amod(bv_expr, x, N);
}
expr* bv2int_translator::smod(expr* bv_expr, unsigned i) {
expr* x = arg(i);
auto N = bv_size(bv_expr);
auto shift = N / 2;
rational r;
if (a.is_numeral(x, r))
return a.mk_int(mod(r + shift, N));
return amod(bv_expr, add(x, a.mk_int(shift)), N);
}
expr_ref bv2int_translator::mul(expr* x, expr* y) {
expr_ref _x(x, m), _y(y, m);
if (a.is_zero(x))
return _x;
if (a.is_zero(y))
return _y;
if (a.is_one(x))
return _y;
if (a.is_one(y))
return _x;
rational v1, v2;
if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
return expr_ref(a.mk_int(v1 * v2), m);
_x = a.mk_mul(x, y);
return _x;
}
expr_ref bv2int_translator::add(expr* x, expr* y) {
expr_ref _x(x, m), _y(y, m);
if (a.is_zero(x))
return _y;
if (a.is_zero(y))
return _x;
rational v1, v2;
if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
return expr_ref(a.mk_int(v1 + v2), m);
_x = a.mk_add(x, y);
return _x;
}
/*
* Perform simplifications that are claimed sound when the bit-vector interpretations of
* mod/div always guard the mod and dividend to be non-zero.
* Potentially shady area is for arithmetic expressions created by int2bv.
* They will be guarded by a modulus which does not disappear.
*/
expr* bv2int_translator::amod(expr* bv_expr, expr* x, rational const& N) {
rational v;
expr* r = nullptr, * c = nullptr, * t = nullptr, * e = nullptr;
if (m.is_ite(x, c, t, e))
r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N));
else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e))
r = x;
else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N)
r = x;
else if (a.is_numeral(x, v))
r = a.mk_int(mod(v, N));
else if (is_bounded(x, N))
r = x;
else
r = a.mk_mod(x, a.mk_int(N));
return r;
}
void bv2int_translator::translate_eq(expr* e) {
expr* x = nullptr, * y = nullptr;
VERIFY(m.is_eq(e, x, y));
SASSERT(bv.is_bv(x));
if (!is_translated(e)) {
ensure_translated(x);
ensure_translated(y);
m_args.reset();
m_args.push_back(a.mk_sub(translated(x), translated(y)));
set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
}
m_preds.push_back(e);
TRACE("bv", tout << mk_pp(e, m) << " " << mk_pp(translated(e), m) << "\n");
ctx.push(push_back_vector(m_preds));
}

78
src/ast/rewriter/bv2int_translator.h Normal file
View file

@ -0,0 +1,78 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
bv2int_translator
Utilities for translating bit-vector constraints into arithmetic.
Author:
Nikolaj Bjorner (nbjorner) 2024-10-27
--*/
#pragma once
#include "util/trail.h"
class bv2int_translator_trail {
public:
virtual void push(push_back_vector<expr_ref_vector> const& c) = 0;
virtual void push(push_back_vector<ptr_vector<app>> const& c) = 0;
virtual void push_idx(set_vector_idx_trail<expr_ref_vector> const& c) = 0;
};
class bv2int_translator {
ast_manager& m;
bv2int_translator_trail& ctx;
bv_util bv;
arith_util a;
obj_map<func_decl, func_decl*> m_new_funs;
expr_ref_vector m_translate, m_args;
ast_ref_vector m_pinned;
ptr_vector<app> m_bv2int, m_int2bv;
expr_ref_vector m_vars, m_preds;
bool m_is_plugin = true;
void set_translated(expr* e, expr* r);
expr* arg(unsigned i) { return m_args.get(i); }
expr* umod(expr* bv_expr, unsigned i);
expr* smod(expr* bv_expr, unsigned i);
bool is_bounded(expr* v, rational const& N);
bool is_non_negative(expr* bv_expr, expr* e);
expr_ref mul(expr* x, expr* y);
expr_ref add(expr* x, expr* y);
expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el);
expr* amod(expr* bv_expr, expr* x, rational const& N);
rational bv_size(expr* bv_expr);
void translate_bv(app* e);
void translate_basic(app* e);
void translate_app(app* e);
void translate_quantifier(quantifier* q);
void translate_var(var* v);
public:
bv2int_translator(ast_manager& m, bv2int_translator_trail& ctx);
void ensure_translated(expr* e);
void translate_eq(expr* e);
bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); }
expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
void internalize_bv(app* e);
void translate_expr(expr* e);
expr_ref_vector const& vars() const { return m_vars; }
expr_ref_vector const& preds() const { return m_preds; }
ptr_vector<app> const& bv2int() const { return m_bv2int; }
ptr_vector<app> const& int2bv() const { return m_int2bv; }
void reset(bool is_plugin);
};

706
src/sat/smt/intblast_solver.cpp
View file

@ -22,6 +22,10 @@ Author:
namespace intblast {
void translator_trail::push(push_back_vector<expr_ref_vector> const& c) { ctx.push(c); }
void translator_trail::push(push_back_vector<ptr_vector<app>> const& c) { ctx.push(c); }
void translator_trail::push_idx(set_vector_idx_trail<expr_ref_vector> const& c) { ctx.push(c); }
solver::solver(euf::solver& ctx) :
th_euf_solver(ctx, symbol("intblast"), ctx.get_manager().get_family_id("bv")),
ctx(ctx),
@ -29,9 +33,8 @@ namespace intblast {
m(ctx.get_manager()),
bv(m),
a(m),
m_translate(m),
m_args(m),
m_pinned(m)
trail(ctx),
m_translator(m, trail)
{}
euf::theory_var solver::mk_var(euf::enode* n) {
@ -85,49 +88,22 @@ namespace intblast {
SASSERT(!n->is_attached_to(get_id()));
mk_var(n);
SASSERT(n->is_attached_to(get_id()));
internalize_bv(a);
m_translator.internalize_bv(a);
return true;
}
void solver::eq_internalized(euf::enode* n) {
expr* e = n->get_expr();
expr* x = nullptr, * y = nullptr;
VERIFY(m.is_eq(n->get_expr(), x, y));
SASSERT(bv.is_bv(x));
if (!is_translated(e)) {
ensure_translated(x);
ensure_translated(y);
m_args.reset();
m_args.push_back(a.mk_sub(translated(x), translated(y)));
set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
}
m_preds.push_back(e);
TRACE("bv", tout << mk_pp(e, m) << " " << mk_pp(translated(e), m) << "\n");
ctx.push(push_back_vector(m_preds));
}
void solver::set_translated(expr* e, expr* r) {
SASSERT(r);
SASSERT(!is_translated(e));
m_translate.setx(e->get_id(), r);
ctx.push(set_vector_idx_trail(m_translate, e->get_id()));
}
void solver::internalize_bv(app* e) {
ensure_translated(e);
if (m.is_bool(e)) {
m_preds.push_back(e);
ctx.push(push_back_vector(m_preds));
}
m_translator.translate_eq(n->get_expr());
}
bool solver::add_bound_axioms() {
if (m_vars_qhead == m_vars.size())
auto const& vars = m_translator.vars();
if (m_vars_qhead == vars.size())
return false;
ctx.push(value_trail(m_vars_qhead));
for (; m_vars_qhead < m_vars.size(); ++m_vars_qhead) {
auto v = m_vars[m_vars_qhead];
auto w = translated(v);
for (; m_vars_qhead < vars.size(); ++m_vars_qhead) {
auto v = vars[m_vars_qhead];
auto w = m_translator.translated(v);
auto sz = rational::power_of_two(bv.get_bv_size(v->get_sort()));
auto lo = ctx.mk_literal(a.mk_ge(w, a.mk_int(0)));
auto hi = ctx.mk_literal(a.mk_le(w, a.mk_int(sz - 1)));
@ -140,12 +116,13 @@ namespace intblast {
}
bool solver::add_predicate_axioms() {
if (m_preds_qhead == m_preds.size())
auto const& preds = m_translator.preds();
if (m_preds_qhead == preds.size())
return false;
ctx.push(value_trail(m_preds_qhead));
for (; m_preds_qhead < m_preds.size(); ++m_preds_qhead) {
expr* e = m_preds[m_preds_qhead];
expr_ref r(translated(e), m);
for (; m_preds_qhead < preds.size(); ++m_preds_qhead) {
expr* e = preds[m_preds_qhead];
expr_ref r(m_translator.translated(e), m);
ctx.get_rewriter()(r);
auto a = expr2literal(e);
auto b = mk_literal(r);
@ -158,31 +135,7 @@ namespace intblast {
bool solver::unit_propagate() {
return add_bound_axioms() || add_predicate_axioms();
}
void solver::ensure_translated(expr* e) {
if (m_translate.get(e->get_id(), nullptr))
return;
ptr_vector<expr> todo;
ast_fast_mark1 visited;
todo.push_back(e);
visited.mark(e);
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];
if (!is_app(e))
continue;
app* a = to_app(e);
if (m.is_bool(e) && a->get_family_id() != bv.get_family_id())
continue;
for (auto arg : *a)
if (!visited.is_marked(arg) && !m_translate.get(arg->get_id(), nullptr)) {
visited.mark(arg);
todo.push_back(arg);
}
}
std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
for (expr* e : todo)
translate_expr(e);
}
}
lbool solver::check_axiom(sat::literal_vector const& lits) {
sat::literal_vector core;
@ -198,14 +151,10 @@ namespace intblast {
}
lbool solver::check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
m_core.reset();
m_vars.reset();
m_is_plugin = false;
m_translator.reset(false);
m_solver = mk_smt2_solver(m, s.params(), symbol::null);
for (unsigned i = 0; i < m_translate.size(); ++i)
m_translate[i] = nullptr;
expr_ref_vector es(m), original_es(m);
for (auto lit : lits)
es.push_back(ctx.literal2expr(lit));
@ -222,8 +171,8 @@ namespace intblast {
translate(es);
for (auto e : m_vars) {
auto v = translated(e);
for (auto e : m_translator.vars()) {
auto v = m_translator.translated(e);
auto b = rational::power_of_two(bv.get_bv_size(e));
m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
@ -331,8 +280,8 @@ namespace intblast {
translate(es);
for (auto e : m_vars) {
auto v = translated(e);
for (auto e : m_translator.vars()) {
auto v = m_translator.translated(e);
auto b = rational::power_of_two(bv.get_bv_size(e));
m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
@ -377,7 +326,7 @@ namespace intblast {
void solver::sorted_subterms(expr_ref_vector& es, ptr_vector<expr>& sorted) {
expr_fast_mark1 visited;
for (expr* e : es) {
if (is_translated(e))
if (m_translator.is_translated(e))
continue;
if (visited.is_marked(e))
continue;
@ -389,7 +338,7 @@ namespace intblast {
if (is_app(e)) {
app* a = to_app(e);
for (expr* arg : *a) {
if (!visited.is_marked(arg) && !is_translated(arg)) {
if (!visited.is_marked(arg) && !m_translator.is_translated(arg)) {
visited.mark(arg);
sorted.push_back(arg);
}
@ -399,7 +348,7 @@ namespace intblast {
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
expr* b = q->get_expr();
if (!visited.is_marked(b) && !is_translated(b)) {
if (!visited.is_marked(b) && !m_translator.is_translated(b)) {
visited.mark(b);
sorted.push_back(b);
}
@ -414,20 +363,20 @@ namespace intblast {
sorted_subterms(es, todo);
for (expr* e : todo)
translate_expr(e);
m_translator.translate_expr(e);
TRACE("bv",
for (expr* e : es)
tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated(e), m) << "\n";
tout << mk_pp(e, m) << "\n->\n" << mk_pp(m_translator.translated(e), m) << "\n";
);
for (unsigned i = 0; i < es.size(); ++i)
es[i] = translated(es.get(i));
es[i] = m_translator.translated(es.get(i));
}
sat::check_result solver::check() {
// ensure that bv2int is injective
for (auto e : m_bv2int) {
for (auto e : m_translator.bv2int()) {
euf::enode* n = expr2enode(e);
euf::enode* r1 = n->get_arg(0)->get_root();
for (auto sib : euf::enode_class(n)) {
@ -449,7 +398,7 @@ namespace intblast {
}
// ensure that int2bv respects values
// bv2int(int2bv(x)) = x mod N
for (auto e : m_int2bv) {
for (auto e : m_translator.int2bv()) {
auto n = expr2enode(e);
auto x = n->get_arg(0)->get_expr();
auto bv2int = bv.mk_bv2int(e);
@ -469,595 +418,12 @@ namespace intblast {
return sat::check_result::CR_DONE;
}
bool solver::is_bounded(expr* x, rational const& N) {
return any_of(m_vars, [&](expr* v) {
return is_translated(v) && translated(v) == x && bv_size(v) <= N;
});
}
bool solver::is_non_negative(expr* bv_expr, expr* e) {
auto N = rational::power_of_two(bv.get_bv_size(bv_expr));
rational r;
if (a.is_numeral(e, r))
return r >= 0;
if (is_bounded(e, N))
return true;
expr* x = nullptr, * y = nullptr;
if (a.is_mul(e, x, y))
return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
if (a.is_add(e, x, y))
return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
return false;
}
expr* solver::umod(expr* bv_expr, unsigned i) {
expr* x = arg(i);
rational N = bv_size(bv_expr);
return amod(bv_expr, x, N);
}
expr* solver::smod(expr* bv_expr, unsigned i) {
expr* x = arg(i);
auto N = bv_size(bv_expr);
auto shift = N / 2;
rational r;
if (a.is_numeral(x, r))
return a.mk_int(mod(r + shift, N));
return amod(bv_expr, add(x, a.mk_int(shift)), N);
}
expr_ref solver::mul(expr* x, expr* y) {
expr_ref _x(x, m), _y(y, m);
if (a.is_zero(x))
return _x;
if (a.is_zero(y))
return _y;
if (a.is_one(x))
return _y;
if (a.is_one(y))
return _x;
rational v1, v2;
if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
return expr_ref(a.mk_int(v1 * v2), m);
_x = a.mk_mul(x, y);
return _x;
}
expr_ref solver::add(expr* x, expr* y) {
expr_ref _x(x, m), _y(y, m);
if (a.is_zero(x))
return _y;
if (a.is_zero(y))
return _x;
rational v1, v2;
if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
return expr_ref(a.mk_int(v1 + v2), m);
_x = a.mk_add(x, y);
return _x;
}
/*
* Perform simplifications that are claimed sound when the bit-vector interpretations of
* mod/div always guard the mod and dividend to be non-zero.
* Potentially shady area is for arithmetic expressions created by int2bv.
* They will be guarded by a modulus which does not disappear.
*/
expr* solver::amod(expr* bv_expr, expr* x, rational const& N) {
rational v;
expr* r = nullptr, *c = nullptr, * t = nullptr, * e = nullptr;
if (m.is_ite(x, c, t, e))
r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N));
else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e))
r = x;
else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N)
r = x;
else if (a.is_numeral(x, v))
r = a.mk_int(mod(v, N));
else if (is_bounded(x, N))
r = x;
else
r = a.mk_mod(x, a.mk_int(N));
return r;
}
rational solver::bv_size(expr* bv_expr) {
return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort()));
}
void solver::translate_expr(expr* e) {
if (is_quantifier(e))
translate_quantifier(to_quantifier(e));
else if (is_var(e))
translate_var(to_var(e));
else {
app* ap = to_app(e);
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
set_translated(e, e);
return;
}
m_args.reset();
for (auto arg : *ap)
m_args.push_back(translated(arg));
if (ap->get_family_id() == basic_family_id)
translate_basic(ap);
else if (ap->get_family_id() == bv.get_family_id())
translate_bv(ap);
else
translate_app(ap);
}
}
void solver::translate_quantifier(quantifier* q) {
if (m_is_plugin) {
set_translated(q, q);
return;
}
if (is_lambda(q))
throw default_exception("lambdas are not supported in intblaster");
expr* b = q->get_expr();
unsigned nd = q->get_num_decls();
ptr_vector<sort> sorts;
for (unsigned i = 0; i < nd; ++i) {
auto s = q->get_decl_sort(i);
if (bv.is_bv_sort(s)) {
NOT_IMPLEMENTED_YET();
sorts.push_back(a.mk_int());
}
else
sorts.push_back(s);
}
b = translated(b);
// TODO if sorts contain integer, then created bounds variables.
set_translated(q, m.update_quantifier(q, b));
}
void solver::translate_var(var* v) {
if (bv.is_bv_sort(v->get_sort()))
set_translated(v, m.mk_var(v->get_idx(), a.mk_int()));
else
set_translated(v, v);
}
// Translate functions that are not built-in or bit-vectors.
// Base method uses fresh functions.
// Other method could use bv2int, int2bv axioms and coercions.
// f(args) = bv2int(f(int2bv(args'))
//
void solver::translate_app(app* e) {
if (m_is_plugin && m.is_bool(e)) {
set_translated(e, e);
return;
}
bool has_bv_sort = bv.is_bv(e);
func_decl* f = e->get_decl();
for (unsigned i = 0; i < m_args.size(); ++i)
if (bv.is_bv(e->get_arg(i)))
m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i));
if (has_bv_sort)
m_vars.push_back(e);
if (m_is_plugin) {
expr* r = m.mk_app(f, m_args);
if (has_bv_sort) {
ctx.push(push_back_vector(m_vars));
r = bv.mk_bv2int(r);
}
set_translated(e, r);
return;
}
else if (has_bv_sort) {
if (f->get_family_id() != null_family_id)
throw default_exception("conversion for interpreted functions is not supported by intblast solver");
func_decl* g = nullptr;
if (!m_new_funs.find(f, g)) {
g = m.mk_fresh_func_decl(e->get_decl()->get_name(), symbol("bv"), f->get_arity(), f->get_domain(), a.mk_int());
m_new_funs.insert(f, g);
}
f = g;
m_pinned.push_back(f);
}
set_translated(e, m.mk_app(f, m_args));
}
void solver::translate_bv(app* e) {
auto bnot = [&](expr* e) {
return a.mk_sub(a.mk_int(-1), e);
};
auto band = [&](expr_ref_vector const& args) {
expr* r = arg(0);
for (unsigned i = 1; i < args.size(); ++i)
r = a.mk_band(bv.get_bv_size(e), r, arg(i));
return r;
};
auto rotate_left = [&](unsigned n) {
auto sz = bv.get_bv_size(e);
n = n % sz;
expr* r = arg(0);
if (n != 0 && sz != 1) {
// r[sz - n - 1 : 0] ++ r[sz - 1 : sz - n]
// r * 2^(sz - n) + (r div 2^n) mod 2^(sz - n)???
// r * A + (r div B) mod A
auto N = bv_size(e);
auto A = rational::power_of_two(sz - n);
auto B = rational::power_of_two(n);
auto hi = mul(r, a.mk_int(A));
auto lo = amod(e, a.mk_idiv(umod(e, 0), a.mk_int(B)), A);
r = add(hi, lo);
}
return r;
};
expr* bv_expr = e;
expr_ref r(m);
auto const& args = m_args;
switch (e->get_decl_kind()) {
case OP_BADD:
r = a.mk_add(args);
break;
case OP_BSUB:
r = a.mk_sub(args.size(), args.data());
break;
case OP_BMUL:
r = a.mk_mul(args);
break;
case OP_ULEQ:
bv_expr = e->get_arg(0);
r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_UGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_ULT:
bv_expr = e->get_arg(0);
r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_UGT:
bv_expr = e->get_arg(0);
r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_SLEQ:
bv_expr = e->get_arg(0);
r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SLT:
bv_expr = e->get_arg(0);
r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SGT:
bv_expr = e->get_arg(0);
r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_BNEG:
r = a.mk_uminus(arg(0));
break;
case OP_CONCAT: {
unsigned sz = 0;
expr_ref new_arg(m);
for (unsigned i = args.size(); i-- > 0;) {
expr* old_arg = e->get_arg(i);
new_arg = umod(old_arg, i);
if (sz > 0) {
new_arg = mul(new_arg, a.mk_int(rational::power_of_two(sz)));
r = add(r, new_arg);
}
else
r = new_arg;
sz += bv.get_bv_size(old_arg->get_sort());
}
break;
}
case OP_EXTRACT: {
unsigned lo, hi;
expr* old_arg;
VERIFY(bv.is_extract(e, lo, hi, old_arg));
r = arg(0);
if (lo > 0)
r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
break;
}
case OP_BV_NUM: {
rational val;
unsigned sz;
VERIFY(bv.is_numeral(e, val, sz));
r = a.mk_int(val);
break;
}
case OP_BUREM:
case OP_BUREM_I: {
expr* x = umod(e, 0), * y = umod(e, 1);
r = if_eq(y, 0, x, a.mk_mod(x, y));
break;
}
case OP_BUDIV:
case OP_BUDIV_I: {
expr* x = umod(e, 0), * y = umod(e, 1);
r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y));
break;
}
case OP_BUMUL_NO_OVFL: {
bv_expr = e->get_arg(0);
r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
break;
}
case OP_BSHL: {
if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
r = a.mk_shl(bv.get_bv_size(e), arg(0),arg(1));
else {
expr* x = arg(0), * y = umod(e, 1);
r = a.mk_int(0);
IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r);
}
break;
}
case OP_BNOT:
r = bnot(arg(0));
break;
case OP_BLSHR:
if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1));
else {
expr* x = arg(0), * y = umod(e, 1);
r = a.mk_int(0);
IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
}
break;
case OP_BASHR:
if (!a.is_numeral(arg(1)))
r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1));
else {
//
// ashr(x, y)
// if y = k & x >= 0 -> x / 2^k
// if y = k & x < 0 -> (x / 2^k) - 2^{N-k}
//
unsigned sz = bv.get_bv_size(e);
rational N = bv_size(e);
expr* x = umod(e, 0), *y = umod(e, 1);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0));
IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < sz; ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
r = if_eq(y, i,
m.mk_ite(signx, add(d, a.mk_int(- rational::power_of_two(sz-i))), d),
r);
}
}
break;
case OP_BOR:
// p | q := (p + q) - band(p, q)
IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
r = arg(0);
for (unsigned i = 1; i < args.size(); ++i)
r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
break;
case OP_BNAND:
r = bnot(band(args));
break;
case OP_BAND:
IF_VERBOSE(2, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
r = band(args);
break;
case OP_BXNOR:
case OP_BXOR: {
// p ^ q := (p + q) - 2*band(p, q);
unsigned sz = bv.get_bv_size(e);
IF_VERBOSE(2, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
r = arg(0);
for (unsigned i = 1; i < args.size(); ++i) {
expr* q = arg(i);
r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q)));
}
if (e->get_decl_kind() == OP_BXNOR)
r = bnot(r);
break;
}
case OP_ZERO_EXT:
bv_expr = e->get_arg(0);
r = umod(bv_expr, 0);
SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
break;
case OP_SIGN_EXT: {
bv_expr = e->get_arg(0);
r = umod(bv_expr, 0);
SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
unsigned arg_sz = bv.get_bv_size(bv_expr);
//unsigned sz = bv.get_bv_size(e);
// rational N = rational::power_of_two(sz);
rational M = rational::power_of_two(arg_sz);
expr* signbit = a.mk_ge(r, a.mk_int(M / 2));
r = m.mk_ite(signbit, a.mk_sub(r, a.mk_int(M)), r);
break;
}
case OP_INT2BV:
m_int2bv.push_back(e);
ctx.push(push_back_vector(m_int2bv));
r = arg(0);
break;
case OP_BV2INT:
m_bv2int.push_back(e);
ctx.push(push_back_vector(m_bv2int));
r = umod(e->get_arg(0), 0);
break;
case OP_BCOMP:
bv_expr = e->get_arg(0);
r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
break;
case OP_BSMOD_I:
case OP_BSMOD: {
expr* x = umod(e, 0), *y = umod(e, 1);
rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N/2));
expr* signy = a.mk_ge(y, a.mk_int(N/2));
expr* u = a.mk_mod(x, y);
// u = 0 -> 0
// y = 0 -> x
// x < 0, y < 0 -> -u
// x < 0, y >= 0 -> y - u
// x >= 0, y < 0 -> y + u
// x >= 0, y >= 0 -> u
r = a.mk_uminus(u);
r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
r = if_eq(u, 0, a.mk_int(0), r);
r = if_eq(y, 0, x, r);
break;
}
case OP_BSDIV_I:
case OP_BSDIV: {
// d = udiv(abs(x), abs(y))
// y = 0, x > 0 -> 1
// y = 0, x <= 0 -> -1
// x = 0, y != 0 -> 0
// x > 0, y < 0 -> -d
// x < 0, y > 0 -> -d
// x > 0, y > 0 -> d
// x < 0, y < 0 -> d
expr* x = umod(e, 0), * y = umod(e, 1);
rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2));
x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(x, y);
r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
break;
}
case OP_BSREM_I:
case OP_BSREM: {
// y = 0 -> x
// else x - sdiv(x, y) * y
expr* x = umod(e, 0), * y = umod(e, 1);
rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2));
expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(absx, absy);
d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = a.mk_sub(x, mul(d, y));
r = if_eq(y, 0, x, r);
break;
}
case OP_ROTATE_LEFT: {
auto n = e->get_parameter(0).get_int();
r = rotate_left(n);
break;
}
case OP_ROTATE_RIGHT: {
unsigned sz = bv.get_bv_size(e);
auto n = e->get_parameter(0).get_int();
r = rotate_left(sz - n);
break;
}
case OP_EXT_ROTATE_LEFT: {
unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1);
r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i)
r = if_eq(y, i, rotate_left(i), r);
break;
}
case OP_EXT_ROTATE_RIGHT: {
unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1);
r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i)
r = if_eq(y, i, rotate_left(sz - i), r);
break;
}
case OP_REPEAT: {
unsigned n = e->get_parameter(0).get_int();
expr* x = umod(e->get_arg(0), 0);
r = x;
rational N = bv_size(e->get_arg(0));
rational N0 = N;
for (unsigned i = 1; i < n; ++i)
r = add(mul(a.mk_int(N), x), r), N *= N0;
break;
}
case OP_BREDOR: {
r = umod(e->get_arg(0), 0);
r = m.mk_not(m.mk_eq(r, a.mk_int(0)));
break;
}
case OP_BREDAND: {
rational N = bv_size(e->get_arg(0));
r = umod(e->get_arg(0), 0);
r = m.mk_not(m.mk_eq(r, a.mk_int(N - 1)));
break;
}
default:
verbose_stream() << mk_pp(e, m) << "\n";
NOT_IMPLEMENTED_YET();
}
set_translated(e, r);
}
expr_ref solver::if_eq(expr* n, unsigned k, expr* th, expr* el) {
rational r;
expr_ref _th(th, m), _el(el, m);
if (bv.is_numeral(n, r)) {
if (r == k)
return expr_ref(th, m);
else
return expr_ref(el, m);
}
return expr_ref(m.mk_ite(m.mk_eq(n, a.mk_int(k)), th, el), m);
}
void solver::translate_basic(app* e) {
if (m.is_eq(e)) {
bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
if (has_bv_arg) {
expr* bv_expr = e->get_arg(0);
rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
if (a.is_numeral(arg(0)) || a.is_numeral(arg(1)) ||
is_bounded(arg(0), N) || is_bounded(arg(1), N)) {
set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)));
}
else {
m_args[0] = a.mk_sub(arg(0), arg(1));
set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0)));
}
}
else
set_translated(e, m.mk_eq(arg(0), arg(1)));
}
else if (m.is_ite(e))
set_translated(e, m.mk_ite(arg(0), arg(1), arg(2)));
else if (m_is_plugin)
set_translated(e, e);
else
set_translated(e, m.mk_app(e->get_decl(), m_args));
}
rational solver::get_value(expr* e) const {
SASSERT(bv.is_bv(e));
model_ref mdl;
m_solver->get_model(mdl);
expr_ref r(m);
r = translated(e);
r = m_translator.translated(e);
rational val;
if (!mdl->eval_expr(r, r, true))
return rational::zero();
@ -1099,7 +465,7 @@ namespace intblast {
}
rational r, N = rational::power_of_two(bv.get_bv_size(e));
expr* te = translated(e);
expr* te = m_translator.translated(e);
model_ref mdlr;
m_solver->get_model(mdlr);
expr_ref value(m);
@ -1143,11 +509,11 @@ namespace intblast {
return;
for (auto n : ctx.get_egraph().nodes()) {
auto e = n->get_expr();
if (!is_translated(e))
if (!m_translator.is_translated(e))
continue;
if (!bv.is_bv(e))
continue;
auto t = translated(e);
auto t = m_translator.translated(e);
expr_ref ei(bv.mk_bv2int(e), m);
expr_ref ti(a.mk_mod(t, a.mk_int(rational::power_of_two(bv.get_bv_size(e)))), m);

52
src/sat/smt/intblast_solver.h
View file

@ -38,6 +38,7 @@ Author:
#include "solver/solver.h"
#include "sat/smt/sat_th.h"
#include "util/statistics.h"
#include "ast/rewriter/bv2int_translator.h"
namespace euf {
class solver;
@ -45,18 +46,31 @@ namespace euf {
namespace intblast {
class translator_trail : public bv2int_translator_trail {
euf::solver& ctx;
public:
translator_trail(euf::solver& ctx):ctx(ctx) {}
void push(push_back_vector<expr_ref_vector> const& c) override;
void push(push_back_vector<ptr_vector<app>> const& c) override;
void push_idx(set_vector_idx_trail<expr_ref_vector> const& c) override;
};
class solver : public euf::th_euf_solver {
euf::solver& ctx;
sat::solver& s;
ast_manager& m;
bv_util bv;
arith_util a;
translator_trail trail;
bv2int_translator m_translator;
scoped_ptr<::solver> m_solver;
obj_map<func_decl, func_decl*> m_new_funs;
expr_ref_vector m_translate, m_args;
ast_ref_vector m_pinned;
//obj_map<func_decl, func_decl*> m_new_funs;
//expr_ref_vector m_translate, m_args;
//ast_ref_vector m_pinned;
sat::literal_vector m_core;
ptr_vector<app> m_bv2int, m_int2bv;
// ptr_vector<app> m_bv2int, m_int2bv;
statistics m_stats;
bool m_is_plugin = true; // when the solver is used as a plugin, then do not translate below quantifiers.
@ -66,33 +80,6 @@ namespace intblast {
bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); }
expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
void set_translated(expr* e, expr* r);
expr* arg(unsigned i) { return m_args.get(i); }
expr* umod(expr* bv_expr, unsigned i);
expr* smod(expr* bv_expr, unsigned i);
bool is_bounded(expr* v, rational const& N);
bool is_non_negative(expr* bv_expr, expr* e);
expr_ref mul(expr* x, expr* y);
expr_ref add(expr* x, expr* y);
expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el);
expr* amod(expr* bv_expr, expr* x, rational const& N);
rational bv_size(expr* bv_expr);
void translate_expr(expr* e);
void translate_bv(app* e);
void translate_basic(app* e);
void translate_app(app* e);
void translate_quantifier(quantifier* q);
void translate_var(var* v);
void ensure_translated(expr* e);
void internalize_bv(app* e);
unsigned m_vars_qhead = 0, m_preds_qhead = 0;
ptr_vector<expr> m_vars, m_preds;
bool add_bound_axioms();
bool add_predicate_axioms();
@ -101,6 +88,9 @@ namespace intblast {
void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
unsigned m_vars_qhead = 0, m_preds_qhead = 0;
public:
solver(euf::solver& ctx);

1
src/smt/CMakeLists.txt
View file

@ -61,6 +61,7 @@ z3_add_component(smt
theory_dl.cpp
theory_dummy.cpp
theory_fpa.cpp
theory_intblast.cpp
theory_lra.cpp
theory_opt.cpp
theory_pb.cpp

14
src/smt/smt_setup.cpp
View file

@ -27,6 +27,7 @@ Revision History:
#include "smt/theory_array.h"
#include "smt/theory_array_full.h"
#include "smt/theory_bv.h"
#include "smt/theory_intblast.h"
#include "smt/theory_datatype.h"
#include "smt/theory_recfun.h"
#include "smt/theory_dummy.h"
@ -473,12 +474,12 @@ namespace smt {
void setup::setup_QF_BV() {
TRACE("setup", tout << "qf-bv\n";);
m_params.setup_QF_BV();
m_context.register_plugin(alloc(smt::theory_bv, m_context));
setup_bv();
}
void setup::setup_QF_AUFBV() {
m_params.setup_QF_AUFBV();
m_context.register_plugin(alloc(smt::theory_bv, m_context));
setup_bv();
setup_arrays();
}
@ -695,7 +696,14 @@ namespace smt {
family_id bv_fid = m_manager.mk_family_id("bv");
if (m_context.get_theory(bv_fid))
return;
switch(m_params.m_bv_mode) {
switch (m_params.m_bv_solver) {
case 2:
m_context.register_plugin(alloc(smt::theory_intblast, m_context));
return;
default:
break;
}
switch (m_params.m_bv_mode) {
case BS_NO_BV:
m_context.register_plugin(alloc(smt::theory_dummy, m_context, bv_fid, "no bit-vector"));
break;

148
src/smt/theory_intblast.cpp Normal file
View file

@ -0,0 +1,148 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
theory_intblast
Author:
Nikolaj Bjorner (nbjorner) 2024-10-27
--*/
#include "smt/smt_context.h"
#include "smt/theory_intblast.h"
namespace smt {
void theory_intblast::translator_trail::push(push_back_vector<expr_ref_vector> const& c) {
ctx.push_trail(c);
}
void theory_intblast::translator_trail::push(push_back_vector<ptr_vector<app>> const& c) {
ctx.push_trail(c);
}
void theory_intblast::translator_trail::push_idx(set_vector_idx_trail<expr_ref_vector> const& c) {
ctx.push_trail(c);
}
theory_intblast::theory_intblast(context& ctx):
theory(ctx, ctx.get_manager().mk_family_id("bv")),
m_trail(ctx),
m_translator(m, m_trail),
bv(m),
a(m)
{}
theory_intblast::~theory_intblast() {}
void theory_intblast::init() {
}
final_check_status theory_intblast::final_check_eh() {
for (auto e : m_translator.bv2int()) {
auto* n = ctx.get_enode(e);
auto* r1 = n->get_arg(0)->get_root();
for (auto sib : *n) {
if (sib == n)
continue;
if (!bv.is_bv2int(sib->get_expr()))
continue;
if (sib->get_arg(0)->get_root() == r1)
continue;
if (bv.get_bv_size(r1->get_expr()) != bv.get_bv_size(sib->get_arg(0)->get_expr()))
continue;
auto a = mk_eq(n->get_expr(), sib->get_expr(), false);
auto b = mk_eq(sib->get_arg(0)->get_expr(), n->get_arg(0)->get_expr(), false);
ctx.mark_as_relevant(a);
ctx.mark_as_relevant(b);
ctx.mk_clause(~a, b, nullptr);
return final_check_status::FC_CONTINUE;
}
}
// ensure that int2bv respects values
// bv2int(int2bv(x)) = x mod N
for (auto e : m_translator.int2bv()) {
auto n = ctx.get_enode(e);
auto x = n->get_arg(0)->get_expr();
auto bv2int = bv.mk_bv2int(e);
ctx.internalize(bv2int, false);
auto N = rational::power_of_two(bv.get_bv_size(e));
auto xModN = a.mk_mod(x, a.mk_int(N));
ctx.internalize(xModN, false);
auto nBv2int = ctx.get_enode(bv2int);
auto nxModN = ctx.get_enode(xModN);
if (nBv2int->get_root() != nxModN->get_root()) {
auto a = mk_eq(nBv2int->get_expr(), nxModN->get_expr(), false);
ctx.mark_as_relevant(a);
ctx.mk_clause(1, &a, nullptr);
return final_check_status::FC_CONTINUE;
}
}
return final_check_status::FC_DONE;
}
bool theory_intblast::add_bound_axioms() {
auto const& vars = m_translator.vars();
if (m_vars_qhead == vars.size())
return false;
ctx.push_trail(value_trail(m_vars_qhead));
for (; m_vars_qhead < vars.size(); ++m_vars_qhead) {
auto v = vars[m_vars_qhead];
auto w = m_translator.translated(v);
auto sz = rational::power_of_two(bv.get_bv_size(v->get_sort()));
auto lo = mk_literal(a.mk_ge(w, a.mk_int(0)));
auto hi = mk_literal(a.mk_le(w, a.mk_int(sz - 1)));
ctx.mark_as_relevant(lo);
ctx.mark_as_relevant(hi);
ctx.mk_clause(1, &lo, nullptr);
ctx.mk_clause(1, &hi, nullptr);
}
return true;
}
bool theory_intblast::add_predicate_axioms() {
auto const& preds = m_translator.preds();
if (m_preds_qhead == preds.size())
return false;
ctx.push_trail(value_trail(m_preds_qhead));
for (; m_preds_qhead < preds.size(); ++m_preds_qhead) {
expr* e = preds[m_preds_qhead];
expr_ref r(m_translator.translated(e), m);
ctx.get_rewriter()(r);
auto a = mk_literal(e);
auto b = mk_literal(r);
ctx.mark_as_relevant(b);
// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
ctx.mk_clause(~a, b, nullptr);
ctx.mk_clause(a, ~b, nullptr);
}
return true;
}
bool theory_intblast::can_propagate() {
return m_preds_qhead < m_translator.preds().size() || m_vars_qhead < m_translator.vars().size();
}
void theory_intblast::propagate() {
add_bound_axioms();
add_predicate_axioms();
}
bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) {
return internalize_term(atom);
}
bool theory_intblast::internalize_term(app* term) {
m_translator.internalize_bv(term);
return true;
}
void theory_intblast::internalize_eq_eh(app * atom, bool_var v) {
m_translator.translate_eq(atom);
}
}

69
src/smt/theory_intblast.h Normal file
View file

@ -0,0 +1,69 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
theory_intblast
Abstract:
Intblast version of bit-vector solver
Author:
Nikolaj Bjorner (nbjorner) 2024-10-24
--*/
#pragma once
#include "util/rlimit.h"
#include "ast/sls/sat_ddfw.h"
#include "smt/smt_theory.h"
#include "model/model.h"
#include "ast/rewriter/bv2int_translator.h"
namespace smt {
class theory_intblast : public theory {
class translator_trail : public bv2int_translator_trail {
context& ctx;
public:
translator_trail(context& ctx):ctx(ctx) {}
void push(push_back_vector<expr_ref_vector> const& c) override;
void push(push_back_vector<ptr_vector<app>> const& c) override;
void push_idx(set_vector_idx_trail<expr_ref_vector> const& c) override;
};
translator_trail m_trail;
bv2int_translator m_translator;
bv_util bv;
arith_util a;
unsigned m_vars_qhead = 0, m_preds_qhead = 0;
bool add_bound_axioms();
bool add_predicate_axioms();
public:
theory_intblast(context& ctx);
~theory_intblast() override;
char const* get_name() const override { return "bv-intblast"; }
void init() override;
smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_intblast, *new_ctx); }
final_check_status final_check_eh() override;
void display(std::ostream& out) const override {}
bool can_propagate() override;
void propagate() override;
bool internalize_atom(app * atom, bool gate_ctx) override;
bool internalize_term(app* term) override;
void internalize_eq_eh(app * atom, bool_var v) override;
void new_eq_eh(theory_var v1, theory_var v2) override {}
void new_diseq_eh(theory_var v1, theory_var v2) override {}
};
}

2
src/smt/theory_lra.cpp
View file

@ -3276,6 +3276,8 @@ public:
for (literal & c : m_core) {
c.neg();
ctx().mark_as_relevant(c);
if (ctx().get_assignment(c) == l_true)
return;
}
TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.data());