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

add eval field to sls-valuation to track temporary values.

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-02-26 14:54:15 -08:00
parent 8f139e862c
commit d774f07eb3
9 changed files with 339 additions and 336 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/ast/sls/bv_sls.cpp
View file

@ -52,9 +52,6 @@ namespace bv {
m_repair_roots.insert(e->get_id()); m_repair_roots.insert(e->get_id());
} }
} }
for (app* t : m_terms.terms())
if (t && !eval_is_correct(t))
m_repair_roots.insert(t->get_id());
} }
void sls::reinit_eval() { void sls::reinit_eval() {
@ -67,7 +64,7 @@ namespace bv {
return m_eval.bval0(e); return m_eval.bval0(e);
} }
else if (bv.is_bv(e)) { else if (bv.is_bv(e)) {
auto& w = m_eval.wval0(e); auto& w = m_eval.wval(e);
if (w.fixed.get(i) || should_keep()) if (w.fixed.get(i) || should_keep())
return w.get_bit(i); return w.get_bit(i);
} }
@ -142,17 +139,21 @@ namespace bv {
void sls::try_repair_down(app* e) { void sls::try_repair_down(app* e) {
unsigned n = e->get_num_args(); unsigned n = e->get_num_args();
if (n > 0) { if (n == 0) {
unsigned s = m_rand(n); m_eval.wval(e).commit_eval();
for (unsigned i = 0; i < n; ++i) { m_repair_up.insert(e->get_id());
auto j = (i + s) % n; }
if (m_eval.try_repair(e, j)) {
set_repair_down(e->get_arg(j)); unsigned s = m_rand(n);
return; for (unsigned i = 0; i < n; ++i) {
} auto j = (i + s) % n;
if (m_eval.try_repair(e, j)) {
set_repair_down(e->get_arg(j));
return;
} }
} }
m_repair_up.insert(e->get_id());
// search a new root / random walk to repair
} }
void sls::try_repair_up(app* e) { void sls::try_repair_up(app* e) {
@ -174,8 +175,10 @@ namespace bv {
return false; return false;
if (m.is_bool(e)) if (m.is_bool(e))
return m_eval.bval0(e) == m_eval.bval1(e); return m_eval.bval0(e) == m_eval.bval1(e);
if (bv.is_bv(e)) if (bv.is_bv(e)) {
return m_eval.wval0(e).eq(m_eval.wval1(e)); auto const& v = m_eval.wval(e);
return v.eval == v.bits();
}
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
@ -187,9 +190,8 @@ namespace bv {
if (!eval_is_correct(to_app(e))) { if (!eval_is_correct(to_app(e))) {
verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
if (bv.is_bv(e)) { if (bv.is_bv(e)) {
auto const& v0 = m_eval.wval0(e); auto const& v = m_eval.wval(e);
auto const& v1 = m_eval.wval1(to_app(e)); verbose_stream() << v << "\n" << v.eval << "\n";
verbose_stream() << v0 << "\n" << v1 << "\n";
} }
} }
if (!is_uninterp_const(e)) if (!is_uninterp_const(e))
@ -199,7 +201,7 @@ namespace bv {
if (m.is_bool(e)) if (m.is_bool(e))
mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e))); mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e)));
else if (bv.is_bv(e)) { else if (bv.is_bv(e)) {
auto const& v = m_eval.wval0(e); auto const& v = m_eval.wval(e);
rational n = v.get_value(); rational n = v.get_value();
mdl->register_decl(f, bv.mk_numeral(n, v.bw)); mdl->register_decl(f, bv.mk_numeral(n, v.bw));
} }
@ -219,7 +221,7 @@ namespace bv {
if (m_repair_roots.contains(e->get_id())) if (m_repair_roots.contains(e->get_id()))
out << "r "; out << "r ";
if (bv.is_bv(e)) if (bv.is_bv(e))
out << m_eval.wval0(e); out << m_eval.wval(e);
else if (m.is_bool(e)) else if (m.is_bool(e))
out << (m_eval.bval0(e)?"T":"F"); out << (m_eval.bval0(e)?"T":"F");
out << "\n"; out << "\n";
@ -239,7 +241,7 @@ namespace bv {
verbose_stream() << (down ? "d #" : "u #") verbose_stream() << (down ? "d #" : "u #")
<< e->get_id() << ": " << e->get_id() << ": "
<< mk_bounded_pp(e, m, 1) << " "; << mk_bounded_pp(e, m, 1) << " ";
if (bv.is_bv(e)) verbose_stream() << m_eval.wval0(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " "); if (bv.is_bv(e)) verbose_stream() << m_eval.wval(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " ");
if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " "; if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " ";
verbose_stream() << "\n"); verbose_stream() << "\n");
} }

2
src/ast/sls/bv_sls.h
View file

