From d6a50e3ebeea29abaa5a2aee624590490fa75dda Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 20 Apr 2021 07:33:10 -0700 Subject: [PATCH] python API sorts: adding functions and tests (#6361) This PR does the following: 1. removes old python sort API test 2. creates a new python sort API test, obtained by translating the (entire) cpp unit test https://github.com/CVC4/CVC4/blob/master/test/unit/api/sort_black.cpp 3. adds support for bags and datatype selectors/testers domain/codomain in the python API. --- src/api/python/cvc4.pxd | 7 + src/api/python/cvc4.pxi | 33 ++ test/api/python/CMakeLists.txt | 1 - test/api/python/test_sort.py | 358 ------------------- test/python/CMakeLists.txt | 1 + test/python/unit/api/test_sort.py | 566 ++++++++++++++++++++++++++++++ 6 files changed, 607 insertions(+), 359 deletions(-) delete mode 100644 test/api/python/test_sort.py create mode 100644 test/python/unit/api/test_sort.py diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 213372892..abc23ea4b 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -142,6 +142,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort mkPredicateSort(const vector[Sort]& sorts) except + Sort mkRecordSort(const vector[pair[string, Sort]]& fields) except + Sort mkSetSort(Sort elemSort) except + + Sort mkBagSort(Sort elemSort) except + Sort mkSequenceSort(Sort elemSort) except + Sort mkUninterpretedSort(const string& symbol) except + Sort mkSortConstructorSort(const string& symbol, size_t arity) except + @@ -282,6 +283,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isRecord() except + bint isArray() except + bint isSet() except + + bint isBag() except + bint isSequence() except + bint isUninterpretedSort() except + bint isSortConstructor() except + @@ -294,12 +296,17 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": size_t getConstructorArity() except + vector[Sort] getConstructorDomainSorts() except + Sort getConstructorCodomainSort() except + + Sort getSelectorDomainSort() except + + Sort getSelectorCodomainSort() except + + Sort getTesterDomainSort() except + + Sort getTesterCodomainSort() except + size_t getFunctionArity() except + vector[Sort] getFunctionDomainSorts() except + Sort getFunctionCodomainSort() except + Sort getArrayIndexSort() except + Sort getArrayElementSort() except + Sort getSetElementSort() except + + Sort getBagElementSort() except + Sort getSequenceElementSort() except + string getUninterpretedSortName() except + bint isUninterpretedSortParameterized() except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index a08e50931..3156b0882 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -554,6 +554,11 @@ cdef class Solver: sort.csort = self.csolver.mkSetSort(elemSort.csort) return sort + def mkBagSort(self, Sort elemSort): + cdef Sort sort = Sort(self) + sort.csort = self.csolver.mkBagSort(elemSort.csort) + return sort + def mkSequenceSort(self, Sort elemSort): cdef Sort sort = Sort(self) sort.csort = self.csolver.mkSequenceSort(elemSort.csort) @@ -1241,6 +1246,9 @@ cdef class Sort: def isSet(self): return self.csort.isSet() + def isBag(self): + return self.csort.isBag() + def isSequence(self): return self.csort.isSequence() @@ -1291,6 +1299,26 @@ cdef class Sort: sort.csort = self.csort.getConstructorCodomainSort() return sort + def getSelectorDomainSort(self): + cdef Sort sort = Sort(self.solver) + sort.csort = self.csort.getSelectorDomainSort() + return sort + + def getSelectorCodomainSort(self): + cdef Sort sort = Sort(self.solver) + sort.csort = self.csort.getSelectorCodomainSort() + return sort + + def getTesterDomainSort(self): + cdef Sort sort = Sort(self.solver) + sort.csort = self.csort.getTesterDomainSort() + return sort + + def getTesterCodomainSort(self): + cdef Sort sort = Sort(self.solver) + sort.csort = self.csort.getTesterCodomainSort() + return sort + def getFunctionArity(self): return self.csort.getFunctionArity() @@ -1322,6 +1350,11 @@ cdef class Sort: sort.csort = self.csort.getSetElementSort() return sort + def getBagElementSort(self): + cdef Sort sort = Sort(self.solver) + sort.csort = self.csort.getBagElementSort() + return sort + def getSequenceElementSort(self): cdef Sort sort = Sort(self.solver) sort.csort = self.csort.getSequenceElementSort() diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index af4c8c183..d6d14b310 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -40,6 +40,5 @@ 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_sort.py b/test/api/python/test_sort.py deleted file mode 100644 index cb8198f98..000000000 --- a/test/api/python/test_sort.py +++ /dev/null @@ -1,358 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Makai Mann, Andres Noetzli, Mudathir Mohamed -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -# in the top-level source directory and their institutional affiliations. -# All rights reserved. See the file COPYING in the top-level source -# directory for licensing information. -# ############################################################################# -## - -import pytest - -import 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/python/CMakeLists.txt b/test/python/CMakeLists.txt index f3566b6ec..59911299b 100644 --- a/test/python/CMakeLists.txt +++ b/test/python/CMakeLists.txt @@ -28,3 +28,4 @@ endmacro() # add specific test files cvc4_add_python_api_test(pytest_solver unit/api/test_solver.py) +cvc4_add_python_api_test(pytest_sort unit/api/test_sort.py) diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py new file mode 100644 index 000000000..b4aa3a11f --- /dev/null +++ b/test/python/unit/api/test_sort.py @@ -0,0 +1,566 @@ +##################### +## test_sort.py +## Top contributors (to current version): +## Yoni Zohar +## This file is part of the CVC4 project. +## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +## ######################################################## +## +## Unit tests for sort API. +## Obtained by translating test/unit/api/sort_black.cpp + +import pytest +import pycvc4 +from pycvc4 import kinds +from pycvc4 import Sort + + +@pytest.fixture +def solver(): + return pycvc4.Solver() + + +def create_datatype_sort(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) + return dtypeSort + + +def create_param_datatype_sort(solver): + 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) + return paramDtypeSort + + +def test_operators_comparison(solver): + solver.getIntegerSort() == Sort(solver) + solver.getIntegerSort() != Sort(solver) + solver.getIntegerSort() < Sort(solver) + solver.getIntegerSort() <= Sort(solver) + solver.getIntegerSort() > Sort(solver) + solver.getIntegerSort() >= Sort(solver) + + +def test_is_boolean(solver): + assert solver.getBooleanSort().isBoolean() + Sort(solver).isBoolean() + + +def test_is_integer(solver): + assert solver.getIntegerSort().isInteger() + assert not solver.getRealSort().isInteger() + Sort(solver).isInteger() + + +def test_is_real(solver): + assert solver.getRealSort().isReal() + assert not solver.getIntegerSort().isReal() + Sort(solver).isReal() + + +def test_is_string(solver): + assert solver.getStringSort().isString() + Sort(solver).isString() + + +def test_is_reg_exp(solver): + assert solver.getRegExpSort().isRegExp() + Sort(solver).isRegExp() + + +def test_is_rounding_mode(solver): + if solver.supportsFloatingPoint(): + assert solver.getRoundingModeSort().isRoundingMode() + Sort(solver).isRoundingMode() + + +def test_is_bit_vector(solver): + assert solver.mkBitVectorSort(8).isBitVector() + Sort(solver).isBitVector() + + +def test_is_floating_point(solver): + if solver.supportsFloatingPoint(): + assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() + Sort(solver).isFloatingPoint() + + +def test_is_datatype(solver): + dt_sort = create_datatype_sort(solver) + assert dt_sort.isDatatype() + Sort(solver).isDatatype() + + +def test_is_parametric_datatype(solver): + param_dt_sort = create_param_datatype_sort(solver) + assert param_dt_sort.isParametricDatatype() + Sort(solver).isParametricDatatype() + + +def test_is_constructor(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + cons_sort = dt[0].getConstructorTerm().getSort() + assert cons_sort.isConstructor() + Sort(solver).isConstructor() + + +def test_is_selector(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + dt0 = dt[0] + dt01 = dt0[1] + cons_sort = dt01.getSelectorTerm().getSort() + assert cons_sort.isSelector() + Sort(solver).isSelector() + + +def test_is_tester(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + cons_sort = dt[0].getTesterTerm().getSort() + assert cons_sort.isTester() + Sort(solver).isTester() + + +def test_is_function(solver): + fun_sort = solver.mkFunctionSort(solver.getRealSort(), + solver.getIntegerSort()) + assert fun_sort.isFunction() + Sort(solver).isFunction() + + +def test_is_predicate(solver): + pred_sort = solver.mkPredicateSort(solver.getRealSort()) + assert pred_sort.isPredicate() + Sort(solver).isPredicate() + + +def test_is_tuple(solver): + tup_sort = solver.mkTupleSort(solver.getRealSort()) + assert tup_sort.isTuple() + Sort(solver).isTuple() + + +def test_is_record(solver): + rec_sort = solver.mkRecordSort([("asdf", solver.getRealSort())]) + assert rec_sort.isRecord() + Sort(solver).isRecord() + + +def test_is_array(solver): + arr_sort = solver.mkArraySort(solver.getRealSort(), + solver.getIntegerSort()) + assert arr_sort.isArray() + Sort(solver).isArray() + + +def test_is_set(solver): + set_sort = solver.mkSetSort(solver.getRealSort()) + assert set_sort.isSet() + Sort(solver).isSet() + + +def test_is_bag(solver): + bag_sort = solver.mkBagSort(solver.getRealSort()) + assert bag_sort.isBag() + Sort(solver).isBag() + + +def test_is_sequence(solver): + seq_sort = solver.mkSequenceSort(solver.getRealSort()) + assert seq_sort.isSequence() + Sort(solver).isSequence() + + +def test_is_uninterpreted(solver): + un_sort = solver.mkUninterpretedSort("asdf") + assert un_sort.isUninterpretedSort() + Sort(solver).isUninterpretedSort() + + +def test_is_sort_constructor(solver): + sc_sort = solver.mkSortConstructorSort("asdf", 1) + assert sc_sort.isSortConstructor() + Sort(solver).isSortConstructor() + + +def test_is_first_class(solver): + fun_sort = solver.mkFunctionSort(solver.getRealSort(), + solver.getIntegerSort()) + assert solver.getIntegerSort().isFirstClass() + assert fun_sort.isFirstClass() + reSort = solver.getRegExpSort() + assert not reSort.isFirstClass() + Sort(solver).isFirstClass() + + +def test_is_function_like(solver): + fun_sort = solver.mkFunctionSort(solver.getRealSort(), + solver.getIntegerSort()) + assert not solver.getIntegerSort().isFunctionLike() + assert fun_sort.isFunctionLike() + + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + cons_sort = dt[0][1].getSelectorTerm().getSort() + assert cons_sort.isFunctionLike() + + Sort(solver).isFunctionLike() + + +def test_is_subsort_of(solver): + assert solver.getIntegerSort().isSubsortOf(solver.getIntegerSort()) + assert solver.getIntegerSort().isSubsortOf(solver.getRealSort()) + assert not solver.getIntegerSort().isSubsortOf(solver.getBooleanSort()) + Sort(solver).isSubsortOf(Sort(solver)) + + +def test_is_comparable_to(solver): + assert solver.getIntegerSort().isComparableTo(solver.getIntegerSort()) + assert solver.getIntegerSort().isComparableTo(solver.getRealSort()) + assert not solver.getIntegerSort().isComparableTo(solver.getBooleanSort()) + Sort(solver).isComparableTo(Sort(solver)) + + +def test_get_datatype(solver): + dtypeSort = create_datatype_sort(solver) + dtypeSort.getDatatype() + # create bv sort, check should fail + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getDatatype() + + +def test_datatype_sorts(solver): + intSort = solver.getIntegerSort() + dtypeSort = create_datatype_sort(solver) + dt = dtypeSort.getDatatype() + assert not dtypeSort.isConstructor() + with pytest.raises(RuntimeError): + dtypeSort.getConstructorCodomainSort() + with pytest.raises(RuntimeError): + dtypeSort.getConstructorDomainSorts() + with pytest.raises(RuntimeError): + 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() + booleanSort = solver.getBooleanSort() + + assert isConsTerm.getSort().getTesterDomainSort() == dtypeSort + assert isConsTerm.getSort().getTesterCodomainSort() == booleanSort + with pytest.raises(RuntimeError): + booleanSort.getTesterDomainSort() + with pytest.raises(RuntimeError): + booleanSort.getTesterCodomainSort() + + # get selector + dselTail = dcons[1] + tailTerm = dselTail.getSelectorTerm() + assert tailTerm.getSort().isSelector() + assert tailTerm.getSort().getSelectorDomainSort() == dtypeSort + assert tailTerm.getSort().getSelectorCodomainSort() == dtypeSort + with pytest.raises(RuntimeError): + booleanSort.getSelectorDomainSort() + with pytest.raises(RuntimeError): + booleanSort.getSelectorCodomainSort() + + +def test_instantiate(solver): + # instantiate parametric datatype, check should not fail + paramDtypeSort = create_param_datatype_sort(solver) + 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(RuntimeError): + dtypeSort.instantiate([solver.getIntegerSort()]) + + +def test_get_function_arity(solver): + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionArity() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getFunctionArity() + + +def test_get_function_domain_sorts(solver): + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionDomainSorts() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getFunctionDomainSorts() + + +def test_get_function_codomain_sort(solver): + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionCodomainSort() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getFunctionCodomainSort() + + +def test_get_array_index_sort(solver): + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayIndexSort() + with pytest.raises(RuntimeError): + indexSort.getArrayIndexSort() + + +def test_get_array_element_sort(solver): + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayElementSort() + with pytest.raises(RuntimeError): + indexSort.getArrayElementSort() + + +def test_get_set_element_sort(solver): + setSort = solver.mkSetSort(solver.getIntegerSort()) + setSort.getSetElementSort() + elementSort = setSort.getSetElementSort() + assert elementSort == solver.getIntegerSort() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getSetElementSort() + + +def test_get_bag_element_sort(solver): + bagSort = solver.mkBagSort(solver.getIntegerSort()) + bagSort.getBagElementSort() + elementSort = bagSort.getBagElementSort() + assert elementSort == solver.getIntegerSort() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getBagElementSort() + + +def test_get_sequence_element_sort(solver): + seqSort = solver.mkSequenceSort(solver.getIntegerSort()) + assert seqSort.isSequence() + seqSort.getSequenceElementSort() + bvSort = solver.mkBitVectorSort(32) + assert not bvSort.isSequence() + with pytest.raises(RuntimeError): + bvSort.getSequenceElementSort() + + +def test_get_uninterpreted_sort_name(solver): + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortName() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getUninterpretedSortName() + + +def test_is_uninterpreted_sort_parameterized(solver): + uSort = solver.mkUninterpretedSort("u") + assert not uSort.isUninterpretedSortParameterized() + sSort = solver.mkSortConstructorSort("s", 1) + siSort = sSort.instantiate([uSort]) + assert siSort.isUninterpretedSortParameterized() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.isUninterpretedSortParameterized() + + +def test_get_uninterpreted_sort_paramsorts(solver): + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortParamSorts() + sSort = solver.mkSortConstructorSort("s", 2) + siSort = sSort.instantiate([uSort, uSort]) + assert len(siSort.getUninterpretedSortParamSorts()) == 2 + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getUninterpretedSortParamSorts() + + +def test_get_uninterpreted_sort_constructor_name(solver): + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorName() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getSortConstructorName() + + +def test_get_uninterpreted_sort_constructor_arity(solver): + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorArity() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getSortConstructorArity() + + +def test_get_bv_size(solver): + bvSort = solver.mkBitVectorSort(32) + bvSort.getBVSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getBVSize() + + +def test_get_fp_exponent_size(solver): + if solver.supportsFloatingPoint(): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPExponentSize() + + +def test_get_fp_significand_size(solver): + if solver.supportsFloatingPoint(): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPSignificandSize() + + +def test_get_datatype_paramsorts(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(RuntimeError): + dtypeSort.getDatatypeParamSorts() + + +def test_get_datatype_arity(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(RuntimeError): + bvSort.getDatatypeArity() + + +def test_get_tuple_length(solver): + tupleSort = solver.mkTupleSort( + [solver.getIntegerSort(), + solver.getIntegerSort()]) + tupleSort.getTupleLength() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getTupleLength() + + +def test_get_tuple_sorts(solver): + tupleSort = solver.mkTupleSort( + [solver.getIntegerSort(), + solver.getIntegerSort()]) + tupleSort.getTupleSorts() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getTupleSorts() + + +def test_sort_compare(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 test_sort_subtyping(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) + + +def test_sort_scoped_tostring(solver): + name = "uninterp-sort" + bvsort8 = solver.mkBitVectorSort(8) + uninterp_sort = solver.mkUninterpretedSort(name) + assert str(bvsort8) == "(_ BitVec 8)" + assert str(uninterp_sort) == name + solver2 = pycvc4.Solver() + assert str(bvsort8) == "(_ BitVec 8)" + assert str(uninterp_sort) == name -- 2.30.2