Normalize val in BitVector(val_str, base) (#6955)

Fixes cpp API's mkBitVector(val_str, base) constructor.

5 files changed, 22 insertions, 2 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index aca5fa981..60ef49cb4 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5044,6 +5044,8 @@ Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const
   CVC5_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
   CVC5_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base)
       << "base 2, 10, or 16";
+  CVC5_API_ARG_CHECK_EXPECTED(s[0] != '-', s)
+      << "a positive value (since no size is specified)";
   //////// all checks before this line
   return mkValHelper<cvc5::BitVector>(cvc5::BitVector(s, base));
 }
@@ -5071,7 +5073,6 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
         << "Overflow in bitvector construction (specified bitvector size "
         << size << " too small to hold value " << s << ")";
   }
-
   return mkValHelper<cvc5::BitVector>(cvc5::BitVector(size, val));
 }
 
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 25057ff2f..a232f9c7e 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3288,7 +3288,8 @@ class CVC5_EXPORT Solver
    * - 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 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
    */
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 6e194ad41..cd0870722 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -76,12 +76,16 @@ class BitVector
    *            bit-vector (4 * size of the given value string)
    *
    * @param num The value of the bit-vector in string representation.
+   *            This cannot be a negative value.
    * @param base The base of the string representation.
    */
   BitVector(const std::string& num, unsigned base = 2)
   {
     CheckArgument(base == 2 || base == 10 || base == 16, base);
+    CheckArgument(num[0] != '-', num);
     d_value = Integer(num, base);
+    CheckArgument(d_value == d_value.abs(), num);
+    // Compute the length, *without* any negative sign.
     switch (base)
     {
       case 10: d_size = d_value.length(); break;
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 453ef1d24..0c4007411 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -323,6 +323,15 @@ TEST_F(TestApiBlackSolver, mkBitVector)
   ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC5ApiException);
   ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC5ApiException);
   ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC5ApiException);
+  // No size and negative string -> error
+  ASSERT_THROW(d_solver.mkBitVector("-1", 2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("-1", 10), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("-f", 16), CVC5ApiException);
+  // size and negative string -> ok
+  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), d_solver.mkBitVector(4, "1111", 2));
+  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), d_solver.mkBitVector(4, "1111", 2));
+  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), d_solver.mkBitVector(4, "1111", 2));
+  ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10));
   ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10));
   ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16));
   ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp
index 2450747cd..98331cc7f 100644
--- a/test/unit/util/bitvector_black.cpp
+++ b/test/unit/util/bitvector_black.cpp
@@ -65,6 +65,11 @@ TEST_F(TestUtilBlackBitVector, string_constructor)
   ASSERT_EQ("000000011010", b4.toString());
   ASSERT_EQ("26", b4.toString(10));
   ASSERT_EQ("1a", b4.toString(16));
+
+  ASSERT_THROW(BitVector("-4", 10), IllegalArgumentException);
+  ASSERT_THROW(BitVector("-0010", 2), IllegalArgumentException);
+  ASSERT_THROW(BitVector("-3210", 4), IllegalArgumentException);
+  ASSERT_EQ(3, BitVector("4", 10).getSize());
 }
 
 TEST_F(TestUtilBlackBitVector, conversions)