From: makaimann Date: Tue, 3 Nov 2020 00:17:21 +0000 (-0800) Subject: Run python tests during make check (#5226) X-Git-Tag: cvc5-1.0.0~2638 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=116114d9277f7b706e30f4c7af3a531e3f75fe86;p=cvc5.git Run python tests during make check (#5226) If building with python bindings, check the pytest is installed, and adds a command to run pytest after the existing make check tests. If built without python bindings, it just uses a null command. Note: the current semantics are such that the pytest tests will not run if the ctest run fails (unless you pass the correct flag to make to continue --ignore-errors I believe). I can look into changing this semantics if that would be preferred. --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b8fefd401..04b36130e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -188,12 +188,6 @@ jobs: export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc4" -type d))" python3 -c "import pycvc4" - - name: Run Pytest - if: matrix.python-bindings - run: | - export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc4" -type d))" - python3 -m pytest ./test/unit/api/python - # Examples are built for non-symfpu builds - name: Check Examples if: matrix.check-examples && runner.os == 'Linux' diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 34a18d9b2..59df71010 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -67,3 +67,9 @@ if (USE_EDITLINE) ) endif() endif() + + +# add Python bindings tests if building with Python bindings +if (BUILD_BINDINGS_PYTHON) + add_subdirectory(python) +endif() diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt new file mode 100644 index 000000000..300038ada --- /dev/null +++ b/test/api/python/CMakeLists.txt @@ -0,0 +1,43 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## +#-----------------------------------------------------------------------------# +# Add Python bindings API tests + +# Check if the pytest Python module is installed. +execute_process( + COMMAND + ${PYTHON_EXECUTABLE} -c "import pytest" + RESULT_VARIABLE + RET_PYTEST + ERROR_QUIET +) + +if(RET_PYTEST) + message(FATAL_ERROR + "Could not find Python module pytest. Install via `pip install pytest'.") +endif() + +macro(cvc4_add_python_api_test name filename) + + # we create test target 'api//myapitest' + # and run it with 'ctest -R "api//myapitest"'. + add_test (NAME api/api/python/${name} + COMMAND ${PYTHON_EXECUTABLE} -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename} + # directory for importing the python bindings + WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) + +endmacro() + +cvc4_add_python_api_test(pytest_datatype_api test_datatype_api.py) +cvc4_add_python_api_test(pytest_grammar test_grammar.py) +cvc4_add_python_api_test(pytest_sort test_sort.py) +cvc4_add_python_api_test(pytest_term test_term.py) +cvc4_add_python_api_test(pytest_to_python_obj test_to_python_obj.py) diff --git a/test/api/python/test_datatype_api.py b/test/api/python/test_datatype_api.py new file mode 100644 index 000000000..c692416c6 --- /dev/null +++ b/test/api/python/test_datatype_api.py @@ -0,0 +1,181 @@ +##################### +## test_datatype_api.py +## Top contributors (to current version): +## Andres Noetzli, Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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 pycvc4 +from pycvc4 import kinds + + +def test_datatype_simply_rec(): + solver = pycvc4.Solver() + + # Create mutual datatypes corresponding to this definition block: + # + # DATATYPE + # wlist = leaf(data: list), + # list = cons(car: wlist, cdr: list) | nil, + # ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) + # END; + + # Make unresolved types as placeholders + unres_wlist = solver.mkUninterpretedSort('wlist') + unres_list = solver.mkUninterpretedSort('list') + unres_ns = solver.mkUninterpretedSort('ns') + unres_types = set([unres_wlist, unres_list, unres_ns]) + + wlist = solver.mkDatatypeDecl('wlist') + leaf = solver.mkDatatypeConstructorDecl('leaf') + leaf.addSelector('data', unres_list) + wlist.addConstructor(leaf) + + dlist = solver.mkDatatypeDecl('list') + cons = solver.mkDatatypeConstructorDecl('cons') + cons.addSelector('car', unres_wlist) + cons.addSelector('cdr', unres_list) + dlist.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dlist.addConstructor(nil) + + ns = solver.mkDatatypeDecl('ns') + elem = solver.mkDatatypeConstructorDecl('elem') + elem.addSelector('ndata', solver.mkSetSort(unres_wlist)) + ns.addConstructor(elem) + elem_array = solver.mkDatatypeConstructorDecl('elemArray') + elem_array.addSelector('ndata', solver.mkArraySort(unres_list, unres_list)) + ns.addConstructor(elem_array) + + # this is well-founded and has no nested recursion + dtdecls = [wlist, dlist, ns] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 3 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[2].getDatatype().isWellFounded() + assert not dtsorts[0].getDatatype().hasNestedRecursion() + assert not dtsorts[1].getDatatype().hasNestedRecursion() + assert not dtsorts[2].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # ns2 = elem2(ndata: array(int,ns2)) | nil2 + # END; + unres_ns2 = solver.mkUninterpretedSort('ns2') + unres_types = set([unres_ns2]) + + ns2 = solver.mkDatatypeDecl('ns2') + elem2 = solver.mkDatatypeConstructorDecl('elem2') + elem2.addSelector('ndata', + solver.mkArraySort(solver.getIntegerSort(), unres_ns2)) + ns2.addConstructor(elem2) + nil2 = solver.mkDatatypeConstructorDecl('nil2') + ns2.addConstructor(nil2) + + # this is not well-founded due to non-simple recursion + dtdecls = [ns2] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray() + elem_sort = dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() + assert elem_sort == dtsorts[0] + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list3 = cons3(car: ns3, cdr: list3) | nil3, + # ns3 = elem3(ndata: set(list3)) + # END + unres_ns3 = solver.mkUninterpretedSort('ns3') + unres_list3 = solver.mkUninterpretedSort('list3') + unres_types = set([unres_ns3, unres_list3]) + + list3 = solver.mkDatatypeDecl('list3') + cons3 = solver.mkDatatypeConstructorDecl('cons3') + cons3.addSelector('car', unres_ns3) + cons3.addSelector('cdr', unres_list3) + list3.addConstructor(cons3) + nil3 = solver.mkDatatypeConstructorDecl('nil3') + list3.addConstructor(nil3) + + ns3 = solver.mkDatatypeDecl('ns3') + elem3 = solver.mkDatatypeConstructorDecl('elem3') + elem3.addSelector('ndata', solver.mkSetSort(unres_list3)) + ns3.addConstructor(elem3) + + # both are well-founded and have nested recursion + dtdecls = [list3, ns3] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 2 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + assert dtsorts[1].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list4 = cons(car: set(ns4), cdr: list4) | nil, + # ns4 = elem(ndata: list4) + # END + unres_ns4 = solver.mkUninterpretedSort('ns4') + unres_list4 = solver.mkUninterpretedSort('list4') + unres_types = set([unres_ns4, unres_list4]) + + list4 = solver.mkDatatypeDecl('list4') + cons4 = solver.mkDatatypeConstructorDecl('cons4') + cons4.addSelector('car', solver.mkSetSort(unres_ns4)) + cons4.addSelector('cdr', unres_list4) + list4.addConstructor(cons4) + nil4 = solver.mkDatatypeConstructorDecl('nil4') + list4.addConstructor(nil4) + + ns4 = solver.mkDatatypeDecl('ns4') + elem4 = solver.mkDatatypeConstructorDecl('elem3') + elem4.addSelector('ndata', unres_list4) + ns4.addConstructor(elem4) + + # both are well-founded and have nested recursion + dtdecls = [list4, ns4] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 2 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + assert dtsorts[1].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil + # END + unres_list5 = solver.mkSortConstructorSort('list5', 1) + unres_types = set([unres_list5]) + + x = solver.mkParamSort('X') + v = [x] + list5 = solver.mkDatatypeDecl('list5', v) + + args = [x] + ur_list_x = unres_list5.instantiate(args) + args = [ur_list_x] + ur_list_list_x = unres_list5.instantiate(args) + + cons5 = solver.mkDatatypeConstructorDecl('cons5') + cons5.addSelector('car', x) + cons5.addSelector('cdr', ur_list_list_x) + list5.addConstructor(cons5) + nil5 = solver.mkDatatypeConstructorDecl('nil5') + list5.addConstructor(nil5) + + # well-founded and has nested recursion + dtdecls = [list5] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py new file mode 100644 index 000000000..5a0d5101f --- /dev/null +++ b/test/api/python/test_grammar.py @@ -0,0 +1,128 @@ +##################### +## test_grammar.py +## Top contributors (to current version): +## Yoni Zohar, Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## +## Translated from test/unit/api/grammar_black.h +## + +import pytest + +import pycvc4 +from pycvc4 import kinds + +def test_add_rule(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + nullTerm = pycvc4.Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + # expecting no error + g = solver.mkSygusGrammar([], [start]) + + g.addRule(start, solver.mkBoolean(False)) + + # expecting errors + with pytest.raises(Exception): + g.addRule(nullTerm, solver.mkBoolean(false)) + with pytest.raises(Exception): + g.addRule(start, nullTerm) + with pytest.raises(Exception): + g.addRule(nts, solver.mkBoolean(false)) + with pytest.raises(Exception): + g.addRule(start, solver.mkInteger(0)) + + # expecting no errors + solver.synthFun("f", {}, boolean, g) + + # expecting an error + with pytest.raises(Exception): + g.addRule(start, solver.mkBoolean(false)) + +def test_add_rules(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + nullTerm = pycvc4.Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar([], [start]) + + g.addRules(start, {solver.mkBoolean(False)}) + + #Expecting errors + with pytest.raises(Exception): + g.addRules(nullTerm, solver.mkBoolean(False)) + with pytest.raises(Exception): + g.addRules(start, {nullTerm}) + with pytest.raises(Exception): + g.addRules(nts, {solver.mkBoolean(False)}) + with pytest.raises(Exception): + g.addRules(start, {solver.mkInteger(0)}) + #Expecting no errors + solver.synthFun("f", {}, boolean, g) + + #Expecting an error + with pytest.raises(Exception): + g.addRules(start, solver.mkBoolean(False)) + +def testAddAnyConstant(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + + nullTerm = pycvc4.Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar({}, {start}) + + g.addAnyConstant(start) + g.addAnyConstant(start) + + with pytest.raises(Exception): + g.addAnyConstant(nullTerm) + with pytest.raises(Exception): + g.addAnyConstant(nts) + + solver.synthFun("f", {}, boolean, g) + + with pytest.raises(Exception): + g.addAnyConstant(start) + + +def testAddAnyVariable(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + + nullTerm = pycvc4.Term(solver) + x = solver.mkVar(boolean) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g1 = solver.mkSygusGrammar({x}, {start}) + g2 = solver.mkSygusGrammar({}, {start}) + + g1.addAnyVariable(start) + g1.addAnyVariable(start) + g2.addAnyVariable(start) + + with pytest.raises(Exception): + g1.addAnyVariable(nullTerm) + with pytest.raises(Exception): + g1.addAnyVariable(nts) + + solver.synthFun("f", {}, boolean, g1) + + with pytest.raises(Exception): + g1.addAnyVariable(start) + diff --git a/test/api/python/test_sort.py b/test/api/python/test_sort.py new file mode 100644 index 000000000..cff92ca8d --- /dev/null +++ b/test/api/python/test_sort.py @@ -0,0 +1,355 @@ +##################### +## test_sort.py +## Top contributors (to current version): +## Makai Mann, Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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 pycvc4 +from pycvc4 import kinds + + +def testGetDatatype(): + solver = pycvc4.Solver() + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + + # expecting no Error + dtypeSort.getDatatype() + + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(Exception): + # expect an exception + bvSort.getDatatype() + + +def testDatatypeSorts(): + solver = pycvc4.Solver() + intSort = solver.getIntegerSort() + # create datatype sort to test + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", intSort) + cons.addSelectorSelf("tail") + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + dt = dtypeSort.getDatatype() + assert not dtypeSort.isConstructor() + + with pytest.raises(Exception): + dtypeSort.getConstructorCodomainSort() + + with pytest.raises(Exception): + dtypeSort.getConstructorDomainSorts() + + with pytest.raises(Exception): + dtypeSort.getConstructorArity() + + # get constructor + dcons = dt[0] + consTerm = dcons.getConstructorTerm() + consSort = consTerm.getSort() + assert consSort.isConstructor() + assert not consSort.isTester() + assert not consSort.isSelector() + assert consSort.getConstructorArity() == 2 + consDomSorts = consSort.getConstructorDomainSorts() + assert consDomSorts[0] == intSort + assert consDomSorts[1] == dtypeSort + assert consSort.getConstructorCodomainSort() == dtypeSort + + # get tester + isConsTerm = dcons.getTesterTerm() + assert isConsTerm.getSort().isTester() + + # get selector + dselTail = dcons[1] + tailTerm = dselTail.getSelectorTerm() + assert tailTerm.getSort().isSelector() + + +def testInstantiate(): + solver = pycvc4.Solver() + # instantiate parametric datatype, check should not fail + sort = solver.mkParamSort("T") + paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) + paramCons = solver.mkDatatypeConstructorDecl("cons") + paramNil = solver.mkDatatypeConstructorDecl("nil") + paramCons.addSelector("head", sort) + paramDtypeSpec.addConstructor(paramCons) + paramDtypeSpec.addConstructor(paramNil) + paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) + paramDtypeSort.instantiate([solver.getIntegerSort()]) + + # instantiate non-parametric datatype sort, check should fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + + with pytest.raises(Exception): + dtypeSort.instantiate([solver.getIntegerSort()]) + + +def testGetFunctionArity(): + solver = pycvc4.Solver() + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionArity() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getFunctionArity() + + +def testGetFunctionDomainSorts(): + solver = pycvc4.Solver() + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionDomainSorts() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getFunctionDomainSorts() + + +def testGetFunctionCodomainSort(): + solver = pycvc4.Solver() + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionCodomainSort() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getFunctionCodomainSort() + +def testGetArrayIndexSort(): + solver = pycvc4.Solver() + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayIndexSort() + + with pytest.raises(Exception): + indexSort.getArrayIndexSort() + +def testGetArrayElementSort(): + solver = pycvc4.Solver() + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayElementSort() + + with pytest.raises(Exception): + indexSort.getArrayElementSort() + +def testGetSetElementSort(): + solver = pycvc4.Solver() + setSort = solver.mkSetSort(solver.getIntegerSort()) + setSort.getSetElementSort() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getSetElementSort() + +def testGetSequenceElementSort(): + solver = pycvc4.Solver() + seqSort = solver.mkSequenceSort(solver.getIntegerSort()) + seqSort.getSequenceElementSort() + bvSort = solver.mkBitVectorSort(32) + assert not bvSort.isSequence() + + with pytest.raises(Exception): + bvSort.getSetElementSort() + +def testGetUninterpretedSortName(): + solver = pycvc4.Solver() + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortName() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getUninterpretedSortName() + +def testIsUninterpretedSortParameterized(): + solver = pycvc4.Solver() + uSort = solver.mkUninterpretedSort("u") + uSort.isUninterpretedSortParameterized() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.isUninterpretedSortParameterized() + +def testGetUninterpretedSortParamSorts(): + solver = pycvc4.Solver() + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortParamSorts() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getUninterpretedSortParamSorts() + +def testGetUninterpretedSortConstructorName(): + solver = pycvc4.Solver() + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorName() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getSortConstructorName() + +def testGetUninterpretedSortConstructorArity(): + solver = pycvc4.Solver() + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorArity() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getSortConstructorArity() + +def testGetBVSize(): + solver = pycvc4.Solver() + bvSort = solver.mkBitVectorSort(32) + bvSort.getBVSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getBVSize() + +def testGetFPExponentSize(): + solver = pycvc4.Solver() + + if solver.supportsFloatingPoint(): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getFPExponentSize() + else: + with pytest.raises(Exception): + solver.mkFloatingPointSort(4, 8) + +def testGetFPSignificandSize(): + solver = pycvc4.Solver() + + if solver.supportsFloatingPoint(): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getFPSignificandSize() + else: + with pytest.raises(Exception): + solver.mkFloatingPointSort(4, 8) + +def testGetDatatypeParamSorts(): + solver = pycvc4.Solver() + # create parametric datatype, check should not fail + sort = solver.mkParamSort("T") + paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) + paramCons = solver.mkDatatypeConstructorDecl("cons") + paramNil = solver.mkDatatypeConstructorDecl("nil") + paramCons.addSelector("head", sort) + paramDtypeSpec.addConstructor(paramCons) + paramDtypeSpec.addConstructor(paramNil) + paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) + paramDtypeSort.getDatatypeParamSorts() + # create non-parametric datatype sort, check should fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + + with pytest.raises(Exception): + dtypeSort.getDatatypeParamSorts() + + +def testGetDatatypeArity(): + solver = pycvc4.Solver() + # create datatype sort, check should not fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + dtypeSort.getDatatypeArity() + # create bv sort, check should fail + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getDatatypeArity() + +def testGetTupleLength(): + solver = pycvc4.Solver() + tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()]) + tupleSort.getTupleLength() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getTupleLength() + +def testGetTupleSorts(): + solver = pycvc4.Solver() + tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()]) + tupleSort.getTupleSorts() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getTupleSorts() + +def testSortCompare(): + solver = pycvc4.Solver() + boolSort = solver.getBooleanSort() + intSort = solver.getIntegerSort() + bvSort = solver.mkBitVectorSort(32) + bvSort2 = solver.mkBitVectorSort(32) + assert bvSort >= bvSort2 + assert bvSort <= bvSort2 + assert (intSort > boolSort) != (intSort < boolSort) + assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort) + +def testSortSubtyping(): + solver = pycvc4.Solver() + intSort = solver.getIntegerSort() + realSort = solver.getRealSort() + assert intSort.isSubsortOf(realSort) + assert not realSort.isSubsortOf(intSort) + assert intSort.isComparableTo(realSort) + assert realSort.isComparableTo(intSort) + + arraySortII = solver.mkArraySort(intSort, intSort) + arraySortIR = solver.mkArraySort(intSort, realSort) + assert not arraySortII.isComparableTo(intSort) + # we do not support subtyping for arrays + assert not arraySortII.isComparableTo(arraySortIR) + + setSortI = solver.mkSetSort(intSort) + setSortR = solver.mkSetSort(realSort) + # we don't support subtyping for sets + assert not setSortI.isComparableTo(setSortR) + assert not setSortI.isSubsortOf(setSortR) + assert not setSortR.isComparableTo(setSortI) + assert not setSortR.isSubsortOf(setSortI) + diff --git a/test/api/python/test_term.py b/test/api/python/test_term.py new file mode 100644 index 000000000..a0c1b4681 --- /dev/null +++ b/test/api/python/test_term.py @@ -0,0 +1,124 @@ +##################### +## test_term.py +## Top contributors (to current version): +## Makai Mann, Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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 pycvc4 +from pycvc4 import kinds + + +def test_getitem(): + solver = pycvc4.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 = pycvc4.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 = pycvc4.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 = pycvc4.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 = pycvc4.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 = pycvc4.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/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py new file mode 100644 index 000000000..eb15e7469 --- /dev/null +++ b/test/api/python/test_to_python_obj.py @@ -0,0 +1,71 @@ +from fractions import Fraction +import pytest + +import pycvc4 +from pycvc4 import kinds + + +def testGetBool(): + solver = pycvc4.Solver() + t = solver.mkTrue() + f = solver.mkFalse() + assert t.toPythonObj() == True + assert f.toPythonObj() == False + + +def testGetInt(): + solver = pycvc4.Solver() + two = solver.mkInteger(2) + assert two.toPythonObj() == 2 + + +def testGetReal(): + solver = pycvc4.Solver() + half = solver.mkReal("1/2") + assert half.toPythonObj() == Fraction(1, 2) + + neg34 = solver.mkReal("-3/4") + assert neg34.toPythonObj() == Fraction(-3, 4) + + neg1 = solver.mkInteger("-1") + assert neg1.toPythonObj() == -1 + + +def testGetBV(): + solver = pycvc4.Solver() + three = solver.mkBitVector(8, 3) + assert three.toPythonObj() == 3 + + +def testGetArray(): + solver = pycvc4.Solver() + arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) + zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) + stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) + + array_dict = stores.toPythonObj() + + assert array_dict[1] == 2 + assert array_dict[2] == 3 + assert array_dict[4] == 5 + # an index that wasn't stored at should give zero + assert array_dict[8] == 0 + + +def testGetSymbol(): + solver = pycvc4.Solver() + solver.mkConst(solver.getBooleanSort(), "x") + + +def testGetString(): + solver = pycvc4.Solver() + + s1 = '"test\n"😃\\u{a}' + t1 = solver.mkString(s1) + assert s1 == t1.toPythonObj() + + s2 = '❤️CVC4❤️' + t2 = solver.mkString(s2) + assert s2 == t2.toPythonObj() diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 61dc6e15f..1412c7f66 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -18,3 +18,4 @@ cvc4_add_unit_test_black(solver_black api) cvc4_add_unit_test_black(sort_black api) cvc4_add_unit_test_black(term_black api) cvc4_add_unit_test_black(grammar_black api) + diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py deleted file mode 100644 index c692416c6..000000000 --- a/test/unit/api/python/test_datatype_api.py +++ /dev/null @@ -1,181 +0,0 @@ -##################### -## test_datatype_api.py -## Top contributors (to current version): -## Andres Noetzli, Makai Mann -## This file is part of the CVC4 project. -## Copyright (c) 2009-2020 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 pycvc4 -from pycvc4 import kinds - - -def test_datatype_simply_rec(): - solver = pycvc4.Solver() - - # Create mutual datatypes corresponding to this definition block: - # - # DATATYPE - # wlist = leaf(data: list), - # list = cons(car: wlist, cdr: list) | nil, - # ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) - # END; - - # Make unresolved types as placeholders - unres_wlist = solver.mkUninterpretedSort('wlist') - unres_list = solver.mkUninterpretedSort('list') - unres_ns = solver.mkUninterpretedSort('ns') - unres_types = set([unres_wlist, unres_list, unres_ns]) - - wlist = solver.mkDatatypeDecl('wlist') - leaf = solver.mkDatatypeConstructorDecl('leaf') - leaf.addSelector('data', unres_list) - wlist.addConstructor(leaf) - - dlist = solver.mkDatatypeDecl('list') - cons = solver.mkDatatypeConstructorDecl('cons') - cons.addSelector('car', unres_wlist) - cons.addSelector('cdr', unres_list) - dlist.addConstructor(cons) - nil = solver.mkDatatypeConstructorDecl("nil") - dlist.addConstructor(nil) - - ns = solver.mkDatatypeDecl('ns') - elem = solver.mkDatatypeConstructorDecl('elem') - elem.addSelector('ndata', solver.mkSetSort(unres_wlist)) - ns.addConstructor(elem) - elem_array = solver.mkDatatypeConstructorDecl('elemArray') - elem_array.addSelector('ndata', solver.mkArraySort(unres_list, unres_list)) - ns.addConstructor(elem_array) - - # this is well-founded and has no nested recursion - dtdecls = [wlist, dlist, ns] - dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) - assert len(dtsorts) == 3 - assert dtsorts[0].getDatatype().isWellFounded() - assert dtsorts[1].getDatatype().isWellFounded() - assert dtsorts[2].getDatatype().isWellFounded() - assert not dtsorts[0].getDatatype().hasNestedRecursion() - assert not dtsorts[1].getDatatype().hasNestedRecursion() - assert not dtsorts[2].getDatatype().hasNestedRecursion() - - # Create mutual datatypes corresponding to this definition block: - # DATATYPE - # ns2 = elem2(ndata: array(int,ns2)) | nil2 - # END; - unres_ns2 = solver.mkUninterpretedSort('ns2') - unres_types = set([unres_ns2]) - - ns2 = solver.mkDatatypeDecl('ns2') - elem2 = solver.mkDatatypeConstructorDecl('elem2') - elem2.addSelector('ndata', - solver.mkArraySort(solver.getIntegerSort(), unres_ns2)) - ns2.addConstructor(elem2) - nil2 = solver.mkDatatypeConstructorDecl('nil2') - ns2.addConstructor(nil2) - - # this is not well-founded due to non-simple recursion - dtdecls = [ns2] - dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) - assert len(dtsorts) == 1 - assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray() - elem_sort = dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() - assert elem_sort == dtsorts[0] - assert dtsorts[0].getDatatype().isWellFounded() - assert dtsorts[0].getDatatype().hasNestedRecursion() - - # Create mutual datatypes corresponding to this definition block: - # DATATYPE - # list3 = cons3(car: ns3, cdr: list3) | nil3, - # ns3 = elem3(ndata: set(list3)) - # END - unres_ns3 = solver.mkUninterpretedSort('ns3') - unres_list3 = solver.mkUninterpretedSort('list3') - unres_types = set([unres_ns3, unres_list3]) - - list3 = solver.mkDatatypeDecl('list3') - cons3 = solver.mkDatatypeConstructorDecl('cons3') - cons3.addSelector('car', unres_ns3) - cons3.addSelector('cdr', unres_list3) - list3.addConstructor(cons3) - nil3 = solver.mkDatatypeConstructorDecl('nil3') - list3.addConstructor(nil3) - - ns3 = solver.mkDatatypeDecl('ns3') - elem3 = solver.mkDatatypeConstructorDecl('elem3') - elem3.addSelector('ndata', solver.mkSetSort(unres_list3)) - ns3.addConstructor(elem3) - - # both are well-founded and have nested recursion - dtdecls = [list3, ns3] - dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) - assert len(dtsorts) == 2 - assert dtsorts[0].getDatatype().isWellFounded() - assert dtsorts[1].getDatatype().isWellFounded() - assert dtsorts[0].getDatatype().hasNestedRecursion() - assert dtsorts[1].getDatatype().hasNestedRecursion() - - # Create mutual datatypes corresponding to this definition block: - # DATATYPE - # list4 = cons(car: set(ns4), cdr: list4) | nil, - # ns4 = elem(ndata: list4) - # END - unres_ns4 = solver.mkUninterpretedSort('ns4') - unres_list4 = solver.mkUninterpretedSort('list4') - unres_types = set([unres_ns4, unres_list4]) - - list4 = solver.mkDatatypeDecl('list4') - cons4 = solver.mkDatatypeConstructorDecl('cons4') - cons4.addSelector('car', solver.mkSetSort(unres_ns4)) - cons4.addSelector('cdr', unres_list4) - list4.addConstructor(cons4) - nil4 = solver.mkDatatypeConstructorDecl('nil4') - list4.addConstructor(nil4) - - ns4 = solver.mkDatatypeDecl('ns4') - elem4 = solver.mkDatatypeConstructorDecl('elem3') - elem4.addSelector('ndata', unres_list4) - ns4.addConstructor(elem4) - - # both are well-founded and have nested recursion - dtdecls = [list4, ns4] - dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) - assert len(dtsorts) == 2 - assert dtsorts[0].getDatatype().isWellFounded() - assert dtsorts[1].getDatatype().isWellFounded() - assert dtsorts[0].getDatatype().hasNestedRecursion() - assert dtsorts[1].getDatatype().hasNestedRecursion() - - # Create mutual datatypes corresponding to this definition block: - # DATATYPE - # list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil - # END - unres_list5 = solver.mkSortConstructorSort('list5', 1) - unres_types = set([unres_list5]) - - x = solver.mkParamSort('X') - v = [x] - list5 = solver.mkDatatypeDecl('list5', v) - - args = [x] - ur_list_x = unres_list5.instantiate(args) - args = [ur_list_x] - ur_list_list_x = unres_list5.instantiate(args) - - cons5 = solver.mkDatatypeConstructorDecl('cons5') - cons5.addSelector('car', x) - cons5.addSelector('cdr', ur_list_list_x) - list5.addConstructor(cons5) - nil5 = solver.mkDatatypeConstructorDecl('nil5') - list5.addConstructor(nil5) - - # well-founded and has nested recursion - dtdecls = [list5] - dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) - assert len(dtsorts) == 1 - assert dtsorts[0].getDatatype().isWellFounded() - assert dtsorts[0].getDatatype().hasNestedRecursion() diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py deleted file mode 100644 index 5a0d5101f..000000000 --- a/test/unit/api/python/test_grammar.py +++ /dev/null @@ -1,128 +0,0 @@ -##################### -## test_grammar.py -## Top contributors (to current version): -## Yoni Zohar, Makai Mann -## This file is part of the CVC4 project. -## Copyright (c) 2009-2020 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. -## -## Translated from test/unit/api/grammar_black.h -## - -import pytest - -import pycvc4 -from pycvc4 import kinds - -def test_add_rule(): - solver = pycvc4.Solver() - boolean = solver.getBooleanSort() - integer = solver.getIntegerSort() - - nullTerm = pycvc4.Term(solver) - start = solver.mkVar(boolean) - nts = solver.mkVar(boolean) - - # expecting no error - g = solver.mkSygusGrammar([], [start]) - - g.addRule(start, solver.mkBoolean(False)) - - # expecting errors - with pytest.raises(Exception): - g.addRule(nullTerm, solver.mkBoolean(false)) - with pytest.raises(Exception): - g.addRule(start, nullTerm) - with pytest.raises(Exception): - g.addRule(nts, solver.mkBoolean(false)) - with pytest.raises(Exception): - g.addRule(start, solver.mkInteger(0)) - - # expecting no errors - solver.synthFun("f", {}, boolean, g) - - # expecting an error - with pytest.raises(Exception): - g.addRule(start, solver.mkBoolean(false)) - -def test_add_rules(): - solver = pycvc4.Solver() - boolean = solver.getBooleanSort() - integer = solver.getIntegerSort() - - nullTerm = pycvc4.Term(solver) - start = solver.mkVar(boolean) - nts = solver.mkVar(boolean) - - g = solver.mkSygusGrammar([], [start]) - - g.addRules(start, {solver.mkBoolean(False)}) - - #Expecting errors - with pytest.raises(Exception): - g.addRules(nullTerm, solver.mkBoolean(False)) - with pytest.raises(Exception): - g.addRules(start, {nullTerm}) - with pytest.raises(Exception): - g.addRules(nts, {solver.mkBoolean(False)}) - with pytest.raises(Exception): - g.addRules(start, {solver.mkInteger(0)}) - #Expecting no errors - solver.synthFun("f", {}, boolean, g) - - #Expecting an error - with pytest.raises(Exception): - g.addRules(start, solver.mkBoolean(False)) - -def testAddAnyConstant(): - solver = pycvc4.Solver() - boolean = solver.getBooleanSort() - - nullTerm = pycvc4.Term(solver) - start = solver.mkVar(boolean) - nts = solver.mkVar(boolean) - - g = solver.mkSygusGrammar({}, {start}) - - g.addAnyConstant(start) - g.addAnyConstant(start) - - with pytest.raises(Exception): - g.addAnyConstant(nullTerm) - with pytest.raises(Exception): - g.addAnyConstant(nts) - - solver.synthFun("f", {}, boolean, g) - - with pytest.raises(Exception): - g.addAnyConstant(start) - - -def testAddAnyVariable(): - solver = pycvc4.Solver() - boolean = solver.getBooleanSort() - - nullTerm = pycvc4.Term(solver) - x = solver.mkVar(boolean) - start = solver.mkVar(boolean) - nts = solver.mkVar(boolean) - - g1 = solver.mkSygusGrammar({x}, {start}) - g2 = solver.mkSygusGrammar({}, {start}) - - g1.addAnyVariable(start) - g1.addAnyVariable(start) - g2.addAnyVariable(start) - - with pytest.raises(Exception): - g1.addAnyVariable(nullTerm) - with pytest.raises(Exception): - g1.addAnyVariable(nts) - - solver.synthFun("f", {}, boolean, g1) - - with pytest.raises(Exception): - g1.addAnyVariable(start) - diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py deleted file mode 100644 index cff92ca8d..000000000 --- a/test/unit/api/python/test_sort.py +++ /dev/null @@ -1,355 +0,0 @@ -##################### -## test_sort.py -## Top contributors (to current version): -## Makai Mann, Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2020 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 pycvc4 -from pycvc4 import kinds - - -def testGetDatatype(): - solver = pycvc4.Solver() - dtypeSpec = solver.mkDatatypeDecl("list") - cons = solver.mkDatatypeConstructorDecl("cons") - cons.addSelector("head", solver.getIntegerSort()) - dtypeSpec.addConstructor(cons) - nil = solver.mkDatatypeConstructorDecl("nil") - dtypeSpec.addConstructor(nil) - dtypeSort = solver.mkDatatypeSort(dtypeSpec) - - # expecting no Error - dtypeSort.getDatatype() - - bvSort = solver.mkBitVectorSort(32) - with pytest.raises(Exception): - # expect an exception - bvSort.getDatatype() - - -def testDatatypeSorts(): - solver = pycvc4.Solver() - intSort = solver.getIntegerSort() - # create datatype sort to test - dtypeSpec = solver.mkDatatypeDecl("list") - cons = solver.mkDatatypeConstructorDecl("cons") - cons.addSelector("head", intSort) - cons.addSelectorSelf("tail") - dtypeSpec.addConstructor(cons) - nil = solver.mkDatatypeConstructorDecl("nil") - dtypeSpec.addConstructor(nil) - dtypeSort = solver.mkDatatypeSort(dtypeSpec) - dt = dtypeSort.getDatatype() - assert not dtypeSort.isConstructor() - - with pytest.raises(Exception): - dtypeSort.getConstructorCodomainSort() - - with pytest.raises(Exception): - dtypeSort.getConstructorDomainSorts() - - with pytest.raises(Exception): - dtypeSort.getConstructorArity() - - # get constructor - dcons = dt[0] - consTerm = dcons.getConstructorTerm() - consSort = consTerm.getSort() - assert consSort.isConstructor() - assert not consSort.isTester() - assert not consSort.isSelector() - assert consSort.getConstructorArity() == 2 - consDomSorts = consSort.getConstructorDomainSorts() - assert consDomSorts[0] == intSort - assert consDomSorts[1] == dtypeSort - assert consSort.getConstructorCodomainSort() == dtypeSort - - # get tester - isConsTerm = dcons.getTesterTerm() - assert isConsTerm.getSort().isTester() - - # get selector - dselTail = dcons[1] - tailTerm = dselTail.getSelectorTerm() - assert tailTerm.getSort().isSelector() - - -def testInstantiate(): - solver = pycvc4.Solver() - # instantiate parametric datatype, check should not fail - sort = solver.mkParamSort("T") - paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) - paramCons = solver.mkDatatypeConstructorDecl("cons") - paramNil = solver.mkDatatypeConstructorDecl("nil") - paramCons.addSelector("head", sort) - paramDtypeSpec.addConstructor(paramCons) - paramDtypeSpec.addConstructor(paramNil) - paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) - paramDtypeSort.instantiate([solver.getIntegerSort()]) - - # instantiate non-parametric datatype sort, check should fail - dtypeSpec = solver.mkDatatypeDecl("list") - cons = solver.mkDatatypeConstructorDecl("cons") - cons.addSelector("head", solver.getIntegerSort()) - dtypeSpec.addConstructor(cons) - nil = solver.mkDatatypeConstructorDecl("nil") - dtypeSpec.addConstructor(nil) - dtypeSort = solver.mkDatatypeSort(dtypeSpec) - - with pytest.raises(Exception): - dtypeSort.instantiate([solver.getIntegerSort()]) - - -def testGetFunctionArity(): - solver = pycvc4.Solver() - funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), - solver.getIntegerSort()) - funSort.getFunctionArity() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getFunctionArity() - - -def testGetFunctionDomainSorts(): - solver = pycvc4.Solver() - funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), - solver.getIntegerSort()) - funSort.getFunctionDomainSorts() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getFunctionDomainSorts() - - -def testGetFunctionCodomainSort(): - solver = pycvc4.Solver() - funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), - solver.getIntegerSort()) - funSort.getFunctionCodomainSort() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getFunctionCodomainSort() - -def testGetArrayIndexSort(): - solver = pycvc4.Solver() - elementSort = solver.mkBitVectorSort(32) - indexSort = solver.mkBitVectorSort(32) - arraySort = solver.mkArraySort(indexSort, elementSort) - arraySort.getArrayIndexSort() - - with pytest.raises(Exception): - indexSort.getArrayIndexSort() - -def testGetArrayElementSort(): - solver = pycvc4.Solver() - elementSort = solver.mkBitVectorSort(32) - indexSort = solver.mkBitVectorSort(32) - arraySort = solver.mkArraySort(indexSort, elementSort) - arraySort.getArrayElementSort() - - with pytest.raises(Exception): - indexSort.getArrayElementSort() - -def testGetSetElementSort(): - solver = pycvc4.Solver() - setSort = solver.mkSetSort(solver.getIntegerSort()) - setSort.getSetElementSort() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getSetElementSort() - -def testGetSequenceElementSort(): - solver = pycvc4.Solver() - seqSort = solver.mkSequenceSort(solver.getIntegerSort()) - seqSort.getSequenceElementSort() - bvSort = solver.mkBitVectorSort(32) - assert not bvSort.isSequence() - - with pytest.raises(Exception): - bvSort.getSetElementSort() - -def testGetUninterpretedSortName(): - solver = pycvc4.Solver() - uSort = solver.mkUninterpretedSort("u") - uSort.getUninterpretedSortName() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getUninterpretedSortName() - -def testIsUninterpretedSortParameterized(): - solver = pycvc4.Solver() - uSort = solver.mkUninterpretedSort("u") - uSort.isUninterpretedSortParameterized() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.isUninterpretedSortParameterized() - -def testGetUninterpretedSortParamSorts(): - solver = pycvc4.Solver() - uSort = solver.mkUninterpretedSort("u") - uSort.getUninterpretedSortParamSorts() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getUninterpretedSortParamSorts() - -def testGetUninterpretedSortConstructorName(): - solver = pycvc4.Solver() - sSort = solver.mkSortConstructorSort("s", 2) - sSort.getSortConstructorName() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getSortConstructorName() - -def testGetUninterpretedSortConstructorArity(): - solver = pycvc4.Solver() - sSort = solver.mkSortConstructorSort("s", 2) - sSort.getSortConstructorArity() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getSortConstructorArity() - -def testGetBVSize(): - solver = pycvc4.Solver() - bvSort = solver.mkBitVectorSort(32) - bvSort.getBVSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - - with pytest.raises(Exception): - setSort.getBVSize() - -def testGetFPExponentSize(): - solver = pycvc4.Solver() - - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - - with pytest.raises(Exception): - setSort.getFPExponentSize() - else: - with pytest.raises(Exception): - solver.mkFloatingPointSort(4, 8) - -def testGetFPSignificandSize(): - solver = pycvc4.Solver() - - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - - with pytest.raises(Exception): - setSort.getFPSignificandSize() - else: - with pytest.raises(Exception): - solver.mkFloatingPointSort(4, 8) - -def testGetDatatypeParamSorts(): - solver = pycvc4.Solver() - # create parametric datatype, check should not fail - sort = solver.mkParamSort("T") - paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) - paramCons = solver.mkDatatypeConstructorDecl("cons") - paramNil = solver.mkDatatypeConstructorDecl("nil") - paramCons.addSelector("head", sort) - paramDtypeSpec.addConstructor(paramCons) - paramDtypeSpec.addConstructor(paramNil) - paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) - paramDtypeSort.getDatatypeParamSorts() - # create non-parametric datatype sort, check should fail - dtypeSpec = solver.mkDatatypeDecl("list") - cons = solver.mkDatatypeConstructorDecl("cons") - cons.addSelector("head", solver.getIntegerSort()) - dtypeSpec.addConstructor(cons) - nil = solver.mkDatatypeConstructorDecl("nil") - dtypeSpec.addConstructor(nil) - dtypeSort = solver.mkDatatypeSort(dtypeSpec) - - with pytest.raises(Exception): - dtypeSort.getDatatypeParamSorts() - - -def testGetDatatypeArity(): - solver = pycvc4.Solver() - # create datatype sort, check should not fail - dtypeSpec = solver.mkDatatypeDecl("list") - cons = solver.mkDatatypeConstructorDecl("cons") - cons.addSelector("head", solver.getIntegerSort()) - dtypeSpec.addConstructor(cons) - nil = solver.mkDatatypeConstructorDecl("nil") - dtypeSpec.addConstructor(nil) - dtypeSort = solver.mkDatatypeSort(dtypeSpec) - dtypeSort.getDatatypeArity() - # create bv sort, check should fail - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getDatatypeArity() - -def testGetTupleLength(): - solver = pycvc4.Solver() - tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()]) - tupleSort.getTupleLength() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getTupleLength() - -def testGetTupleSorts(): - solver = pycvc4.Solver() - tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()]) - tupleSort.getTupleSorts() - bvSort = solver.mkBitVectorSort(32) - - with pytest.raises(Exception): - bvSort.getTupleSorts() - -def testSortCompare(): - solver = pycvc4.Solver() - boolSort = solver.getBooleanSort() - intSort = solver.getIntegerSort() - bvSort = solver.mkBitVectorSort(32) - bvSort2 = solver.mkBitVectorSort(32) - assert bvSort >= bvSort2 - assert bvSort <= bvSort2 - assert (intSort > boolSort) != (intSort < boolSort) - assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort) - -def testSortSubtyping(): - solver = pycvc4.Solver() - intSort = solver.getIntegerSort() - realSort = solver.getRealSort() - assert intSort.isSubsortOf(realSort) - assert not realSort.isSubsortOf(intSort) - assert intSort.isComparableTo(realSort) - assert realSort.isComparableTo(intSort) - - arraySortII = solver.mkArraySort(intSort, intSort) - arraySortIR = solver.mkArraySort(intSort, realSort) - assert not arraySortII.isComparableTo(intSort) - # we do not support subtyping for arrays - assert not arraySortII.isComparableTo(arraySortIR) - - setSortI = solver.mkSetSort(intSort) - setSortR = solver.mkSetSort(realSort) - # we don't support subtyping for sets - assert not setSortI.isComparableTo(setSortR) - assert not setSortI.isSubsortOf(setSortR) - assert not setSortR.isComparableTo(setSortI) - assert not setSortR.isSubsortOf(setSortI) - diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py deleted file mode 100644 index a0c1b4681..000000000 --- a/test/unit/api/python/test_term.py +++ /dev/null @@ -1,124 +0,0 @@ -##################### -## test_term.py -## Top contributors (to current version): -## Makai Mann, Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2020 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 pycvc4 -from pycvc4 import kinds - - -def test_getitem(): - solver = pycvc4.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 = pycvc4.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 = pycvc4.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 = pycvc4.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 = pycvc4.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 = pycvc4.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/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py deleted file mode 100644 index eb15e7469..000000000 --- a/test/unit/api/python/test_to_python_obj.py +++ /dev/null @@ -1,71 +0,0 @@ -from fractions import Fraction -import pytest - -import pycvc4 -from pycvc4 import kinds - - -def testGetBool(): - solver = pycvc4.Solver() - t = solver.mkTrue() - f = solver.mkFalse() - assert t.toPythonObj() == True - assert f.toPythonObj() == False - - -def testGetInt(): - solver = pycvc4.Solver() - two = solver.mkInteger(2) - assert two.toPythonObj() == 2 - - -def testGetReal(): - solver = pycvc4.Solver() - half = solver.mkReal("1/2") - assert half.toPythonObj() == Fraction(1, 2) - - neg34 = solver.mkReal("-3/4") - assert neg34.toPythonObj() == Fraction(-3, 4) - - neg1 = solver.mkInteger("-1") - assert neg1.toPythonObj() == -1 - - -def testGetBV(): - solver = pycvc4.Solver() - three = solver.mkBitVector(8, 3) - assert three.toPythonObj() == 3 - - -def testGetArray(): - solver = pycvc4.Solver() - arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) - zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) - stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) - - array_dict = stores.toPythonObj() - - assert array_dict[1] == 2 - assert array_dict[2] == 3 - assert array_dict[4] == 5 - # an index that wasn't stored at should give zero - assert array_dict[8] == 0 - - -def testGetSymbol(): - solver = pycvc4.Solver() - solver.mkConst(solver.getBooleanSort(), "x") - - -def testGetString(): - solver = pycvc4.Solver() - - s1 = '"test\n"😃\\u{a}' - t1 = solver.mkString(s1) - assert s1 == t1.toPythonObj() - - s2 = '❤️CVC4❤️' - t2 = solver.mkString(s2) - assert s2 == t2.toPythonObj()