From 5502891bb07179b24b664ea3d6a9877e8c3eb0a4 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 3 Jun 2021 16:57:29 -0700 Subject: [PATCH] Adding unit tests for the datatypes python API (#6658) This commit adds unit tests that are translated from `datatype_api_black.cpp`. One API function is also added to the python API. This is the last part of the python api unit tests for datatypes. Co-authored-by: Andres Noetzli --- src/api/python/cvc5.pxd | 1 + src/api/python/cvc5.pxi | 5 + test/python/unit/api/test_datatype_api.py | 234 ++++++++++++++++++++++ 3 files changed, 240 insertions(+) diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 2ad8cef5c..fdc1872e7 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -75,6 +75,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": DatatypeSelector operator[](const string& name) except + string getName() except + Term getConstructorTerm() except + + Term getSpecializedConstructorTerm(const Sort& retSort) except + Term getTesterTerm() except + size_t getNumSelectors() except + DatatypeSelector getSelector(const string& name) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 8599a1cd1..3339543f3 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -196,6 +196,11 @@ cdef class DatatypeConstructor: term.cterm = self.cdc.getConstructorTerm() return term + def getSpecializedConstructorTerm(self, Sort retSort): + cdef Term term = Term(self.solver) + term.cterm = self.cdc.getSpecializedConstructorTerm(retSort.csort) + return term + def getTesterTerm(self): cdef Term term = Term(self.solver) term.cterm = self.cdc.getTesterTerm() diff --git a/test/python/unit/api/test_datatype_api.py b/test/python/unit/api/test_datatype_api.py index 708942e98..24a47bd76 100644 --- a/test/python/unit/api/test_datatype_api.py +++ b/test/python/unit/api/test_datatype_api.py @@ -294,3 +294,237 @@ def test_parametric_datatype(solver): assert not pairIntReal.isSubsortOf(pairIntInt) assert not pairRealInt.isSubsortOf(pairIntInt) assert pairIntInt.isSubsortOf(pairIntInt) + + +def test_datatype_simply_rec(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 + unresTypes = set([]) + unresWList = solver.mkUninterpretedSort("wlist") + unresList = solver.mkUninterpretedSort("list") + unresNs = solver.mkUninterpretedSort("ns") + unresTypes.add(unresWList) + unresTypes.add(unresList) + unresTypes.add(unresNs) + + wlist = solver.mkDatatypeDecl("wlist") + leaf = solver.mkDatatypeConstructorDecl("leaf") + leaf.addSelector("data", unresList) + wlist.addConstructor(leaf) + + llist = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("car", unresWList) + cons.addSelector("cdr", unresList) + llist.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + llist.addConstructor(nil) + + ns = solver.mkDatatypeDecl("ns") + elem = solver.mkDatatypeConstructorDecl("elem") + elem.addSelector("ndata", solver.mkSetSort(unresWList)) + ns.addConstructor(elem) + elemArray = solver.mkDatatypeConstructorDecl("elemArray") + elemArray.addSelector("ndata", solver.mkArraySort(unresList, unresList)) + ns.addConstructor(elemArray) + + dtdecls = [wlist, llist, ns] + # this is well-founded and has no nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + 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 + + unresTypes.clear() + unresNs2 = solver.mkUninterpretedSort("ns2") + unresTypes.add(unresNs2) + + ns2 = solver.mkDatatypeDecl("ns2") + elem2 = solver.mkDatatypeConstructorDecl("elem2") + elem2.addSelector("ndata", + solver.mkArraySort(solver.getIntegerSort(), unresNs2)) + ns2.addConstructor(elem2) + nil2 = solver.mkDatatypeConstructorDecl("nil2") + ns2.addConstructor(nil2) + + dtdecls.clear() + dtdecls.append(ns2) + + # this is not well-founded due to non-simple recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray() + assert dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() \ + == 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 + + unresTypes.clear() + unresNs3 = solver.mkUninterpretedSort("ns3") + unresTypes.add(unresNs3) + unresList3 = solver.mkUninterpretedSort("list3") + unresTypes.add(unresList3) + + list3 = solver.mkDatatypeDecl("list3") + cons3 = solver.mkDatatypeConstructorDecl("cons3") + cons3.addSelector("car", unresNs3) + cons3.addSelector("cdr", unresList3) + list3.addConstructor(cons3) + nil3 = solver.mkDatatypeConstructorDecl("nil3") + list3.addConstructor(nil3) + + ns3 = solver.mkDatatypeDecl("ns3") + elem3 = solver.mkDatatypeConstructorDecl("elem3") + elem3.addSelector("ndata", solver.mkSetSort(unresList3)) + ns3.addConstructor(elem3) + + dtdecls.clear() + dtdecls.append(list3) + dtdecls.append(ns3) + + # both are well-founded and have nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + 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 + unresTypes.clear() + unresNs4 = solver.mkUninterpretedSort("ns4") + unresTypes.add(unresNs4) + unresList4 = solver.mkUninterpretedSort("list4") + unresTypes.add(unresList4) + + list4 = solver.mkDatatypeDecl("list4") + cons4 = solver.mkDatatypeConstructorDecl("cons4") + cons4.addSelector("car", solver.mkSetSort(unresNs4)) + cons4.addSelector("cdr", unresList4) + list4.addConstructor(cons4) + nil4 = solver.mkDatatypeConstructorDecl("nil4") + list4.addConstructor(nil4) + + ns4 = solver.mkDatatypeDecl("ns4") + elem4 = solver.mkDatatypeConstructorDecl("elem3") + elem4.addSelector("ndata", unresList4) + ns4.addConstructor(elem4) + + dtdecls.clear() + dtdecls.append(list4) + dtdecls.append(ns4) + + # both are well-founded and have nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + 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 + unresTypes.clear() + unresList5 = solver.mkSortConstructorSort("list5", 1) + unresTypes.add(unresList5) + + v = [] + x = solver.mkParamSort("X") + v.append(x) + list5 = solver.mkDatatypeDecl("list5", v) + + args = [x] + urListX = unresList5.instantiate(args) + args[0] = urListX + urListListX = unresList5.instantiate(args) + + cons5 = solver.mkDatatypeConstructorDecl("cons5") + cons5.addSelector("car", x) + cons5.addSelector("cdr", urListListX) + list5.addConstructor(cons5) + nil5 = solver.mkDatatypeConstructorDecl("nil5") + list5.addConstructor(nil5) + + dtdecls.clear() + dtdecls.append(list5) + + # well-founded and has nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + + +def test_datatype_specialized_cons(solver): + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # plist[X] = pcons(car: X, cdr: plist[X]) | pnil + # END + + # Make unresolved types as placeholders + unresTypes = set([]) + unresList = solver.mkSortConstructorSort("plist", 1) + unresTypes.add(unresList) + + v = [] + x = solver.mkParamSort("X") + v.append(x) + plist = solver.mkDatatypeDecl("plist", v) + + args = [x] + urListX = unresList.instantiate(args) + + pcons = solver.mkDatatypeConstructorDecl("pcons") + pcons.addSelector("car", x) + pcons.addSelector("cdr", urListX) + plist.addConstructor(pcons) + nil5 = solver.mkDatatypeConstructorDecl("pnil") + plist.addConstructor(nil5) + + dtdecls = [plist] + + # make the datatype sorts + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 1 + d = dtsorts[0].getDatatype() + nilc = d[0] + + isort = solver.getIntegerSort() + iargs = [isort] + listInt = dtsorts[0].instantiate(iargs) + + testConsTerm = Term(solver) + # get the specialized constructor term for list[Int] + testConsTerm = nilc.getSpecializedConstructorTerm(listInt) + assert testConsTerm != nilc.getConstructorTerm() + # error to get the specialized constructor term for Int + with pytest.raises(RuntimeError): + nilc.getSpecializedConstructorTerm(isort) -- 2.30.2