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))
return mkValHelper<cvc5::BitVector>(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>(cvc5::BitVector(s, base));
-}
-
Term Solver::mkBVFromStrHelper(uint32_t size,
const std::string& s,
uint32_t base) 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
/**
* 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)
cdef Py_ssize_t size
cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
if isinstance(useEscSequences, bool):
- term.cterm = self.csolver.mkString(s.encode(), <bint> useEscSequences)
+ term.cterm = self.csolver.mkString(
+ s.encode(), <bint> useEscSequences)
else:
term.cterm = self.csolver.mkString(c_wstring(tmp, size))
PyMem_Free(tmp)
'''
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(<uint32_t> size)
- else:
- assert isinstance(args[0], str)
- val = args[0]
- term.cterm = self.csolver.mkBitVector(<const string&> str(val).encode())
+ term.cterm = self.csolver.mkBitVector(<uint32_t> 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(<uint32_t> size, <uint32_t> val)
- else:
- assert isinstance(args[0], str)
- assert isinstance(args[1], int)
- val = args[0]
- base = args[1]
- term.cterm = self.csolver.mkBitVector(<const string&> str(val).encode(), <uint32_t> 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(
+ <uint32_t> size, <uint32_t> 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(<uint32_t> size, <const string&> str(val).encode(), <uint32_t> 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(<uint32_t> size_or_str)
- else:
- term.cterm = self.csolver.mkBitVector(<uint32_t> size_or_str,
- <const string &> str(val).encode(),
- 10)
- elif isinstance(size_or_str, str):
- # handle default value
- if val is None:
- term.cterm = self.csolver.mkBitVector(
- <const string &> size_or_str.encode())
- else:
- term.cterm = self.csolver.mkBitVector(
- <const string &> size_or_str.encode(), <uint32_t> 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(
+ <uint32_t> size,
+ <const string&> str(val).encode(),
+ <uint32_t> 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):
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):
| 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); }
{
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
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) ==\
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):
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()
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()
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)
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),
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)
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());
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));
}
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());
projects / cvc5.git / commitdiff