diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-02-23 18:02:53 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-23 18:02:53 -0800 |
commit | cb8e3b305ecf83cde0380f9198fa6d3f795362cd (patch) | |
tree | cbae726a0df059c89bdbfaaf36fcb3f356e7d298 /src | |
parent | cef98b9c073c6c1a1535f4f45589a86cfaab1c33 (diff) |
Add unit tests for BitVector, minor BV rewrite fix (#1622)
This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 9 | ||||
-rw-r--r-- | src/util/bitvector.cpp | 2 |
2 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d91067d1e..a4be19253 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1303,10 +1303,13 @@ inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) { t = node[1][0]; c = node[0]; } - BitVector bv_c = c.getConst<BitVector>(); - BitVector bv_max = - BitVector(utils::getSize(c)).setBit(utils::getSize(t) - 1); + if (utils::getSize(t) == utils::getSize(c)) + { + return false; + } + + BitVector bv_c = c.getConst<BitVector>(); BitVector c_hi = c.getConst<BitVector>().extract(utils::getSize(c) - 1, utils::getSize(t)); BitVector zero = BitVector(c_hi.getSize(), Integer(0)); diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 2d94be875..549c94dc9 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -90,6 +90,8 @@ BitVector BitVector::concat(const BitVector& other) const BitVector BitVector::extract(unsigned high, unsigned low) const { + CheckArgument(high < d_size, high); + CheckArgument(low <= high, low); return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low)); } |