diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-09-30 17:26:46 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-30 17:26:46 -0700 |
| commit | d7f92f70bb8ff221dc3d7cb086e5e2e237dadc67 (patch) | |
| tree | 26916ced6f98142dd9dc04c454ff6d0c8161a8d6 /src/theory/bv | |
| parent | aa65c60968d0b8c0a7cd47adb2e9e1a684c0332a (diff) | |
BitVector: Extend interface of setBit to set it to a specific value. (#5173)
Previously, BitVector::setBit only allowed to set the bit at the given
index to 1. This changes its behavior to be also able to set it to 0.
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index dd0d47078..20dac35cd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1893,7 +1893,7 @@ inline bool RewriteRule<SignExtendUltConst>::applies(TNode node) unsigned size_c = utils::getSize(c); unsigned msb_x_pos = utils::getSize(x) - 1; // (1 << (n - 1))) - BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos); + BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos, true); // (~0 << (n - 1)) BitVector bv_upper_bits = (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos)); @@ -1929,7 +1929,7 @@ inline Node RewriteRule<SignExtendUltConst>::apply(TNode node) unsigned msb_x_pos = utils::getSize(x) - 1; Node c_lo = utils::mkConst(bv_c.extract(msb_x_pos, 0)); // (1 << (n - 1))) - BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos); + BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos, true); // (~0 << (n - 1)) BitVector bv_upper_bits = (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos)); |