BitVector: Allow base 10 in constructor. (#2870)

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)