From: yoni206 Date: Mon, 3 May 2021 06:35:47 +0000 (-0700) Subject: Python API tests for terms -- Part 1 (#6468) X-Git-Tag: cvc5-1.0.0~1805 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0daac05ab78459a3f3d773daea41e5eee9aa78f2;p=cvc5.git Python API tests for terms -- Part 1 (#6468) This PR removes the old python api tests for terms from test/api/python/test_term.py and replaces it with a new test file test/python/unit/api/test_term.py. The new test file is obtained by translating test/unit/api/term_black.cpp. In this PR I only include the tests that pass without requiring any change to the python API. The next PR will add functions to the python API that are currently not supported, along with corresponding tests. Comment: This was originally done in #6460 on the wrong fork. Now it is re-opened, and addresses all comments given there. --- diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index 246755492..87ddbb5d6 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -40,5 +40,4 @@ endmacro() cvc5_add_python_api_test(pytest_datatype_api test_datatype_api.py) cvc5_add_python_api_test(pytest_grammar test_grammar.py) -cvc5_add_python_api_test(pytest_term test_term.py) cvc5_add_python_api_test(pytest_to_python_obj test_to_python_obj.py) diff --git a/test/api/python/test_term.py b/test/api/python/test_term.py deleted file mode 100644 index c0625095b..000000000 --- a/test/api/python/test_term.py +++ /dev/null @@ -1,127 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Makai Mann, Andres Noetzli -# -# 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. -# ############################################################################# -## - -import pytest - -import pycvc5 -from pycvc5 import kinds - - -def test_getitem(): - solver = pycvc5.Solver() - intsort = solver.getIntegerSort() - x = solver.mkConst(intsort, 'x') - y = solver.mkConst(intsort, 'y') - xpy = solver.mkTerm(kinds.Plus, x, y) - - assert xpy[0] == x - assert xpy[1] == y - - -def test_get_kind(): - solver = pycvc5.Solver() - intsort = solver.getIntegerSort() - x = solver.mkConst(intsort, 'x') - y = solver.mkConst(intsort, 'y') - xpy = solver.mkTerm(kinds.Plus, x, y) - assert xpy.getKind() == kinds.Plus - - funsort = solver.mkFunctionSort(intsort, intsort) - f = solver.mkConst(funsort, 'f') - assert f.getKind() == kinds.Constant - - fx = solver.mkTerm(kinds.ApplyUf, f, x) - assert fx.getKind() == kinds.ApplyUf - - # Sequence kinds do not exist internally, test that the API properly - # converts them back. - seqsort = solver.mkSequenceSort(intsort) - s = solver.mkConst(seqsort, 's') - ss = solver.mkTerm(kinds.SeqConcat, s, s) - assert ss.getKind() == kinds.SeqConcat - - -def test_eq(): - solver = pycvc5.Solver() - usort = solver.mkUninterpretedSort('u') - x = solver.mkConst(usort, 'x') - y = solver.mkConst(usort, 'y') - z = x - - assert x == x - assert x == z - assert not (x != x) - assert x != y - assert y != z - - -def test_get_sort(): - solver = pycvc5.Solver() - intsort = solver.getIntegerSort() - bvsort8 = solver.mkBitVectorSort(8) - - x = solver.mkConst(intsort, 'x') - y = solver.mkConst(intsort, 'y') - - a = solver.mkConst(bvsort8, 'a') - b = solver.mkConst(bvsort8, 'b') - - assert x.getSort() == intsort - assert solver.mkTerm(kinds.Plus, x, y).getSort() == intsort - - assert a.getSort() == bvsort8 - assert solver.mkTerm(kinds.BVConcat, a, b).getSort() == solver.mkBitVectorSort(16) - -def test_get_op(): - solver = pycvc5.Solver() - intsort = solver.getIntegerSort() - funsort = solver.mkFunctionSort(intsort, intsort) - - x = solver.mkConst(intsort, 'x') - f = solver.mkConst(funsort, 'f') - - fx = solver.mkTerm(kinds.ApplyUf, f, x) - - assert not x.hasOp() - - try: - op = x.getOp() - assert False - except: - assert True - - assert fx.hasOp() - assert fx.getOp().getKind() == kinds.ApplyUf - # equivalent check - assert fx.getOp() == solver.mkOp(kinds.ApplyUf) - - -def test_const_sequence_elements(): - solver = pycvc5.Solver() - realsort = solver.getRealSort() - seqsort = solver.mkSequenceSort(realsort) - s = solver.mkEmptySequence(seqsort) - - assert s.getKind() == kinds.ConstSequence - # empty sequence has zero elements - cs = s.getConstSequenceElements() - assert len(cs) == 0 - - # A seq.unit app is not a constant sequence (regardless of whether it is - # applied to a constant). - su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1)) - try: - su.getConstSequenceElements() - assert False - except: - assert True diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt index 92fcb2a48..b7de1cbb0 100644 --- a/test/python/CMakeLists.txt +++ b/test/python/CMakeLists.txt @@ -29,3 +29,4 @@ endmacro() # add specific test files cvc5_add_python_api_test(pytest_solver unit/api/test_solver.py) cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py) +cvc5_add_python_api_test(pytest_term unit/api/test_term.py) diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py new file mode 100644 index 000000000..ea4ec2427 --- /dev/null +++ b/test/python/unit/api/test_term.py @@ -0,0 +1,786 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Makai Mann, Andres Noetzli +# +# 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. +# ############################################################################# +## + + + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort, Term + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_eq(solver): + uSort = solver.mkUninterpretedSort("u") + x = solver.mkVar(uSort, "x") + y = solver.mkVar(uSort, "y") + z = Term(solver) + + assert x == x + assert not x != x + assert not x == y + assert x != y + assert not (x == z) + assert x != z + +def test_get_kind(solver): + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(uSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + n = Term(solver) + with pytest.raises(RuntimeError): + n.getKind() + x = solver.mkVar(uSort, "x") + x.getKind() + y = solver.mkVar(uSort, "y") + y.getKind() + + f = solver.mkVar(funSort1, "f") + f.getKind() + p = solver.mkVar(funSort2, "p") + p.getKind() + + zero = solver.mkInteger(0) + zero.getKind() + + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x.getKind() + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y.getKind() + sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum.getKind() + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.getKind() + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y.getKind() + + # Sequence kinds do not exist internally, test that the API properly + # converts them back. + seqSort = solver.mkSequenceSort(intSort) + s = solver.mkConst(seqSort, "s") + ss = solver.mkTerm(kinds.SeqConcat, s, s) + assert ss.getKind() == kinds.SeqConcat + +def test_get_sort(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + n = Term(solver) + with pytest.raises(RuntimeError): + n.getSort() + x = solver.mkVar(bvSort, "x") + x.getSort() + assert x.getSort() == bvSort + y = solver.mkVar(bvSort, "y") + y.getSort() + assert y.getSort() == bvSort + + f = solver.mkVar(funSort1, "f") + f.getSort() + assert f.getSort() == funSort1 + p = solver.mkVar(funSort2, "p") + p.getSort() + assert p.getSort() == funSort2 + + zero = solver.mkInteger(0) + zero.getSort() + assert zero.getSort() == intSort + + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x.getSort() + assert f_x.getSort() == intSort + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y.getSort() + assert f_y.getSort() == intSort + sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum.getSort() + assert sum.getSort() == intSort + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.getSort() + assert p_0.getSort() == boolSort + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y.getSort() + assert p_f_y.getSort() == boolSort + +def test_is_null(solver): + x = Term(solver) + assert x.isNull() + x = solver.mkVar(solver.mkBitVectorSort(4), "x") + assert not x.isNull() + +def test_not_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + with pytest.raises(RuntimeError): + Term(solver).notTerm() + b = solver.mkTrue() + b.notTerm() + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.notTerm() + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.notTerm() + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.notTerm() + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.notTerm() + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.notTerm() + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.notTerm() + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.notTerm() + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.notTerm() + +def test_and_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).andTerm(b) + with pytest.raises(RuntimeError): + b.andTerm(Term(solver)) + b.andTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.andTerm(b) + with pytest.raises(RuntimeError): + x.andTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.andTerm(b) + with pytest.raises(RuntimeError): + f.andTerm(x) + with pytest.raises(RuntimeError): + f.andTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.andTerm(b) + with pytest.raises(RuntimeError): + p.andTerm(x) + with pytest.raises(RuntimeError): + p.andTerm(f) + with pytest.raises(RuntimeError): + p.andTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.andTerm(b) + with pytest.raises(RuntimeError): + zero.andTerm(x) + with pytest.raises(RuntimeError): + zero.andTerm(f) + with pytest.raises(RuntimeError): + zero.andTerm(p) + with pytest.raises(RuntimeError): + zero.andTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.andTerm(b) + with pytest.raises(RuntimeError): + f_x.andTerm(x) + with pytest.raises(RuntimeError): + f_x.andTerm(f) + with pytest.raises(RuntimeError): + f_x.andTerm(p) + with pytest.raises(RuntimeError): + f_x.andTerm(zero) + with pytest.raises(RuntimeError): + f_x.andTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.andTerm(b) + with pytest.raises(RuntimeError): + sum.andTerm(x) + with pytest.raises(RuntimeError): + sum.andTerm(f) + with pytest.raises(RuntimeError): + sum.andTerm(p) + with pytest.raises(RuntimeError): + sum.andTerm(zero) + with pytest.raises(RuntimeError): + sum.andTerm(f_x) + with pytest.raises(RuntimeError): + sum.andTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.andTerm(b) + with pytest.raises(RuntimeError): + p_0.andTerm(x) + with pytest.raises(RuntimeError): + p_0.andTerm(f) + with pytest.raises(RuntimeError): + p_0.andTerm(p) + with pytest.raises(RuntimeError): + p_0.andTerm(zero) + with pytest.raises(RuntimeError): + p_0.andTerm(f_x) + with pytest.raises(RuntimeError): + p_0.andTerm(sum) + p_0.andTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.andTerm(b) + with pytest.raises(RuntimeError): + p_f_x.andTerm(x) + with pytest.raises(RuntimeError): + p_f_x.andTerm(f) + with pytest.raises(RuntimeError): + p_f_x.andTerm(p) + with pytest.raises(RuntimeError): + p_f_x.andTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.andTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.andTerm(sum) + p_f_x.andTerm(p_0) + p_f_x.andTerm(p_f_x) + +def test_or_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).orTerm(b) + with pytest.raises(RuntimeError): + b.orTerm(Term(solver)) + b.orTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.orTerm(b) + with pytest.raises(RuntimeError): + x.orTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.orTerm(b) + with pytest.raises(RuntimeError): + f.orTerm(x) + with pytest.raises(RuntimeError): + f.orTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.orTerm(b) + with pytest.raises(RuntimeError): + p.orTerm(x) + with pytest.raises(RuntimeError): + p.orTerm(f) + with pytest.raises(RuntimeError): + p.orTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.orTerm(b) + with pytest.raises(RuntimeError): + zero.orTerm(x) + with pytest.raises(RuntimeError): + zero.orTerm(f) + with pytest.raises(RuntimeError): + zero.orTerm(p) + with pytest.raises(RuntimeError): + zero.orTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.orTerm(b) + with pytest.raises(RuntimeError): + f_x.orTerm(x) + with pytest.raises(RuntimeError): + f_x.orTerm(f) + with pytest.raises(RuntimeError): + f_x.orTerm(p) + with pytest.raises(RuntimeError): + f_x.orTerm(zero) + with pytest.raises(RuntimeError): + f_x.orTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.orTerm(b) + with pytest.raises(RuntimeError): + sum.orTerm(x) + with pytest.raises(RuntimeError): + sum.orTerm(f) + with pytest.raises(RuntimeError): + sum.orTerm(p) + with pytest.raises(RuntimeError): + sum.orTerm(zero) + with pytest.raises(RuntimeError): + sum.orTerm(f_x) + with pytest.raises(RuntimeError): + sum.orTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.orTerm(b) + with pytest.raises(RuntimeError): + p_0.orTerm(x) + with pytest.raises(RuntimeError): + p_0.orTerm(f) + with pytest.raises(RuntimeError): + p_0.orTerm(p) + with pytest.raises(RuntimeError): + p_0.orTerm(zero) + with pytest.raises(RuntimeError): + p_0.orTerm(f_x) + with pytest.raises(RuntimeError): + p_0.orTerm(sum) + p_0.orTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.orTerm(b) + with pytest.raises(RuntimeError): + p_f_x.orTerm(x) + with pytest.raises(RuntimeError): + p_f_x.orTerm(f) + with pytest.raises(RuntimeError): + p_f_x.orTerm(p) + with pytest.raises(RuntimeError): + p_f_x.orTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.orTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.orTerm(sum) + p_f_x.orTerm(p_0) + p_f_x.orTerm(p_f_x) + +def test_xor_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).xorTerm(b) + with pytest.raises(RuntimeError): + b.xorTerm(Term(solver)) + b.xorTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.xorTerm(b) + with pytest.raises(RuntimeError): + x.xorTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.xorTerm(b) + with pytest.raises(RuntimeError): + f.xorTerm(x) + with pytest.raises(RuntimeError): + f.xorTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.xorTerm(b) + with pytest.raises(RuntimeError): + p.xorTerm(x) + with pytest.raises(RuntimeError): + p.xorTerm(f) + with pytest.raises(RuntimeError): + p.xorTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.xorTerm(b) + with pytest.raises(RuntimeError): + zero.xorTerm(x) + with pytest.raises(RuntimeError): + zero.xorTerm(f) + with pytest.raises(RuntimeError): + zero.xorTerm(p) + with pytest.raises(RuntimeError): + zero.xorTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.xorTerm(b) + with pytest.raises(RuntimeError): + f_x.xorTerm(x) + with pytest.raises(RuntimeError): + f_x.xorTerm(f) + with pytest.raises(RuntimeError): + f_x.xorTerm(p) + with pytest.raises(RuntimeError): + f_x.xorTerm(zero) + with pytest.raises(RuntimeError): + f_x.xorTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.xorTerm(b) + with pytest.raises(RuntimeError): + sum.xorTerm(x) + with pytest.raises(RuntimeError): + sum.xorTerm(f) + with pytest.raises(RuntimeError): + sum.xorTerm(p) + with pytest.raises(RuntimeError): + sum.xorTerm(zero) + with pytest.raises(RuntimeError): + sum.xorTerm(f_x) + with pytest.raises(RuntimeError): + sum.xorTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.xorTerm(b) + with pytest.raises(RuntimeError): + p_0.xorTerm(x) + with pytest.raises(RuntimeError): + p_0.xorTerm(f) + with pytest.raises(RuntimeError): + p_0.xorTerm(p) + with pytest.raises(RuntimeError): + p_0.xorTerm(zero) + with pytest.raises(RuntimeError): + p_0.xorTerm(f_x) + with pytest.raises(RuntimeError): + p_0.xorTerm(sum) + p_0.xorTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.xorTerm(b) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(x) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(f) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(p) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(sum) + p_f_x.xorTerm(p_0) + p_f_x.xorTerm(p_f_x) + +def test_eq_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).eqTerm(b) + with pytest.raises(RuntimeError): + b.eqTerm(Term(solver)) + b.eqTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.eqTerm(b) + x.eqTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.eqTerm(b) + with pytest.raises(RuntimeError): + f.eqTerm(x) + f.eqTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.eqTerm(b) + with pytest.raises(RuntimeError): + p.eqTerm(x) + with pytest.raises(RuntimeError): + p.eqTerm(f) + p.eqTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.eqTerm(b) + with pytest.raises(RuntimeError): + zero.eqTerm(x) + with pytest.raises(RuntimeError): + zero.eqTerm(f) + with pytest.raises(RuntimeError): + zero.eqTerm(p) + zero.eqTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.eqTerm(b) + with pytest.raises(RuntimeError): + f_x.eqTerm(x) + with pytest.raises(RuntimeError): + f_x.eqTerm(f) + with pytest.raises(RuntimeError): + f_x.eqTerm(p) + f_x.eqTerm(zero) + f_x.eqTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.eqTerm(b) + with pytest.raises(RuntimeError): + sum.eqTerm(x) + with pytest.raises(RuntimeError): + sum.eqTerm(f) + with pytest.raises(RuntimeError): + sum.eqTerm(p) + sum.eqTerm(zero) + sum.eqTerm(f_x) + sum.eqTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.eqTerm(b) + with pytest.raises(RuntimeError): + p_0.eqTerm(x) + with pytest.raises(RuntimeError): + p_0.eqTerm(f) + with pytest.raises(RuntimeError): + p_0.eqTerm(p) + with pytest.raises(RuntimeError): + p_0.eqTerm(zero) + with pytest.raises(RuntimeError): + p_0.eqTerm(f_x) + with pytest.raises(RuntimeError): + p_0.eqTerm(sum) + p_0.eqTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.eqTerm(b) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(x) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(f) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(p) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(sum) + p_f_x.eqTerm(p_0) + p_f_x.eqTerm(p_f_x) + +def test_imp_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).impTerm(b) + with pytest.raises(RuntimeError): + b.impTerm(Term(solver)) + b.impTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.impTerm(b) + with pytest.raises(RuntimeError): + x.impTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.impTerm(b) + with pytest.raises(RuntimeError): + f.impTerm(x) + with pytest.raises(RuntimeError): + f.impTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.impTerm(b) + with pytest.raises(RuntimeError): + p.impTerm(x) + with pytest.raises(RuntimeError): + p.impTerm(f) + with pytest.raises(RuntimeError): + p.impTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.impTerm(b) + with pytest.raises(RuntimeError): + zero.impTerm(x) + with pytest.raises(RuntimeError): + zero.impTerm(f) + with pytest.raises(RuntimeError): + zero.impTerm(p) + with pytest.raises(RuntimeError): + zero.impTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.impTerm(b) + with pytest.raises(RuntimeError): + f_x.impTerm(x) + with pytest.raises(RuntimeError): + f_x.impTerm(f) + with pytest.raises(RuntimeError): + f_x.impTerm(p) + with pytest.raises(RuntimeError): + f_x.impTerm(zero) + with pytest.raises(RuntimeError): + f_x.impTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.impTerm(b) + with pytest.raises(RuntimeError): + sum.impTerm(x) + with pytest.raises(RuntimeError): + sum.impTerm(f) + with pytest.raises(RuntimeError): + sum.impTerm(p) + with pytest.raises(RuntimeError): + sum.impTerm(zero) + with pytest.raises(RuntimeError): + sum.impTerm(f_x) + with pytest.raises(RuntimeError): + sum.impTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.impTerm(b) + with pytest.raises(RuntimeError): + p_0.impTerm(x) + with pytest.raises(RuntimeError): + p_0.impTerm(f) + with pytest.raises(RuntimeError): + p_0.impTerm(p) + with pytest.raises(RuntimeError): + p_0.impTerm(zero) + with pytest.raises(RuntimeError): + p_0.impTerm(f_x) + with pytest.raises(RuntimeError): + p_0.impTerm(sum) + p_0.impTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.impTerm(b) + with pytest.raises(RuntimeError): + p_f_x.impTerm(x) + with pytest.raises(RuntimeError): + p_f_x.impTerm(f) + with pytest.raises(RuntimeError): + p_f_x.impTerm(p) + with pytest.raises(RuntimeError): + p_f_x.impTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.impTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.impTerm(sum) + p_f_x.impTerm(p_0) + p_f_x.impTerm(p_f_x) + +def test_ite_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).iteTerm(b, b) + with pytest.raises(RuntimeError): + b.iteTerm(Term(solver), b) + with pytest.raises(RuntimeError): + b.iteTerm(b, Term(solver)) + b.iteTerm(b, b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + b.iteTerm(x, x) + b.iteTerm(b, b) + with pytest.raises(RuntimeError): + b.iteTerm(x, b) + with pytest.raises(RuntimeError): + x.iteTerm(x, x) + with pytest.raises(RuntimeError): + x.iteTerm(x, b) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.iteTerm(b, b) + with pytest.raises(RuntimeError): + x.iteTerm(b, x) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.iteTerm(b, b) + with pytest.raises(RuntimeError): + p.iteTerm(x, b) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.iteTerm(x, x) + with pytest.raises(RuntimeError): + zero.iteTerm(x, b) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.iteTerm(b, b) + with pytest.raises(RuntimeError): + f_x.iteTerm(b, x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.iteTerm(x, x) + with pytest.raises(RuntimeError): + sum.iteTerm(b, x) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.iteTerm(b, b) + p_0.iteTerm(x, x) + with pytest.raises(RuntimeError): + p_0.iteTerm(x, b) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.iteTerm(b, b) + p_f_x.iteTerm(x, x) + with pytest.raises(RuntimeError): + p_f_x.iteTerm(x, b) + +def test_term_assignment(solver): + t1 = solver.mkInteger(1) + t2 = t1 + t2 = solver.mkInteger(2) + assert t1 == solver.mkInteger(1) + +def test_const_array(solver): + intsort = solver.getIntegerSort() + arrsort = solver.mkArraySort(intsort, intsort) + a = solver.mkConst(arrsort, "a") + one = solver.mkInteger(1) + constarr = solver.mkConstArray(arrsort, one) + + assert constarr.getKind() == kinds.ConstArray + assert constarr.getConstArrayBase() == one + with pytest.raises(RuntimeError): + a.getConstArrayBase() + + arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) + zero_array = solver.mkConstArray(arrsort, solver.mkReal(0)) + stores = solver.mkTerm( + kinds.Store, zero_array, solver.mkReal(1), solver.mkReal(2)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5)) + +def test_const_sequence_elements(solver): + realsort = solver.getRealSort() + seqsort = solver.mkSequenceSort(realsort) + s = solver.mkEmptySequence(seqsort) + + assert s.getKind() == kinds.ConstSequence + # empty sequence has zero elements + cs = s.getConstSequenceElements() + assert len(cs) == 0 + + # A seq.unit app is not a constant sequence (regardless of whether it is + # applied to a constant). + su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1)) + with pytest.raises(RuntimeError): + su.getConstSequenceElements() + +def test_term_scoped_to_string(solver): + intsort = solver.getIntegerSort() + x = solver.mkConst(intsort, "x") + assert str(x) == "x" + solver2 = pycvc5.Solver() + assert str(x) == "x"