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.
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'
)
endif()
endif()
+
+
+# add Python bindings tests if building with Python bindings
+if (BUILD_BINDINGS_PYTHON)
+ add_subdirectory(python)
+endif()
--- /dev/null
+#####################
+## 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)
--- /dev/null
+#####################
+## 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()
--- /dev/null
+#####################
+## 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)
+
--- /dev/null
+#####################
+## 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)
+
--- /dev/null
+#####################
+## 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
--- /dev/null
+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()
cvc4_add_unit_test_black(sort_black api)
cvc4_add_unit_test_black(term_black api)
cvc4_add_unit_test_black(grammar_black api)
+
+++ /dev/null
-#####################
-## 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()
+++ /dev/null
-#####################
-## 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)
-
+++ /dev/null
-#####################
-## 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)
-
+++ /dev/null
-#####################
-## 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
+++ /dev/null
-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()
projects / cvc5.git / commitdiff