@ -99,7 +99,7 @@ namespace bv {
/** /**
* Retrieve valuation * Retrieve valuation
*/ */
sls_valuation const& wval(expr* e) const { return m_eval.wval0(e); } sls_valuation const& wval(expr* e) const { return m_eval.wval(e); }
model_ref get_model(); model_ref get_model();

413
src/ast/sls/bv_sls_eval.cpp
View file

@ -37,7 +37,7 @@ namespace bv {
init_eval_bv(a); init_eval_bv(a);
else if (is_uninterp(e)) { else if (is_uninterp(e)) {
if (bv.is_bv(e)) { if (bv.is_bv(e)) {
auto& v = wval0(e); auto& v = wval(e);
for (unsigned i = 0; i < v.bw; ++i) for (unsigned i = 0; i < v.bw; ++i)
m_tmp.set(i, eval(e, i)); m_tmp.set(i, eval(e, i));
v.set(m_tmp); v.set(m_tmp);
@ -80,12 +80,10 @@ namespace bv {
bool sls_eval::add_bit_vector(expr* e) { bool sls_eval::add_bit_vector(expr* e) {
auto bw = bv.get_bv_size(e); auto bw = bv.get_bv_size(e);
m_values0.reserve(e->get_id() + 1); m_values.reserve(e->get_id() + 1);
if (m_values0.get(e->get_id())) if (m_values.get(e->get_id()))
return false; return false;
m_values1.reserve(e->get_id() + 1); m_values.set(e->get_id(), alloc_valuation(bw));
m_values0.set(e->get_id(), alloc_valuation(bw));
m_values1.set(e->get_id(), alloc(sls_pre_valuation, bw));
return true; return true;
} }
@ -115,9 +113,9 @@ namespace bv {
m_eval.setx(id, bval1(e), false); m_eval.setx(id, bval1(e), false);
else if (m.is_ite(e)) { else if (m.is_ite(e)) {
SASSERT(bv.is_bv(e->get_arg(1))); SASSERT(bv.is_bv(e->get_arg(1)));
auto& val = wval0(e); auto& val = wval(e);
auto& val_th = wval0(e->get_arg(1)); auto& val_th = wval(e->get_arg(1));
auto& val_el = wval0(e->get_arg(2)); auto& val_el = wval(e->get_arg(2));
if (bval0(e->get_arg(0))) if (bval0(e->get_arg(0)))
val.set(val_th.bits()); val.set(val_th.bits());
else else
@ -129,10 +127,8 @@ namespace bv {
} }
void sls_eval::init_eval_bv(app* e) { void sls_eval::init_eval_bv(app* e) {
if (bv.is_bv(e)) { if (bv.is_bv(e))
auto& v = wval0(e); eval(e).commit_eval();
v.set(wval1(e).bits());
}
else if (m.is_bool(e)) else if (m.is_bool(e))
m_eval.setx(e->get_id(), bval1_bv(e), false); m_eval.setx(e->get_id(), bval1_bv(e), false);
} }
@ -174,8 +170,8 @@ namespace bv {
if (m.is_bool(a)) if (m.is_bool(a))
return bval0(a) == bval0(b); return bval0(a) == bval0(b);
else if (bv.is_bv(a)) { else if (bv.is_bv(a)) {
auto const& va = wval0(a); auto const& va = wval(a);
auto const& vb = wval0(b); auto const& vb = wval(b);
return va.eq(vb); return va.eq(vb);
} }
return m.are_equal(a, b); return m.are_equal(a, b);
@ -221,15 +217,15 @@ namespace bv {
SASSERT(e->get_family_id() == bv.get_fid()); SASSERT(e->get_family_id() == bv.get_fid());
auto ucompare = [&](std::function<bool(int)> const& f) { auto ucompare = [&](std::function<bool(int)> const& f) {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
return f(mpn.compare(a.bits().data(), a.nw, b.bits().data(), b.nw)); 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} // x <s y <=> x + 2^{bw-1} <u y + 2^{bw-1}
auto scompare = [&](std::function<bool(int)> const& f) { auto scompare = [&](std::function<bool(int)> const& f) {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
add_p2_1(a, m_tmp); add_p2_1(a, m_tmp);
add_p2_1(b, m_tmp2); add_p2_1(b, m_tmp2);
return f(mpn.compare(m_tmp.data(), a.nw, m_tmp2.data(), b.nw)); return f(mpn.compare(m_tmp.data(), a.nw, m_tmp2.data(), b.nw));
@ -237,8 +233,8 @@ namespace bv {
auto umul_overflow = [&]() { auto umul_overflow = [&]() {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
return a.set_mul(m_tmp2, a.bits(), b.bits()); return a.set_mul(m_tmp2, a.bits(), b.bits());
}; };
@ -263,7 +259,7 @@ namespace bv {
expr* child; expr* child;
unsigned idx; unsigned idx;
VERIFY(bv.is_bit2bool(e, child, idx)); VERIFY(bv.is_bit2bool(e, child, idx));
auto& a = wval0(child); auto& a = wval(child);
return a.get_bit(idx); return a.get_bit(idx);
} }
case OP_BUMUL_NO_OVFL: case OP_BUMUL_NO_OVFL:
@ -272,8 +268,8 @@ namespace bv {
return umul_overflow(); return umul_overflow();
case OP_BUADD_OVFL: { case OP_BUADD_OVFL: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
return a.set_add(m_tmp, a.bits(), b.bits()); return a.set_add(m_tmp, a.bits(), b.bits());
} }
case OP_BNEG_OVFL: case OP_BNEG_OVFL:
@ -300,18 +296,18 @@ namespace bv {
return bval0(e); return bval0(e);
} }
sls_valuation& sls_eval::wval1(app* e) const { sls_valuation& sls_eval::eval(app* e) const {
auto& val = *m_values1[e->get_id()]; auto& val = *m_values[e->get_id()];
wval1(e, val); eval(e, val);
return val; return val;
} }
void sls_eval::wval1(app* e, sls_pre_valuation& val) const { void sls_eval::eval(app* e, sls_valuation& val) const {
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
if (m.is_ite(e)) { if (m.is_ite(e)) {
SASSERT(bv.is_bv(e->get_arg(1))); SASSERT(bv.is_bv(e->get_arg(1)));
auto& val_th = wval0(e->get_arg(1)); auto& val_th = wval(e->get_arg(1));
auto& val_el = wval0(e->get_arg(2)); auto& val_el = wval(e->get_arg(2));
if (bval0(e->get_arg(0))) if (bval0(e->get_arg(0)))
val.set(val_th.bits()); val.set(val_th.bits());
else else
@ -319,7 +315,7 @@ namespace bv {
return; return;
} }
if (e->get_family_id() == null_family_id) { if (e->get_family_id() == null_family_id) {
val.set(wval0(e).bits()); val.set(wval(e).bits());
return; return;
} }
auto set_sdiv = [&]() { auto set_sdiv = [&]() {
@ -331,8 +327,8 @@ namespace bv {
// x < 0, y > 0 -> -d // x < 0, y > 0 -> -d
// x > 0, y > 0 -> d // x > 0, y > 0 -> d
// x < 0, y < 0 -> d // x < 0, y < 0 -> d
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
bool sign_a = a.sign(); bool sign_a = a.sign();
bool sign_b = b.sign(); bool sign_b = b.sign();
if (b.is_zero()) { if (b.is_zero()) {
@ -358,13 +354,13 @@ namespace bv {
if (sign_a == sign_b) if (sign_a == sign_b)
val.set(m_tmp3); val.set(m_tmp3);
else else
val.set_sub(val.bits(), m_zero, m_tmp3); val.set_sub(val.eval, m_zero, m_tmp3);
} }
}; };
auto mk_rotate_left = [&](unsigned n) { auto mk_rotate_left = [&](unsigned n) {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
VERIFY(try_repair_rotate_left(a, val, a.bw - n)); VERIFY(try_repair_rotate_left(a.bits(), val, a.bw - n));
}; };
SASSERT(e->get_family_id() == bv.get_fid()); SASSERT(e->get_family_id() == bv.get_fid());
@ -378,98 +374,98 @@ namespace bv {
} }
case OP_BAND: { case OP_BAND: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
val.bits()[i] = a.bits()[i] & b.bits()[i]; val.eval[i] = a.bits()[i] & b.bits()[i];
break; break;
} }
case OP_BOR: { case OP_BOR: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
val.bits()[i] = a.bits()[i] | b.bits()[i]; val.eval[i] = a.bits()[i] | b.bits()[i];
break; break;
} }
case OP_BXOR: { case OP_BXOR: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
val.bits()[i] = a.bits()[i] ^ b.bits()[i]; val.eval[i] = a.bits()[i] ^ b.bits()[i];
break; break;
} }
case OP_BNAND: { case OP_BNAND: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
val.bits()[i] = ~(a.bits()[i] & b.bits()[i]); val.eval[i] = ~(a.bits()[i] & b.bits()[i]);
break; break;
} }
case OP_BADD: { case OP_BADD: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
val.set_add(val.bits(), a.bits(), b.bits()); val.set_add(val.eval, a.bits(), b.bits());
break; break;
} }
case OP_BSUB: { case OP_BSUB: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
val.set_sub(val.bits(), a.bits(), b.bits()); val.set_sub(val.eval, a.bits(), b.bits());
break; break;
} }
case OP_BMUL: { case OP_BMUL: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
val.set_mul(m_tmp2, a.bits(), b.bits()); val.set_mul(m_tmp2, a.bits(), b.bits());
val.set(m_tmp2); val.set(m_tmp2);
break; break;
} }
case OP_CONCAT: { case OP_CONCAT: {
SASSERT(e->get_num_args() == 2); SASSERT(e->get_num_args() == 2);
auto const& a = wval0(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval0(e->get_arg(1)); auto const& b = wval(e->get_arg(1));
for (unsigned i = 0; i < b.bw; ++i) for (unsigned i = 0; i < b.bw; ++i)
val.set_bit(i, b.get_bit(i)); val.eval.set(i, b.get_bit(i));
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
val.set_bit(i + b.bw, a.get_bit(i)); val.eval.set(i + b.bw, a.get_bit(i));
break; break;
} }
case OP_EXTRACT: { case OP_EXTRACT: {
expr* child; expr* child;
unsigned lo, hi; unsigned lo, hi;
VERIFY(bv.is_extract(e, lo, hi, child)); VERIFY(bv.is_extract(e, lo, hi, child));
auto const& a = wval0(child); auto const& a = wval(child);
SASSERT(lo <= hi && hi + 1 <= a.bw && hi - lo + 1 == val.bw); SASSERT(lo <= hi && hi + 1 <= a.bw && hi - lo + 1 == val.bw);
for (unsigned i = lo; i <= hi; ++i) for (unsigned i = lo; i <= hi; ++i)
val.set_bit(i - lo, a.get_bit(i)); val.eval.set(i - lo, a.get_bit(i));
break; break;
} }
case OP_BNOT: { case OP_BNOT: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
val.bits()[i] = ~a.bits()[i]; val.eval[i] = ~a.bits()[i];
break; break;
} }
case OP_BNEG: { case OP_BNEG: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
val.set_sub(val.bits(), m_zero, a.bits()); val.set_sub(val.eval, m_zero, a.bits());
break; break;
} }
case OP_BIT0: case OP_BIT0:
val.bits().set(0, false); val.eval.set(0, false);
break; break;
case OP_BIT1: case OP_BIT1:
val.bits().set(0, true); val.eval.set(0, true);
break; break;
case OP_BSHL: { case OP_BSHL: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
auto sh = b.to_nat(b.bw); auto sh = b.to_nat(b.bw);
if (sh == 0) if (sh == 0)
val.set(a.bits()); val.set(a.bits());
@ -477,13 +473,13 @@ namespace bv {
val.set_zero(); val.set_zero();
else { else {
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
val.bits().set(i, i >= sh && a.get_bit(i - sh)); val.eval.set(i, i >= sh && a.get_bit(i - sh));
} }
break; break;
} }
case OP_BLSHR: { case OP_BLSHR: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
auto sh = b.to_nat(b.bw); auto sh = b.to_nat(b.bw);
if (sh == 0) if (sh == 0)
val.set(a.bits()); val.set(a.bits());
@ -491,13 +487,13 @@ namespace bv {
val.set_zero(); val.set_zero();
else { else {
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
val.bits().set(i, i + sh < a.bw && a.get_bit(i + sh)); val.eval.set(i, i + sh < a.bw && a.get_bit(i + sh));
} }
break; break;
} }
case OP_BASHR: { case OP_BASHR: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
auto sh = b.to_nat(b.bw); auto sh = b.to_nat(b.bw);
auto sign = a.sign(); auto sign = a.sign();
if (sh == 0) if (sh == 0)
@ -519,7 +515,7 @@ namespace bv {
break; break;
} }
case OP_SIGN_EXT: { case OP_SIGN_EXT: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, a.get_bit(i)); m_tmp.set(i, a.get_bit(i));
bool sign = a.sign(); bool sign = a.sign();
@ -528,7 +524,7 @@ namespace bv {
break; break;
} }
case OP_ZERO_EXT: { case OP_ZERO_EXT: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, a.get_bit(i)); m_tmp.set(i, a.get_bit(i));
val.set_range(m_tmp, a.bw, val.bw, false); val.set_range(m_tmp, a.bw, val.bw, false);
@ -538,8 +534,8 @@ namespace bv {
case OP_BUREM: case OP_BUREM:
case OP_BUREM_I: case OP_BUREM_I:
case OP_BUREM0: { case OP_BUREM0: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
if (b.is_zero()) if (b.is_zero())
val.set(a.bits()); val.set(a.bits());
@ -559,8 +555,8 @@ namespace bv {
// x < 0, y >= 0 -> y - u // x < 0, y >= 0 -> y - u
// x >= 0, y < 0 -> y + u // x >= 0, y < 0 -> y + u
// x >= 0, y >= 0 -> u // x >= 0, y >= 0 -> u
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
if (b.is_zero()) if (b.is_zero())
val.set(a.bits()); val.set(a.bits());
else { else {
@ -576,11 +572,11 @@ namespace bv {
if (val.is_zero(m_tmp2)) if (val.is_zero(m_tmp2))
val.set(m_tmp2); val.set(m_tmp2);
else if (a.sign() && b.sign()) else if (a.sign() && b.sign())
val.set_sub(val.bits(), m_zero, m_tmp2); val.set_sub(val.eval, m_zero, m_tmp2);
else if (a.sign()) else if (a.sign())
val.set_sub(val.bits(), b.bits(), m_tmp2); val.set_sub(val.eval, b.bits(), m_tmp2);
else if (b.sign()) else if (b.sign())
val.set_add(val.bits(), b.bits(), m_tmp2); val.set_add(val.eval, b.bits(), m_tmp2);
else else
val.set(m_tmp2); val.set(m_tmp2);
} }
@ -590,8 +586,8 @@ namespace bv {
case OP_BUDIV_I: case OP_BUDIV_I:
case OP_BUDIV0: { case OP_BUDIV0: {
// x div 0 = -1 // x div 0 = -1
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
if (b.is_zero()) if (b.is_zero())
val.set(m_minus_one); val.set(m_minus_one);
else { else {
@ -613,14 +609,14 @@ namespace bv {
// b = 0 -> a // b = 0 -> a
// else a - sdiv(a, b) * b // else a - sdiv(a, b) * b
// //
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
if (b.is_zero()) if (b.is_zero())
val.set(a.bits()); val.set(a.bits());
else { else {
set_sdiv(); set_sdiv();
val.set_mul(m_tmp, val.bits(), b.bits()); val.set_mul(m_tmp, val.bits(), b.bits());
val.set_sub(val.bits(), a.bits(), m_tmp); val.set_sub(val.eval, a.bits(), m_tmp);
} }
break; break;
} }
@ -635,7 +631,7 @@ namespace bv {
break; break;
} }
case OP_EXT_ROTATE_LEFT: { case OP_EXT_ROTATE_LEFT: {
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
rational n = b.get_value(); rational n = b.get_value();
n = mod(n, rational(val.bw)); n = mod(n, rational(val.bw));
SASSERT(n.is_unsigned()); SASSERT(n.is_unsigned());
@ -643,7 +639,7 @@ namespace bv {
break; break;
} }
case OP_EXT_ROTATE_RIGHT: { case OP_EXT_ROTATE_RIGHT: {
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
rational n = b.get_value(); rational n = b.get_value();
n = mod(n, rational(val.bw)); n = mod(n, rational(val.bw));
SASSERT(n.is_unsigned()); SASSERT(n.is_unsigned());
@ -682,7 +678,7 @@ namespace bv {
UNREACHABLE(); UNREACHABLE();
break; break;
} }
val.clear_overflow_bits(val.bits()); val.clear_overflow_bits(val.eval);
} }
digit_t sls_eval::random_bits() { digit_t sls_eval::random_bits() {
@ -728,21 +724,21 @@ namespace bv {
bool sls_eval::try_repair_bv(app* e, unsigned i) { bool sls_eval::try_repair_bv(app* e, unsigned i) {
switch (e->get_decl_kind()) { switch (e->get_decl_kind()) {
case OP_BAND: case OP_BAND:
return try_repair_band(wval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_band(eval_value(e), wval(e, i), wval(e, 1 - i));
case OP_BOR: case OP_BOR:
return try_repair_bor(wval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_bor(eval_value(e), wval(e, i), wval(e, 1 - i));
case OP_BXOR: case OP_BXOR:
return try_repair_bxor(wval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_bxor(eval_value(e), wval(e, i), wval(e, 1 - i));
case OP_BADD: case OP_BADD:
return try_repair_add(wval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_add(eval_value(e), wval(e, i), wval(e, 1 - i));
case OP_BSUB: case OP_BSUB:
return try_repair_sub(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_sub(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_BMUL: case OP_BMUL:
return try_repair_mul(wval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_mul(eval_value(e), wval(e, i), wval(e, 1 - i));
case OP_BNOT: case OP_BNOT:
return try_repair_bnot(wval0(e), wval0(e, i)); return try_repair_bnot(eval_value(e), wval(e, i));
case OP_BNEG: case OP_BNEG:
return try_repair_bneg(wval0(e), wval0(e, i)); return try_repair_bneg(eval_value(e), wval(e, i));
case OP_BIT0: case OP_BIT0:
return false; return false;
case OP_BIT1: case OP_BIT1:
@ -753,89 +749,89 @@ namespace bv {
return false; return false;
case OP_ULEQ: case OP_ULEQ:
if (i == 0) if (i == 0)
return try_repair_ule(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_ule(bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_uge(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_uge(bval0(e), wval(e, i), wval(e, 1 - i));
case OP_UGEQ: case OP_UGEQ:
if (i == 0) if (i == 0)
return try_repair_uge(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_uge(bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_ule(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_ule(bval0(e), wval(e, i), wval(e, 1 - i));
case OP_UGT: case OP_UGT:
if (i == 0) if (i == 0)
return try_repair_ule(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_ule(!bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_uge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_uge(!bval0(e), wval(e, i), wval(e, 1 - i));
case OP_ULT: case OP_ULT:
if (i == 0) if (i == 0)
return try_repair_uge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_uge(!bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_ule(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_ule(!bval0(e), wval(e, i), wval(e, 1 - i));
case OP_SLEQ: case OP_SLEQ:
if (i == 0) if (i == 0)
return try_repair_sle(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sle(bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_sge(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sge(bval0(e), wval(e, i), wval(e, 1 - i));
case OP_SGEQ: case OP_SGEQ:
if (i == 0) if (i == 0)
return try_repair_sge(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sge(bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_sle(bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sle(bval0(e), wval(e, i), wval(e, 1 - i));
case OP_SGT: case OP_SGT:
if (i == 0) if (i == 0)
return try_repair_sle(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sle(!bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_sge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sge(!bval0(e), wval(e, i), wval(e, 1 - i));
case OP_SLT: case OP_SLT:
if (i == 0) if (i == 0)
return try_repair_sge(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sge(!bval0(e), wval(e, i), wval(e, 1 - i));
else else
return try_repair_sle(!bval0(e), wval0(e, i), wval0(e, 1 - i)); return try_repair_sle(!bval0(e), wval(e, i), wval(e, 1 - i));
case OP_BASHR: case OP_BASHR:
return try_repair_ashr(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_ashr(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_BLSHR: case OP_BLSHR:
return try_repair_lshr(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_lshr(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_BSHL: case OP_BSHL:
return try_repair_shl(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_shl(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_BIT2BOOL: { case OP_BIT2BOOL: {
unsigned idx; unsigned idx;
expr* arg; expr* arg;
VERIFY(bv.is_bit2bool(e, arg, idx)); VERIFY(bv.is_bit2bool(e, arg, idx));
return try_repair_bit2bool(wval0(e, 0), idx); return try_repair_bit2bool(wval(e, 0), idx);
} }
case OP_BUDIV: case OP_BUDIV:
case OP_BUDIV_I: case OP_BUDIV_I:
case OP_BUDIV0: case OP_BUDIV0:
return try_repair_udiv(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_udiv(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_BUREM: case OP_BUREM:
case OP_BUREM_I: case OP_BUREM_I:
case OP_BUREM0: case OP_BUREM0:
return try_repair_urem(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_urem(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_ROTATE_LEFT: case OP_ROTATE_LEFT:
return try_repair_rotate_left(wval0(e), wval0(e, 0), e->get_parameter(0).get_int()); return try_repair_rotate_left(eval_value(e), wval(e, 0), e->get_parameter(0).get_int());
case OP_ROTATE_RIGHT: case OP_ROTATE_RIGHT:
return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e).bw - e->get_parameter(0).get_int()); return try_repair_rotate_left(eval_value(e), wval(e, 0), wval(e).bw - e->get_parameter(0).get_int());
case OP_EXT_ROTATE_LEFT: case OP_EXT_ROTATE_LEFT:
return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_rotate_left(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_EXT_ROTATE_RIGHT: case OP_EXT_ROTATE_RIGHT:
return try_repair_rotate_right(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_rotate_right(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_ZERO_EXT: case OP_ZERO_EXT:
return try_repair_zero_ext(wval0(e), wval0(e, 0)); return try_repair_zero_ext(eval_value(e), wval(e, 0));
case OP_SIGN_EXT: case OP_SIGN_EXT:
return try_repair_sign_ext(wval0(e), wval0(e, 0)); return try_repair_sign_ext(eval_value(e), wval(e, 0));
case OP_CONCAT: case OP_CONCAT:
return try_repair_concat(wval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_concat(eval_value(e), wval(e, 0), wval(e, 1), i);
case OP_EXTRACT: { case OP_EXTRACT: {
unsigned hi, lo; unsigned hi, lo;
expr* arg; expr* arg;
VERIFY(bv.is_extract(e, lo, hi, arg)); VERIFY(bv.is_extract(e, lo, hi, arg));
return try_repair_extract(wval0(e), wval0(arg), lo); return try_repair_extract(eval_value(e), wval(arg), lo);
} }
case OP_BUMUL_NO_OVFL: case OP_BUMUL_NO_OVFL:
return try_repair_umul_ovfl(!bval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_umul_ovfl(!bval0(e), wval(e, 0), wval(e, 1), i);
case OP_BUMUL_OVFL: case OP_BUMUL_OVFL:
return try_repair_umul_ovfl(bval0(e), wval0(e, 0), wval0(e, 1), i); return try_repair_umul_ovfl(bval0(e), wval(e, 0), wval(e, 1), i);
case OP_BUADD_OVFL: case OP_BUADD_OVFL:
case OP_BCOMP: case OP_BCOMP:
case OP_BNAND: case OP_BNAND:
@ -891,8 +887,8 @@ namespace bv {
return true; return true;
} }
else if (bv.is_bv(child)) { else if (bv.is_bv(child)) {
auto & a = wval0(e->get_arg(i)); auto & a = wval(e->get_arg(i));
auto & b = wval0(e->get_arg(1 - i)); auto & b = wval(e->get_arg(1 - i));
if (is_true) if (is_true)
return a.try_set(b.bits()); return a.try_set(b.bits());
else { else {
@ -938,7 +934,7 @@ namespace bv {
return true; return true;
} }
if (bv.is_bv(e)) if (bv.is_bv(e))
return wval0(child).try_set(wval0(e).bits()); return wval(child).try_set(wval(e).bits());
return false; return false;
} }
@ -964,9 +960,9 @@ namespace bv {
// e[i] = 0 & b[i] = 0 -> a[i] = random // e[i] = 0 & b[i] = 0 -> a[i] = random
// a := e[i] | (~b[i] & a[i]) // a := e[i] | (~b[i] & a[i])
bool sls_eval::try_repair_band(bvval const& e, bvval& a, bvval const& b) { bool sls_eval::try_repair_band(bvect const& e, bvval& a, bvval const& b) {
for (unsigned i = 0; i < e.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = (e.bits()[i] & ~a.fixed[i]) | (~b.bits()[i] & ~a.fixed[i] & random_bits()); m_tmp[i] = (e[i] & ~a.fixed[i]) | (~b.bits()[i] & ~a.fixed[i] & random_bits());
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
@ -975,15 +971,15 @@ namespace bv {
// set a[i] to 1 where b[i] = 0, e[i] = 1 // set a[i] to 1 where b[i] = 0, e[i] = 1
// set a[i] to 0 where e[i] = 0, a[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) { bool sls_eval::try_repair_bor(bvect const& e, bvval& a, bvval const& b) {
for (unsigned i = 0; i < e.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = e.bits()[i] & (~b.bits()[i] | random_bits()); m_tmp[i] = e[i] & (~b.bits()[i] | random_bits());
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
bool sls_eval::try_repair_bxor(bvval const& e, bvval& a, bvval const& b) { bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) {
for (unsigned i = 0; i < e.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = e.bits()[i] ^ b.bits()[i]; m_tmp[i] = e[i] ^ b.bits()[i];
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
@ -993,21 +989,21 @@ namespace bv {
// first try to set a := e - b // first try to set a := e - b
// If this fails, set a to a random value // If this fails, set a to a random value
// //
bool sls_eval::try_repair_add(bvval const& e, bvval& a, bvval const& b) { bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
a.set_sub(m_tmp, e.bits(), b.bits()); a.set_sub(m_tmp, e, b.bits());
if (a.try_set(m_tmp)) if (a.try_set(m_tmp))
return true; return true;
a.get_variant(m_tmp, m_rand); a.get_variant(m_tmp, m_rand);
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
bool sls_eval::try_repair_sub(bvval const& e, bvval& a, bvval & b, unsigned i) { bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
if (i == 0) if (i == 0)
// e = a - b -> a := e + b // e = a - b -> a := e + b
a.set_add(m_tmp, e.bits(), b.bits()); a.set_add(m_tmp, e, b.bits());
else else
// b := a - e // b := a - e
b.set_sub(m_tmp, a.bits(), e.bits()); b.set_sub(m_tmp, a.bits(), e);
if (a.try_set(m_tmp)) if (a.try_set(m_tmp))
return true; return true;
// fall back to a random value // fall back to a random value
@ -1019,13 +1015,13 @@ namespace bv {
* e = a*b, then a = e * b^-1 * e = a*b, then a = e * b^-1
* 8*e = a*(2b), then a = 4e*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) { bool sls_eval::try_repair_mul(bvect const& e, bvval& a, bvval const& b) {
unsigned parity_e = e.parity(e.bits()); unsigned parity_e = b.parity(e);
unsigned parity_b = b.parity(b.bits()); unsigned parity_b = b.parity(b.bits());
if (e.is_zero()) { if (b.is_zero(e)) {
a.get_variant(m_tmp, m_rand); a.get_variant(m_tmp, m_rand);
for (unsigned i = 0; i < e.bw - parity_b; ++i) for (unsigned i = 0; i < b.bw - parity_b; ++i)
m_tmp.set(i, false); m_tmp.set(i, false);
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
@ -1046,7 +1042,7 @@ namespace bv {
b.get(y); b.get(y);
if (parity_b > 0) { if (parity_b > 0) {
b.shift_right(y, parity_b); b.shift_right(y, parity_b);
for (unsigned i = parity_b; i < e.bw; ++i) for (unsigned i = parity_b; i < b.bw; ++i)
y.set(i, m_rand() % 2 == 0); y.set(i, m_rand() % 2 == 0);
} }
@ -1092,22 +1088,22 @@ namespace bv {
a.set_mul(m_tmp, tb, y); a.set_mul(m_tmp, tb, y);
SASSERT(a.is_one(m_tmp)); SASSERT(a.is_one(m_tmp));
#endif #endif
e.get(m_tmp2); b.get(m_tmp2);
if (parity_e > 0 && parity_b > 0) if (parity_e > 0 && parity_b > 0)
b.shift_right(m_tmp2, std::min(parity_b, parity_e)); b.shift_right(m_tmp2, std::min(parity_b, parity_e));
a.set_mul(m_tmp, tb, m_tmp2); a.set_mul(m_tmp, tb, m_tmp2);
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
bool sls_eval::try_repair_bnot(bvval const& e, bvval& a) { bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {
for (unsigned i = 0; i < e.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = ~e.bits()[i]; m_tmp[i] = ~e[i];
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
bool sls_eval::try_repair_bneg(bvval const& e, bvval& a) { bool sls_eval::try_repair_bneg(bvect const& e, bvval& a) {
e.set_sub(m_tmp, m_zero, e.bits()); a.set_sub(m_tmp, m_zero, e);
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
@ -1261,11 +1257,11 @@ namespace bv {
return a.try_set_bit(idx, !a.get_bit(idx)); return a.try_set_bit(idx, !a.get_bit(idx));
} }
bool sls_eval::try_repair_shl(bvval const& e, bvval& a, bvval& b, unsigned i) { bool sls_eval::try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
unsigned sh = b.to_nat(b.bw); unsigned sh = b.to_nat(b.bw);
if (sh == 0) if (sh == 0)
return a.try_set(e.bits()); return a.try_set(e);
else if (sh >= b.bw) else if (sh >= b.bw)
return false; return false;
else { else {
@ -1275,9 +1271,9 @@ namespace bv {
// a[bw - sh - 1: 0] = e[bw - 1: sh] // a[bw - sh - 1: 0] = e[bw - 1: sh]
// a[bw - 1: bw - sh] = unchanged // a[bw - 1: bw - sh] = unchanged
// //
for (unsigned i = 0; i < e.bw - sh; ++i) for (unsigned i = 0; i < a.bw - sh; ++i)
m_tmp.set(i, e.get_bit(sh + i)); m_tmp.set(i, e.get(sh + i));
for (unsigned i = e.bw - sh; i < e.bw; ++i) for (unsigned i = a.bw - sh; i < a.bw; ++i)
m_tmp.set(i, a.get_bit(i)); m_tmp.set(i, a.get_bit(i));
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
@ -1292,13 +1288,13 @@ namespace bv {
return false; return false;
} }
bool sls_eval::try_repair_ashr(bvval const& e, bvval & a, bvval& b, unsigned i) { bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
unsigned sh = b.to_nat(b.bw); unsigned sh = b.to_nat(b.bw);
if (sh == 0) if (sh == 0)
return a.try_set(e.bits()); return a.try_set(e);
else if (sh >= b.bw) { else if (sh >= b.bw) {
if (e.get_bit(e.bw - 1)) if (e.get(a.bw - 1))
return a.try_set_bit(a.bw - 1, true); return a.try_set_bit(a.bw - 1, true);
else else
return a.try_set_bit(a.bw - 1, false); return a.try_set_bit(a.bw - 1, false);
@ -1309,7 +1305,7 @@ namespace bv {
// a[sh-1:0] = a[sh-1:0] // a[sh-1:0] = a[sh-1:0]
// ignore sign // ignore sign
for (unsigned i = sh; i < a.bw; ++i) for (unsigned i = sh; i < a.bw; ++i)
m_tmp.set(i, e.get_bit(i - sh)); m_tmp.set(i, e.get(i - sh));
for (unsigned i = 0; i < sh; ++i) for (unsigned i = 0; i < sh; ++i)
m_tmp.set(i, a.get_bit(i)); m_tmp.set(i, a.get_bit(i));
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
@ -1325,7 +1321,7 @@ namespace bv {
} }
} }
bool sls_eval::try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i) { bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {
return try_repair_ashr(e, a, b, i); return try_repair_ashr(e, a, b, i);
} }
@ -1334,29 +1330,28 @@ namespace bv {
// b = 0 => e = -1 // nothing to repair on a // b = 0 => e = -1 // nothing to repair on a
// e != -1 => max(a) >=u e // e != -1 => max(a) >=u e
bool sls_eval::try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i) { bool sls_eval::try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones()) if (a.is_zero(e) && a.is_ones(a.fixed) && a.is_ones())
return false; return false;
if (b.is_zero()) if (b.is_zero())
return false; return false;
if (!e.is_ones()) { if (!a.is_ones(e)) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = ~a.fixed[i] | a.bits()[i]; m_tmp[i] = ~a.fixed[i] | a.bits()[i];
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
if (e.bits() > m_tmp) if (e > m_tmp)
return false; return false;
} }
// e = 1 => a := b // e = 1 => a := b
if (e.is_one()) { if (a.is_one(e)) {
a.set(m_tmp, b.bits()); a.set(m_tmp, b.bits());
return a.set_repair(false, m_tmp); return a.set_repair(false, m_tmp);
} }
// b * e + r = a // b * e + r = a
b.get_variant(m_tmp, m_rand); if (mul_overflow_on_fixed(b, e)) {
while (mul_overflow_on_fixed(e, m_tmp)) { a.get_variant(m_tmp, m_rand);
auto i = b.msb(m_tmp); return a.set_repair(random_bool(), m_tmp);
m_tmp.set(i, false);
} }
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
@ -1369,13 +1364,13 @@ namespace bv {
return a.set_repair(true, m_tmp3); return a.set_repair(true, m_tmp3);
} }
else { else {
if (e.is_one() && a.is_zero()) { if (a.is_one(e) && a.is_zero()) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = random_bits(); m_tmp[i] = random_bits();
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
return b.set_repair(true, m_tmp); return b.set_repair(true, m_tmp);
} }
if (e.is_one()) { if (a.is_one(e)) {
a.set(m_tmp, a.bits()); a.set(m_tmp, a.bits());
return b.set_repair(true, m_tmp); return b.set_repair(true, m_tmp);
} }
@ -1390,7 +1385,7 @@ namespace bv {
while (a.bits() < m_tmp) while (a.bits() < m_tmp)
m_tmp.set(a.msb(m_tmp), false); m_tmp.set(a.msb(m_tmp), false);
a.set_sub(m_tmp2, a.bits(), m_tmp); a.set_sub(m_tmp2, a.bits(), m_tmp);
set_div(m_tmp2, e.bits(), a.bw, m_tmp3, m_tmp4); set_div(m_tmp2, e, a.bw, m_tmp3, m_tmp4);
return b.set_repair(random_bool(), m_tmp4); return b.set_repair(random_bool(), m_tmp4);
} }
} }
@ -1405,11 +1400,11 @@ namespace bv {
// (s != t => exists y . (mcb(x, y) and y >u t and (s - t) mod y = 0) // (s != t => exists y . (mcb(x, y) and y >u t and (s - t) mod y = 0)
bool sls_eval::try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i) { bool sls_eval::try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
if (b.is_zero()) { if (b.is_zero()) {
a.set(m_tmp, e.bits()); a.set(m_tmp, e);
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
// a urem b = e: b*y + e = a // a urem b = e: b*y + e = a
@ -1427,12 +1422,11 @@ namespace bv {
} }
while (true) { while (true) {
a.set_mul(m_tmp2, m_tmp, b.bits()); a.set_mul(m_tmp2, m_tmp, b.bits());
if (!add_overflow_on_fixed(e, m_tmp2)) if (!a.set_add(m_tmp3, m_tmp2, e))
break; break;
auto i = b.msb(m_tmp); auto i = b.msb(m_tmp);
m_tmp.set(i, false); m_tmp.set(i, false);
} }
a.set_add(m_tmp3, m_tmp2, e.bits());
return a.set_repair(random_bool(), m_tmp3); return a.set_repair(random_bool(), m_tmp3);
} }
else { else {
@ -1445,7 +1439,7 @@ namespace bv {
// lower y as long as y*b overflows with fixed bits in b // lower y as long as y*b overflows with fixed bits in b
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = random_bits(); m_tmp[i] = random_bits();
a.set_sub(m_tmp2, a.bits(), e.bits()); a.set_sub(m_tmp2, a.bits(), e);
set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4); set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4);
a.clear_overflow_bits(m_tmp3); a.clear_overflow_bits(m_tmp3);
return b.set_repair(random_bool(), m_tmp3); return b.set_repair(random_bool(), m_tmp3);
@ -1466,17 +1460,17 @@ namespace bv {
return a.set_mul(m_tmp4, m_tmp3, t); return a.set_mul(m_tmp4, m_tmp3, t);
} }
bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const { bool sls_eval::try_repair_rotate_left(bvect const& e, bvval& a, unsigned n) const {
// a := rotate_right(e, n) // a := rotate_right(e, n)
n = (a.bw - n) % a.bw; n = (a.bw - n) % a.bw;
for (unsigned i = a.bw - n; i < a.bw; ++i) for (unsigned i = a.bw - n; i < a.bw; ++i)
m_tmp.set(i + n - a.bw, e.get_bit(i)); m_tmp.set(i + n - a.bw, e.get(i));
for (unsigned i = 0; i < a.bw - n; ++i) for (unsigned i = 0; i < a.bw - n; ++i)
m_tmp.set(i + n, e.get_bit(i)); m_tmp.set(i + n, e.get(i));
return a.set_repair(true, m_tmp); return a.set_repair(true, m_tmp);
} }
bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i) { bool sls_eval::try_repair_rotate_left(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
rational n = b.get_value(); rational n = b.get_value();
n = mod(n, rational(b.bw)); n = mod(n, rational(b.bw));
@ -1490,7 +1484,7 @@ namespace bv {
} }
} }
bool sls_eval::try_repair_rotate_right(bvval const& e, bvval& a, bvval& b, unsigned i) { bool sls_eval::try_repair_rotate_right(bvect const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) { if (i == 0) {
rational n = b.get_value(); rational n = b.get_value();
n = mod(b.bw - n, rational(b.bw)); n = mod(b.bw - n, rational(b.bw));
@ -1533,11 +1527,13 @@ namespace bv {
// prefix of e must be 1s or 0 and match bit position of last bit in a. // prefix of e must be 1s or 0 and match bit position of last bit in a.
// set a to suffix of e, matching signs. // set a to suffix of e, matching signs.
// //
bool sls_eval::try_repair_sign_ext(bvval const& e, bvval& a) { bool sls_eval::try_repair_sign_ext(bvect const& e, bvval& a) {
for (unsigned i = a.bw; i < e.bw; ++i) for (unsigned i = a.bw; i < e.bw; ++i)
if (e.get_bit(i) != e.get_bit(a.bw - 1)) if (e.get(i) != e.get(a.bw - 1))
return false; return false;
e.get(m_tmp);
for (unsigned i = 0; i < e.bw; ++i)
m_tmp[i] = e[i];
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
@ -1545,25 +1541,27 @@ namespace bv {
// //
// prefix of e must be 0s. // prefix of e must be 0s.
// //
bool sls_eval::try_repair_zero_ext(bvval const& e, bvval& a) { bool sls_eval::try_repair_zero_ext(bvect const& e, bvval& a) {
for (unsigned i = a.bw; i < e.bw; ++i) for (unsigned i = a.bw; i < e.bw; ++i)
if (e.get_bit(i)) if (e.get(i))
return false; return false;
e.get(m_tmp);
for (unsigned i = 0; i < e.bw; ++i)
m_tmp[i] = e[i];
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned idx) { bool sls_eval::try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned idx) {
if (idx == 0) { if (idx == 0) {
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, e.get_bit(i + b.bw)); m_tmp.set(i, e.get(i + b.bw));
a.clear_overflow_bits(m_tmp); a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
else { else {
for (unsigned i = 0; i < b.bw; ++i) for (unsigned i = 0; i < b.bw; ++i)
m_tmp.set(i, e.get_bit(i)); m_tmp.set(i, e.get(i));
b.clear_overflow_bits(m_tmp); b.clear_overflow_bits(m_tmp);
return b.try_set(m_tmp); return b.try_set(m_tmp);
} }
@ -1574,7 +1572,7 @@ namespace bv {
// for the randomized assignment, // for the randomized assignment,
// set a outside of [hi:lo] to random values with preference to 0 or 1 bits // set a outside of [hi:lo] to random values with preference to 0 or 1 bits
// //
bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) { bool sls_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
if (m_rand() % m_config.m_prob_randomize_extract <= 100) { if (m_rand() % m_config.m_prob_randomize_extract <= 100) {
a.get_variant(m_tmp, m_rand); a.get_variant(m_tmp, m_rand);
if (0 == (m_rand() % 2)) { if (0 == (m_rand() % 2)) {
@ -1591,7 +1589,7 @@ namespace bv {
else else
a.get(m_tmp); a.get(m_tmp);
for (unsigned i = 0; i < e.bw; ++i) for (unsigned i = 0; i < e.bw; ++i)
m_tmp.set(i + lo, e.get_bit(i)); m_tmp.set(i + lo, e.get(i));
return a.try_set(m_tmp); return a.try_set(m_tmp);
} }
@ -1625,8 +1623,11 @@ namespace bv {
m_eval[e->get_id()] = b; m_eval[e->get_id()] = b;
return true; return true;
} }
if (bv.is_bv(e)) if (bv.is_bv(e)) {
return wval0(e).try_set(wval1(to_app(e)).bits()); auto& v = eval(to_app(e));
v.commit_eval();
return true;
}
return false; return false;
} }
} }

53
src/ast/sls/bv_sls_eval.h
View file

@ -42,8 +42,7 @@ namespace bv {
scoped_ptr_vector<sls_valuation> m_values0; // expr-id -> bv valuation scoped_ptr_vector<sls_valuation> m_values; // expr-id -> bv valuation
scoped_ptr_vector<sls_pre_valuation> m_values1; // expr-id -> bv valuation
bool_vector m_eval; // expr-id -> boolean valuation bool_vector m_eval; // expr-id -> boolean valuation
bool_vector m_fixed; // expr-id -> is Boolean fixed bool_vector m_fixed; // expr-id -> is Boolean fixed
@ -77,36 +76,36 @@ namespace bv {
bool try_repair_xor(app* e, unsigned i); bool try_repair_xor(app* e, unsigned i);
bool try_repair_ite(app* e, unsigned i); bool try_repair_ite(app* e, unsigned i);
bool try_repair_implies(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_band(bvect const& e, bvval& a, bvval const& b);
bool try_repair_bor(bvval const& e, bvval& a, bvval const& b); bool try_repair_bor(bvect const& e, bvval& a, bvval const& b);
bool try_repair_add(bvval const& e, bvval& a, bvval const& b); bool try_repair_add(bvect const& e, bvval& a, bvval const& b);
bool try_repair_sub(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_sub(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_mul(bvval const& e, bvval& a, bvval const& b); bool try_repair_mul(bvect const& e, bvval& a, bvval const& b);
bool try_repair_bxor(bvval const& e, bvval& a, bvval const& b); bool try_repair_bxor(bvect const& e, bvval& a, bvval const& b);
bool try_repair_bnot(bvval const& e, bvval& a); bool try_repair_bnot(bvect const& e, bvval& a);
bool try_repair_bneg(bvval const& e, bvval& a); bool try_repair_bneg(bvect const& e, bvval& a);
bool try_repair_ule(bool e, bvval& a, bvval const& b); 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_uge(bool e, bvval& a, bvval const& b);
bool try_repair_sle(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); bool try_repair_sge(bool e, bvval& a, bvval const& b);
bool try_repair_sge(bvval& a, bvect const& b, bvect const& p2); bool try_repair_sge(bvval& a, bvect const& b, bvect const& p2);
bool try_repair_sle(bvval& a, bvect const& b, bvect const& p2); bool try_repair_sle(bvval& a, bvect const& b, bvect const& p2);
bool try_repair_shl(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_ashr(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_ashr(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_bit2bool(bvval& a, unsigned idx); bool try_repair_bit2bool(bvval& a, unsigned idx);
bool try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const; bool try_repair_rotate_left(bvect const& e, bvval& a, unsigned n) const;
bool try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_rotate_left(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_rotate_right(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_rotate_right(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_ule(bool e, bvval& a, bvect const& t); bool try_repair_ule(bool e, bvval& a, bvect const& t);
bool try_repair_uge(bool e, bvval& a, bvect const& t); bool try_repair_uge(bool e, bvval& a, bvect const& t);
bool try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i); bool try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i);
bool try_repair_zero_ext(bvval const& e, bvval& a); bool try_repair_zero_ext(bvect const& e, bvval& a);
bool try_repair_sign_ext(bvval const& e, bvval& a); bool try_repair_sign_ext(bvect const& e, bvval& a);
bool try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i); bool try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_extract(bvval const& e, bvval& a, unsigned lo); bool try_repair_extract(bvect const& e, bvval& a, unsigned lo);
void add_p2_1(bvval const& a, bvect& t) const; void add_p2_1(bvval const& a, bvect& t) const;
bool add_overflow_on_fixed(bvval const& a, bvect const& t); bool add_overflow_on_fixed(bvval const& a, bvect const& t);
@ -117,9 +116,11 @@ namespace bv {
digit_t random_bits(); digit_t random_bits();
bool random_bool() { return m_rand() % 2 == 0; } bool random_bool() { return m_rand() % 2 == 0; }
sls_valuation& wval0(app* e, unsigned i) { return wval0(e->get_arg(i)); } sls_valuation& wval(app* e, unsigned i) { return wval(e->get_arg(i)); }
void wval1(app* e, sls_pre_valuation& val) const; void eval(app* e, sls_valuation& val) const;
bvect const& eval_value(app* e) const { return wval(e).eval; }
public: public:
sls_eval(ast_manager& m); sls_eval(ast_manager& m);
@ -138,7 +139,7 @@ namespace bv {
bool bval0(expr* e) const { return m_eval[e->get_id()]; } bool bval0(expr* e) const { return m_eval[e->get_id()]; }
sls_valuation& wval0(expr* e) const { return *m_values0[e->get_id()]; } sls_valuation& wval(expr* e) const { return *m_values[e->get_id()]; }
bool is_fixed0(expr* e) const { return m_fixed[e->get_id()]; } bool is_fixed0(expr* e) const { return m_fixed[e->get_id()]; }
@ -148,7 +149,7 @@ namespace bv {
bool bval1(app* e) const; bool bval1(app* e) const;
bool can_eval1(app* e) const; bool can_eval1(app* e) const;
sls_valuation& wval1(app* e) const; sls_valuation& eval(app* e) const;
/** /**
* Override evaluaton. * Override evaluaton.

50
src/ast/sls/bv_sls_fixed.cpp
View file

@ -109,7 +109,7 @@ namespace bv {
init_range(s, -a, nullptr, rational(0), false); init_range(s, -a, nullptr, rational(0), false);
} }
else if (bv.is_bit2bool(e, s, idx)) { else if (bv.is_bit2bool(e, s, idx)) {
auto& val = wval0(s); auto& val = wval(s);
val.try_set_bit(idx, !sign); val.try_set_bit(idx, !sign);
val.fixed.set(idx, true); val.fixed.set(idx, true);
val.init_fixed(); val.init_fixed();
@ -132,7 +132,7 @@ namespace bv {
// a <= y + b // a <= y + b
if (a == 0) if (a == 0)
return; return;
auto& v = wval0(y); auto& v = wval(y);
if (!sign) if (!sign)
v.add_range(a - b, -b); v.add_range(a - b, -b);
else else
@ -142,7 +142,7 @@ namespace bv {
if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0) if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0)
return; return;
auto& v = wval0(x); auto& v = wval(x);
if (!sign) if (!sign)
v.add_range(-a, b - a + 1); v.add_range(-a, b - a + 1);
else else
@ -151,7 +151,7 @@ namespace bv {
else if (x == y) { else if (x == y) {
if (a == b) if (a == b)
return; return;
auto& v = wval0(x); auto& v = wval(x);
if (!sign) if (!sign)
v.add_range(-a, -b); v.add_range(-a, -b);
else else
@ -174,15 +174,15 @@ namespace bv {
x = nullptr; x = nullptr;
} }
sls_valuation& sls_fixed::wval0(expr* e) { sls_valuation& sls_fixed::wval(expr* e) {
return ev.wval0(e); return ev.wval(e);
} }
void sls_fixed::init_fixed_basic(app* e) { void sls_fixed::init_fixed_basic(app* e) {
if (bv.is_bv(e) && m.is_ite(e)) { if (bv.is_bv(e) && m.is_ite(e)) {
auto& val = wval0(e); auto& val = wval(e);
auto& val_th = wval0(e->get_arg(1)); auto& val_th = wval(e->get_arg(1));
auto& val_el = wval0(e->get_arg(2)); auto& val_el = wval(e->get_arg(2));
for (unsigned i = 0; i < val.nw; ++i) 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)); val.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits(i) ^ val_th.bits(i));
val.init_fixed(); val.init_fixed();
@ -219,7 +219,7 @@ namespace bv {
void sls_fixed::set_fixed_bw(app* e) { void sls_fixed::set_fixed_bw(app* e) {
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
SASSERT(e->get_family_id() == bv.get_fid()); SASSERT(e->get_family_id() == bv.get_fid());
auto& v = ev.wval0(e); auto& v = ev.wval(e);
if (all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) { if (all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) {
for (unsigned i = 0; i < v.bw; ++i) for (unsigned i = 0; i < v.bw; ++i)
v.fixed.set(i, true); v.fixed.set(i, true);
@ -228,37 +228,37 @@ namespace bv {
} }
switch (e->get_decl_kind()) { switch (e->get_decl_kind()) {
case OP_BAND: { case OP_BAND: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
// (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits) // (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits)
for (unsigned i = 0; i < a.nw; ++i) 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)); v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits(i)) | (b.fixed[i] & ~b.bits(i));
break; break;
} }
case OP_BOR: { case OP_BOR: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
// (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits) // (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits)
for (unsigned i = 0; i < a.nw; ++i) 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)); v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits(i)) | (b.fixed[i] & b.bits(i));
break; break;
} }
case OP_BXOR: { case OP_BXOR: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = a.fixed[i] & b.fixed[i]; v.fixed[i] = a.fixed[i] & b.fixed[i];
break; break;
} }
case OP_BNOT: { case OP_BNOT: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = a.fixed[i]; v.fixed[i] = a.fixed[i];
break; break;
} }
case OP_BADD: { case OP_BADD: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
rational r; rational r;
if (bv.is_numeral(e->get_arg(0), r) && b.has_range()) if (bv.is_numeral(e->get_arg(0), r) && b.has_range())
v.add_range(r + b.lo(), r + b.hi()); v.add_range(r + b.lo(), r + b.hi());
@ -282,8 +282,8 @@ namespace bv {
break; break;
} }
case OP_BMUL: { case OP_BMUL: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
unsigned j = 0, k = 0, zj = 0, zk = 0, hzj = 0, hzk = 0; unsigned j = 0, k = 0, zj = 0, zk = 0, hzj = 0, hzk = 0;
// i'th bit depends on bits j + k = i // i'th bit depends on bits j + k = i
// if the first j, resp k bits are 0, the bits j + k are 0 // if the first j, resp k bits are 0, the bits j + k are 0
@ -333,8 +333,8 @@ namespace bv {
break; break;
} }
case OP_CONCAT: { case OP_CONCAT: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
auto& b = wval0(e->get_arg(1)); auto& b = wval(e->get_arg(1));
for (unsigned i = 0; i < b.bw; ++i) for (unsigned i = 0; i < b.bw; ++i)
v.fixed.set(i, b.fixed.get(i)); v.fixed.set(i, b.fixed.get(i));
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
@ -345,13 +345,13 @@ namespace bv {
expr* child; expr* child;
unsigned lo, hi; unsigned lo, hi;
VERIFY(bv.is_extract(e, lo, hi, child)); VERIFY(bv.is_extract(e, lo, hi, child));
auto& a = wval0(child); auto& a = wval(child);
for (unsigned i = lo; i <= hi; ++i) for (unsigned i = lo; i <= hi; ++i)
v.fixed.set(i - lo, a.fixed.get(i)); v.fixed.set(i - lo, a.fixed.get(i));
break; break;
} }
case OP_BNEG: { case OP_BNEG: {
auto& a = wval0(e->get_arg(0)); auto& a = wval(e->get_arg(0));
bool pfixed = true; bool pfixed = true;
for (unsigned i = 0; i < v.bw; ++i) { for (unsigned i = 0; i < v.bw; ++i) {
if (pfixed && a.fixed.get(i)) if (pfixed && a.fixed.get(i))

2
src/ast/sls/bv_sls_fixed.h
View file

@ -41,7 +41,7 @@ namespace bv {
bool is_fixed1_basic(app* e) const; bool is_fixed1_basic(app* e) const;
void set_fixed_bw(app* e); void set_fixed_bw(app* e);
sls_valuation& wval0(expr* e); sls_valuation& wval(expr* e);
public: public:
sls_fixed(sls_eval& ev); sls_fixed(sls_eval& ev);

58
src/ast/sls/sls_valuation.cpp
View file

@ -56,15 +56,34 @@ namespace bv {
return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) >= 0; return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) >= 0;
} }
std::ostream& operator<<(std::ostream& out, bvect const& v) {
out << std::hex;
bool nz = false;
for (unsigned i = v.nw; i-- > 0;) {
auto w = v[i];
if (i + 1 == v.nw)
w &= v.mask;
if (nz)
out << std::setw(8) << std::setfill('0') << w;
else if (w != 0)
out << w, nz = true;
}
if (!nz)
out << "0";
out << std::dec;
return out;
}
sls_valuation::sls_valuation(unsigned bw) { sls_valuation::sls_valuation(unsigned bw) {
set_bw(bw); set_bw(bw);
m_lo.set_bw(bw); m_lo.set_bw(bw);
m_hi.set_bw(bw); m_hi.set_bw(bw);
m_bits.set_bw(bw); m_bits.set_bw(bw);
fixed.set_bw(bw); fixed.set_bw(bw);
eval.set_bw(bw);
// have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated // have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
m_lo[i] = 0, m_hi[i] = 0, m_bits[i] = 0, fixed[i] = 0; m_lo[i] = 0, m_hi[i] = 0, m_bits[i] = 0, fixed[i] = 0, eval[i] = 0;
fixed[nw - 1] = ~mask; fixed[nw - 1] = ~mask;
} }
@ -76,6 +95,16 @@ namespace bv {
mask = ~(digit_t)0; mask = ~(digit_t)0;
} }
void sls_valuation::commit_eval() {
DEBUG_CODE(
for (unsigned i = 0; i < nw; ++i)
VERIFY(0 == (fixed[i] & (m_bits[i] ^ eval[i])));
);
for (unsigned i = 0; i < nw; ++i)
m_bits[i] = eval[i];
SASSERT(well_formed());
}
bool sls_valuation::in_range(bvect const& bits) const { bool sls_valuation::in_range(bvect const& bits) const {
mpn_manager m; mpn_manager m;
auto c = m.compare(m_lo.data(), nw, m_hi.data(), nw); auto c = m.compare(m_lo.data(), nw, m_hi.data(), nw);
@ -303,9 +332,7 @@ namespace bv {
if (!ok) if (!ok)
VERIFY(try_down ? round_up(dst) : round_down(dst)); VERIFY(try_down ? round_up(dst) : round_down(dst));
DEBUG_CODE(SASSERT(0 == (mask & (fixed[nw-1] & (m_bits[nw-1] ^ dst[nw-1])))); for (unsigned i = 0; i + 1 < nw; ++i) SASSERT(0 == (fixed[i] & (m_bits[i] ^ dst[i])));); DEBUG_CODE(SASSERT(0 == (mask & (fixed[nw-1] & (m_bits[nw-1] ^ dst[nw-1])))); for (unsigned i = 0; i + 1 < nw; ++i) SASSERT(0 == (fixed[i] & (m_bits[i] ^ dst[i]))););
if (m_bits == dst) set(eval, dst);
return false;
set(m_bits, dst);
SASSERT(well_formed()); SASSERT(well_formed());
return true; return true;
} }
@ -452,8 +479,8 @@ namespace bv {
} }
SASSERT(!has_overflow(m_lo)); SASSERT(!has_overflow(m_lo));
SASSERT(!has_overflow(m_hi)); SASSERT(!has_overflow(m_hi));
if (!in_range(m_bits)) if (!in_range(eval))
set(m_bits, m_lo); set(eval, m_lo);
SASSERT(well_formed()); SASSERT(well_formed());
} }
@ -518,7 +545,7 @@ namespace bv {
auto set_fixed_bit = [&](unsigned i, bool b) { auto set_fixed_bit = [&](unsigned i, bool b) {
if (!fixed.get(i)) { if (!fixed.get(i)) {
fixed.set(i, true); fixed.set(i, true);
m_bits.set(i, b); eval.set(i, b);
} }
}; };
@ -575,22 +602,5 @@ namespace bv {
return c == 1; return c == 1;
} }
std::ostream& sls_valuation::print_bits(std::ostream& out, bvect const& v) const {
bool nz = false;
for (unsigned i = nw; i-- > 0;) {
auto w = v[i];
if (i + 1 == nw)
w &= mask;
if (nz)
out << std::setw(8) << std::setfill('0') << w;
else if (w != 0)
out << w, nz = true;
}
if (!nz)
out << "0";
return out;
}
} }

45
src/ast/sls/sls_valuation.h
View file

@ -28,10 +28,11 @@ Author:
namespace bv { namespace bv {
class bvect : public svector<digit_t> { class bvect : public svector<digit_t> {
public:
unsigned bw = 0; unsigned bw = 0;
unsigned nw = 0; unsigned nw = 0;
unsigned mask = 0; unsigned mask = 0;
public:
bvect() {} bvect() {}
bvect(unsigned sz) : svector(sz, (unsigned)0) {} bvect(unsigned sz) : svector(sz, (unsigned)0) {}
void set_bw(unsigned bw); void set_bw(unsigned bw);
@ -54,6 +55,7 @@ namespace bv {
friend bool operator>(bvect const& a, bvect const& b); friend bool operator>(bvect const& a, bvect const& b);
friend bool operator<=(bvect const& a, bvect const& b); friend bool operator<=(bvect const& a, bvect const& b);
friend bool operator>=(bvect const& a, bvect const& b); friend bool operator>=(bvect const& a, bvect const& b);
friend std::ostream& operator<<(std::ostream& out, bvect const& v);
private: private:
@ -76,6 +78,7 @@ namespace bv {
bool operator>=(bvect const& a, bvect const& b); bool operator>=(bvect const& a, bvect const& b);
bool operator>(bvect const& a, bvect const& b); bool operator>(bvect const& a, bvect const& b);
inline bool operator!=(bvect const& a, bvect const& b) { return !(a == b); } inline bool operator!=(bvect const& a, bvect const& b) { return !(a == b); }
std::ostream& operator<<(std::ostream& out, bvect const& v);
class sls_valuation { class sls_valuation {
protected: protected:
@ -87,13 +90,12 @@ namespace bv {
bool round_up(bvect& dst) const; bool round_up(bvect& dst) const;
bool round_down(bvect& dst) const; bool round_down(bvect& dst) const;
std::ostream& print_bits(std::ostream& out, bvect const& bits) const;
public: public:
unsigned bw; // bit-width unsigned bw; // bit-width
unsigned nw; // num words unsigned nw; // num words
bvect fixed; // bit assignment and don't care bit bvect fixed; // bit assignment and don't care bit
bvect eval; // current evaluation
sls_valuation(unsigned bw); sls_valuation(unsigned bw);
@ -103,25 +105,28 @@ namespace bv {
digit_t bits(unsigned i) const { return m_bits[i]; } digit_t bits(unsigned i) const { return m_bits[i]; }
bvect const& bits() const { return m_bits; } bvect const& bits() const { return m_bits; }
void commit_eval();
bool get_bit(unsigned i) const { return m_bits.get(i); } bool get_bit(unsigned i) const { return m_bits.get(i); }
bool try_set_bit(unsigned i, bool b) { bool try_set_bit(unsigned i, bool b) {
SASSERT(in_range(m_bits)); SASSERT(in_range(m_bits));
if (fixed.get(i) && get_bit(i) != b) if (fixed.get(i) && get_bit(i) != b)
return false; return false;
m_bits.set(i, b); eval.set(i, b);
if (in_range(m_bits)) if (in_range(m_bits))
return true; return true;
m_bits.set(i, !b); eval.set(i, !b);
return false; return false;
} }
void set_value(bvect& bits, rational const& r); void set_value(bvect& bits, rational const& r);
rational get_value() const { return get_value(m_bits); } rational get_value() const { return get_value(m_bits); }
rational get_eval() const { return get_value(eval); }
rational lo() const { return get_value(m_lo); } rational lo() const { return get_value(m_lo); }
rational hi() const { return get_value(m_hi); } rational hi() const { return get_value(m_hi); }
void get(bvect& dst) const; void get(bvect& dst) const;
void add_range(rational lo, rational hi); void add_range(rational lo, rational hi);
bool has_range() const { return m_lo != m_hi; } bool has_range() const { return m_lo != m_hi; }
@ -209,8 +214,8 @@ namespace bv {
void set(bvect const& src) { void set(bvect const& src) {
for (unsigned i = nw; i-- > 0; ) for (unsigned i = nw; i-- > 0; )
m_bits[i] = src[i]; eval[i] = src[i];
clear_overflow_bits(m_bits); clear_overflow_bits(eval);
} }
void set_zero(bvect& out) const { void set_zero(bvect& out) const {
@ -225,7 +230,7 @@ namespace bv {
} }
void set_zero() { void set_zero() {
set_zero(m_bits); set_zero(eval);
} }
void sub1(bvect& out) const { void sub1(bvect& out) const {
@ -272,20 +277,11 @@ namespace bv {
unsigned to_nat(unsigned max_n); unsigned to_nat(unsigned max_n);
std::ostream& display(std::ostream& out) const { std::ostream& display(std::ostream& out) const {
out << std::hex; out << m_bits;
print_bits(out, m_bits);
out << " fix:"; out << " fix:";
print_bits(out, fixed); out << fixed;
if (m_lo != m_hi)
if (m_lo != m_hi) { out << " [" << m_lo << ", " << m_hi << "[";
out << " [";
print_bits(out, m_lo);
out << ", ";
print_bits(out, m_hi);
out << "[";
}
out << std::dec;
return out; return out;
} }
@ -295,13 +291,6 @@ namespace bv {
}; };
class sls_pre_valuation : public sls_valuation {
public:
sls_pre_valuation(unsigned bw) :sls_valuation(bw) {}
bvect& bits() { return m_bits; }
void set_bit(unsigned i, bool v) { m_bits.set(i, v); }
};
inline std::ostream& operator<<(std::ostream& out, sls_valuation const& v) { return v.display(out); } inline std::ostream& operator<<(std::ostream& out, sls_valuation const& v) { return v.display(out); }
} }

8
src/test/sls_test.cpp
View file

@ -36,7 +36,7 @@ namespace bv {
rw(r); rw(r);
if (bv.is_bv(e)) { if (bv.is_bv(e)) {
auto const& val = ev.wval0(e); auto const& val = ev.wval(e);
rational n1, n2; rational n1, n2;
n1 = val.get_value(); n1 = val.get_value();
@ -164,15 +164,15 @@ namespace bv {
} }
} }
if (bv.is_bv(e1)) { if (bv.is_bv(e1)) {
auto& val1 = ev.wval0(e1); auto& val1 = ev.wval(e1);
auto& val2 = ev.wval0(e2); auto& val2 = ev.wval(e2);
if (!val1.eq(val2)) { if (!val1.eq(val2)) {
val2.set(val1.bits()); val2.set(val1.bits());
auto rep2 = ev.try_repair(to_app(e2), idx); auto rep2 = ev.try_repair(to_app(e2), idx);
if (!rep2) { if (!rep2) {
verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n"; verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n";
} }
auto val3 = ev.wval0(e2); auto val3 = ev.wval(e2);
if (!val3.eq(val1)) { if (!val3.eq(val1)) {
verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n"; verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n";
} }