diff options
Diffstat (limited to 'test/python')
-rw-r--r-- | test/python/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/python/unit/api/test_op.py | 178 | ||||
-rw-r--r-- | test/python/unit/api/test_result.py | 115 | ||||
-rw-r--r-- | test/python/unit/api/test_solver.py | 388 | ||||
-rw-r--r-- | test/python/unit/api/test_sort.py | 32 |
5 files changed, 635 insertions, 80 deletions
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt index 54134b510..5b681ca36 100644 --- a/test/python/CMakeLists.txt +++ b/test/python/CMakeLists.txt @@ -33,3 +33,5 @@ cvc5_add_python_api_test(pytest_term unit/api/test_term.py) cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py) cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py) cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py) +cvc5_add_python_api_test(pytest_op unit/api/test_op.py) +cvc5_add_python_api_test(pytest_result unit/api/test_result.py) diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py new file mode 100644 index 000000000..07a57a5c6 --- /dev/null +++ b/test/python/unit/api/test_op.py @@ -0,0 +1,178 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Unit tests for op API. +# +# Obtained by translating test/unit/api/op_black.cpp +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort +from pycvc5 import Op + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_get_kind(solver): + x = solver.mkOp(kinds.BVExtract, 31, 1) + x.getKind() + + +def test_is_null(solver): + x = Op(solver) + assert x.isNull() + x = solver.mkOp(kinds.BVExtract, 31, 1) + assert not x.isNull() + + +def test_op_from_kind(solver): + solver.mkOp(kinds.Plus) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract) + + +def test_get_num_indices(solver): + plus = solver.mkOp(kinds.Plus) + divisible = solver.mkOp(kinds.Divisible, 4) + bitvector_repeat = solver.mkOp(kinds.BVRepeat, 5) + bitvector_zero_extend = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_sign_extend = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_rotate_left = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_right = solver.mkOp(kinds.BVRotateRight, 9) + int_to_bitvector = solver.mkOp(kinds.IntToBV, 10) + iand = solver.mkOp(kinds.Iand, 3) + floatingpoint_to_ubv = solver.mkOp(kinds.FPToUbv, 11) + floatingopint_to_sbv = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_fp_ieee_bitvector = solver.mkOp(kinds.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_floatingpoint = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_real = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_signed_bitvector = solver.mkOp(kinds.FPToFpSignedBV, 4, + 25) + floatingpoint_to_fp_unsigned_bitvector = solver.mkOp( + kinds.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_generic = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + regexp_loop = solver.mkOp(kinds.RegexpLoop, 2, 3) + + assert 0 == plus.getNumIndices() + assert 1 == divisible.getNumIndices() + assert 1 == bitvector_repeat.getNumIndices() + assert 1 == bitvector_zero_extend.getNumIndices() + assert 1 == bitvector_sign_extend.getNumIndices() + assert 1 == bitvector_rotate_left.getNumIndices() + assert 1 == bitvector_rotate_right.getNumIndices() + assert 1 == int_to_bitvector.getNumIndices() + assert 1 == iand.getNumIndices() + assert 1 == floatingpoint_to_ubv.getNumIndices() + assert 1 == floatingopint_to_sbv.getNumIndices() + assert 2 == floatingpoint_to_fp_ieee_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_floatingpoint.getNumIndices() + assert 2 == floatingpoint_to_fp_real.getNumIndices() + assert 2 == floatingpoint_to_fp_signed_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_unsigned_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_generic.getNumIndices() + assert 2 == regexp_loop.getNumIndices() + + +def test_get_indices_string(solver): + x = Op(solver) + with pytest.raises(RuntimeError): + x.getIndices() + + divisible_ot = solver.mkOp(kinds.Divisible, 4) + assert divisible_ot.isIndexed() + divisible_idx = divisible_ot.getIndices() + assert divisible_idx == "4" + + +def test_get_indices_uint(solver): + bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + assert bitvector_repeat_ot.isIndexed() + bitvector_repeat_idx = bitvector_repeat_ot.getIndices() + assert bitvector_repeat_idx == 5 + + bitvector_zero_extend_ot = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices() + assert bitvector_zero_extend_idx == 6 + + bitvector_sign_extend_ot = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices() + assert bitvector_sign_extend_idx == 7 + + bitvector_rotate_left_ot = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices() + assert bitvector_rotate_left_idx == 8 + + bitvector_rotate_right_ot = solver.mkOp(kinds.BVRotateRight, 9) + bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices() + assert bitvector_rotate_right_idx == 9 + + int_to_bitvector_ot = solver.mkOp(kinds.IntToBV, 10) + int_to_bitvector_idx = int_to_bitvector_ot.getIndices() + assert int_to_bitvector_idx == 10 + + floatingpoint_to_ubv_ot = solver.mkOp(kinds.FPToUbv, 11) + floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices() + assert floatingpoint_to_ubv_idx == 11 + + floatingpoint_to_sbv_ot = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices() + assert floatingpoint_to_sbv_idx == 13 + + +def test_get_indices_pair_uint(solver): + bitvector_extract_ot = solver.mkOp(kinds.BVExtract, 4, 0) + assert bitvector_extract_ot.isIndexed() + bitvector_extract_indices = bitvector_extract_ot.getIndices() + assert bitvector_extract_indices == (4, 0) + + floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp( + kinds.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25) + + floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices( + ) + assert floatingpoint_to_fp_floatingpoint_indices == (4, 25) + + floatingpoint_to_fp_real_ot = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices() + assert floatingpoint_to_fp_real_indices == (4, 25) + + floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp( + kinds.FPToFpSignedBV, 4, 25) + floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25) + + floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp( + kinds.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25) + + floatingpoint_to_fp_generic_ot = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices( + ) + assert floatingpoint_to_fp_generic_indices == (4, 25) + + +def test_op_scoping_to_string(solver): + bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + op_repr = str(bitvector_repeat_ot) + assert str(bitvector_repeat_ot) == op_repr diff --git a/test/python/unit/api/test_result.py b/test/python/unit/api/test_result.py new file mode 100644 index 000000000..bd97646f9 --- /dev/null +++ b/test/python/unit/api/test_result.py @@ -0,0 +1,115 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Unit tests for result API. +# +# Obtained by translating test/unit/api/result_black.cpp +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Result +from pycvc5 import UnknownExplanation + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_is_null(solver): + res_null = Result(solver) + assert res_null.isNull() + assert not res_null.isSat() + assert not res_null.isUnsat() + assert not res_null.isSatUnknown() + assert not res_null.isEntailed() + assert not res_null.isNotEntailed() + assert not res_null.isEntailmentUnknown() + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res = solver.checkSat() + assert not res.isNull() + + +def test_eq(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res2 = solver.checkSat() + res3 = solver.checkSat() + res = res2 + assert res == res2 + assert res3 == res2 + + +def test_is_sat(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res = solver.checkSat() + assert res.isSat() + assert not res.isSatUnknown() + + +def test_is_unsat(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkSat() + assert res.isUnsat() + assert not res.isSatUnknown() + + +def test_is_sat_unknown(solver): + solver.setLogic("QF_NIA") + solver.setOption("incremental", "false") + solver.setOption("solve-int-as-bv", "32") + int_sort = solver.getIntegerSort() + x = solver.mkVar(int_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkSat() + assert not res.isSat() + assert res.isSatUnknown() + + +def test_is_entailed(solver): + solver.setOption("incremental", "true") + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkConst(u_sort, "x") + y = solver.mkConst(u_sort, "y") + a = x.eqTerm(y).notTerm() + b = x.eqTerm(y) + solver.assertFormula(a) + entailed = solver.checkEntailed(a) + assert entailed.isEntailed() + assert not entailed.isEntailmentUnknown() + not_entailed = solver.checkEntailed(b) + assert not_entailed.isNotEntailed() + assert not not_entailed.isEntailmentUnknown() + + +def test_is_entailment_unknown(solver): + solver.setLogic("QF_NIA") + solver.setOption("incremental", "false") + solver.setOption("solve-int-as-bv", "32") + int_sort = solver.getIntegerSort() + x = solver.mkVar(int_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkEntailed(x.eqTerm(x)) + assert not res.isEntailed() + assert res.isEntailmentUnknown() + print(type(pycvc5.RoundTowardZero)) + print(type(pycvc5.UnknownReason)) + assert res.getUnknownExplanation() == pycvc5.UnknownReason diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 44ce684dd..8b3ce944e 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -32,11 +32,7 @@ def test_recoverable_exception(solver): def test_supports_floating_point(solver): - if solver.supportsFloatingPoint(): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) - else: - with pytest.raises(RuntimeError): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) def test_get_boolean_sort(solver): @@ -47,6 +43,10 @@ def test_get_integer_sort(solver): solver.getIntegerSort() +def test_get_null_sort(solver): + solver.getNullSort() + + def test_get_real_sort(solver): solver.getRealSort() @@ -60,11 +60,7 @@ def test_get_string_sort(solver): def test_get_rounding_mode_sort(solver): - if solver.supportsFloatingPoint(): - solver.getRoundingModeSort() - else: - with pytest.raises(RuntimeError): - solver.getRoundingModeSort() + solver.getRoundingModeSort() def test_mk_array_sort(solver): @@ -79,10 +75,9 @@ def test_mk_array_sort(solver): solver.mkArraySort(boolSort, intSort) solver.mkArraySort(realSort, bvSort) - if (solver.supportsFloatingPoint()): - fpSort = solver.mkFloatingPointSort(3, 5) - solver.mkArraySort(fpSort, fpSort) - solver.mkArraySort(bvSort, fpSort) + fpSort = solver.mkFloatingPointSort(3, 5) + solver.mkArraySort(fpSort, fpSort) + solver.mkArraySort(bvSort, fpSort) slv = pycvc5.Solver() with pytest.raises(RuntimeError): @@ -96,15 +91,11 @@ def test_mk_bit_vector_sort(solver): def test_mk_floating_point_sort(solver): - if solver.supportsFloatingPoint(): - solver.mkFloatingPointSort(4, 8) - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(0, 8) - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(4, 0) - else: - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(4, 8) + solver.mkFloatingPointSort(4, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(0, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(4, 0) def test_mk_datatype_sort(solver): @@ -257,6 +248,15 @@ def test_mk_set_sort(solver): slv.mkSetSort(solver.mkBitVectorSort(4)) +def test_mk_bag_sort(solver): + solver.mkBagSort(solver.getBooleanSort()) + solver.mkBagSort(solver.getIntegerSort()) + solver.mkBagSort(solver.mkBitVectorSort(4)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkBagSort(solver.mkBitVectorSort(4)) + + def test_mk_sequence_sort(solver): solver.mkSequenceSort(solver.getBooleanSort()) solver.mkSequenceSort(\ @@ -290,6 +290,42 @@ def test_mk_tuple_sort(solver): slv.mkTupleSort([solver.getIntegerSort()]) +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, "-127", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(size0, val1) + with pytest.raises(RuntimeError): + solver.mkBitVector(size0, val2) + with pytest.raises(RuntimeError): + solver.mkBitVector("", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector("10", 3) + with pytest.raises(RuntimeError): + solver.mkBitVector("20", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "101010101", 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) + assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101" + assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111" + assert solver.mkBitVector(8, "-1", 10) ==\ + solver.mkBitVector(8, "FF", 16) + + def test_mk_var(solver): boolSort = solver.getBooleanSort() intSort = solver.getIntegerSort() @@ -313,11 +349,7 @@ def test_mk_boolean(solver): def test_mk_rounding_mode(solver): - if solver.supportsFloatingPoint(): - solver.mkRoundingMode(pycvc5.RoundTowardZero) - else: - with pytest.raises(RuntimeError): - solver.mkRoundingMode(pycvc5.RoundTowardZero) + solver.mkRoundingMode(pycvc5.RoundTowardZero) def test_mk_uninterpreted_const(solver): @@ -329,15 +361,31 @@ def test_mk_uninterpreted_const(solver): slv.mkUninterpretedConst(solver.getBooleanSort(), 1) +def test_mk_abstract_value(solver): + solver.mkAbstractValue("1") + with pytest.raises(ValueError): + solver.mkAbstractValue("0") + with pytest.raises(ValueError): + solver.mkAbstractValue("-1") + with pytest.raises(ValueError): + solver.mkAbstractValue("1.2") + with pytest.raises(ValueError): + solver.mkAbstractValue("1/2") + with pytest.raises(ValueError): + solver.mkAbstractValue("asdf") + + solver.mkAbstractValue(1) + with pytest.raises(ValueError): + solver.mkAbstractValue(-1) + with pytest.raises(ValueError): + solver.mkAbstractValue(0) + + def test_mk_floating_point(solver): t1 = solver.mkBitVector(8) t2 = solver.mkBitVector(4) t3 = solver.mkInteger(2) - if (solver.supportsFloatingPoint()): - solver.mkFloatingPoint(3, 5, t1) - else: - with pytest.raises(RuntimeError): - solver.mkFloatingPoint(3, 5, t1) + solver.mkFloatingPoint(3, 5, t1) with pytest.raises(RuntimeError): solver.mkFloatingPoint(0, 5, pycvc5.Term(solver)) @@ -350,10 +398,9 @@ def test_mk_floating_point(solver): with pytest.raises(RuntimeError): solver.mkFloatingPoint(3, 5, t2) - if (solver.supportsFloatingPoint()): - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkFloatingPoint(3, 5, t1) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkFloatingPoint(3, 5, t1) def test_mk_empty_set(solver): @@ -367,6 +414,17 @@ def test_mk_empty_set(solver): slv.mkEmptySet(s) +def test_mk_empty_bag(solver): + slv = pycvc5.Solver() + s = solver.mkBagSort(solver.getBooleanSort()) + solver.mkEmptyBag(pycvc5.Sort(solver)) + solver.mkEmptyBag(s) + with pytest.raises(RuntimeError): + solver.mkEmptyBag(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.mkEmptyBag(s) + + def test_mk_empty_sequence(solver): slv = pycvc5.Solver() s = solver.mkSequenceSort(solver.getBooleanSort()) @@ -382,43 +440,50 @@ def test_mk_false(solver): def test_mk_nan(solver): - if (solver.supportsFloatingPoint()): - solver.mkNaN(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNaN(3, 5) + solver.mkNaN(3, 5) def test_mk_neg_zero(solver): - if (solver.supportsFloatingPoint()): - solver.mkNegZero(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNegZero(3, 5) + solver.mkNegZero(3, 5) def test_mk_neg_inf(solver): - if (solver.supportsFloatingPoint()): - solver.mkNegInf(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNegInf(3, 5) + solver.mkNegInf(3, 5) def test_mk_pos_inf(solver): - if (solver.supportsFloatingPoint()): - solver.mkPosInf(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkPosInf(3, 5) + solver.mkPosInf(3, 5) def test_mk_pos_zero(solver): - if (solver.supportsFloatingPoint()): - solver.mkPosZero(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkPosZero(3, 5) + solver.mkPosZero(3, 5) + + +def test_mk_op(solver): + # mkOp(Kind kind, Kind k) + with pytest.raises(ValueError): + solver.mkOp(kinds.BVExtract, kinds.Equal) + + # mkOp(Kind kind, const std::string& arg) + solver.mkOp(kinds.Divisible, "2147483648") + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, "asdf") + + # mkOp(Kind kind, uint32_t arg) + solver.mkOp(kinds.Divisible, 1) + solver.mkOp(kinds.BVRotateLeft, 1) + solver.mkOp(kinds.BVRotateRight, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, 1) + + # mkOp(Kind kind, uint32_t arg1, uint32_t arg2) + solver.mkOp(kinds.BVExtract, 1, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.Divisible, 1, 2) + + # mkOp(Kind kind, std::vector<uint32_t> args) + args = [1, 2, 2] + solver.mkOp(kinds.TupleProject, args) def test_mk_pi(solver): @@ -568,11 +633,210 @@ def test_mk_sep_nil(solver): slv.mkSepNil(solver.getIntegerSort()) +def test_mk_string(solver): + solver.mkString("") + solver.mkString("asdfasdf") + str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\"" + str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\ + "\"asdf\\u{5c}nasdf\"" + + +def test_mk_term(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [a, b] + v2 = [a, pycvc5.Term(solver)] + v3 = [a, solver.mkTrue()] + v4 = [solver.mkInteger(1), solver.mkInteger(2)] + v5 = [solver.mkInteger(1), pycvc5.Term(solver)] + v6 = [] + slv = pycvc5.Solver() + + # mkTerm(Kind kind) const + solver.mkPi() + solver.mkTerm(kinds.RegexpEmpty) + solver.mkTerm(kinds.RegexpSigma) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ConstBV) + + # mkTerm(Kind kind, Term child) const + solver.mkTerm(kinds.Not, solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, a) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Not, solver.mkTrue()) + + # mkTerm(Kind kind, Term child1, Term child2) const + solver.mkTerm(kinds.Equal, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, solver.mkTrue()) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Equal, a, b) + + # mkTerm(Kind kind, Term child1, Term child2, Term child3) const + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + solver.mkTrue()) + + # mkTerm(Kind kind, const std::vector<Term>& children) const + solver.mkTerm(kinds.Equal, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v3) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Distinct, v6) + + +def test_mk_term_from_op(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [solver.mkInteger(1), solver.mkInteger(2)] + v2 = [solver.mkInteger(1), pycvc5.Term(solver)] + v3 = [] + v4 = [solver.mkInteger(5)] + slv = pycvc5.Solver() + + # simple operator terms + opterm1 = solver.mkOp(kinds.BVExtract, 2, 1) + opterm2 = solver.mkOp(kinds.Divisible, 1) + + # list datatype + sort = solver.mkParamSort("T") + listDecl = solver.mkDatatypeDecl("paramlist", sort) + cons = solver.mkDatatypeConstructorDecl("cons") + nil = solver.mkDatatypeConstructorDecl("nil") + cons.addSelector("head", sort) + cons.addSelectorSelf("tail") + listDecl.addConstructor(cons) + listDecl.addConstructor(nil) + listSort = solver.mkDatatypeSort(listDecl) + intListSort =\ + listSort.instantiate([solver.getIntegerSort()]) + c = solver.mkConst(intListSort, "c") + lis = listSort.getDatatype() + + # list datatype constructor and selector operator terms + consTerm1 = lis.getConstructorTerm("cons") + consTerm2 = lis.getConstructor("cons").getConstructorTerm() + nilTerm1 = lis.getConstructorTerm("nil") + nilTerm2 = lis.getConstructor("nil").getConstructorTerm() + headTerm1 = lis["cons"].getSelectorTerm("head") + headTerm2 = lis["cons"].getSelector("head").getSelectorTerm() + tailTerm1 = lis["cons"].getSelectorTerm("tail") + tailTerm2 = lis["cons"]["tail"].getSelectorTerm() + + # mkTerm(Op op, Term term) const + solver.mkTerm(kinds.ApplyConstructor, nilTerm1) + solver.mkTerm(kinds.ApplyConstructor, nilTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, nilTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, consTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, headTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor, nilTerm1) + + # mkTerm(Op op, Term child) const + solver.mkTerm(opterm1, a) + solver.mkTerm(opterm2, solver.mkInteger(1)) + solver.mkTerm(kinds.ApplySelector, headTerm1, c) + solver.mkTerm(kinds.ApplySelector, tailTerm2, c) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0)) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm1, a) + + # mkTerm(Op op, Term child1, Term child2) const + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0), + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1)) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor,\ + consTerm1,\ + solver.mkInteger(0),\ + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + + # mkTerm(Op op, Term child1, Term child2, Term child3) const + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1), + pycvc5.Term(solver)) + + # mkTerm(Op op, const std::vector<Term>& children) const + solver.mkTerm(opterm2, v4) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v3) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm2, v4) + + def test_mk_true(solver): solver.mkTrue() solver.mkTrue() +def test_mk_tuple(solver): + solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) + + with pytest.raises(RuntimeError): + solver.mkTuple([], [solver.mkBitVector("101", 2)]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.mkBitVectorSort(4)], + [solver.mkBitVector("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)]) + with pytest.raises(RuntimeError): + slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + + def test_mk_universe_set(solver): solver.mkUniverseSet(solver.getBooleanSort()) with pytest.raises(RuntimeError): diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index 5e86382ee..def539cf4 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -89,9 +89,8 @@ def test_is_reg_exp(solver): def test_is_rounding_mode(solver): - if solver.supportsFloatingPoint(): - assert solver.getRoundingModeSort().isRoundingMode() - Sort(solver).isRoundingMode() + assert solver.getRoundingModeSort().isRoundingMode() + Sort(solver).isRoundingMode() def test_is_bit_vector(solver): @@ -100,9 +99,8 @@ def test_is_bit_vector(solver): def test_is_floating_point(solver): - if solver.supportsFloatingPoint(): - assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() - Sort(solver).isFloatingPoint() + assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() + Sort(solver).isFloatingPoint() def test_is_datatype(solver): @@ -447,21 +445,19 @@ def test_get_bv_size(solver): def test_get_fp_exponent_size(solver): - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(RuntimeError): - setSort.getFPExponentSize() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPExponentSize() def test_get_fp_significand_size(solver): - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(RuntimeError): - setSort.getFPSignificandSize() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPSignificandSize() def test_get_datatype_paramsorts(solver): |