diff options
Diffstat (limited to 'src/api/cpp/cvc5.h')
-rw-r--r-- | src/api/cpp/cvc5.h | 22 |
1 files changed, 6 insertions, 16 deletions
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3226dd4fd..3c0241311 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3304,6 +3304,9 @@ class CVC5_EXPORT Solver /** * Create a bit-vector constant of given size and value. + * + * Note: The given value must fit into a bit-vector of the given size. + * * @param size the bit-width of the bit-vector sort * @param val the value of the constant * @return the bit-vector constant @@ -3311,24 +3314,11 @@ class CVC5_EXPORT Solver Term mkBitVector(uint32_t size, uint64_t val = 0) const; /** - * 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. - * This cannot be negative. - * @param base the base of the string representation (2, 10, or 16) - * @return the bit-vector constant - */ - 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 of * base 2, 10 or 16. + * + * Note: The given value must fit into a bit-vector of the given size. + * * @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) |