From 74e73f2b8468ce2e43e9684b7f883f07d3e5a769 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Feb 2024 17:45:03 -0800 Subject: [PATCH] reorg to use datatypes --- src/ast/sls/bv_sls.cpp | 3 +- src/ast/sls/bv_sls_eval.cpp | 169 +++++++++----------- src/ast/sls/bv_sls_eval.h | 18 +-- src/ast/sls/bv_sls_fixed.cpp | 25 +-- src/ast/sls/sls_valuation.cpp | 261 ++++++++++++++++++------------- src/ast/sls/sls_valuation.h | 279 ++++++++++++++++++++-------------- 6 files changed, 414 insertions(+), 341 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 35f014773..e8402c957 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -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)); } } diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index ceea3e7ba..5ccdc7540 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -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& 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 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 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 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 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 const& a, svector const& b, unsigned bw, - svector& quot, svector& 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) diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 4669c24b2..b379f7e85 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -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 m_tmp, m_tmp2, m_tmp3, m_tmp4, m_zero, m_one, m_minus_one; - svector 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 const& t); - bool try_repair_uge(bool e, bvval& a, svector 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& t) const; + void add_p2_1(bvval const& a, bvect& t) const; - bool add_overflow_on_fixed(bvval const& a, svector const& t); - bool mul_overflow_on_fixed(bvval const& a, svector const& t); - void set_div(svector const& a, svector const& b, unsigned nw, - svector& quot, svector& 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; } diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 05d9599c1..0037bb5ca 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -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: { diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 03daab05b..a0a21a534 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -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 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 const& a, svector 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 const& a, svector 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 const& a, svector 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 const& a, svector 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& 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 const& src, svector& 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 const& src, svector& 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& 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& 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& 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& 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& 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 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& 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 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& 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& 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 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 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& 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 hi1(nw + 1, (unsigned)0); - svector 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& out, svector const& a, svector 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& out, svector const& a, svector 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& out, svector const& a, svector 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 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; + } + + } diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 3a14074e7..88b8efa59 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -27,124 +27,195 @@ Author: namespace bv { + + + class bvect : public svector { + 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 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 lo, hi; // range assignment to bit-vector, as wrap-around interval - svector 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 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& bits, rational const& r); - void get_value(svector const& bits, rational& r) const; - void get(svector& 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& bits); - void clear_overflow_bits(svector& bits) const; - bool in_range(svector const& bits) const; - bool can_set(svector 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 const& other) const { return eq(other, m_bits); } - bool eq(svector const& a, svector const& b) const; - bool gt(svector const& a, svector const& b) const; - bool lt(svector const& a, svector const& b) const; - bool le(svector const& a, svector 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 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 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 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 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 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& out) const; - void max_feasible(svector& 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 const& src) const; + unsigned msb(bvect const& src) const; - bool is_power_of2(svector 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 const& src, svector& dst) const; - bool get_at_least(svector const& src, svector& dst) const; - bool round_up(svector& dst) const; - bool round_down(svector& dst) const; - bool set_repair(bool try_down, svector& 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 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 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& out) const { + void set_zero(bvect& out) const { for (unsigned i = 0; i < nw; ++i) out[i] = 0; } - void set_one(svector& 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& 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& out, svector const& a, svector const& b) const; - bool set_add(svector& out, svector const& a, svector const& b) const; - bool set_mul(svector& out, svector const& a, svector const& b, bool check_overflow = true) const; - void shift_right(svector& 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& 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& d, unsigned bit_idx, bool val) const { - auto _val = static_cast(0 - static_cast(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& 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& dst, svector 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 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 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 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 const& bits, unsigned bit_idx) { - return bits[bit_idx / (8 * sizeof(digit_t))]; - } - static digit_t& get_bit_word(svector& 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& bits() { return m_bits; } + bvect& bits() { return m_bits; } + void set_bit(unsigned i, bool v) { set(m_bits, i, v); } + };