From 63804c52962837d33e1fe633ec68e6b0a30d603d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Feb 2024 21:19:06 -0800 Subject: [PATCH] na --- src/ast/sls/bv_sls.cpp | 2 +- src/ast/sls/bv_sls_eval.cpp | 87 ++++++++++++----------- src/ast/sls/bv_sls_fixed.cpp | 44 ++++++------ src/ast/sls/sls_valuation.cpp | 84 +++++++++-------------- src/ast/sls/sls_valuation.h | 126 ++++++++++++++-------------------- 5 files changed, 148 insertions(+), 195 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index e8402c95756..e091eb4b526 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -67,7 +67,7 @@ namespace bv { } else if (bv.is_bv(e)) { auto& w = m_eval.wval0(e); - if (w.get(w.fixed, i) || should_keep()) + if (w.fixed.get(i) || should_keep()) return w.get_bit(i); } return m_rand() % 2 == 0; diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 5ccdc7540bd..5a26dc55bfa 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -39,7 +39,7 @@ namespace bv { if (bv.is_bv(e)) { auto& v = wval0(e); for (unsigned i = 0; i < v.bw; ++i) - v.set(m_tmp, i, eval(e, i)); + m_tmp.set(i, eval(e, i)); v.set(m_tmp); } else if (m.is_bool(e)) @@ -462,10 +462,10 @@ namespace bv { break; } case OP_BIT0: - val.set(val.bits(), 0, false); + val.bits().set(0, false); break; case OP_BIT1: - val.set(val.bits(), 0, true); + val.bits().set(0, true); break; case OP_BSHL: { auto& a = wval0(e->get_arg(0)); @@ -477,7 +477,7 @@ namespace bv { val.set_zero(); else { for (unsigned i = 0; i < a.bw; ++i) - val.set(val.bits(), i, i >= sh && a.get_bit(i - sh)); + val.bits().set(i, i >= sh && a.get_bit(i - sh)); } break; } @@ -491,7 +491,7 @@ namespace bv { val.set_zero(); else { for (unsigned i = 0; i < a.bw; ++i) - val.set(val.bits(), i, i + sh < a.bw && a.get_bit(i + sh)); + val.bits().set(i, i + sh < a.bw && a.get_bit(i + sh)); } break; } @@ -511,7 +511,7 @@ namespace bv { for (unsigned i = 0; i < a.nw; ++i) m_tmp[i] = 0; for (unsigned i = 0; i < a.bw; ++i) - val.set(m_tmp, i, i + sh < a.bw && a.get_bit(i + sh)); + m_tmp.set(i, i + sh < a.bw && a.get_bit(i + sh)); if (sign) val.set_range(m_tmp, a.bw - sh, a.bw, true); val.set(m_tmp); @@ -521,7 +521,7 @@ namespace bv { case OP_SIGN_EXT: { auto& a = wval0(e->get_arg(0)); for (unsigned i = 0; i < a.bw; ++i) - val.set(m_tmp, i, a.get_bit(i)); + m_tmp.set(i, a.get_bit(i)); bool sign = a.sign(); val.set_range(m_tmp, a.bw, val.bw, sign); val.set(m_tmp); @@ -530,7 +530,7 @@ namespace bv { case OP_ZERO_EXT: { auto& a = wval0(e->get_arg(0)); for (unsigned i = 0; i < a.bw; ++i) - val.set(m_tmp, 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(m_tmp); break; @@ -904,12 +904,12 @@ namespace bv { unsigned start = m_rand(a.bw); for (unsigned idx = 0; idx < a.bw; ++idx) { unsigned j = (idx + start) % a.bw; - if (!a.get(a.fixed, j)) { - a.set(m_tmp, idx, !b.get_bit(j)); + if (!a.fixed.get(j)) { + m_tmp.set(idx, !b.get_bit(j)); bool r = a.try_set(m_tmp); if (r) return true; - a.set(m_tmp, j, b.get_bit(j)); + m_tmp.set(j, b.get_bit(j)); } } // could be due to bounds? @@ -1042,18 +1042,18 @@ namespace bv { // x*ta + y*tb = x - auto bw = a.bw; + b.get(y); 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 + x[a.nw] = 0; + + a.set_bw((a.nw + 1)* 8 * sizeof(digit_t)); + y.set_bw(a.bw); // enable comparisons a.set_zero(x); - a.set(x, bw, true); + x.set(b.bw, true); // x = 2 ^ b.bw a.set_one(ta); a.set_zero(tb); @@ -1078,8 +1078,7 @@ namespace bv { a.set(tb, aux); // tb := aux } - a.bw = bw; - a.nw = a.nw - 1; + a.set_bw(b.bw); y.set_bw(0); // x*a + y*b = 1 @@ -1099,7 +1098,7 @@ namespace bv { verbose_stream() << m_tmp[i]; verbose_stream() << "\n"; #endif - SASSERT(m_tmp.is_one()); + SASSERT(a.is_one(m_tmp)); #endif e.get(m_tmp2); if (parity_e > 0 && parity_b > 0) @@ -1130,6 +1129,7 @@ namespace bv { } bool sls_eval::try_repair_bneg(bvval const& e, bvval& a) { + e.set_sub(m_tmp, m_zero, e.bits()); return a.set_repair(random_bool(), m_tmp); } @@ -1167,9 +1167,9 @@ namespace bv { } void sls_eval::add_p2_1(bvval const& a, bvect& t) const { - a.set(m_zero, a.bw - 1, true); + m_zero.set(a.bw - 1, true); a.set_add(t, a.bits(), m_zero); - a.set(m_zero, a.bw - 1, false); + m_zero.set(a.bw - 1, false); a.clear_overflow_bits(t); } @@ -1183,9 +1183,8 @@ namespace bv { a.set_add(m_tmp2, t, m_one); if (a.is_zero(m_tmp2)) return false; - if (!a.get_at_least(m_tmp2, m_tmp)) { - return false; - } + if (!a.get_at_least(m_tmp2, m_tmp)) + return false; } return a.set_repair(random_bool(), m_tmp); } @@ -1224,9 +1223,9 @@ namespace bv { // a[bw - 1: bw - sh] = unchanged // for (unsigned i = 0; i < e.bw - sh; ++i) - e.set(m_tmp, i, e.get_bit(sh + i)); + m_tmp.set(i, e.get_bit(sh + i)); for (unsigned i = e.bw - sh; i < e.bw; ++i) - e.set(m_tmp, i, a.get_bit(i)); + m_tmp.set(i, a.get_bit(i)); return a.try_set(m_tmp); } } @@ -1257,9 +1256,9 @@ namespace bv { // a[sh-1:0] = a[sh-1:0] // ignore sign for (unsigned i = sh; i < a.bw; ++i) - a.set(m_tmp, i, e.get_bit(i - sh)); + m_tmp.set(i, e.get_bit(i - sh)); for (unsigned i = 0; i < sh; ++i) - a.set(m_tmp, i, a.get_bit(i)); + m_tmp.set(i, a.get_bit(i)); a.clear_overflow_bits(m_tmp); return a.try_set(m_tmp); } @@ -1284,7 +1283,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.fixed.is_ones() && a.is_ones()) + if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones()) return false; if (b.is_zero()) return false; @@ -1306,15 +1305,15 @@ namespace bv { b.clear_overflow_bits(m_tmp); while (mul_overflow_on_fixed(e, m_tmp)) { auto i = b.msb(m_tmp); - b.set(m_tmp, i, false); + m_tmp.set(i, false); } for (unsigned i = 0; i < a.nw; ++i) m_tmp2[i] = random_bits(); b.clear_overflow_bits(m_tmp2); while (b.bits() < m_tmp2) - b.set(m_tmp2, b.msb(m_tmp2), false); + m_tmp2.set(b.msb(m_tmp2), false); while (a.set_add(m_tmp3, m_tmp, m_tmp2)) - b.set(m_tmp2, b.msb(m_tmp2), false); + m_tmp2.set(b.msb(m_tmp2), false); return a.set_repair(true, m_tmp3); } else { @@ -1337,7 +1336,7 @@ namespace bv { a.clear_overflow_bits(m_tmp); // ensure r <= m while (a.bits() < m_tmp) - a.set(m_tmp, a.msb(m_tmp), false); + m_tmp.set(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); return b.set_repair(random_bool(), m_tmp4); @@ -1372,14 +1371,14 @@ namespace bv { a.clear_overflow_bits(m_tmp); while (mul_overflow_on_fixed(b, m_tmp)) { auto i = b.msb(m_tmp); - b.set(m_tmp, i, false); + m_tmp.set(i, false); } while (true) { a.set_mul(m_tmp2, m_tmp, b.bits()); if (!add_overflow_on_fixed(e, m_tmp2)) break; auto i = b.msb(m_tmp); - b.set(m_tmp, i, false); + m_tmp.set(i, false); } a.set_add(m_tmp3, m_tmp2, e.bits()); return a.set_repair(random_bool(), m_tmp3); @@ -1419,11 +1418,10 @@ namespace bv { // a := rotate_right(e, n) n = (a.bw - n) % a.bw; for (unsigned i = a.bw - n; i < a.bw; ++i) - a.set(m_tmp, i + n - a.bw, e.get_bit(i)); + m_tmp.set(i + n - a.bw, e.get_bit(i)); for (unsigned i = 0; i < a.bw - n; ++i) - a.set(m_tmp, i + n, e.get_bit(i)); - a.set_repair(true, m_tmp); - return true; + m_tmp.set(i + n, e.get_bit(i)); + return a.set_repair(true, m_tmp); } bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i) { @@ -1436,8 +1434,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); } } @@ -1491,13 +1488,13 @@ namespace bv { bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i) { if (i == 0) { for (unsigned i = 0; i < a.bw; ++i) - a.set(m_tmp, i, e.get_bit(i + b.bw)); + m_tmp.set(i, e.get_bit(i + b.bw)); a.clear_overflow_bits(m_tmp); return a.set_repair(random_bool(), m_tmp); } else { for (unsigned i = 0; i < b.bw; ++i) - b.set(m_tmp, i, e.get_bit(i)); + m_tmp.set(i, e.get_bit(i)); b.clear_overflow_bits(m_tmp); return b.set_repair(random_bool(), m_tmp); } diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 0037bb5ca3b..770ad3223f4 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -111,7 +111,7 @@ namespace bv { else if (bv.is_bit2bool(e, s, idx)) { auto& val = wval0(s); val.try_set_bit(idx, !sign); - val.set(val.fixed, idx, true); + val.fixed.set(idx, true); val.init_fixed(); } } @@ -222,7 +222,7 @@ namespace bv { auto& v = ev.wval0(e); if (all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) { for (unsigned i = 0; i < v.bw; ++i) - v.set(v.fixed, i, true); + v.fixed.set(i, true); ev.m_fixed.setx(e->get_id(), true, false); return; } @@ -272,16 +272,16 @@ namespace bv { } bool pfixed = true; for (unsigned i = 0; i < v.bw; ++i) { - if (pfixed && a.get(a.fixed, i) && b.get(b.fixed, i)) - v.set(v.fixed, i, true); - else if (!pfixed && a.get(a.fixed, i) && b.get(b.fixed, i) && + if (pfixed && a.fixed.get(i) && b.fixed.get(i)) + v.fixed.set(i, true); + else if (!pfixed && a.fixed.get(i) && b.fixed.get(i) && !a.get_bit(i) && !b.get_bit(i)) { pfixed = true; - v.set(v.fixed, i, false); + v.fixed.set(i, false); } else { pfixed = false; - v.set(v.fixed, i, false); + v.fixed.set(i, false); } } @@ -294,36 +294,36 @@ namespace bv { // i'th bit depends on bits j + k = i // if the first j, resp k bits are 0, the bits j + k are 0 for (; j < v.bw; ++j) - if (!a.get(a.fixed, j)) + if (!a.fixed.get(j)) break; for (; k < v.bw; ++k) - if (!b.get(b.fixed, k)) + if (!b.fixed.get(k)) break; for (; zj < v.bw; ++zj) - if (!a.get(a.fixed, zj) || a.get_bit(zj)) + if (!a.fixed.get(zj) || a.get_bit(zj)) break; for (; zk < v.bw; ++zk) - if (!b.get(b.fixed, zk) || b.get_bit(zk)) + if (!b.fixed.get(zk) || b.get_bit(zk)) break; for (; hzj < v.bw; ++hzj) - if (!a.get(a.fixed, v.bw - hzj - 1) || a.get_bit(v.bw - hzj - 1)) + if (!a.fixed.get(v.bw - hzj - 1) || a.get_bit(v.bw - hzj - 1)) break; for (; hzk < v.bw; ++hzk) - if (!b.get(b.fixed, v.bw - hzk - 1) || b.get_bit(v.bw - hzk - 1)) + if (!b.fixed.get(v.bw - hzk - 1) || b.get_bit(v.bw - hzk - 1)) break; if (j > 0 && k > 0) { for (unsigned i = 0; i < std::min(k, j); ++i) { SASSERT(!v.get_bit(i)); - v.set(v.fixed, i, true); + v.fixed.set(i, true); } } // lower zj + jk bits are 0 if (zk > 0 || zj > 0) { for (unsigned i = 0; i < zk + zj; ++i) { SASSERT(!v.get_bit(i)); - v.set(v.fixed, i, true); + v.fixed.set(i, true); } } // upper bits are 0, if enough high order bits of a, b are 0. @@ -333,7 +333,7 @@ namespace bv { hzk = v.bw - hzk; for (unsigned i = hzj + hzk - 1; i < v.bw; ++i) { SASSERT(!v.get_bit(i)); - v.set(v.fixed, i, true); + v.fixed.set(i, true); } } break; @@ -342,9 +342,9 @@ namespace bv { auto& a = wval0(e->get_arg(0)); auto& b = wval0(e->get_arg(1)); for (unsigned i = 0; i < b.bw; ++i) - v.set(v.fixed, i, b.get(b.fixed, i)); + v.fixed.set(i, b.fixed.get(i)); for (unsigned i = 0; i < a.bw; ++i) - v.set(v.fixed, i + b.bw, a.get(a.fixed, i)); + v.fixed.set(i + b.bw, a.fixed.get(i)); break; } case OP_EXTRACT: { @@ -353,18 +353,18 @@ namespace bv { VERIFY(bv.is_extract(e, lo, hi, child)); auto& a = wval0(child); for (unsigned i = lo; i <= hi; ++i) - v.set(v.fixed, i - lo, a.get(a.fixed, i)); + v.fixed.set(i - lo, a.fixed.get(i)); break; } case OP_BNEG: { auto& a = wval0(e->get_arg(0)); bool pfixed = true; for (unsigned i = 0; i < v.bw; ++i) { - if (pfixed && a.get(a.fixed, i)) - v.set(v.fixed, i, true); + if (pfixed && a.fixed.get(i)) + v.fixed.set(i, true); else { pfixed = false; - v.set(v.fixed, i, false); + v.fixed.set(i, false); } } break; diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index a0a21a53480..523bc99c4f6 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -31,60 +31,33 @@ namespace bv { 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()); + SASSERT(a.nw > 0); 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; + sls_valuation::sls_valuation(unsigned bw) { + set_bw(bw); lo.set_bw(bw); hi.set_bw(bw); m_bits.set_bw(bw); @@ -92,8 +65,15 @@ namespace bv { // 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; - for (unsigned i = bw; i < 8 * sizeof(digit_t) * nw; ++i) - set(fixed, i, true); + fixed[nw - 1] = ~mask; + } + + void sls_valuation::set_bw(unsigned b) { + bw = b; + 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; } bool sls_valuation::in_range(bvect const& bits) const { @@ -308,11 +288,11 @@ namespace bv { for (unsigned i = 0; i < bw; ++i) { if (p >= max_n) { for (unsigned j = i; j < bw; ++j) - if (get(d, j)) + if (d.get(j)) return max_n; return value; } - if (get(d, i)) + if (d.get(i)) value += p; p <<= 1; } @@ -322,7 +302,7 @@ namespace bv { 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); + out.set(i, i + shift < bw ? m_bits.get(i + shift) : false); SASSERT(well_formed()); } @@ -384,18 +364,18 @@ namespace bv { if (lo == hi) return; for (unsigned i = bw; i-- > 0; ) { - if (!get(fixed, i)) + if (!fixed.get(i)) continue; - if (get(m_bits, i) == get(lo, i)) + if (m_bits.get(i) == lo.get(i)) continue; - if (get(m_bits, i)) { - set(lo, i, true); + if (m_bits.get(i)) { + lo.set(i, true); for (unsigned j = i; j-- > 0; ) - set(lo, j, get(fixed, j) && get(m_bits, j)); + lo.set(j, fixed.get(j) && m_bits.get(j)); } else { for (unsigned j = bw; j-- > 0; ) - set(lo, j, get(fixed, j) && get(m_bits, j)); + lo.set(j, fixed.get(j) && m_bits.get(j)); } break; } @@ -406,18 +386,18 @@ namespace bv { mpn_manager().sub(hi.data(), nw, one.data(), nw, hi1.data(), &c); clear_overflow_bits(hi1); for (unsigned i = bw; i-- > 0; ) { - if (!get(fixed, i)) + if (!fixed.get(i)) continue; - if (get(m_bits, i) == get(hi1, i)) + if (m_bits.get(i) == hi1.get(i)) continue; - if (get(hi1, i)) { - set(hi1, i, false); + if (hi1.get(i)) { + hi1.set(i, false); for (unsigned j = i; j-- > 0; ) - set(hi1, j, !get(fixed, j) || get(m_bits, j)); + hi1.set(j, !fixed.get(j) || m_bits.get(j)); } else { for (unsigned j = bw; j-- > 0; ) - set(hi1, j, get(fixed, j) && get(m_bits, j)); + hi1.set(j, fixed.get(j) && m_bits.get(j)); } mpn_manager().add(hi1.data(), nw, one.data(), nw, hi.data(), nw + 1, &c); clear_overflow_bits(hi); @@ -426,16 +406,16 @@ namespace bv { // set fixed bits based on bounds auto set_fixed_bit = [&](unsigned i, bool b) { - if (!get(fixed, i)) { - set(fixed, i, true); - set(m_bits, i, b); + if (!fixed.get(i)) { + fixed.set(i, true); + m_bits.set(i, b); } }; // set most significant bits if (lo < hi) { unsigned i = bw; - for (; i-- > 0 && !get(hi, i); ) + for (; i-- > 0 && !hi.get(i); ) set_fixed_bit(i, false); if (is_power_of2(hi)) @@ -447,7 +427,7 @@ namespace bv { clear_overflow_bits(hi1); if (hi == hi1) { for (unsigned i = 0; i < bw; ++i) - set_fixed_bit(i, get(lo, i)); + set_fixed_bit(i, lo.get(i)); } SASSERT(well_formed()); } diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 88b8efa5956..c7852a82a96 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -27,63 +27,22 @@ Module Name: namespace bv { - - class bvect : public svector { unsigned bw = 0; unsigned nw = 0; unsigned mask = 0; public: bvect() {} - bvect(unsigned sz): svector(sz, (unsigned)0) {} + 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]); @@ -135,19 +94,26 @@ namespace bv { unsigned bw; // bit-width unsigned nw; // num words bvect fixed; // bit assignment and don't care bit + sls_valuation(unsigned bw); + void set_bw(unsigned bw); + unsigned num_bytes() const { return (bw + 7) / 8; } digit_t bits(unsigned i) const { return m_bits[i]; } bvect const& bits() const { return m_bits; } - bool get_bit(unsigned i) const { return get(m_bits, i); } + bool get_bit(unsigned i) const { return m_bits.get(i); } bool try_set_bit(unsigned i, bool b) { - if (get(fixed, i) && get_bit(i) != b) + SASSERT(in_range(m_bits)); + if (fixed.get(i) && get_bit(i) != b) return false; - set(m_bits, i, b); - return true; + m_bits.set(i, b); + if (in_range(m_bits)) + return true; + m_bits.set(i, !b); + return false; } void set_value(bvect& bits, rational const& r); @@ -161,24 +127,49 @@ namespace bv { bool has_range() const { return lo != hi; } void init_fixed(); - void clear_overflow_bits(bvect& bits) const { bits.clear_overflow_bits(); } + void clear_overflow_bits(bvect& bits) const { + SASSERT(nw > 0); + bits[nw - 1] &= mask; + SASSERT(!has_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 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(bvect const& a) const { + SASSERT(!has_overflow(a)); + for (unsigned i = 0; i < nw; ++i) + if (a[i] != 0) + return false; + return true; + } - bool is_ones() const { return m_bits.is_ones(); } + bool is_ones() const { return is_ones(m_bits); } + + bool is_ones(bvect const& a) const { + SASSERT(!has_overflow(a)); + for (unsigned i = 0; i + 1 < nw; ++i) + if (0 != ~a[i]) + return false; + return 0 == (mask & ~a[nw - 1]); + } - bool is_one() const { return m_bits.is_one(); } - // bool is_one(bvect const& a) const { return a.is_one(); } + bool is_one() const { return is_one(m_bits); } + bool is_one(bvect const& a) const { + SASSERT(!has_overflow(a)); + for (unsigned i = 1; i < nw; ++i) + if (0 != a[i]) + return false; + return 1 == a[0]; + } - bool sign() const { return get(m_bits, bw - 1); } + bool sign() const { return m_bits.get(bw - 1); } - bool has_overflow(bvect const& bits) const { return bits.has_overflow(); } + bool has_overflow(bvect const& bits) const { return 0 != (bits[nw - 1] & ~mask); } unsigned parity(bvect const& bits) const { return bits.parity(); } @@ -227,12 +218,12 @@ namespace bv { void sub1(bvect& out) const { for (unsigned i = 0; i < bw; ++i) { - if (get(out, i)) { - set(out, i, false); + if (out.get(i)) { + out.set(i, false); return; } else - set(out, i, true); + out.set(i, true); } } @@ -243,11 +234,7 @@ namespace bv { void set_range(bvect& dst, unsigned lo, unsigned hi, bool b) { for (unsigned i = lo; i < hi; ++i) - set(dst, i, b); - } - - void set(bvect& d, unsigned bit_idx, bool val) const { - d.set(bit_idx, val); + dst.set(i, b); } void set(bvect& dst, unsigned v) const { @@ -261,14 +248,9 @@ namespace bv { dst[i] = src[i]; } - bool get(bvect const& d, unsigned bit_idx) const { - return d.get(bit_idx); - } - unsigned to_nat(unsigned max_n); std::ostream& display(std::ostream& out) const { - out << "V:"; out << std::hex; print_bits(out, m_bits); @@ -290,19 +272,13 @@ namespace bv { return !has_overflow(m_bits) && (!has_range() || in_range(m_bits)); } - private: - - - }; class sls_pre_valuation : public sls_valuation { public: - sls_pre_valuation(unsigned bw):sls_valuation(bw) {} + sls_pre_valuation(unsigned bw) :sls_valuation(bw) {} bvect& bits() { return m_bits; } - void set_bit(unsigned i, bool v) { set(m_bits, i, v); } - - + 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); }