diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-03-18 16:07:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-18 16:07:03 -0700 |
commit | 7e3457b0e16cacef456287ae761c5293be1209d5 (patch) | |
tree | 0be91c1ed36950cbb17e2ad3484e89636b518c45 /src | |
parent | 192aa1b5d98ca1a0a2c5e5c8ec603ebb9d14d261 (diff) |
BitVector: Allow base 10 in constructor. (#2870)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.h | 16 | ||||
-rw-r--r-- | src/util/bitvector.h | 22 |
2 files changed, 33 insertions, 5 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index b6049d5b3..2c266b11d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2047,7 +2047,14 @@ class CVC4_PUBLIC Solver Term mkBitVector(const char* s, uint32_t base = 2) const; /** - * Create a bit-vector constant from a given string. + * Create a bit-vector constant from a given string of base 2, 10 or 16. + * + * The size of resulting bit-vector is + * - base 2: the size of the binary string + * - base 10: the min. size required to represent the decimal as a bit-vector + * - base 16: the max. size required to represent the hexadecimal as a + * bit-vector (4 * size of the given value string) + * * @param s the string representation of the constant * @param base the base of the string representation (2, 10, or 16) * @return the bit-vector constant @@ -2055,7 +2062,9 @@ class CVC4_PUBLIC Solver Term mkBitVector(const std::string& s, uint32_t base = 2) const; /** - * Create a bit-vector constant of a given bit-width from a given string. + * Create a bit-vector constant of a given bit-width from a given string of + * base 2, 10 or 16. + * * @param size the bit-width of the constant * @param s the string representation of the constant * @param base the base of the string representation (2, 10, or 16) @@ -2064,7 +2073,8 @@ class CVC4_PUBLIC Solver Term mkBitVector(uint32_t size, const char* s, uint32_t base) const; /** - * Create a bit-vector constant of a given bit-width from a given string. + * Create a bit-vector constant of a given bit-width from a given string of + * base 2, 10 or 16. * @param size the bit-width of the constant * @param s the string representation of the constant * @param base the base of the string representation (2, 10, or 16) diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 13c1f14dd..034a7774b 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -66,11 +66,29 @@ class CVC4_PUBLIC BitVector { } + /** + * BitVector constructor. + * + * The value of the bit-vector is passed in as string of base 2, 10 or 16. + * The size of resulting bit-vector is + * - base 2: the size of the binary string + * - base 10: the min. size required to represent the decimal as a bit-vector + * - base 16: the max. size required to represent the hexadecimal as a + * bit-vector (4 * size of the given value string) + * + * @param num The value of the bit-vector in string representation. + * @param base The base of the string representation. + */ BitVector(const std::string& num, unsigned base = 2) { - CheckArgument(base == 2 || base == 16, base); - d_size = base == 2 ? num.size() : num.size() * 4; + CheckArgument(base == 2 || base == 10 || base == 16, base); d_value = Integer(num, base); + switch (base) + { + case 10: d_size = d_value.length(); break; + case 16: d_size = num.size() * 4; break; + default: d_size = num.size(); + } } ~BitVector() {} |