From: Aina Niemetz Date: Mon, 23 Aug 2021 16:50:06 +0000 (-0700) Subject: api: Require size argument for mkBitVector. (#6998) X-Git-Tag: cvc5-1.0.0~1351 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99af3afc7e1cd80b62e151fb7c35cee7cf08d785;p=cvc5.git 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). --- diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 0001f726b..d6ba8d754 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -61,8 +61,14 @@ if __name__ == "__main__": slv.pop() # constrain x, y, z between -3.14 and 3.14 (also disallows NaN and infinity) - a = slv.mkFloatingPoint(8, 24, slv.mkBitVector("11000000010010001111010111000011", 2)) # -3.14 - b = slv.mkFloatingPoint(8, 24, slv.mkBitVector("01000000010010001111010111000011", 2)) # 3.14 + a = slv.mkFloatingPoint( + 8, + 24, + slv.mkBitVector(32, "11000000010010001111010111000011", 2)) # -3.14 + b = slv.mkFloatingPoint( + 8, + 24, + slv.mkBitVector(32, "01000000010010001111010111000011", 2)) # 3.14 bounds_x = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, x), slv.mkTerm(kinds.FPLeq, x, b)) bounds_y = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, y), slv.mkTerm(kinds.FPLeq, y, b)) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index f5e2c8f0c..12c59c0de 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5037,17 +5037,6 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const return mkValHelper(cvc5::BitVector(size, val)); } -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(s, base)); -} - Term Solver::mkBVFromStrHelper(uint32_t size, const std::string& s, uint32_t base) const @@ -5948,16 +5937,6 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkBitVector(const std::string& s, uint32_t base) const -{ - NodeManagerScope scope(getNodeManager()); - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return mkBVFromStrHelper(s, base); - //////// - CVC5_API_TRY_CATCH_END; -} - Term Solver::mkBitVector(uint32_t size, const std::string& s, uint32_t base) const 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,31 +3304,21 @@ 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 */ 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) diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 210eb0639..7c9a70642 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -832,7 +832,8 @@ cdef class Solver: cdef Py_ssize_t size cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size) if isinstance(useEscSequences, bool): - term.cterm = self.csolver.mkString(s.encode(), useEscSequences) + term.cterm = self.csolver.mkString( + s.encode(), useEscSequences) else: term.cterm = self.csolver.mkString(c_wstring(tmp, size)) PyMem_Free(tmp) @@ -853,62 +854,43 @@ cdef class Solver: ''' Supports the following arguments: Term mkBitVector(int size, int val=0) - Term mkBitVector(string val, int base = 2) Term mkBitVector(int size, string val, int base) ''' cdef Term term = Term(self) + if len(args) == 0: + raise ValueError("Missing arguments to mkBitVector") + size = args[0] + if not isinstance(size, int): + raise ValueError( + "Invalid first argument to mkBitVector '{}', " + "expected bit-vector size".format(size)) if len(args) == 1: - size_or_val = args[0] - if isinstance(args[0], int): - size = args[0] - term.cterm = self.csolver.mkBitVector( size) - else: - assert isinstance(args[0], str) - val = args[0] - term.cterm = self.csolver.mkBitVector( str(val).encode()) + term.cterm = self.csolver.mkBitVector( size) elif len(args) == 2: - if isinstance(args[0], int): - size = args[0] - assert isinstance(args[1], int) - val = args[1] - term.cterm = self.csolver.mkBitVector( size, val) - else: - assert isinstance(args[0], str) - assert isinstance(args[1], int) - val = args[0] - base = args[1] - term.cterm = self.csolver.mkBitVector( str(val).encode(), base) + val = args[1] + if not isinstance(val, int): + raise ValueError( + "Invalid second argument to mkBitVector '{}', " + "expected integer value".format(size)) + term.cterm = self.csolver.mkBitVector( + size, val) elif len(args) == 3: - assert isinstance(args[0], int) - assert isinstance(args[1], str) - assert isinstance(args[2], int) - size = args[0] - val = args[1] - base = args[2] - term.cterm = self.csolver.mkBitVector( size, str(val).encode(), base) - return term - - - def mkBitVector(self, size_or_str, val = None): - cdef Term term = Term(self) - if isinstance(size_or_str, int): - if val is None: - term.cterm = self.csolver.mkBitVector( size_or_str) - else: - term.cterm = self.csolver.mkBitVector( size_or_str, - str(val).encode(), - 10) - elif isinstance(size_or_str, str): - # handle default value - if val is None: - term.cterm = self.csolver.mkBitVector( - size_or_str.encode()) - else: - term.cterm = self.csolver.mkBitVector( - size_or_str.encode(), val) + val = args[1] + base = args[2] + if not isinstance(val, str): + raise ValueError( + "Invalid second argument to mkBitVector '{}', " + "expected value string".format(size)) + if not isinstance(base, int): + raise ValueError( + "Invalid third argument to mkBitVector '{}', " + "expected base given as integer".format(size)) + term.cterm = self.csolver.mkBitVector( + size, + str(val).encode(), + base) else: - raise ValueError("Unexpected inputs {} to" - " mkBitVector".format((size_or_str, val))) + raise ValueError("Unexpected inputs to mkBitVector") return term def mkConstArray(self, Sort sort, Term val): @@ -956,8 +938,9 @@ cdef class Solver: try: term.cterm = self.csolver.mkAbstractValue(str(index).encode()) except: - raise ValueError("mkAbstractValue expects a str representing a number" - " or an int, but got{}".format(index)) + raise ValueError( + "mkAbstractValue expects a str representing a number" + " or an int, but got{}".format(index)) return term def mkFloatingPoint(self, int exp, int sig, Term val): diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index c0a42ac26..f0cb0fc78 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2196,12 +2196,12 @@ simpleTerm[cvc5::api::Term& f] | HEX_LITERAL { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); - f = SOLVER->mkBitVector(hexString, 16); + f = SOLVER->mkBitVector(hexString.size() * 4, hexString, 16); } | BINARY_LITERAL { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); - f = SOLVER->mkBitVector(binString, 2); + f = SOLVER->mkBitVector(binString.size(), binString, 2); } /* record literals */ | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c3cf3ea66..22a042951 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1756,13 +1756,13 @@ termAtomic[cvc5::api::Term& atomTerm] { Assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - atomTerm = SOLVER->mkBitVector(hexStr, 16); + atomTerm = SOLVER->mkBitVector(hexStr.size() * 4, hexStr, 16); } | BINARY_LITERAL { Assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0); std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); - atomTerm = SOLVER->mkBitVector(binStr, 2); + atomTerm = SOLVER->mkBitVector(binStr.size(), binStr, 2); } // String constant diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 8b3ce944e..db49f8bea 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -291,35 +291,64 @@ def test_mk_tuple_sort(solver): def test_mk_bit_vector(solver): - size0 = 0 - size1 = 8 - size2 = 32 - val1 = 2 - val2 = 2 - solver.mkBitVector(size1, val1) - solver.mkBitVector(size2, val2) - solver.mkBitVector("1010", 2) - solver.mkBitVector("1010", 10) - solver.mkBitVector("1234", 10) - solver.mkBitVector("1010", 16) - solver.mkBitVector("a09f", 16) + solver.mkBitVector(8, 2) + solver.mkBitVector(32, 2) + + solver.mkBitVector(4, "1010", 2) + solver.mkBitVector(8, "0101", 2) + solver.mkBitVector(8, "-1111111", 2) + solver.mkBitVector(8, "00000101", 2) solver.mkBitVector(8, "-127", 10) + solver.mkBitVector(8, "255", 10) + solver.mkBitVector(10, "1010", 10) + solver.mkBitVector(11, "1234", 10) + solver.mkBitVector(8, "-7f", 16) + solver.mkBitVector(8, "a0", 16) + solver.mkBitVector(16, "1010", 16) + solver.mkBitVector(16, "a09f", 16) + with pytest.raises(RuntimeError): - solver.mkBitVector(size0, val1) + solver.mkBitVector(0, 2) with pytest.raises(RuntimeError): - solver.mkBitVector(size0, val2) + solver.mkBitVector(0, "-127", 10) with pytest.raises(RuntimeError): - solver.mkBitVector("", 2) + solver.mkBitVector(0, "a0", 16) + + with pytest.raises(RuntimeError): + solver.mkBitVector(2, "", 2) + with pytest.raises(RuntimeError): - solver.mkBitVector("10", 3) + solver.mkBitVector(8, "101", 5) with pytest.raises(RuntimeError): - solver.mkBitVector("20", 2) + solver.mkBitVector(8, "127", 11) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "a0", 21) + with pytest.raises(RuntimeError): solver.mkBitVector(8, "101010101", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-11111111", 2) with pytest.raises(RuntimeError): solver.mkBitVector(8, "-256", 10) - assert solver.mkBitVector("1010", 2) == solver.mkBitVector("10", 10) - assert solver.mkBitVector("1010", 2) == solver.mkBitVector("a", 16) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "257", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-a0", 16) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "fffff", 16) + + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "10201010", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-25x", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "2x7", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "fzff", 16) + + assert solver.mkBitVector(8, "0101", 2) == solver.mkBitVector(8, "00000101", 2) + assert solver.mkBitVector(4, "1010", 2) == solver.mkBitVector(4, "10", 10) + assert solver.mkBitVector(4, "1010", 2) == solver.mkBitVector(4, "a", 16) assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101" assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111" assert solver.mkBitVector(8, "-1", 10) ==\ @@ -820,21 +849,21 @@ def test_mk_true(solver): def test_mk_tuple(solver): - solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector(3, "101", 2)]) solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) with pytest.raises(RuntimeError): - solver.mkTuple([], [solver.mkBitVector("101", 2)]) + solver.mkTuple([], [solver.mkBitVector(3, "101", 2)]) with pytest.raises(RuntimeError): solver.mkTuple([solver.mkBitVectorSort(4)], - [solver.mkBitVector("101", 2)]) + [solver.mkBitVector(3, "101", 2)]) with pytest.raises(RuntimeError): solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")]) slv = pycvc5.Solver() with pytest.raises(RuntimeError): - slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector("101", 2)]) + slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector(3, "101", 2)]) with pytest.raises(RuntimeError): - slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector(3, "101", 2)]) def test_mk_universe_set(solver): diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py index e78188079..e65299676 100644 --- a/test/python/unit/api/test_term.py +++ b/test/python/unit/api/test_term.py @@ -1040,7 +1040,7 @@ def test_get_uninterpreted_const(solver): def test_get_floating_point(solver): - bvval = solver.mkBitVector("0000110000000011") + bvval = solver.mkBitVector(16, "0000110000000011", 2) fp = solver.mkFloatingPoint(5, 11, bvval) assert fp.isFloatingPointValue() @@ -1181,12 +1181,12 @@ def test_get_boolean(solver): def test_get_bit_vector(solver): b1 = solver.mkBitVector(8, 15) - b2 = solver.mkBitVector("00001111", 2) - b3 = solver.mkBitVector("15", 10) - b4 = solver.mkBitVector("0f", 16) - b5 = solver.mkBitVector(8, "00001111", 2) - b6 = solver.mkBitVector(8, "15", 10) - b7 = solver.mkBitVector(8, "0f", 16) + b2 = solver.mkBitVector(8, "00001111", 2) + b3 = solver.mkBitVector(8, "15", 10) + b4 = solver.mkBitVector(8, "0f", 16) + b5 = solver.mkBitVector(9, "00001111", 2); + b6 = solver.mkBitVector(9, "15", 10); + b7 = solver.mkBitVector(9, "0f", 16); assert b1.isBitVectorValue() assert b2.isBitVectorValue() @@ -1202,19 +1202,19 @@ def test_get_bit_vector(solver): assert "00001111" == b2.getBitVectorValue(2) assert "15" == b2.getBitVectorValue(10) assert "f" == b2.getBitVectorValue(16) - assert "1111" == b3.getBitVectorValue(2) + assert "00001111" == b3.getBitVectorValue(2) assert "15" == b3.getBitVectorValue(10) assert "f" == b3.getBitVectorValue(16) assert "00001111" == b4.getBitVectorValue(2) assert "15" == b4.getBitVectorValue(10) assert "f" == b4.getBitVectorValue(16) - assert "00001111" == b5.getBitVectorValue(2) + assert "000001111" == b5.getBitVectorValue(2) assert "15" == b5.getBitVectorValue(10) assert "f" == b5.getBitVectorValue(16) - assert "00001111" == b6.getBitVectorValue(2) + assert "000001111" == b6.getBitVectorValue(2) assert "15" == b6.getBitVectorValue(10) assert "f" == b6.getBitVectorValue(16) - assert "00001111" == b7.getBitVectorValue(2) + assert "000001111" == b7.getBitVectorValue(2) assert "15" == b7.getBitVectorValue(10) assert "f" == b7.getBitVectorValue(16) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 0c4007411..99a60aa76 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -306,34 +306,43 @@ TEST_F(TestApiBlackSolver, mkTupleSort) TEST_F(TestApiBlackSolver, mkBitVector) { - uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2; - uint64_t val2 = 2; - ASSERT_NO_THROW(d_solver.mkBitVector(size1, val1)); - ASSERT_NO_THROW(d_solver.mkBitVector(size2, val2)); - ASSERT_NO_THROW(d_solver.mkBitVector("1010", 2)); - ASSERT_NO_THROW(d_solver.mkBitVector("1010", 10)); - ASSERT_NO_THROW(d_solver.mkBitVector("1234", 10)); - ASSERT_NO_THROW(d_solver.mkBitVector("1010", 16)); - ASSERT_NO_THROW(d_solver.mkBitVector("a09f", 16)); + ASSERT_NO_THROW(d_solver.mkBitVector(8, 2)); + ASSERT_NO_THROW(d_solver.mkBitVector(32, 2)); + ASSERT_NO_THROW(d_solver.mkBitVector(8, "-1111111", 2)); + ASSERT_NO_THROW(d_solver.mkBitVector(8, "0101", 2)); + ASSERT_NO_THROW(d_solver.mkBitVector(8, "00000101", 2)); ASSERT_NO_THROW(d_solver.mkBitVector(8, "-127", 10)); - ASSERT_THROW(d_solver.mkBitVector(size0, val1), CVC5ApiException); - ASSERT_THROW(d_solver.mkBitVector(size0, val2), CVC5ApiException); - ASSERT_THROW(d_solver.mkBitVector("", 2), CVC5ApiException); - ASSERT_THROW(d_solver.mkBitVector("10", 3), CVC5ApiException); - ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkBitVector(8, "255", 10)); + ASSERT_NO_THROW(d_solver.mkBitVector(8, "-7f", 16)); + ASSERT_NO_THROW(d_solver.mkBitVector(8, "a0", 16)); + + ASSERT_THROW(d_solver.mkBitVector(0, 2), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(0, "-127", 10), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(0, "a0", 16), CVC5ApiException); + + ASSERT_THROW(d_solver.mkBitVector(8, "", 2), CVC5ApiException); + + ASSERT_THROW(d_solver.mkBitVector(8, "101", 5), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "128", 11), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "a0", 21), CVC5ApiException); + + ASSERT_THROW(d_solver.mkBitVector(8, "-11111111", 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_THROW(d_solver.mkBitVector(8, "257", 10), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "-a0", 16), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "fffff", 16), CVC5ApiException); + + ASSERT_THROW(d_solver.mkBitVector(8, "10201010", 2), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "-25x", 10), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "2x7", 10), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector(8, "fzff", 16), CVC5ApiException); + + ASSERT_EQ(d_solver.mkBitVector(8, "0101", 2), + d_solver.mkBitVector(8, "00000101", 2)); 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(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111"); ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10), @@ -778,25 +787,25 @@ TEST_F(TestApiBlackSolver, mkTrue) TEST_F(TestApiBlackSolver, mkTuple) { ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)}, - {d_solver.mkBitVector("101", 2)})); + {d_solver.mkBitVector(3, "101", 2)})); ASSERT_NO_THROW( d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")})); - ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}), + ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector(3, "101", 2)}), CVC5ApiException); ASSERT_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(4)}, - {d_solver.mkBitVector("101", 2)}), + {d_solver.mkBitVector(3, "101", 2)}), CVC5ApiException); ASSERT_THROW( d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}), CVC5ApiException); Solver slv; - ASSERT_THROW( - slv.mkTuple({d_solver.mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}), - CVC5ApiException); - ASSERT_THROW( - slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver.mkBitVector("101", 2)}), - CVC5ApiException); + ASSERT_THROW(slv.mkTuple({d_solver.mkBitVectorSort(3)}, + {slv.mkBitVector(3, "101", 2)}), + CVC5ApiException); + ASSERT_THROW(slv.mkTuple({slv.mkBitVectorSort(3)}, + {d_solver.mkBitVector(3, "101", 2)}), + CVC5ApiException); } TEST_F(TestApiBlackSolver, mkUniverseSet) diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 96ee1ba47..fe5838cd4 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -845,12 +845,12 @@ TEST_F(TestApiBlackTerm, getBoolean) TEST_F(TestApiBlackTerm, getBitVector) { Term b1 = d_solver.mkBitVector(8, 15); - Term b2 = d_solver.mkBitVector("00001111", 2); - Term b3 = d_solver.mkBitVector("15", 10); - Term b4 = d_solver.mkBitVector("0f", 16); - Term b5 = d_solver.mkBitVector(8, "00001111", 2); - Term b6 = d_solver.mkBitVector(8, "15", 10); - Term b7 = d_solver.mkBitVector(8, "0f", 16); + Term b2 = d_solver.mkBitVector(8, "00001111", 2); + Term b3 = d_solver.mkBitVector(8, "15", 10); + Term b4 = d_solver.mkBitVector(8, "0f", 16); + Term b5 = d_solver.mkBitVector(9, "00001111", 2); + Term b6 = d_solver.mkBitVector(9, "15", 10); + Term b7 = d_solver.mkBitVector(9, "0f", 16); ASSERT_TRUE(b1.isBitVectorValue()); ASSERT_TRUE(b2.isBitVectorValue()); @@ -866,19 +866,19 @@ TEST_F(TestApiBlackTerm, getBitVector) ASSERT_EQ("00001111", b2.getBitVectorValue(2)); ASSERT_EQ("15", b2.getBitVectorValue(10)); ASSERT_EQ("f", b2.getBitVectorValue(16)); - ASSERT_EQ("1111", b3.getBitVectorValue(2)); + ASSERT_EQ("00001111", b3.getBitVectorValue(2)); ASSERT_EQ("15", b3.getBitVectorValue(10)); ASSERT_EQ("f", b3.getBitVectorValue(16)); ASSERT_EQ("00001111", b4.getBitVectorValue(2)); ASSERT_EQ("15", b4.getBitVectorValue(10)); ASSERT_EQ("f", b4.getBitVectorValue(16)); - ASSERT_EQ("00001111", b5.getBitVectorValue(2)); + ASSERT_EQ("000001111", b5.getBitVectorValue(2)); ASSERT_EQ("15", b5.getBitVectorValue(10)); ASSERT_EQ("f", b5.getBitVectorValue(16)); - ASSERT_EQ("00001111", b6.getBitVectorValue(2)); + ASSERT_EQ("000001111", b6.getBitVectorValue(2)); ASSERT_EQ("15", b6.getBitVectorValue(10)); ASSERT_EQ("f", b6.getBitVectorValue(16)); - ASSERT_EQ("00001111", b7.getBitVectorValue(2)); + ASSERT_EQ("000001111", b7.getBitVectorValue(2)); ASSERT_EQ("15", b7.getBitVectorValue(10)); ASSERT_EQ("f", b7.getBitVectorValue(16)); } @@ -915,7 +915,7 @@ TEST_F(TestApiBlackTerm, getTuple) TEST_F(TestApiBlackTerm, getFloatingPoint) { - Term bvval = d_solver.mkBitVector("0000110000000011"); + Term bvval = d_solver.mkBitVector(16, "0000110000000011", 2); Term fp = d_solver.mkFloatingPoint(5, 11, bvval); ASSERT_TRUE(fp.isFloatingPointValue());