mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
reorg to use datatypes
This commit is contained in:
parent
48026edd7f
commit
74e73f2b84
|
@ -211,8 +211,7 @@ namespace bv {
|
|||
mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e)));
|
||||
else if (bv.is_bv(e)) {
|
||||
auto const& v = m_eval.wval0(e);
|
||||
rational n;
|
||||
v.get_value(v.bits(), n);
|
||||
rational n = v.get_value();
|
||||
mdl->register_decl(f, bv.mk_numeral(n, v.bw));
|
||||
}
|
||||
}
|
||||
|
|
|
@ -470,7 +470,7 @@ namespace bv {
|
|||
case OP_BSHL: {
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
auto sh = b.to_nat(b.bits(), b.bw);
|
||||
auto sh = b.to_nat(b.bw);
|
||||
if (sh == 0)
|
||||
val.set(a.bits());
|
||||
else if (sh >= b.bw)
|
||||
|
@ -484,7 +484,7 @@ namespace bv {
|
|||
case OP_BLSHR: {
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
auto sh = b.to_nat(b.bits(), b.bw);
|
||||
auto sh = b.to_nat(b.bw);
|
||||
if (sh == 0)
|
||||
val.set(a.bits());
|
||||
else if (sh >= b.bw)
|
||||
|
@ -498,7 +498,7 @@ namespace bv {
|
|||
case OP_BASHR: {
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
auto sh = b.to_nat(b.bits(), b.bw);
|
||||
auto sh = b.to_nat(b.bw);
|
||||
auto sign = a.sign();
|
||||
if (sh == 0)
|
||||
val.set(a.bits());
|
||||
|
@ -636,8 +636,7 @@ namespace bv {
|
|||
}
|
||||
case OP_EXT_ROTATE_LEFT: {
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
rational n;
|
||||
b.get_value(b.bits(), n);
|
||||
rational n = b.get_value();
|
||||
n = mod(n, rational(val.bw));
|
||||
SASSERT(n.is_unsigned());
|
||||
mk_rotate_left(n.get_unsigned());
|
||||
|
@ -645,8 +644,7 @@ namespace bv {
|
|||
}
|
||||
case OP_EXT_ROTATE_RIGHT: {
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
rational n;
|
||||
b.get_value(b.bits(), n);
|
||||
rational n = b.get_value();
|
||||
n = mod(n, rational(val.bw));
|
||||
SASSERT(n.is_unsigned());
|
||||
mk_rotate_left(val.bw - n.get_unsigned());
|
||||
|
@ -694,10 +692,10 @@ namespace bv {
|
|||
return r;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair(app* e, unsigned i) {
|
||||
bool sls_eval::try_repair(app* e, unsigned i) {
|
||||
if (is_fixed0(e->get_arg(i)))
|
||||
return false;
|
||||
if (e->get_family_id() == basic_family_id)
|
||||
else if (e->get_family_id() == basic_family_id)
|
||||
return try_repair_basic(e, i);
|
||||
if (e->get_family_id() == bv.get_family_id())
|
||||
return try_repair_bv(e, i);
|
||||
|
@ -1049,8 +1047,10 @@ namespace bv {
|
|||
if (parity_b > 0)
|
||||
b.shift_right(y, parity_b);
|
||||
y[a.nw] = 0;
|
||||
|
||||
a.nw = a.nw + 1;
|
||||
a.bw = 8 * sizeof(digit_t) * a.nw;
|
||||
y.set_bw(a.bw);
|
||||
// x = 2 ^ b.bw
|
||||
a.set_zero(x);
|
||||
a.set(x, bw, true);
|
||||
|
@ -1061,11 +1061,11 @@ namespace bv {
|
|||
a.set_one(nextb);
|
||||
|
||||
rem.reserve(2 * a.nw);
|
||||
SASSERT(a.le(y, x));
|
||||
while (a.gt(y, m_zero)) {
|
||||
SASSERT(a.le(y, x));
|
||||
SASSERT(y <= x);
|
||||
while (y > m_zero) {
|
||||
SASSERT(y <= x);
|
||||
set_div(x, y, a.bw, quot, rem); // quot, rem := quot_rem(x, y)
|
||||
SASSERT(a.le(rem, y));
|
||||
SASSERT(y >= rem);
|
||||
a.set(x, y); // x := y
|
||||
a.set(y, rem); // y := rem
|
||||
a.set(aux, nexta); // aux := nexta
|
||||
|
@ -1080,6 +1080,7 @@ namespace bv {
|
|||
|
||||
a.bw = bw;
|
||||
a.nw = a.nw - 1;
|
||||
y.set_bw(0);
|
||||
// x*a + y*b = 1
|
||||
|
||||
#if Z3DEBUG
|
||||
|
@ -1098,7 +1099,7 @@ namespace bv {
|
|||
verbose_stream() << m_tmp[i];
|
||||
verbose_stream() << "\n";
|
||||
#endif
|
||||
SASSERT(b.is_one(m_tmp));
|
||||
SASSERT(m_tmp.is_one());
|
||||
#endif
|
||||
e.get(m_tmp2);
|
||||
if (parity_e > 0 && parity_b > 0)
|
||||
|
@ -1117,23 +1118,20 @@ namespace bv {
|
|||
auto inv_b = nb.pseudo_inverse(b.bw);
|
||||
rational na = mod(inv_b * ne, rational::power_of_two(a.bw));
|
||||
a.set_value(m_tmp, na);
|
||||
a.set_repair(random_bool(), m_tmp);
|
||||
#endif
|
||||
return true;
|
||||
return a.set_repair(random_bool(), m_tmp);
|
||||
#endif
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_bnot(bvval const& e, bvval& a) {
|
||||
for (unsigned i = 0; i < e.nw; ++i)
|
||||
m_tmp[i] = ~e.bits()[i];
|
||||
a.clear_overflow_bits(m_tmp);
|
||||
a.set_repair(random_bool(), m_tmp);
|
||||
return true;
|
||||
return a.set_repair(random_bool(), m_tmp);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_bneg(bvval const& e, bvval& a) {
|
||||
a.set_sub(m_tmp, m_zero, e.bits());
|
||||
a.set_repair(random_bool(), m_tmp);
|
||||
return true;
|
||||
e.set_sub(m_tmp, m_zero, e.bits());
|
||||
return a.set_repair(random_bool(), m_tmp);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
|
||||
|
@ -1147,38 +1145,35 @@ namespace bv {
|
|||
// a <=s b <-> a + p2 <=u b + p2
|
||||
|
||||
bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
|
||||
//add_p2_1(b, m_tmp4);
|
||||
a.set(m_tmp, b.bits());
|
||||
if (e) {
|
||||
a.set_repair(true, m_tmp);
|
||||
return a.set_repair(true, m_tmp);
|
||||
}
|
||||
else {
|
||||
a.set_add(m_tmp2, m_tmp, m_one);
|
||||
a.set_repair(false, m_tmp2);
|
||||
return a.set_repair(false, m_tmp2);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) {
|
||||
a.set(m_tmp, b.bits());
|
||||
if (e) {
|
||||
a.set_repair(false, m_tmp);
|
||||
return a.set_repair(false, m_tmp);
|
||||
}
|
||||
else {
|
||||
a.set_sub(m_tmp2, m_tmp, m_one);
|
||||
a.set_repair(true, m_tmp2);
|
||||
}
|
||||
return true;
|
||||
return a.set_repair(true, m_tmp2);
|
||||
}
|
||||
}
|
||||
|
||||
void sls_eval::add_p2_1(bvval const& a, svector<digit_t>& t) const {
|
||||
void sls_eval::add_p2_1(bvval const& a, bvect& t) const {
|
||||
a.set(m_zero, a.bw - 1, true);
|
||||
a.set_add(t, a.bits(), m_zero);
|
||||
a.set(m_zero, a.bw - 1, false);
|
||||
a.clear_overflow_bits(t);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_ule(bool e, bvval& a, svector<digit_t> const& t) {
|
||||
bool sls_eval::try_repair_ule(bool e, bvval& a, bvect const& t) {
|
||||
if (e) {
|
||||
if (!a.get_at_most(t, m_tmp))
|
||||
return false;
|
||||
|
@ -1192,11 +1187,10 @@ namespace bv {
|
|||
return false;
|
||||
}
|
||||
}
|
||||
a.set_repair(random_bool(), m_tmp);
|
||||
return true;
|
||||
return a.set_repair(random_bool(), m_tmp);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_uge(bool e, bvval& a, svector<digit_t> const& t) {
|
||||
bool sls_eval::try_repair_uge(bool e, bvval& a, bvect const& t) {
|
||||
if (e) {
|
||||
if (!a.get_at_least(t, m_tmp))
|
||||
return false;
|
||||
|
@ -1208,19 +1202,16 @@ namespace bv {
|
|||
if (!a.get_at_most(m_tmp2, m_tmp))
|
||||
return false;
|
||||
}
|
||||
a.set_repair(random_bool(), m_tmp);
|
||||
return true;
|
||||
return a.set_repair(random_bool(), m_tmp);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_bit2bool(bvval& a, unsigned idx) {
|
||||
a.set(m_tmp, a.bits());
|
||||
a.set(m_tmp, idx, !a.get_bit(idx));
|
||||
return a.try_set(m_tmp);
|
||||
bool sls_eval::try_repair_bit2bool(bvval& a, unsigned 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) {
|
||||
if (i == 0) {
|
||||
unsigned sh = b.to_nat(b.bits(), b.bw);
|
||||
unsigned sh = b.to_nat(b.bw);
|
||||
if (sh == 0)
|
||||
return a.try_set(e.bits());
|
||||
else if (sh >= b.bw)
|
||||
|
@ -1251,23 +1242,14 @@ namespace bv {
|
|||
|
||||
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);
|
||||
unsigned sh = b.to_nat(b.bw);
|
||||
if (sh == 0)
|
||||
return a.try_set(e.bits());
|
||||
else if (sh >= b.bw) {
|
||||
if (e.get_bit(e.bw - 1)) {
|
||||
if (!a.get_bit(a.bw - 1) && !a.get(a.fixed, a.bw - 1))
|
||||
a.set_bit(a.bw - 1, true);
|
||||
else
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
if (a.get_bit(a.bw - 1) && !a.get(a.fixed, a.bw - 1))
|
||||
a.set_bit(a.bw - 1, false);
|
||||
else
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
if (e.get_bit(e.bw - 1))
|
||||
return a.try_set_bit(a.bw - 1, true);
|
||||
else
|
||||
return a.try_set_bit(a.bw - 1, false);
|
||||
}
|
||||
else {
|
||||
// e = a >> sh
|
||||
|
@ -1289,7 +1271,6 @@ namespace bv {
|
|||
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) {
|
||||
|
@ -1303,7 +1284,7 @@ namespace bv {
|
|||
|
||||
bool sls_eval::try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
if (i == 0) {
|
||||
if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones())
|
||||
if (e.is_zero() && a.fixed.is_ones() && a.is_ones())
|
||||
return false;
|
||||
if (b.is_zero())
|
||||
return false;
|
||||
|
@ -1311,14 +1292,13 @@ namespace bv {
|
|||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
m_tmp[i] = ~a.fixed[i] | a.bits()[i];
|
||||
a.clear_overflow_bits(m_tmp);
|
||||
if (a.lt(m_tmp, e.bits()))
|
||||
if (e.bits() > m_tmp)
|
||||
return false;
|
||||
}
|
||||
// e = 1 => a := b
|
||||
if (e.is_one()) {
|
||||
a.set(m_tmp, b.bits());
|
||||
a.set_repair(false, m_tmp);
|
||||
return true;
|
||||
return a.set_repair(false, m_tmp);
|
||||
}
|
||||
// b * e + r = a
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
|
@ -1331,25 +1311,23 @@ namespace bv {
|
|||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
m_tmp2[i] = random_bits();
|
||||
b.clear_overflow_bits(m_tmp2);
|
||||
while (b.gt(m_tmp2, b.bits()))
|
||||
while (b.bits() < m_tmp2)
|
||||
b.set(m_tmp2, b.msb(m_tmp2), false);
|
||||
while (a.set_add(m_tmp3, m_tmp, m_tmp2))
|
||||
b.set(m_tmp2, b.msb(m_tmp2), false);
|
||||
a.set_repair(true, m_tmp3);
|
||||
return a.set_repair(true, m_tmp3);
|
||||
}
|
||||
else {
|
||||
if (e.is_one() && a.is_zero()) {
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
m_tmp[i] = random_bits();
|
||||
a.clear_overflow_bits(m_tmp);
|
||||
b.set_repair(true, m_tmp);
|
||||
return true;
|
||||
return b.set_repair(true, m_tmp);
|
||||
}
|
||||
if (e.is_one()) {
|
||||
b.set(m_tmp, a.bits());
|
||||
b.set_repair(true, m_tmp);
|
||||
return true;
|
||||
}
|
||||
a.set(m_tmp, a.bits());
|
||||
return b.set_repair(true, m_tmp);
|
||||
}
|
||||
|
||||
// e * b + r = a
|
||||
// b = (a - r) udiv e
|
||||
|
@ -1358,13 +1336,12 @@ namespace bv {
|
|||
m_tmp[i] = random_bits();
|
||||
a.clear_overflow_bits(m_tmp);
|
||||
// ensure r <= m
|
||||
while (a.lt(a.bits(), m_tmp))
|
||||
while (a.bits() < m_tmp)
|
||||
a.set(m_tmp, a.msb(m_tmp), false);
|
||||
a.set_sub(m_tmp2, a.bits(), m_tmp);
|
||||
set_div(m_tmp2, e.bits(), a.bw, m_tmp3, m_tmp4);
|
||||
b.set_repair(random_bool(), m_tmp4);
|
||||
return b.set_repair(random_bool(), m_tmp4);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// table III in Niemetz et al
|
||||
|
@ -1405,8 +1382,7 @@ namespace bv {
|
|||
b.set(m_tmp, i, false);
|
||||
}
|
||||
a.set_add(m_tmp3, m_tmp2, e.bits());
|
||||
a.set_repair(random_bool(), m_tmp3);
|
||||
return true;
|
||||
return a.set_repair(random_bool(), m_tmp3);
|
||||
}
|
||||
else {
|
||||
// a urem b = e: b*y + e = a
|
||||
|
@ -1421,19 +1397,18 @@ namespace bv {
|
|||
a.set_sub(m_tmp2, a.bits(), e.bits());
|
||||
set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4);
|
||||
a.clear_overflow_bits(m_tmp3);
|
||||
b.set_repair(random_bool(), m_tmp3);
|
||||
return true;
|
||||
return b.set_repair(random_bool(), m_tmp3);
|
||||
}
|
||||
}
|
||||
|
||||
bool sls_eval::add_overflow_on_fixed(bvval const& a, svector<digit_t> const& t) {
|
||||
bool sls_eval::add_overflow_on_fixed(bvval const& a, bvect const& t) {
|
||||
a.set(m_tmp3, m_zero);
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
m_tmp3[i] = a.fixed[i] & a.bits()[i];
|
||||
return a.set_add(m_tmp4, t, m_tmp3);
|
||||
}
|
||||
|
||||
bool sls_eval::mul_overflow_on_fixed(bvval const& a, svector<digit_t> const& t) {
|
||||
bool sls_eval::mul_overflow_on_fixed(bvval const& a, bvect const& t) {
|
||||
a.set(m_tmp3, m_zero);
|
||||
for (unsigned i = 0; i < a.nw; ++i)
|
||||
m_tmp3[i] = a.fixed[i] & a.bits()[i];
|
||||
|
@ -1453,8 +1428,7 @@ namespace bv {
|
|||
|
||||
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);
|
||||
rational n = b.get_value();
|
||||
n = mod(n, rational(b.bw));
|
||||
return try_repair_rotate_left(e, a, n.get_unsigned());
|
||||
}
|
||||
|
@ -1469,8 +1443,7 @@ namespace bv {
|
|||
|
||||
bool sls_eval::try_repair_rotate_right(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
if (i == 0) {
|
||||
rational n;
|
||||
b.get_value(b.bits(), n);
|
||||
rational n = b.get_value();
|
||||
n = mod(b.bw - n, rational(b.bw));
|
||||
return try_repair_rotate_left(e, a, n.get_unsigned());
|
||||
}
|
||||
|
@ -1478,8 +1451,7 @@ namespace bv {
|
|||
SASSERT(i == 1);
|
||||
unsigned sh = m_rand(b.bw);
|
||||
b.set(m_tmp, sh);
|
||||
b.set_repair(random_bool(), m_tmp);
|
||||
return true;
|
||||
return b.set_repair(random_bool(), m_tmp);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1488,32 +1460,32 @@ namespace bv {
|
|||
// maximize
|
||||
if (i == 0) {
|
||||
a.max_feasible(m_tmp);
|
||||
a.set_repair(false, m_tmp);
|
||||
return a.set_repair(false, m_tmp);
|
||||
}
|
||||
else {
|
||||
b.max_feasible(m_tmp);
|
||||
b.set_repair(false, m_tmp);
|
||||
return b.set_repair(false, m_tmp);
|
||||
}
|
||||
}
|
||||
else {
|
||||
// minimize
|
||||
if (i == 0) {
|
||||
a.min_feasible(m_tmp);
|
||||
a.set_repair(true, m_tmp);
|
||||
return a.set_repair(true, m_tmp);
|
||||
}
|
||||
else {
|
||||
b.min_feasible(m_tmp);
|
||||
b.set_repair(true, m_tmp);
|
||||
return b.set_repair(true, m_tmp);
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_zero_ext(bvval const& e, bvval& a) {
|
||||
bool change = false;
|
||||
for (unsigned i = 0; i < a.bw; ++i)
|
||||
if (!a.get(a.fixed, i))
|
||||
a.set_bit(i, e.get_bit(i));
|
||||
return true;
|
||||
if (a.try_set_bit(i, e.get_bit(i)))
|
||||
change = true;
|
||||
return change;
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i) {
|
||||
|
@ -1532,16 +1504,15 @@ namespace bv {
|
|||
}
|
||||
|
||||
bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) {
|
||||
bool change = false;
|
||||
for (unsigned i = 0; i < e.bw; ++i)
|
||||
if (a.get(a.fixed, i + lo) && a.get_bit(i + lo) != e.get_bit(i))
|
||||
return false;
|
||||
for (unsigned i = 0; i < e.bw; ++i)
|
||||
a.set_bit(i + lo, e.get_bit(i));
|
||||
return true;
|
||||
if (a.try_set_bit(i + lo, e.get_bit(i)))
|
||||
change = true;
|
||||
return change;
|
||||
}
|
||||
|
||||
void sls_eval::set_div(svector<digit_t> const& a, svector<digit_t> const& b, unsigned bw,
|
||||
svector<digit_t>& quot, svector<digit_t>& rem) const {
|
||||
void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw,
|
||||
bvect& quot, bvect& rem) const {
|
||||
unsigned nw = (bw + 8 * sizeof(digit_t) - 1) / (8 * sizeof(digit_t));
|
||||
unsigned bnw = nw;
|
||||
while (bnw > 1 && b[bnw - 1] == 0)
|
||||
|
|
|
@ -40,8 +40,8 @@ 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_tmp3, m_tmp4, m_zero, m_one, m_minus_one;
|
||||
svector<digit_t> m_a, m_b, m_nextb, m_nexta, m_aux;
|
||||
mutable bvect m_tmp, m_tmp2, m_tmp3, m_tmp4, m_zero, m_one, m_minus_one;
|
||||
bvect m_a, m_b, m_nextb, m_nexta, m_aux;
|
||||
|
||||
using bvval = sls_valuation;
|
||||
|
||||
|
@ -91,18 +91,18 @@ namespace bv {
|
|||
bool try_repair_rotate_left(bvval 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_right(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_ule(bool e, bvval& a, svector<digit_t> const& t);
|
||||
bool try_repair_uge(bool e, bvval& a, svector<digit_t> 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_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_zero_ext(bvval const& e, bvval& a);
|
||||
bool try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i);
|
||||
bool try_repair_extract(bvval const& e, bvval& a, unsigned lo);
|
||||
void add_p2_1(bvval const& a, svector<digit_t>& t) const;
|
||||
void add_p2_1(bvval const& a, bvect& t) const;
|
||||
|
||||
bool add_overflow_on_fixed(bvval const& a, svector<digit_t> const& t);
|
||||
bool mul_overflow_on_fixed(bvval const& a, svector<digit_t> const& t);
|
||||
void set_div(svector<digit_t> const& a, svector<digit_t> const& b, unsigned nw,
|
||||
svector<digit_t>& quot, svector<digit_t>& rem) const;
|
||||
bool add_overflow_on_fixed(bvval const& a, bvect const& t);
|
||||
bool mul_overflow_on_fixed(bvval const& a, bvect const& t);
|
||||
void set_div(bvect const& a, bvect const& b, unsigned nw,
|
||||
bvect& quot, bvect& rem) const;
|
||||
|
||||
digit_t random_bits();
|
||||
bool random_bool() { return m_rand() % 2 == 0; }
|
||||
|
|
|
@ -110,7 +110,7 @@ namespace bv {
|
|||
}
|
||||
else if (bv.is_bit2bool(e, s, idx)) {
|
||||
auto& val = wval0(s);
|
||||
val.set_bit(idx, !sign);
|
||||
val.try_set_bit(idx, !sign);
|
||||
val.set(val.fixed, idx, true);
|
||||
val.init_fixed();
|
||||
}
|
||||
|
@ -259,6 +259,17 @@ namespace bv {
|
|||
case OP_BADD: {
|
||||
auto& a = wval0(e->get_arg(0));
|
||||
auto& b = wval0(e->get_arg(1));
|
||||
rational r;
|
||||
if (bv.is_numeral(e->get_arg(0), r) && b.has_range()) {
|
||||
auto rlo = b.get_lo();
|
||||
auto rhi = b.get_hi();
|
||||
v.add_range(r + rlo, r + rhi);
|
||||
}
|
||||
if (bv.is_numeral(e->get_arg(1), r) && a.has_range()) {
|
||||
auto rlo = a.get_lo();
|
||||
auto rhi = a.get_hi();
|
||||
v.add_range(r + rlo, r + rhi);
|
||||
}
|
||||
bool pfixed = true;
|
||||
for (unsigned i = 0; i < v.bw; ++i) {
|
||||
if (pfixed && a.get(a.fixed, i) && b.get(b.fixed, i))
|
||||
|
@ -273,17 +284,7 @@ namespace bv {
|
|||
v.set(v.fixed, i, false);
|
||||
}
|
||||
}
|
||||
rational r, rlo, rhi;
|
||||
if (bv.is_numeral(e->get_arg(0), r) && !b.eq(b.lo, b.hi)) {
|
||||
b.get_value(b.lo, rlo);
|
||||
b.get_value(b.hi, rhi);
|
||||
v.add_range(r + rlo, r + rhi);
|
||||
}
|
||||
if (bv.is_numeral(e->get_arg(1), r) && !a.eq(a.lo, a.hi)) {
|
||||
a.get_value(a.lo, rlo);
|
||||
a.get_value(a.hi, rhi);
|
||||
v.add_range(r + rlo, r + rhi);
|
||||
}
|
||||
|
||||
break;
|
||||
}
|
||||
case OP_BMUL: {
|
||||
|
|
|
@ -22,12 +22,73 @@ Author:
|
|||
|
||||
namespace bv {
|
||||
|
||||
sls_valuation::sls_valuation(unsigned bw): bw(bw) {
|
||||
void bvect::set_bw(unsigned bw) {
|
||||
this->bw = bw;
|
||||
nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t));
|
||||
lo.reserve(nw + 1);
|
||||
hi.reserve(nw + 1);
|
||||
m_bits.reserve(nw + 1);
|
||||
fixed.reserve(nw + 1);
|
||||
mask = (1 << (bw % (8 * sizeof(digit_t)))) - 1;
|
||||
if (mask == 0)
|
||||
mask = ~(digit_t)0;
|
||||
reserve(nw + 1);
|
||||
}
|
||||
|
||||
void bvect::clear_overflow_bits() {
|
||||
SASSERT(nw > 0);
|
||||
(*this)[nw - 1] &= mask;
|
||||
SASSERT(!has_overflow());
|
||||
}
|
||||
|
||||
void bvect::set_sub(bvect const& a, bvect const& b) {
|
||||
digit_t c;
|
||||
mpn_manager().sub(a.data(), a.nw, b.data(), a.nw, data(), &c);
|
||||
set_bw(bw);
|
||||
clear_overflow_bits();
|
||||
}
|
||||
|
||||
bool operator==(bvect const& a, bvect const& b) {
|
||||
SASSERT(a.nw > 0);
|
||||
SASSERT(!a.has_overflow());
|
||||
SASSERT(!b.has_overflow());
|
||||
return 0 == mpn_manager().compare(a.data(), a.nw, b.data(), a.nw);
|
||||
}
|
||||
|
||||
bool operator<(bvect const& a, bvect const& b) {
|
||||
SASSERT(a.nw > 0);
|
||||
SASSERT(!a.has_overflow());
|
||||
SASSERT(!b.has_overflow());
|
||||
return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) < 0;
|
||||
}
|
||||
|
||||
bool operator>(bvect const& a, bvect const& b) {
|
||||
SASSERT(a.nw > 0);
|
||||
SASSERT(!a.has_overflow());
|
||||
SASSERT(!b.has_overflow());
|
||||
return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) > 0;
|
||||
}
|
||||
|
||||
bool operator<=(bvect const& a, bvect const& b) {
|
||||
SASSERT(a.nw > 0);
|
||||
SASSERT(!a.has_overflow());
|
||||
SASSERT(!b.has_overflow());
|
||||
return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) <= 0;
|
||||
}
|
||||
|
||||
bool operator>=(bvect const& a, bvect const& b) {
|
||||
SASSERT(a.nw > 0);
|
||||
SASSERT(!a.has_overflow());
|
||||
SASSERT(!b.has_overflow());
|
||||
return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) >= 0;
|
||||
}
|
||||
|
||||
|
||||
sls_valuation::sls_valuation(unsigned bw) : bw(bw) {
|
||||
nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t));
|
||||
mask = (1 << (bw % (8 * sizeof(digit_t)))) - 1;
|
||||
if (mask == 0)
|
||||
mask = ~(digit_t)0;
|
||||
lo.set_bw(bw);
|
||||
hi.set_bw(bw);
|
||||
m_bits.set_bw(bw);
|
||||
fixed.set_bw(bw);
|
||||
// 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, m_bits[i] = 0, fixed[i] = 0;
|
||||
|
@ -35,8 +96,8 @@ namespace bv {
|
|||
set(fixed, i, true);
|
||||
}
|
||||
|
||||
bool sls_valuation::in_range(svector<digit_t> const& bits) const {
|
||||
mpn_manager m;
|
||||
bool sls_valuation::in_range(bvect const& bits) const {
|
||||
mpn_manager m;
|
||||
auto c = m.compare(lo.data(), nw, hi.data(), nw);
|
||||
SASSERT(!has_overflow(bits));
|
||||
// full range
|
||||
|
@ -53,39 +114,6 @@ namespace bv {
|
|||
m.compare(bits.data(), nw, hi.data(), nw) < 0;
|
||||
}
|
||||
|
||||
bool sls_valuation::eq(svector<digit_t> const& a, svector<digit_t> const& b) const {
|
||||
SASSERT(!has_overflow(a));
|
||||
SASSERT(!has_overflow(b));
|
||||
return 0 == memcmp(a.data(), b.data(), num_bytes());
|
||||
}
|
||||
|
||||
bool sls_valuation::gt(svector<digit_t> const& a, svector<digit_t> const& b) const {
|
||||
SASSERT(!has_overflow(a));
|
||||
SASSERT(!has_overflow(b));
|
||||
mpn_manager m;
|
||||
return m.compare(a.data(), nw, b.data(), nw) > 0;
|
||||
}
|
||||
|
||||
bool sls_valuation::lt(svector<digit_t> const& a, svector<digit_t> const& b) const {
|
||||
SASSERT(!has_overflow(a));
|
||||
SASSERT(!has_overflow(b));
|
||||
mpn_manager m;
|
||||
return m.compare(a.data(), nw, b.data(), nw) < 0;
|
||||
}
|
||||
|
||||
bool sls_valuation::le(svector<digit_t> const& a, svector<digit_t> const& b) const {
|
||||
SASSERT(!has_overflow(a));
|
||||
SASSERT(!has_overflow(b));
|
||||
mpn_manager m;
|
||||
return m.compare(a.data(), nw, b.data(), nw) <= 0;
|
||||
}
|
||||
|
||||
void sls_valuation::clear_overflow_bits(svector<digit_t>& bits) const {
|
||||
for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i)
|
||||
set(bits, i, false);
|
||||
SASSERT(!has_overflow(bits));
|
||||
}
|
||||
|
||||
//
|
||||
// largest dst <= src and dst is feasible
|
||||
// set dst := src & (~fixed | bits)
|
||||
|
@ -100,7 +128,7 @@ namespace bv {
|
|||
// set dst := hi - 1
|
||||
//
|
||||
|
||||
bool sls_valuation::get_at_most(svector<digit_t> const& src, svector<digit_t>& dst) const {
|
||||
bool sls_valuation::get_at_most(bvect const& src, bvect& dst) const {
|
||||
SASSERT(!has_overflow(src));
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
dst[i] = src[i] & (~fixed[i] | m_bits[i]);
|
||||
|
@ -137,7 +165,7 @@ namespace bv {
|
|||
// if hi <= dst < lo
|
||||
// set dst := lo
|
||||
//
|
||||
bool sls_valuation::get_at_least(svector<digit_t> const& src, svector<digit_t>& dst) const {
|
||||
bool sls_valuation::get_at_least(bvect const& src, bvect& dst) const {
|
||||
SASSERT(!has_overflow(src));
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
dst[i] = (~fixed[i] & src[i]) | (fixed[i] & m_bits[i]);
|
||||
|
@ -161,51 +189,52 @@ namespace bv {
|
|||
return round_up(dst);
|
||||
}
|
||||
|
||||
bool sls_valuation::round_up(svector<digit_t>& dst) const {
|
||||
if (lt(lo, hi)) {
|
||||
if (le(hi, dst))
|
||||
bool sls_valuation::round_up(bvect& dst) const {
|
||||
if (lo < hi) {
|
||||
if (hi <= dst)
|
||||
return false;
|
||||
if (lt(dst, lo))
|
||||
if (lo > dst)
|
||||
set(dst, lo);
|
||||
}
|
||||
else if (le(hi, dst) && lt(dst, lo))
|
||||
else if (hi <= dst && lo > dst)
|
||||
set(dst, lo);
|
||||
SASSERT(!has_overflow(dst));
|
||||
return true;
|
||||
}
|
||||
|
||||
bool sls_valuation::round_down(svector<digit_t>& dst) const {
|
||||
if (lt(lo, hi)) {
|
||||
if (lt(dst, lo))
|
||||
bool sls_valuation::round_down(bvect& dst) const {
|
||||
if (lo < hi) {
|
||||
if (lo > dst)
|
||||
return false;
|
||||
if (le(hi, dst)) {
|
||||
if (hi <= dst) {
|
||||
set(dst, hi);
|
||||
sub1(dst);
|
||||
}
|
||||
}
|
||||
else if (le(hi, dst) && lt(dst, lo)) {
|
||||
else if (hi <= dst && lo > dst) {
|
||||
set(dst, hi);
|
||||
sub1(dst);
|
||||
}
|
||||
SASSERT(!has_overflow(dst));
|
||||
SASSERT(well_formed());
|
||||
return true;
|
||||
}
|
||||
|
||||
bool sls_valuation::set_repair(bool try_down, svector<digit_t>& dst) {
|
||||
bool sls_valuation::set_repair(bool try_down, bvect& dst) {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
|
||||
bool ok = try_down ? round_down(dst) : round_up(dst);
|
||||
if (!ok)
|
||||
VERIFY(try_down ? round_up(dst) : round_down(dst));
|
||||
if (eq(m_bits, 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]))););
|
||||
if (m_bits == dst)
|
||||
return false;
|
||||
set(m_bits, dst);
|
||||
SASSERT(!has_overflow(dst));
|
||||
SASSERT(well_formed());
|
||||
return true;
|
||||
}
|
||||
|
||||
void sls_valuation::min_feasible(svector<digit_t>& out) const {
|
||||
if (gt(hi, lo)) {
|
||||
void sls_valuation::min_feasible(bvect& out) const {
|
||||
if (lo < hi) {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
out[i] = lo[i];
|
||||
}
|
||||
|
@ -216,8 +245,8 @@ namespace bv {
|
|||
SASSERT(!has_overflow(out));
|
||||
}
|
||||
|
||||
void sls_valuation::max_feasible(svector<digit_t>& out) const {
|
||||
if (gt(hi, lo)) {
|
||||
void sls_valuation::max_feasible(bvect& out) const {
|
||||
if (lo < hi) {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
out[i] = hi[i];
|
||||
sub1(out);
|
||||
|
@ -229,53 +258,49 @@ namespace bv {
|
|||
SASSERT(!has_overflow(out));
|
||||
}
|
||||
|
||||
unsigned sls_valuation::msb(svector<digit_t> const& src) const {
|
||||
unsigned sls_valuation::msb(bvect const& src) const {
|
||||
SASSERT(!has_overflow(src));
|
||||
for (unsigned i = nw; i-- > 0; )
|
||||
for (unsigned i = nw; i-- > 0; )
|
||||
if (src[i] != 0)
|
||||
return i * 8 * sizeof(digit_t) + log2(src[i]);
|
||||
return i * 8 * sizeof(digit_t) + log2(src[i]);
|
||||
return bw;
|
||||
}
|
||||
|
||||
void sls_valuation::set_value(svector<digit_t>& bits, rational const& n) {
|
||||
for (unsigned i = 0; i < bw; ++i)
|
||||
set(bits, i, n.get_bit(i));
|
||||
void sls_valuation::set_value(bvect& bits, rational const& n) {
|
||||
for (unsigned i = 0; i < bw; ++i)
|
||||
bits.set(i, n.get_bit(i));
|
||||
clear_overflow_bits(bits);
|
||||
}
|
||||
|
||||
void sls_valuation::get_value(svector<digit_t> const& bits, rational& r) const {
|
||||
rational p(1);
|
||||
r = 0;
|
||||
rational sls_valuation::get_value(bvect const& bits) const {
|
||||
rational p(1), r(0);
|
||||
for (unsigned i = 0; i < nw; ++i) {
|
||||
r += p * rational(bits[i]);
|
||||
p *= rational::power_of_two(8*sizeof(digit_t));
|
||||
p *= rational::power_of_two(8 * sizeof(digit_t));
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
void sls_valuation::get(svector<digit_t>& dst) const {
|
||||
void sls_valuation::get(bvect& dst) const {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
dst[i] = m_bits[i];
|
||||
}
|
||||
|
||||
void sls_valuation::set1(svector<digit_t>& bits) {
|
||||
for (unsigned i = 0; i < bw; ++i)
|
||||
set(bits, i, true);
|
||||
}
|
||||
|
||||
//
|
||||
// new_bits != bits => ~fixed
|
||||
// 0 = (new_bits ^ bits) & fixed
|
||||
// also check that new_bits are in range
|
||||
//
|
||||
bool sls_valuation::can_set(svector<digit_t> const& new_bits) const {
|
||||
bool sls_valuation::can_set(bvect const& new_bits) const {
|
||||
SASSERT(!has_overflow(new_bits));
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
if (0 != ((new_bits[i] ^ m_bits[i]) & fixed[i]))
|
||||
return false;
|
||||
return false;
|
||||
return in_range(new_bits);
|
||||
}
|
||||
|
||||
unsigned sls_valuation::to_nat(svector<digit_t> const& d, unsigned max_n) {
|
||||
unsigned sls_valuation::to_nat(unsigned max_n) {
|
||||
bvect const& d = m_bits;
|
||||
SASSERT(!has_overflow(d));
|
||||
SASSERT(max_n < UINT_MAX / 2);
|
||||
unsigned p = 1;
|
||||
|
@ -287,34 +312,36 @@ namespace bv {
|
|||
return max_n;
|
||||
return value;
|
||||
}
|
||||
if (get(d, i))
|
||||
value += p;
|
||||
if (get(d, i))
|
||||
value += p;
|
||||
p <<= 1;
|
||||
}
|
||||
return value;
|
||||
}
|
||||
|
||||
void sls_valuation::shift_right(svector<digit_t>& out, unsigned shift) const {
|
||||
void sls_valuation::shift_right(bvect& out, unsigned shift) const {
|
||||
SASSERT(shift < bw);
|
||||
for (unsigned i = 0; i < bw; ++i)
|
||||
set(out, i, i + shift < bw ? get(m_bits, i + shift) : false);
|
||||
SASSERT(!has_overflow(out));
|
||||
SASSERT(well_formed());
|
||||
}
|
||||
|
||||
void sls_valuation::add_range(rational l, rational h) {
|
||||
|
||||
l = mod(l, rational::power_of_two(bw));
|
||||
h = mod(h, rational::power_of_two(bw));
|
||||
if (h == l)
|
||||
return;
|
||||
|
||||
if (eq(lo, hi)) {
|
||||
|
||||
SASSERT(is_zero(fixed)); // ranges can only be added before fixed bits are set.
|
||||
|
||||
if (lo == hi) {
|
||||
set_value(lo, l);
|
||||
set_value(hi, h);
|
||||
}
|
||||
else {
|
||||
rational old_lo, old_hi;
|
||||
get_value(lo, old_lo);
|
||||
get_value(hi, old_hi);
|
||||
else {
|
||||
auto old_lo = get_value(lo);
|
||||
auto old_hi = get_value(hi);
|
||||
if (old_lo < old_hi) {
|
||||
if (old_lo < l && l < old_hi)
|
||||
set_value(lo, l),
|
||||
|
@ -332,10 +359,12 @@ namespace bv {
|
|||
else if (old_hi < old_lo && (h < old_hi || old_lo < h))
|
||||
set_value(hi, h);
|
||||
}
|
||||
}
|
||||
}
|
||||
SASSERT(!has_overflow(lo));
|
||||
SASSERT(!has_overflow(hi));
|
||||
init_fixed();
|
||||
if (!in_range(m_bits))
|
||||
set(m_bits, lo);
|
||||
SASSERT(well_formed());
|
||||
}
|
||||
|
||||
//
|
||||
|
@ -352,7 +381,7 @@ namespace bv {
|
|||
// lo < hi, set most significant bits based on hi
|
||||
//
|
||||
void sls_valuation::init_fixed() {
|
||||
if (eq(lo, hi))
|
||||
if (lo == hi)
|
||||
return;
|
||||
for (unsigned i = bw; i-- > 0; ) {
|
||||
if (!get(fixed, i))
|
||||
|
@ -370,8 +399,8 @@ namespace bv {
|
|||
}
|
||||
break;
|
||||
}
|
||||
svector<digit_t> hi1(nw + 1, (unsigned)0);
|
||||
svector<digit_t> one(nw + 1, (unsigned)0);
|
||||
bvect hi1(nw + 1);
|
||||
bvect one(nw + 1);
|
||||
one[0] = 1;
|
||||
digit_t c;
|
||||
mpn_manager().sub(hi.data(), nw, one.data(), nw, hi1.data(), &c);
|
||||
|
@ -401,14 +430,14 @@ namespace bv {
|
|||
set(fixed, i, true);
|
||||
set(m_bits, i, b);
|
||||
}
|
||||
};
|
||||
};
|
||||
|
||||
// set most significant bits
|
||||
if (lt(lo, hi)) {
|
||||
if (lo < hi) {
|
||||
unsigned i = bw;
|
||||
for (; i-- > 0 && !get(hi, i); )
|
||||
for (; i-- > 0 && !get(hi, i); )
|
||||
set_fixed_bit(i, false);
|
||||
|
||||
|
||||
if (is_power_of2(hi))
|
||||
set_fixed_bit(i, false);
|
||||
}
|
||||
|
@ -416,30 +445,31 @@ namespace bv {
|
|||
// lo + 1 = hi: then bits = lo
|
||||
mpn_manager().add(lo.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c);
|
||||
clear_overflow_bits(hi1);
|
||||
if (eq(hi1, hi)) {
|
||||
if (hi == hi1) {
|
||||
for (unsigned i = 0; i < bw; ++i)
|
||||
set_fixed_bit(i, get(lo, i));
|
||||
set_fixed_bit(i, get(lo, i));
|
||||
}
|
||||
SASSERT(!has_overflow(m_bits));
|
||||
SASSERT(well_formed());
|
||||
}
|
||||
|
||||
void sls_valuation::set_sub(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const {
|
||||
void sls_valuation::set_sub(bvect& out, bvect const& a, bvect const& b) const {
|
||||
digit_t c;
|
||||
mpn_manager().sub(a.data(), nw, b.data(), nw, out.data(), &c);
|
||||
clear_overflow_bits(out);
|
||||
out.set_bw(bw);
|
||||
}
|
||||
|
||||
bool sls_valuation::set_add(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const {
|
||||
bool sls_valuation::set_add(bvect& out, bvect const& a, bvect const& b) const {
|
||||
digit_t c;
|
||||
mpn_manager().add(a.data(), nw, b.data(), nw, out.data(), nw + 1, &c);
|
||||
bool ovfl = out[nw] != 0 || has_overflow(out);
|
||||
clear_overflow_bits(out);
|
||||
out.set_bw(bw);
|
||||
return ovfl;
|
||||
}
|
||||
|
||||
bool sls_valuation::set_mul(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b, bool check_overflow) const {
|
||||
bool sls_valuation::set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow) const {
|
||||
mpn_manager().mul(a.data(), nw, b.data(), nw, out.data());
|
||||
|
||||
bool ovfl = false;
|
||||
if (check_overflow) {
|
||||
ovfl = has_overflow(out);
|
||||
|
@ -447,14 +477,33 @@ namespace bv {
|
|||
ovfl |= out[i] != 0;
|
||||
}
|
||||
clear_overflow_bits(out);
|
||||
out.set_bw(bw);
|
||||
return ovfl;
|
||||
}
|
||||
|
||||
bool sls_valuation::is_power_of2(svector<digit_t> const& src) const {
|
||||
bool sls_valuation::is_power_of2(bvect const& src) const {
|
||||
unsigned c = 0;
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
c += get_num_1bits(src[i]);
|
||||
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;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
|
@ -27,124 +27,195 @@ Author:
|
|||
|
||||
namespace bv {
|
||||
|
||||
|
||||
|
||||
class bvect : public svector<digit_t> {
|
||||
unsigned bw = 0;
|
||||
unsigned nw = 0;
|
||||
unsigned mask = 0;
|
||||
public:
|
||||
bvect() {}
|
||||
bvect(unsigned sz): svector(sz, (unsigned)0) {}
|
||||
void set_bw(unsigned bw);
|
||||
|
||||
void clear_overflow_bits();
|
||||
void set_sub(bvect const& a, bvect const& b);
|
||||
|
||||
bool is_one() const {
|
||||
SASSERT(bw > 0);
|
||||
SASSERT(!has_overflow());
|
||||
for (unsigned i = 1; i < nw; ++i)
|
||||
if (0 != (*this)[i])
|
||||
return false;
|
||||
return 1 == (*this)[0];
|
||||
}
|
||||
|
||||
bool is_ones() const {
|
||||
SASSERT(bw > 0);
|
||||
auto const& a = *this;
|
||||
for (unsigned i = 0; i + 1 < nw; ++i)
|
||||
if (0 != ~a[i])
|
||||
return false;
|
||||
return ((~a[nw - 1]) & mask) == 0;
|
||||
}
|
||||
|
||||
bool is_zero() const {
|
||||
SASSERT(bw > 0);
|
||||
auto const& a = *this;
|
||||
for (unsigned i = 0; i + 1 < nw; ++i)
|
||||
if (a[i] != 0)
|
||||
return false;
|
||||
return (a[nw - 1] & mask) == 0;
|
||||
}
|
||||
|
||||
bool has_overflow() const {
|
||||
SASSERT(bw > 0);
|
||||
for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i)
|
||||
if (get(i))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool get(unsigned bit_idx) const {
|
||||
return (get_bit_word(bit_idx) & get_pos_mask(bit_idx)) != 0;
|
||||
}
|
||||
|
||||
|
||||
unsigned parity() const {
|
||||
SASSERT(bw > 0);
|
||||
SASSERT(!has_overflow());
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
if ((*this)[i] != 0)
|
||||
return (8 * sizeof(digit_t) * i) + trailing_zeros((*this)[i]);
|
||||
return bw;
|
||||
}
|
||||
|
||||
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);
|
||||
|
||||
private:
|
||||
|
||||
static digit_t get_pos_mask(unsigned bit_idx) {
|
||||
return (digit_t)1 << (digit_t)(bit_idx % (8 * sizeof(digit_t)));
|
||||
}
|
||||
|
||||
digit_t get_bit_word(unsigned bit_idx) const {
|
||||
return (*this)[bit_idx / (8 * sizeof(digit_t))];
|
||||
}
|
||||
|
||||
digit_t& get_bit_word(unsigned bit_idx) {
|
||||
return (*this)[bit_idx / (8 * sizeof(digit_t))];
|
||||
}
|
||||
};
|
||||
|
||||
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);
|
||||
bool operator>(bvect const& a, bvect const& b);
|
||||
inline bool operator!=(bvect const& a, bvect const& b) { return !(a == b); }
|
||||
|
||||
class sls_valuation {
|
||||
protected:
|
||||
svector<digit_t> m_bits;
|
||||
bvect m_bits;
|
||||
bvect lo, hi; // range assignment to bit-vector, as wrap-around interval
|
||||
|
||||
unsigned mask;
|
||||
rational get_value(bvect const& bits) const;
|
||||
bool round_up(bvect& dst) const;
|
||||
bool round_down(bvect& dst) const;
|
||||
|
||||
std::ostream& print_bits(std::ostream& out, bvect const& bits) const;
|
||||
|
||||
|
||||
public:
|
||||
unsigned bw; // bit-width
|
||||
unsigned nw; // num words
|
||||
svector<digit_t> lo, hi; // range assignment to bit-vector, as wrap-around interval
|
||||
svector<digit_t> fixed; // bit assignment and don't care bit
|
||||
bvect fixed; // bit assignment and don't care bit
|
||||
sls_valuation(unsigned bw);
|
||||
|
||||
unsigned num_bytes() const { return (bw + 7) / 8; }
|
||||
|
||||
digit_t bits(unsigned i) const { return m_bits[i]; }
|
||||
svector<digit_t> const& bits() const { return m_bits; }
|
||||
bvect const& bits() const { return m_bits; }
|
||||
|
||||
bool get_bit(unsigned i) const { return get(m_bits, i); }
|
||||
bool try_set_bit(unsigned i, bool b) {
|
||||
if (get(fixed, i) && get_bit(i) != b)
|
||||
return false;
|
||||
set(m_bits, i, b);
|
||||
return true;
|
||||
}
|
||||
|
||||
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 set_value(bvect& bits, rational const& r);
|
||||
|
||||
rational get_value() const { return get_value(m_bits); }
|
||||
rational get_lo() const { return get_value(lo); }
|
||||
rational get_hi() const { return get_value(hi); }
|
||||
|
||||
void get(bvect& dst) const;
|
||||
void add_range(rational lo, rational hi);
|
||||
bool has_range() const { return lo != hi; }
|
||||
void init_fixed();
|
||||
void set1(svector<digit_t>& bits);
|
||||
|
||||
void clear_overflow_bits(svector<digit_t>& bits) const;
|
||||
bool in_range(svector<digit_t> const& bits) const;
|
||||
bool can_set(svector<digit_t> const& bits) const;
|
||||
void clear_overflow_bits(bvect& bits) const { bits.clear_overflow_bits(); }
|
||||
bool in_range(bvect const& bits) const;
|
||||
bool can_set(bvect const& bits) const;
|
||||
|
||||
bool eq(sls_valuation const& other) const { return eq(other.m_bits); }
|
||||
bool eq(bvect const& other) const { return other == m_bits; }
|
||||
|
||||
bool eq(svector<digit_t> const& other) const { return eq(other, m_bits); }
|
||||
bool eq(svector<digit_t> const& a, svector<digit_t> const& b) const;
|
||||
bool gt(svector<digit_t> const& a, svector<digit_t> const& b) const;
|
||||
bool lt(svector<digit_t> const& a, svector<digit_t> const& b) const;
|
||||
bool le(svector<digit_t> const& a, svector<digit_t> const& b) const;
|
||||
bool is_zero() const { return m_bits.is_zero(); }
|
||||
bool is_zero(bvect const& a) const { return a.is_zero(); }
|
||||
|
||||
bool is_zero() const { return is_zero(m_bits); }
|
||||
bool is_zero(svector<digit_t> const& a) const {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
if (a[i] != 0)
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
bool is_ones() const { return is_ones(m_bits); }
|
||||
bool is_ones(svector<digit_t> const& a) const {
|
||||
auto bound = bw % (sizeof(digit_t) * 8) == 0 ? nw : nw - 1;
|
||||
for (unsigned i = 0; i < bound; ++i)
|
||||
if (a[i] != (a[i] ^ 0))
|
||||
return false;
|
||||
if (bound < nw) {
|
||||
for (unsigned i = bound * sizeof(digit_t) * 8; i < bw; ++i)
|
||||
if (!get(a, i))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
bool is_ones() const { return m_bits.is_ones(); }
|
||||
|
||||
bool is_one() const { return is_one(m_bits); }
|
||||
bool is_one(svector<digit_t> const& bits) const {
|
||||
if (1 != bits[0])
|
||||
return false;
|
||||
for (unsigned i = 1; i < nw; ++i)
|
||||
if (0 != bits[i])
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
bool is_one() const { return m_bits.is_one(); }
|
||||
// bool is_one(bvect const& a) const { return a.is_one(); }
|
||||
|
||||
bool sign() const { return get(m_bits, bw - 1); }
|
||||
|
||||
bool has_overflow(svector<digit_t> const& bits) const {
|
||||
for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i)
|
||||
if (get(bits, i))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
bool has_overflow(bvect const& bits) const { return bits.has_overflow(); }
|
||||
|
||||
unsigned parity(svector<digit_t> const& bits) const {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
if (bits[i] != 0)
|
||||
return (8 * sizeof(digit_t) * i) + trailing_zeros(bits[i]);
|
||||
return bw;
|
||||
}
|
||||
unsigned parity(bvect const& bits) const { return bits.parity(); }
|
||||
|
||||
void min_feasible(svector<digit_t>& out) const;
|
||||
void max_feasible(svector<digit_t>& out) const;
|
||||
void min_feasible(bvect& out) const;
|
||||
void max_feasible(bvect& out) const;
|
||||
|
||||
// most significant bit or bw if src = 0
|
||||
unsigned msb(svector<digit_t> const& src) const;
|
||||
unsigned msb(bvect const& src) const;
|
||||
|
||||
bool is_power_of2(svector<digit_t> const& src) const;
|
||||
bool is_power_of2(bvect const& src) const;
|
||||
|
||||
// retrieve largest number at or below (above) src which is feasible
|
||||
// with respect to fixed, lo, hi.
|
||||
bool get_at_most(svector<digit_t> const& src, svector<digit_t>& dst) const;
|
||||
bool get_at_least(svector<digit_t> const& src, svector<digit_t>& dst) const;
|
||||
bool round_up(svector<digit_t>& dst) const;
|
||||
bool round_down(svector<digit_t>& dst) const;
|
||||
bool set_repair(bool try_down, svector<digit_t>& dst);
|
||||
bool get_at_most(bvect const& src, bvect& dst) const;
|
||||
bool get_at_least(bvect const& src, bvect& dst) const;
|
||||
|
||||
bool try_set(svector<digit_t> const& src) {
|
||||
bool set_repair(bool try_down, bvect& dst);
|
||||
|
||||
bool try_set(bvect const& src) {
|
||||
if (!can_set(src))
|
||||
return false;
|
||||
set(src);
|
||||
return true;
|
||||
}
|
||||
|
||||
void set(svector<digit_t> const& src) {
|
||||
void set(bvect const& src) {
|
||||
for (unsigned i = nw; i-- > 0; )
|
||||
m_bits[i] = src[i];
|
||||
clear_overflow_bits(m_bits);
|
||||
}
|
||||
|
||||
void set_zero(svector<digit_t>& out) const {
|
||||
void set_zero(bvect& out) const {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
out[i] = 0;
|
||||
}
|
||||
|
||||
void set_one(svector<digit_t>& out) const {
|
||||
void set_one(bvect& out) const {
|
||||
for (unsigned i = 1; i < nw; ++i)
|
||||
out[i] = 0;
|
||||
out[0] = 1;
|
||||
|
@ -154,7 +225,7 @@ namespace bv {
|
|||
set_zero(m_bits);
|
||||
}
|
||||
|
||||
void sub1(svector<digit_t>& out) const {
|
||||
void sub1(bvect& out) const {
|
||||
for (unsigned i = 0; i < bw; ++i) {
|
||||
if (get(out, i)) {
|
||||
set(out, i, false);
|
||||
|
@ -165,90 +236,72 @@ namespace bv {
|
|||
}
|
||||
}
|
||||
|
||||
void set_sub(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const;
|
||||
bool set_add(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const;
|
||||
bool set_mul(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b, bool check_overflow = true) const;
|
||||
void shift_right(svector<digit_t>& out, unsigned shift) const;
|
||||
void set_sub(bvect& out, bvect const& a, bvect const& b) const;
|
||||
bool set_add(bvect& out, bvect const& a, bvect const& b) const;
|
||||
bool set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow = true) const;
|
||||
void shift_right(bvect& out, unsigned shift) const;
|
||||
|
||||
void set_range(svector<digit_t>& dst, unsigned lo, unsigned hi, bool b) {
|
||||
void set_range(bvect& dst, unsigned lo, unsigned hi, bool b) {
|
||||
for (unsigned i = lo; i < hi; ++i)
|
||||
set(dst, i, b);
|
||||
}
|
||||
|
||||
void set(svector<digit_t>& d, unsigned bit_idx, bool val) const {
|
||||
auto _val = static_cast<digit_t>(0 - static_cast<digit_t>(val));
|
||||
get_bit_word(d, bit_idx) ^= (_val ^ get_bit_word(d, bit_idx)) & get_pos_mask(bit_idx);
|
||||
void set(bvect& d, unsigned bit_idx, bool val) const {
|
||||
d.set(bit_idx, val);
|
||||
}
|
||||
|
||||
void set(svector<digit_t>& dst, unsigned v) const {
|
||||
void set(bvect& dst, unsigned v) const {
|
||||
dst[0] = v;
|
||||
for (unsigned i = 1; i < nw; ++i)
|
||||
dst[i] = 0;
|
||||
}
|
||||
|
||||
void set(svector<digit_t>& dst, svector<digit_t> const& src) const {
|
||||
void set(bvect& dst, bvect const& src) const {
|
||||
for (unsigned i = 0; i < nw; ++i)
|
||||
dst[i] = src[i];
|
||||
}
|
||||
|
||||
bool get(svector<digit_t> const& d, unsigned bit_idx) const {
|
||||
return (get_bit_word(d, bit_idx) & get_pos_mask(bit_idx)) != 0;
|
||||
bool get(bvect const& d, unsigned bit_idx) const {
|
||||
return d.get(bit_idx);
|
||||
}
|
||||
|
||||
unsigned to_nat(svector<digit_t> const& d, unsigned max_n);
|
||||
|
||||
|
||||
unsigned to_nat(unsigned max_n);
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
out << "V:";
|
||||
out << std::hex;
|
||||
auto print_bits = [&](svector<digit_t> const& v) {
|
||||
bool nz = false;
|
||||
for (unsigned i = nw; i-- > 0;)
|
||||
if (nz)
|
||||
out << std::setw(8) << std::setfill('0') << v[i];
|
||||
else if (v[i] != 0)
|
||||
out << v[i], nz = true;
|
||||
if (!nz)
|
||||
out << "0";
|
||||
};
|
||||
|
||||
print_bits(m_bits);
|
||||
print_bits(out, m_bits);
|
||||
out << " fix:";
|
||||
print_bits(fixed);
|
||||
print_bits(out, fixed);
|
||||
|
||||
if (!eq(lo, hi)) {
|
||||
if (lo != hi) {
|
||||
out << " [";
|
||||
print_bits(lo);
|
||||
print_bits(out, lo);
|
||||
out << ", ";
|
||||
print_bits(hi);
|
||||
print_bits(out, hi);
|
||||
out << "[";
|
||||
}
|
||||
out << std::dec;
|
||||
return out;
|
||||
}
|
||||
|
||||
// TODO move:
|
||||
void set_bit(unsigned i, bool v) { set(m_bits, i, v); }
|
||||
bool well_formed() const {
|
||||
return !has_overflow(m_bits) && (!has_range() || in_range(m_bits));
|
||||
}
|
||||
|
||||
private:
|
||||
static digit_t get_pos_mask(unsigned bit_idx) {
|
||||
return (digit_t)1 << (digit_t)(bit_idx % (8 * sizeof(digit_t)));
|
||||
}
|
||||
|
||||
static digit_t get_bit_word(svector<digit_t> const& bits, unsigned bit_idx) {
|
||||
return bits[bit_idx / (8 * sizeof(digit_t))];
|
||||
}
|
||||
|
||||
static digit_t& get_bit_word(svector<digit_t>& bits, unsigned bit_idx) {
|
||||
return bits[bit_idx / (8 * sizeof(digit_t))];
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
class sls_pre_valuation : public sls_valuation {
|
||||
public:
|
||||
sls_pre_valuation(unsigned bw):sls_valuation(bw) {}
|
||||
svector<digit_t>& bits() { return m_bits; }
|
||||
bvect& bits() { return m_bits; }
|
||||
void set_bit(unsigned i, bool v) { set(m_bits, i, v); }
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue