mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
add tests for evaluation
This commit is contained in:
Nikolaj Bjorner
parent
1cf008dd0a
commit
ddf2d28350
|
|
@ -89,12 +89,14 @@ namespace bv {
|
|||
|
||||
sls_valuation* sls_eval::alloc_valuation(unsigned bit_width) {
|
||||
auto* r = alloc(sls_valuation, bit_width);
|
||||
while (m_tmp.size() < r->nw) {
|
||||
while (m_tmp.size() < 2 * r->nw) {
|
||||
m_tmp.push_back(0);
|
||||
m_tmp2.push_back(0);
|
||||
m_tmp2.push_back(0);
|
||||
m_tmp2.push_back(0);
|
||||
m_tmp3.push_back(0);
|
||||
m_tmp4.push_back(0);
|
||||
m_zero.push_back(0);
|
||||
m_one.push_back(0);
|
||||
m_minus_one.push_back(~0);
|
||||
m_one[0] = 1;
|
||||
}
|
||||
return r;
|
||||
|
|
@ -195,9 +197,11 @@ namespace bv {
|
|||
auto& b = wval0(e->get_arg(1));
|
||||
unsigned c;
|
||||
a.set(m_zero, a.bw - 1, true);
|
||||
mpn.add(a.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp.data(), a.nw, &c);
|
||||
mpn.add(b.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp2.data(), a.nw, &c);
|
||||
mpn.add(a.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp.data(), a.nw + 1, &c);
|
||||
mpn.add(b.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp2.data(), a.nw + 1, &c);
|
||||
a.set(m_zero, a.bw - 1, false);
|
||||
a.clear_overflow_bits(m_tmp);
|
||||
a.clear_overflow_bits(m_tmp2);
|
||||
return f(mpn.compare(m_tmp.data(), a.nw, m_tmp2.data(), b.nw));
|
||||
};
|
||||
|
||||
|
|
@ -209,8 +213,7 @@ namespace bv {
|
|||
for (unsigned i = a.nw; i < 2 * a.nw; ++i)
|
||||
if (m_tmp2[i] != 0)
|
||||
return true;
|
||||
return !a.has_overflow(m_tmp);
|
||||
return true;
|
||||
return a.has_overflow(m_tmp2);
|
||||
};
|
||||
|
||||
switch (e->get_decl_kind()) {
|
||||
|
|
@ -246,7 +249,7 @@ namespace bv {
|
|||
auto const& a = wval0(e->get_arg(0));
|
||||
auto const& b = wval0(e->get_arg(1));
|
||||
digit_t c = 0;
|
||||
mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp.data(), a.nw, &c);
|
||||
mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp.data(), a.nw + 1, &c);
|
||||
return c != 0 || a.has_overflow(m_tmp);
|
||||
}
|
||||
case OP_BNEG_OVFL:
|
||||
|
|
@ -295,6 +298,63 @@ namespace bv {
|
|||
val.set(wval0(e).bits);
|
||||
return;
|
||||
}
|
||||
auto set_sdiv = [&]() {
|
||||
// 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
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
if (a.is_zero() && b.is_zero())
|
||||
val.set(m_minus_one);
|
||||
else if (a.is_zero())
|
||||
val.set(m_zero);
|
||||
else if (b.is_zero())
|
||||
val.set(m_minus_one);
|
||||
else if (!a.sign() && b.is_zero())
|
||||
val.set(m_one);
|
||||
else {
|
||||
bool sign_a = a.sign();
|
||||
bool sign_b = b.sign();
|
||||
digit_t c;
|
||||
|
||||
if (sign_a)
|
||||
mpn.sub(m_zero.data(), a.nw, a.bits.data(), a.nw, m_tmp.data(), &c);
|
||||
else
|
||||
a.get(m_tmp);
|
||||
val.clear_overflow_bits(m_tmp);
|
||||
|
||||
if (sign_b)
|
||||
mpn.sub(m_zero.data(), a.nw, b.bits.data(), a.nw, m_tmp2.data(), &c);
|
||||
else
|
||||
b.get(m_tmp2);
|
||||
val.clear_overflow_bits(m_tmp2);
|
||||
|
||||
mpn.div(m_tmp.data(), a.nw, m_tmp2.data(), a.nw, m_tmp3.data(), m_tmp4.data());
|
||||
if (sign_a == sign_b)
|
||||
val.set(m_tmp3);
|
||||
else
|
||||
mpn.sub(m_zero.data(), a.nw, m_tmp3.data(), a.nw, m_tmp.data(), &c),
|
||||
val.set(m_tmp);
|
||||
}
|
||||
};
|
||||
|
||||
auto mk_rotate_left = [&](unsigned n) {
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
if (n == 0 || a.bw == 1)
|
||||
val.set(a.bits);
|
||||
else {
|
||||
for (unsigned i = a.bw - n; i < a.bw; ++i)
|
||||
val.set(val.bits, i + n - a.bw, a.get(a.bits, i));
|
||||
for (unsigned i = 0; i < a.bw - n; ++i)
|
||||
val.set(val.bits, i + a.bw - n, a.get(a.bits, i));
|
||||
}
|
||||
};
|
||||
|
||||
SASSERT(e->get_family_id() == bv.get_fid());
|
||||
switch (e->get_decl_kind()) {
|
||||
case OP_BV_NUM: {
|
||||
|
|
@ -307,7 +367,7 @@ namespace bv {
|
|||
SASSERT(e->get_num_args() == 2);
|
||||
auto const& a = wval0(e->get_arg(0));
|
||||
auto const& b = wval0(e->get_arg(1));
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = a.bits[i] & b.bits[i];
|
||||
break;
|
||||
}
|
||||
|
|
@ -315,7 +375,7 @@ namespace bv {
|
|||
SASSERT(e->get_num_args() == 2);
|
||||
auto const& a = wval0(e->get_arg(0));
|
||||
auto const& b = wval0(e->get_arg(1));
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = a.bits[i] | b.bits[i];
|
||||
break;
|
||||
}
|
||||
|
|
@ -323,7 +383,7 @@ namespace bv {
|
|||
SASSERT(e->get_num_args() == 2);
|
||||
auto const& a = wval0(e->get_arg(0));
|
||||
auto const& b = wval0(e->get_arg(1));
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = a.bits[i] ^ b.bits[i];
|
||||
break;
|
||||
}
|
||||
|
|
@ -331,7 +391,7 @@ namespace bv {
|
|||
SASSERT(e->get_num_args() == 2);
|
||||
auto const& a = wval0(e->get_arg(0));
|
||||
auto const& b = wval0(e->get_arg(1));
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = ~(a.bits[i] & b.bits[i]);
|
||||
break;
|
||||
}
|
||||
|
|
@ -340,7 +400,15 @@ namespace bv {
|
|||
auto const& a = wval0(e->get_arg(0));
|
||||
auto const& b = wval0(e->get_arg(1));
|
||||
digit_t c;
|
||||
mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), val.nw, &c);
|
||||
mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), val.nw + 1, &c);
|
||||
break;
|
||||
}
|
||||
case OP_BSUB: {
|
||||
SASSERT(e->get_num_args() == 2);
|
||||
auto const& a = wval0(e->get_arg(0));
|
||||
auto const& b = wval0(e->get_arg(1));
|
||||
digit_t c;
|
||||
mpn.sub(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), &c);
|
||||
break;
|
||||
}
|
||||
case OP_BMUL: {
|
||||
|
|
@ -393,17 +461,13 @@ namespace bv {
|
|||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
auto sh = b.to_nat(b.bits, b.bw);
|
||||
if (sh == 0) {
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = a.bits[i];
|
||||
}
|
||||
else if (sh >= b.bw) {
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = 0;
|
||||
}
|
||||
if (sh == 0)
|
||||
val.set(a.bits);
|
||||
else if (sh >= b.bw)
|
||||
val.set_zero();
|
||||
else {
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
val.set(val.bits, i, i >= sh && b.get(b.bits, i - sh));
|
||||
val.set(val.bits, i, i >= sh && a.get(a.bits, i - sh));
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
@ -411,17 +475,13 @@ namespace bv {
|
|||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
auto sh = b.to_nat(b.bits, b.bw);
|
||||
if (sh == 0) {
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = a.bits[i];
|
||||
}
|
||||
else if (sh >= b.bw) {
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = 0;
|
||||
}
|
||||
if (sh == 0)
|
||||
val.set(a.bits);
|
||||
else if (sh >= b.bw)
|
||||
val.set_zero();
|
||||
else {
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
val.set(val.bits, i, i + sh < a.bw && b.get(b.bits, i + sh));
|
||||
val.set(val.bits, i, i + sh < a.bw && a.get(a.bits, i + sh));
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
@ -429,33 +489,31 @@ namespace bv {
|
|||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
auto sh = b.to_nat(b.bits, b.bw);
|
||||
auto sign = a.get(a.bits, a.bw - 1);
|
||||
if (sh == 0) {
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = a.bits[i];
|
||||
}
|
||||
auto sign = a.sign();
|
||||
if (sh == 0)
|
||||
val.set(a.bits);
|
||||
else if (sh >= b.bw) {
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = sign ? ~0 : 0;
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
val.set(val.bits, i, i + sh < a.bw && b.get(b.bits, i + sh));
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
val.set(val.bits, i, i + sh < a.bw && a.get(a.bits, i + sh));
|
||||
if (sign)
|
||||
val.set_range(val.bits, 0, a.bw - sh, true);
|
||||
val.set_range(val.bits, a.bw - sh, a.bw, true);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case OP_SIGN_EXT: {
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
a.set(val.bits);
|
||||
bool sign = a.get(a.bits, a.bw - 1);
|
||||
val.set(a.bits);
|
||||
bool sign = a.sign();
|
||||
val.set_range(val.bits, a.bw, val.bw, sign);
|
||||
break;
|
||||
}
|
||||
case OP_ZERO_EXT: {
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
a.set(val.bits);
|
||||
val.set(a.bits);
|
||||
val.set_range(val.bits, a.bw, val.bw, false);
|
||||
break;
|
||||
}
|
||||
|
|
@ -505,7 +563,7 @@ namespace bv {
|
|||
mpn.sub(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), &c),
|
||||
val.set(m_tmp);
|
||||
else if (b.sign())
|
||||
mpn.add(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), a.nw, &c),
|
||||
mpn.add(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), a.nw + 1, &c),
|
||||
val.set(m_tmp);
|
||||
else
|
||||
val.set(m_tmp2);
|
||||
|
|
@ -518,11 +576,8 @@ namespace bv {
|
|||
// x div 0 = -1
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
if (b.is_zero()) {
|
||||
val.set(m_zero);
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
val.bits[i] = ~val.bits[i];
|
||||
}
|
||||
if (b.is_zero())
|
||||
val.set(m_minus_one);
|
||||
else {
|
||||
mpn.div(a.bits.data(), a.nw,
|
||||
b.bits.data(), b.nw,
|
||||
|
|
@ -535,17 +590,57 @@ namespace bv {
|
|||
|
||||
case OP_BSDIV:
|
||||
case OP_BSDIV_I:
|
||||
case OP_BSDIV0:
|
||||
// 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
|
||||
|
||||
|
||||
case OP_BSDIV0: {
|
||||
set_sdiv();
|
||||
break;
|
||||
}
|
||||
case OP_BSREM:
|
||||
case OP_BSREM0:
|
||||
case OP_BSREM_I: {
|
||||
// y = 0 -> x
|
||||
// else x - sdiv(x, y) * y
|
||||
//
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
if (b.is_zero())
|
||||
val.set(a.bits);
|
||||
else {
|
||||
digit_t c;
|
||||
set_sdiv();
|
||||
mpn.mul(val.bits.data(), a.nw, b.bits.data(), a.nw, m_tmp.data());
|
||||
mpn.sub(a.bits.data(), a.nw, m_tmp.data(), a.nw, m_tmp2.data(), &c);
|
||||
val.set(m_tmp2);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case OP_ROTATE_LEFT: {
|
||||
unsigned n = e->get_parameter(0).get_int() % val.bw;
|
||||
mk_rotate_left(n);
|
||||
break;
|
||||
}
|
||||
case OP_ROTATE_RIGHT: {
|
||||
unsigned n = e->get_parameter(0).get_int() % val.bw;
|
||||
mk_rotate_left(val.bw - n);
|
||||
break;
|
||||
}
|
||||
case OP_EXT_ROTATE_LEFT: {
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
rational n;
|
||||
b.get_value(b.bits, n);
|
||||
n = mod(n, rational(val.bw));
|
||||
SASSERT(n.is_unsigned());
|
||||
mk_rotate_left(n.get_unsigned());
|
||||
break;
|
||||
}
|
||||
case OP_EXT_ROTATE_RIGHT: {
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
rational n;
|
||||
b.get_value(b.bits, n);
|
||||
n = mod(n, rational(val.bw));
|
||||
SASSERT(n.is_unsigned());
|
||||
mk_rotate_left(val.bw - n.get_unsigned());
|
||||
break;
|
||||
}
|
||||
case OP_BREDAND:
|
||||
case OP_BREDOR:
|
||||
case OP_BXNOR:
|
||||
|
|
@ -693,22 +788,37 @@ namespace bv {
|
|||
VERIFY(bv.is_bit2bool(e, arg, idx));
|
||||
return try_repair_bit2bool(wval0(e, 0), idx);
|
||||
}
|
||||
case OP_BSDIV:
|
||||
case OP_BSDIV_I:
|
||||
case OP_BSDIV0:
|
||||
return try_repair_sdiv(wval0(e), wval0(e, 0), wval0(e, 1), i);
|
||||
case OP_BUDIV:
|
||||
case OP_BUDIV_I:
|
||||
case OP_BUDIV0:
|
||||
return try_repair_udiv(wval0(e), wval0(e, 0), wval0(e, 1), i);
|
||||
case OP_BUREM:
|
||||
case OP_BUREM_I:
|
||||
case OP_BUREM0:
|
||||
return try_repair_urem(wval0(e), wval0(e, 0), wval0(e, 1), i);
|
||||
case OP_BSREM:
|
||||
case OP_BSREM_I:
|
||||
case OP_BSREM0:
|
||||
return try_repair_srem(wval0(e), wval0(e, 0), wval0(e, 1), i);
|
||||
case OP_BSMOD:
|
||||
case OP_BSMOD_I:
|
||||
case OP_BSMOD0:
|
||||
return try_repair_smod(wval0(e), wval0(e, 0), wval0(e, 1), i);
|
||||
case OP_ROTATE_LEFT:
|
||||
return try_repair_rotate_left(wval0(e), wval0(e, 0), e->get_parameter(0).get_int());
|
||||
case OP_ROTATE_RIGHT:
|
||||
return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e).bw - e->get_parameter(0).get_int());
|
||||
case OP_EXT_ROTATE_LEFT:
|
||||
return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e, 1), i);
|
||||
case OP_EXT_ROTATE_RIGHT:
|
||||
case OP_BCOMP:
|
||||
case OP_BNAND:
|
||||
case OP_BREDAND:
|
||||
case OP_BREDOR:
|
||||
case OP_BSDIV:
|
||||
case OP_BSDIV_I:
|
||||
case OP_BSDIV0:
|
||||
case OP_BUDIV:
|
||||
case OP_BUDIV_I:
|
||||
case OP_BUDIV0:
|
||||
case OP_BUREM:
|
||||
case OP_BUREM_I:
|
||||
case OP_BUREM0:
|
||||
case OP_BSMOD:
|
||||
case OP_BSMOD_I:
|
||||
case OP_BSMOD0:
|
||||
case OP_BXNOR:
|
||||
case OP_BNEG_OVFL:
|
||||
case OP_BSADD_OVFL:
|
||||
|
|
@ -883,7 +993,7 @@ namespace bv {
|
|||
return a.try_set(b.bits);
|
||||
else {
|
||||
digit_t c;
|
||||
mpn.add(b.bits.data(), a.nw, m_one.data(), a.nw, &c, a.nw, m_tmp.data());
|
||||
mpn.add(b.bits.data(), a.nw, m_one.data(), a.nw, &c, a.nw + 1, m_tmp.data());
|
||||
return a.try_set(m_tmp);
|
||||
}
|
||||
}
|
||||
|
|
@ -918,9 +1028,8 @@ namespace bv {
|
|||
unsigned sh = b.to_nat(b.bits, b.bw);
|
||||
if (sh == 0)
|
||||
return a.try_set(e.bits);
|
||||
else if (sh >= b.bw) {
|
||||
return false;
|
||||
}
|
||||
else if (sh >= b.bw)
|
||||
return false;
|
||||
else {
|
||||
//
|
||||
// e = a << sh
|
||||
|
|
@ -936,29 +1045,91 @@ namespace bv {
|
|||
}
|
||||
}
|
||||
else {
|
||||
// NB. blind sub-range of possible values for b
|
||||
SASSERT(i == 1);
|
||||
unsigned sh = m_rand(a.bw + 1);
|
||||
b.set(m_tmp, sh);
|
||||
return b.try_set(m_tmp);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_ashr(bvval const& e, bvval & a, bvval& b, unsigned i) {
|
||||
if (i == 0) {
|
||||
|
||||
unsigned sh = b.to_nat(b.bits, b.bw);
|
||||
if (sh == 0)
|
||||
return a.try_set(e.bits);
|
||||
else if (sh >= b.bw)
|
||||
return false;
|
||||
else {
|
||||
// e = a >> sh
|
||||
// a[bw-1:sh] = e[bw-sh-1:0]
|
||||
// a[sh-1:0] = a[sh-1:0]
|
||||
// ignore sign
|
||||
for (unsigned i = 0; i < a.bw - sh; ++i)
|
||||
a.set(m_tmp, i + sh, e.get(e.bits, i));
|
||||
for (unsigned i = 0; i < sh; ++i)
|
||||
a.set(m_tmp, i, a.get(a.bits, i));
|
||||
return a.try_set(m_tmp);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
||||
// NB. blind sub-range of possible values for b
|
||||
SASSERT(i == 1);
|
||||
unsigned sh = m_rand(a.bw + 1);
|
||||
b.set(m_tmp, sh);
|
||||
return b.try_set(m_tmp);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
if (i == 0) {
|
||||
return try_repair_ashr(e, a, b, i);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_sdiv(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) {
|
||||
// a := rotate_right(e, n)
|
||||
n = (n % a.bw) - n;
|
||||
for (unsigned i = a.bw - n; i < a.bw; ++i)
|
||||
a.set(m_tmp, i + n - a.bw, e.get(e.bits, i));
|
||||
for (unsigned i = 0; i < a.bw - n; ++i)
|
||||
a.set(m_tmp, i + a.bw - n, e.get(e.bits, i));
|
||||
return a.try_set(m_tmp);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
if (i == 0) {
|
||||
rational n;
|
||||
b.get_value(b.bits, n);
|
||||
n = mod(n, rational(b.bw));
|
||||
return try_repair_rotate_left(e, a, n.get_unsigned());
|
||||
}
|
||||
else {
|
||||
|
||||
}
|
||||
return false;
|
||||
SASSERT(i == 1);
|
||||
unsigned sh = m_rand(b.bw);
|
||||
b.set(m_tmp, sh);
|
||||
return b.try_set(m_tmp);
|
||||
}
|
||||
}
|
||||
|
||||
void sls_eval::repair_up(expr* e) {
|
||||
|
|
|
|||
|
|
@ -27,10 +27,11 @@ namespace bv {
|
|||
|
||||
class sls_eval {
|
||||
friend class sls_fixed;
|
||||
friend class sls_test;
|
||||
ast_manager& m;
|
||||
bv_util bv;
|
||||
sls_fixed m_fix;
|
||||
mutable mpn_manager mpn;
|
||||
mutable mpn_manager mpn;
|
||||
ptr_vector<expr> m_todo;
|
||||
random_gen m_rand;
|
||||
|
||||
|
|
@ -38,7 +39,7 @@ namespace bv {
|
|||
bool_vector m_eval; // expr-id -> boolean valuation
|
||||
bool_vector m_fixed; // expr-id -> is Boolean fixed
|
||||
|
||||
mutable svector<digit_t> m_tmp, m_tmp2, m_zero, m_one;
|
||||
mutable svector<digit_t> m_tmp, m_tmp2, m_tmp3, m_tmp4, m_zero, m_one, m_minus_one;
|
||||
|
||||
using bvval = sls_valuation;
|
||||
|
||||
|
|
@ -82,6 +83,14 @@ namespace bv {
|
|||
bool try_repair_ashr(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_bit2bool(bvval& a, unsigned idx);
|
||||
bool try_repair_sdiv(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n);
|
||||
bool try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
|
||||
|
||||
sls_valuation& wval0(app* e, unsigned i) { return wval0(e->get_arg(i)); }
|
||||
|
||||
|
|
@ -123,7 +132,6 @@ namespace bv {
|
|||
m_eval[e->get_id()] = b;
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
* Try to invert value of child to repair value assignment of parent.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -25,10 +25,10 @@ namespace bv {
|
|||
sls_valuation::sls_valuation(unsigned bw): bw(bw) {
|
||||
nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t));
|
||||
unsigned num_bytes = nw * sizeof(digit_t);
|
||||
lo.reserve(nw);
|
||||
hi.reserve(nw);
|
||||
bits.reserve(nw);
|
||||
fixed.reserve(nw);
|
||||
lo.reserve(nw + 1);
|
||||
hi.reserve(nw + 1);
|
||||
bits.reserve(nw + 1);
|
||||
fixed.reserve(nw + 1);
|
||||
// have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
lo[i] = 0, hi[i] = 0, bits[i] = 0, fixed[i] = 0;
|
||||
|
|
@ -84,6 +84,11 @@ namespace bv {
|
|||
}
|
||||
}
|
||||
|
||||
void sls_valuation::get(svector<digit_t>& dst) const {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
dst[i] = bits[i];
|
||||
}
|
||||
|
||||
void sls_valuation::set1(svector<digit_t>& bits) {
|
||||
for (unsigned i = 0; i < bw; ++i)
|
||||
set(bits, i, true);
|
||||
|
|
|
|||
|
|
@ -40,8 +40,10 @@ namespace bv {
|
|||
|
||||
void set_value(svector<digit_t>& bits, rational const& r);
|
||||
void get_value(svector<digit_t> const& bits, rational& r) const;
|
||||
void get(svector<digit_t>& dst) const;
|
||||
void add_range(rational lo, rational hi);
|
||||
void set1(svector<digit_t>& bits);
|
||||
|
||||
|
||||
void clear_overflow_bits(svector<digit_t>& bits) const;
|
||||
bool can_set(svector<digit_t> const& bits) const;
|
||||
|
|
@ -90,6 +92,11 @@ namespace bv {
|
|||
clear_overflow_bits(bits);
|
||||
}
|
||||
|
||||
void set_zero() {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
bits[i] = 0;
|
||||
}
|
||||
|
||||
|
||||
void set_fixed(svector<digit_t> const& src) {
|
||||
for (unsigned i = nw; i-- > 0; )
|
||||
|
|
|
|||
|
|
@ -108,6 +108,7 @@ add_executable(test-z3
|
|||
simple_parser.cpp
|
||||
simplex.cpp
|
||||
simplifier.cpp
|
||||
sls_test.cpp
|
||||
small_object_allocator.cpp
|
||||
smt2print_parse.cpp
|
||||
smt_context.cpp
|
||||
|
|
|
|||
|
|
@ -267,4 +267,5 @@ int main(int argc, char ** argv) {
|
|||
TST(distribution);
|
||||
TST(euf_bv_plugin);
|
||||
TST(euf_arith_plugin);
|
||||
TST(sls_test);
|
||||
}
|
||||
|
|
|
|||
203
src/test/sls_test.cpp
Normal file
203
src/test/sls_test.cpp
Normal file
|
|
@ -0,0 +1,203 @@
|
|||
|
||||
#include "ast/sls/bv_sls_eval.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
namespace bv {
|
||||
class sls_test {
|
||||
ast_manager& m;
|
||||
bv_util bv;
|
||||
|
||||
public:
|
||||
sls_test(ast_manager& m):
|
||||
m(m),
|
||||
bv(m)
|
||||
{}
|
||||
|
||||
void check_eval(expr* e) {
|
||||
std::function<bool(expr*, unsigned)> value = [](expr*, unsigned) {
|
||||
return false;
|
||||
};
|
||||
expr_ref_vector es(m);
|
||||
bv_util bv(m);
|
||||
es.push_back(e);
|
||||
sls_eval ev(m);
|
||||
ev.init_eval(es, value);
|
||||
th_rewriter rw(m);
|
||||
expr_ref r(e, m);
|
||||
rw(r);
|
||||
|
||||
if (bv.is_bv(e)) {
|
||||
auto const& val = ev.wval0(e);
|
||||
rational n1, n2;
|
||||
|
||||
val.get_value(val.bits, n1);
|
||||
|
||||
VERIFY(bv.is_numeral(r, n2));
|
||||
if (n1 != n2) {
|
||||
verbose_stream() << mk_pp(e, m) << " computed value " << val << "\n";
|
||||
verbose_stream() << "should be " << n2 << "\n";
|
||||
}
|
||||
SASSERT(n1 == n2);
|
||||
VERIFY(n1 == n2);
|
||||
}
|
||||
else if (m.is_bool(e)) {
|
||||
auto val1 = ev.bval0(e);
|
||||
auto val2 = m.is_true(r) ? true : false;
|
||||
if (val1 != val2) {
|
||||
verbose_stream() << mk_pp(e, m) << " computed value " << val1 << " at odds with definition\n";
|
||||
}
|
||||
SASSERT(val1 == val2);
|
||||
VERIFY(val1 == val2);
|
||||
}
|
||||
}
|
||||
|
||||
void check(expr* a, expr* b) {
|
||||
expr_ref e(m);
|
||||
auto& validator = *this;
|
||||
e = bv.mk_bv_add(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_mul(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_sub(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_udiv(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_sdiv(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_srem(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_urem(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_smod(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_shl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_ashr(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_lshr(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_and(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_or(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_xor(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_neg(a);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bv_not(a);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvumul_ovfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvumul_no_ovfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_zero_extend(3, a);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_sign_extend(3, a);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_ule(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_sle(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_concat(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_extract(6, 3, a);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvuadd_ovfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
|
||||
#if 0
|
||||
|
||||
e = bv.mk_bvsadd_ovfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvneg_ovfl(a);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvsmul_no_ovfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvsmul_no_udfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvsmul_ovfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_bvsdiv_ovfl(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
#endif
|
||||
|
||||
#if 0
|
||||
e = bv.mk_rotate_left(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_rotate_right(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_rotate_left_ext(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
e = bv.mk_rotate_right_ext(a, b);
|
||||
validator.check_eval(e);
|
||||
|
||||
#endif
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
|
||||
static void test_eval1() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
bv_util bv(m);
|
||||
|
||||
expr_ref e(m);
|
||||
|
||||
bv::sls_test validator(m);
|
||||
|
||||
unsigned k = 0;
|
||||
for (unsigned i = 0; i < 256; ++i) {
|
||||
expr_ref a(bv.mk_numeral(rational(i), 8), m);
|
||||
for (unsigned j = 0; j < 256; ++j) {
|
||||
expr_ref b(bv.mk_numeral(rational(j), 8), m);
|
||||
|
||||
++k;
|
||||
if (k % 1000 == 0)
|
||||
verbose_stream() << "tests " << k << "\n";
|
||||
|
||||
validator.check(a, b);
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void tst_sls_test() {
|
||||
test_eval1();
|
||||
}
|
||||
Loading…
Reference in a new issue