mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fixes

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-12 14:53:10 -08:00
parent 7247bbb78f
commit 9b435eda90
1 changed files with 14 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -28,8 +28,8 @@ namespace intblast {
m(ctx.get_manager()), m(ctx.get_manager()),
bv(m), bv(m),
a(m), a(m),
m_args(m), m_translate(m),
m_translate(m) m_args(m)
{} {}
euf::theory_var solver::mk_var(euf::enode* n) { euf::theory_var solver::mk_var(euf::enode* n) {
@ -100,6 +100,8 @@ namespace intblast {
for (auto arg : *e) for (auto arg : *e)
m_args.push_back(translated(arg)); m_args.push_back(translated(arg));
translate_bv(e); translate_bv(e);
// possibly wait until propagation?
if (m.is_bool(e)) if (m.is_bool(e))
add_equiv(expr2literal(e), mk_literal(translated(e))); add_equiv(expr2literal(e), mk_literal(translated(e)));
add_bound_axioms(); add_bound_axioms();
@ -468,6 +470,8 @@ namespace intblast {
return; return;
} }
else if (has_bv_sort) { 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; func_decl* g = nullptr;
if (!m_new_funs.find(f, g)) { 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()); g = m.mk_fresh_func_decl(e->get_decl()->get_name(), symbol("bv"), f->get_arity(), f->get_domain(), a.mk_int());
@ -558,7 +562,6 @@ namespace intblast {
unsigned lo, hi; unsigned lo, hi;
expr* old_arg; expr* old_arg;
VERIFY(bv.is_extract(e, lo, hi, old_arg)); VERIFY(bv.is_extract(e, lo, hi, old_arg));
unsigned sz = hi - lo + 1;
expr* r = arg(0); expr* r = arg(0);
if (lo > 0) if (lo > 0)
r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo))); r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
@ -611,10 +614,10 @@ namespace intblast {
break; break;
} }
case OP_BNAND: case OP_BNAND:
r = (bnot(band(args))); r = bnot(band(args));
break; break;
case OP_BAND: case OP_BAND:
r = (band(args)); r = band(args);
break; break;
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations; // From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24 // found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
@ -635,18 +638,18 @@ namespace intblast {
bv_rewriter_params p(ctx.s().params()); bv_rewriter_params p(ctx.s().params());
expr* x = arg(0), * y = arg(1); expr* x = arg(0), * y = arg(1);
if (p.hi_div0()) if (p.hi_div0())
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_idiv(x, y)); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_idiv(x, umod(e, 1)));
else else
r = a.mk_idiv(x, y); r = a.mk_idiv(x, umod(e, 1));
break; break;
} }
case OP_BUREM: { case OP_BUREM: {
bv_rewriter_params p(ctx.s().params()); bv_rewriter_params p(ctx.s().params());
expr* x = arg(0), * y = arg(1); expr* x = arg(0), * y = arg(1);
if (p.hi_div0()) if (p.hi_div0())
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_mod(x, y)); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_mod(x, umod(e, 1)));
else else
r = a.mk_mod(x, y); r = a.mk_mod(x, umod(e, 1));
break; break;
} }
@ -694,7 +697,7 @@ namespace intblast {
case OP_BV2INT: case OP_BV2INT:
m_bv2int.push_back(e); m_bv2int.push_back(e);
ctx.push(push_back_vector(m_bv2int)); ctx.push(push_back_vector(m_bv2int));
r = arg(0); r = umod(e->get_arg(0), 0);
break; break;
case OP_BCOMP: case OP_BCOMP:
case OP_ROTATE_LEFT: case OP_ROTATE_LEFT:
@ -758,6 +761,7 @@ namespace intblast {
if (!e) if (!e)
return false; return false;
dep.add(n, e); dep.add(n, e);
return true;
} }
// TODO: handle dependencies properly by using arithmetical model to retrieve values of translated // TODO: handle dependencies properly by using arithmetical model to retrieve values of translated