diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.h | 16 |
1 files changed, 13 insertions, 3 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) |