diff options
author | makaimann <makaim@stanford.edu> | 2020-11-02 16:17:21 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-02 16:17:21 -0800 |
commit | 116114d9277f7b706e30f4c7af3a531e3f75fe86 (patch) | |
tree | 6ebb38e127f46d1e6d89aa8bb7e7afa6fc1ad8fb /test/api/python | |
parent | 5eb06a56099612e96303429fd8a9158ed8ad3121 (diff) |
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.
Diffstat (limited to 'test/api/python')
-rw-r--r-- | test/api/python/CMakeLists.txt | 43 | ||||
-rw-r--r-- | test/api/python/test_datatype_api.py | 181 | ||||
-rw-r--r-- | test/api/python/test_grammar.py | 128 | ||||
-rw-r--r-- | test/api/python/test_sort.py | 355 | ||||
-rw-r--r-- | test/api/python/test_term.py | 124 | ||||
-rw-r--r-- | test/api/python/test_to_python_obj.py | 71 |
6 files changed, 902 insertions, 0 deletions
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/<output_dir>/myapitest' + # and run it with 'ctest -R "api/<output_dir>/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() |