diff options
| -rw-r--r-- | src/api/cvc4cpp.h | 16 | ||||
| -rw-r--r-- | src/util/bitvector.h | 22 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 15 |
3 files changed, 44 insertions, 9 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() {} diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index e3f9e0852..c42854fce 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -267,16 +267,23 @@ void SolverBlack::testMkBitVector() { uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2; uint64_t val2 = 2; + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 10)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1234", 10)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("a09f", 16)); TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val1), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("", 2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("10", 3), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("20", 2), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16)); TS_ASSERT_THROWS(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&); + TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), + d_solver->mkBitVector("10", 10)); + TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), + d_solver->mkBitVector("a", 16)); TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(), "0bin01010101"); TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), |