Normalize val in BitVector(val_str, base) (#6955)
authorAlex Ozdemir <aozdemir@hmc.edu>
Thu, 5 Aug 2021 21:15:02 +0000 (14:15 -0700)
committerGitHub <noreply@github.com>
Thu, 5 Aug 2021 21:15:02 +0000 (21:15 +0000)
Fixes cpp API's mkBitVector(val_str, base) constructor.

src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/util/bitvector.h
test/unit/api/solver_black.cpp
test/unit/util/bitvector_black.cpp

index aca5fa9813989a35fbe8f72ac61748fed688f437..60ef49cb4833ab1aaba2ea8aac30e8b1e2e4cb27 100644 (file)
@@ -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));
 }
 
index 25057ff2f9fc6b3b452949443579c5ad900fe9f9..a232f9c7e70beae45cac96efd117b1d99253b878 100644 (file)
@@ -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
    */
index 6e194ad41ec28dfcbe5e70482ba216690b4ab6dd..cd0870722561d237775c076dca0c3b3f03a347b6 100644 (file)
@@ -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;
index 453ef1d24e8566eecb9c06781c13fdefdd77f93b..0c40074113ec4e415a36152c241d213c12ebcce2 100644 (file)
@@ -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");
index 2450747cdd0b24c1fea7ced8a577ef02e346ca57..98331cc7f8a6c50fdc8948ede786d7d96c02553c 100644 (file)
@@ -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)