From 7e3457b0e16cacef456287ae761c5293be1209d5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 18 Mar 2019 16:07:03 -0700 Subject: BitVector: Allow base 10 in constructor. (#2870) --- src/api/cvc4cpp.h | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'src/api') 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) -- cgit v1.2.3