From 3830d80ce312e8633b9de6311b809bd9418ddd4a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 1 Sep 2020 23:37:14 -0700 Subject: [API] Fix Python Examples (#4943) When testing the API examples, Python examples were not included. This commit changes that and fixes multiple minor issues that came up once the tests were enabled: - It adds `Solver::supportsFloatingPoint()` as an API method that returns whether CVC4 is configured to support floating-point numbers or not (this is useful for failing gracefully when floating-point support is not available, e.g. in the case of our floating-point example). - It updates the `expections.py` example to use the new API. - It fixes the `sygus-fun.py` example. The example was passing a _set_ of non-terminals to `Solver::mkSygusGrammar()` but the order in which the non-terminals are passed in matters because the first non-terminal is considered to be the starting terminal. The commit also updates the documentation of that function. - It fixes the Python API for datatypes. The `__getitem__` function had a typo and the `datatypes.py` example was crashing as a result. --- src/api/python/cvc4.pxi | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'src/api/python/cvc4.pxi') diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index a51307d21..3caead057 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -21,7 +21,8 @@ from cvc4 cimport Grammar as c_Grammar from cvc4 cimport Sort as c_Sort from cvc4 cimport SortHashFunction as c_SortHashFunction from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE -from cvc4 cimport ROUND_TOWARD_ZERO, ROUND_NEAREST_TIES_TO_AWAY +from cvc4 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO +from cvc4 cimport ROUND_NEAREST_TIES_TO_AWAY from cvc4 cimport Term as c_Term from cvc4 cimport TermHashFunction as c_TermHashFunction @@ -88,7 +89,7 @@ cdef class Datatype: if isinstance(index, int) and index >= 0: dc.cdc = self.cd[( index)] elif isinstance(index, str): - dc.cdc = self.cd[( name.encode())] + dc.cdc = self.cd[( index.encode())] else: raise ValueError("Expecting a non-negative integer or string") return dc @@ -395,6 +396,9 @@ cdef class Solver: def __dealloc__(self): del self.csolver + def supportsFloatingPoint(self): + return self.csolver.supportsFloatingPoint() + def getBooleanSort(self): cdef Sort sort = Sort(self) sort.csort = self.csolver.getBooleanSort() @@ -415,9 +419,9 @@ cdef class Solver: sort.csort = self.csolver.getRegExpSort() return sort - def getRoundingmodeSort(self): + def getRoundingModeSort(self): cdef Sort sort = Sort(self) - sort.csort = self.csolver.getRoundingmodeSort() + sort.csort = self.csolver.getRoundingModeSort() return sort def getStringSort(self): @@ -1457,6 +1461,7 @@ cdef class Term: cdef __rounding_modes = { ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", ROUND_TOWARD_POSITIVE: "RoundTowardPositive", + ROUND_TOWARD_NEGATIVE: "RoundTowardNegative", ROUND_TOWARD_ZERO: "RoundTowardZero", ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" } -- cgit v1.2.3 From 0f9fb31069d51e003a39b0e93f506324dec2bdac Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 2 Sep 2020 14:02:26 -0700 Subject: [Python API] Add missing methods to Datatype/Term (#4998) Fixes #4942. The Python API was missing some methods related to datatypes. Most importantly, it was missing mkDatatypeSorts, which meant that datatypes with unresolved placeholders could not be resolved. This commit adds missing methods and ports the corresponding tests of datatype_api_black.h to Python. The commit also adds support for __getitem__ in Term. --- src/api/cvc4cpp.cpp | 9 +- src/api/cvc4cpp.h | 9 +- src/api/python/cvc4.pxd | 10 ++ src/api/python/cvc4.pxi | 47 ++++++++ test/unit/api/python/test_datatype_api.py | 171 ++++++++++++++++++++++++++++++ test/unit/api/python/test_term.py | 11 ++ 6 files changed, 249 insertions(+), 8 deletions(-) create mode 100644 test/unit/api/python/test_datatype_api.py (limited to 'src/api/python/cvc4.pxi') diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 6c39bfb91..5b3384439 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3148,8 +3148,8 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const } std::vector Solver::mkDatatypeSortsInternal( - std::vector& dtypedecls, - std::set& unresolvedSorts) const + const std::vector& dtypedecls, + const std::set& unresolvedSorts) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3367,8 +3367,9 @@ std::vector Solver::mkDatatypeSorts( CVC4_API_SOLVER_TRY_CATCH_END; } -std::vector Solver::mkDatatypeSorts(std::vector& dtypedecls, - std::set& unresolvedSorts) const +std::vector Solver::mkDatatypeSorts( + const std::vector& dtypedecls, + const std::set& unresolvedSorts) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index d92660920..acf34abf9 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2254,8 +2254,9 @@ class CVC4_PUBLIC Solver * @param unresolvedSorts the list of unresolved sorts * @return the datatype sorts */ - std::vector mkDatatypeSorts(std::vector& dtypedecls, - std::set& unresolvedSorts) const; + std::vector mkDatatypeSorts( + const std::vector& dtypedecls, + const std::set& unresolvedSorts) const; /** * Create function sort. @@ -3353,8 +3354,8 @@ class CVC4_PUBLIC Solver * @return the datatype sorts */ std::vector mkDatatypeSortsInternal( - std::vector& dtypedecls, - std::set& unresolvedSorts) const; + const std::vector& dtypedecls, + const std::set& unresolvedSorts) const; /** * Synthesize n-ary function following specified syntactic constraints. diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 841fbb44d..76dcc5317 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -1,6 +1,7 @@ # import dereference and increment operators from cython.operator cimport dereference as deref, preincrement as inc from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t +from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector from libcpp.pair cimport pair @@ -27,6 +28,12 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Term getConstructorTerm(const string& name) except + size_t getNumConstructors() except + bint isParametric() except + + bint isCodatatype() except + + bint isTuple() except + + bint isRecord() except + + bint isFinite() except + + bint isWellFounded() except + + bint hasNestedRecursion() except + string toString() except + cppclass const_iterator: const_iterator() except + @@ -127,6 +134,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Sort mkBitVectorSort(uint32_t size) except + Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except + Sort mkDatatypeSort(DatatypeDecl dtypedecl) except + + vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls, + const set[Sort]& unresolvedSorts) except + Sort mkFunctionSort(Sort domain, Sort codomain) except + Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except + Sort mkParamSort(const string& symbol) except + @@ -313,6 +322,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Term() bint operator==(const Term&) except + bint operator!=(const Term&) except + + Term operator[](size_t idx) except + Kind getKind() except + Sort getSort() except + Term substitute(const vector[Term] es, const vector[Term] & reps) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 3caead057..8c4bfe5e5 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -3,6 +3,7 @@ import sys from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t from libcpp.pair cimport pair +from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector @@ -110,6 +111,24 @@ cdef class Datatype: def isParametric(self): return self.cd.isParametric() + def isCodatatype(self): + return self.cd.isCodatatype() + + def isTuple(self): + return self.cd.isTuple() + + def isRecord(self): + return self.cd.isRecord() + + def isFinite(self): + return self.cd.isFinite() + + def isWellFounded(self): + return self.cd.isWellFounded() + + def hasNestedRecursion(self): + return self.cd.hasNestedRecursion() + def __str__(self): return self.cd.toString().decode() @@ -449,6 +468,26 @@ cdef class Solver: sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd) return sort + def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts): + sorts = [] + + cdef vector[c_DatatypeDecl] decls + for decl in dtypedecls: + decls.push_back(( decl).cdd) + + cdef set[c_Sort] usorts + for usort in unresolvedSorts: + usorts.insert(( usort).csort) + + csorts = self.csolver.mkDatatypeSorts( + decls, usorts) + for csort in csorts: + sort = Sort(self) + sort.csort = csort + sorts.append(sort) + + return sorts + def mkFunctionSort(self, sorts, Sort codomain): cdef Sort sort = Sort(self) @@ -1354,6 +1393,14 @@ cdef class Term: def __ne__(self, Term other): return self.cterm != other.cterm + def __getitem__(self, int index): + cdef Term term = Term(self.solver) + if index >= 0: + term.cterm = self.cterm[index] + else: + raise ValueError("Expecting a non-negative integer or string") + return term + def __str__(self): return self.cterm.toString().decode() diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py new file mode 100644 index 000000000..a5499ffd6 --- /dev/null +++ b/test/unit/api/python/test_datatype_api.py @@ -0,0 +1,171 @@ +import pytest + +import pycvc4 +from pycvc4 import kinds + + +def test_datatype_simply_rec(): + solver = pycvc4.Solver() + + # Create mutual datatypes corresponding to this definition block: + # + # DATATYPE + # wlist = leaf(data: list), + # list = cons(car: wlist, cdr: list) | nil, + # ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) + # END; + + # Make unresolved types as placeholders + unres_wlist = solver.mkUninterpretedSort('wlist') + unres_list = solver.mkUninterpretedSort('list') + unres_ns = solver.mkUninterpretedSort('ns') + unres_types = set([unres_wlist, unres_list, unres_ns]) + + wlist = solver.mkDatatypeDecl('wlist') + leaf = solver.mkDatatypeConstructorDecl('leaf') + leaf.addSelector('data', unres_list) + wlist.addConstructor(leaf) + + dlist = solver.mkDatatypeDecl('list') + cons = solver.mkDatatypeConstructorDecl('cons') + cons.addSelector('car', unres_wlist) + cons.addSelector('cdr', unres_list) + dlist.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dlist.addConstructor(nil) + + ns = solver.mkDatatypeDecl('ns') + elem = solver.mkDatatypeConstructorDecl('elem') + elem.addSelector('ndata', solver.mkSetSort(unres_wlist)) + ns.addConstructor(elem) + elem_array = solver.mkDatatypeConstructorDecl('elemArray') + elem_array.addSelector('ndata', solver.mkArraySort(unres_list, unres_list)) + ns.addConstructor(elem_array) + + # this is well-founded and has no nested recursion + dtdecls = [wlist, dlist, ns] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 3 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[2].getDatatype().isWellFounded() + assert not dtsorts[0].getDatatype().hasNestedRecursion() + assert not dtsorts[1].getDatatype().hasNestedRecursion() + assert not dtsorts[2].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # ns2 = elem2(ndata: array(int,ns2)) | nil2 + # END; + unres_ns2 = solver.mkUninterpretedSort('ns2') + unres_types = set([unres_ns2]) + + ns2 = solver.mkDatatypeDecl('ns2') + elem2 = solver.mkDatatypeConstructorDecl('elem2') + elem2.addSelector('ndata', + solver.mkArraySort(solver.getIntegerSort(), unres_ns2)) + ns2.addConstructor(elem2) + nil2 = solver.mkDatatypeConstructorDecl('nil2') + ns2.addConstructor(nil2) + + # this is not well-founded due to non-simple recursion + dtdecls = [ns2] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray() + elem_sort = dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() + assert elem_sort == dtsorts[0] + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list3 = cons3(car: ns3, cdr: list3) | nil3, + # ns3 = elem3(ndata: set(list3)) + # END + unres_ns3 = solver.mkUninterpretedSort('ns3') + unres_list3 = solver.mkUninterpretedSort('list3') + unres_types = set([unres_ns3, unres_list3]) + + list3 = solver.mkDatatypeDecl('list3') + cons3 = solver.mkDatatypeConstructorDecl('cons3') + cons3.addSelector('car', unres_ns3) + cons3.addSelector('cdr', unres_list3) + list3.addConstructor(cons3) + nil3 = solver.mkDatatypeConstructorDecl('nil3') + list3.addConstructor(nil3) + + ns3 = solver.mkDatatypeDecl('ns3') + elem3 = solver.mkDatatypeConstructorDecl('elem3') + elem3.addSelector('ndata', solver.mkSetSort(unres_list3)) + ns3.addConstructor(elem3) + + # both are well-founded and have nested recursion + dtdecls = [list3, ns3] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 2 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + assert dtsorts[1].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list4 = cons(car: set(ns4), cdr: list4) | nil, + # ns4 = elem(ndata: list4) + # END + unres_ns4 = solver.mkUninterpretedSort('ns4') + unres_list4 = solver.mkUninterpretedSort('list4') + unres_types = set([unres_ns4, unres_list4]) + + list4 = solver.mkDatatypeDecl('list4') + cons4 = solver.mkDatatypeConstructorDecl('cons4') + cons4.addSelector('car', solver.mkSetSort(unres_ns4)) + cons4.addSelector('cdr', unres_list4) + list4.addConstructor(cons4) + nil4 = solver.mkDatatypeConstructorDecl('nil4') + list4.addConstructor(nil4) + + ns4 = solver.mkDatatypeDecl('ns4') + elem4 = solver.mkDatatypeConstructorDecl('elem3') + elem4.addSelector('ndata', unres_list4) + ns4.addConstructor(elem4) + + # both are well-founded and have nested recursion + dtdecls = [list4, ns4] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 2 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + assert dtsorts[1].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil + # END + unres_list5 = solver.mkSortConstructorSort('list5', 1) + unres_types = set([unres_list5]) + + x = solver.mkParamSort('X') + v = [x] + list5 = solver.mkDatatypeDecl('list5', v) + + args = [x] + ur_list_x = unres_list5.instantiate(args) + args = [ur_list_x] + ur_list_list_x = unres_list5.instantiate(args) + + cons5 = solver.mkDatatypeConstructorDecl('cons5') + cons5.addSelector('car', x) + cons5.addSelector('cdr', ur_list_list_x) + list5.addConstructor(cons5) + nil5 = solver.mkDatatypeConstructorDecl('nil5') + list5.addConstructor(nil5) + + # well-founded and has nested recursion + dtdecls = [list5] + dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index b135e4510..ca8d4c741 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -4,6 +4,17 @@ 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() -- cgit v1.2.3