api: Require size argument for mkBitVector. (#6998)

This removes support for creating bit-vectors from a string without a
size argument. We further also now require that the base argument is
always given (it has no default value).

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)