Fixes cpp API's mkBitVector(val_str, base) constructor.
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));
}
<< "Overflow in bitvector construction (specified bitvector size "
<< size << " too small to hold value " << s << ")";
}
-
return mkValHelper<cvc5::BitVector>(cvc5::BitVector(size, val));
}
* - 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
*/
* 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;
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");
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)