diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-11 22:45:03 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-11 20:45:03 -0700 |
commit | f48b987d63fef3f698e02c9a48fdba33ffb1c564 (patch) | |
tree | 90b29c6276f692582cb7040d32172fb802075f10 /src | |
parent | 6e69899967624b04c98c3d291693bae6d32401f6 (diff) |
Simplifications to the Datatypes API (#4040)
Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument.
I updated the Python files, although would be helpful to double check this is correct.
Co-authored-by: makaimann <makaim@stanford.edu>
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 50 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 65 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 13 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 32 |
4 files changed, 25 insertions, 135 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ff25bbabb..037243ea4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1737,32 +1737,6 @@ size_t TermHashFunction::operator()(const Term& t) const /* Datatypes */ /* -------------------------------------------------------------------------- */ -/* DatatypeSelectorDecl ----------------------------------------------------- */ - -DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, Sort sort) - : d_name(name), d_sort(sort) -{ -} - -DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, - DatatypeDeclSelfSort sort) - : d_name(name), d_sort(Sort(CVC4::Type())) -{ -} - -std::string DatatypeSelectorDecl::toString() const -{ - std::stringstream ss; - ss << d_name << ": " << d_sort; - return ss.str(); -} - -std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) -{ - out << dtdecl.toString(); - return out; -} - /* DatatypeConstructorDecl -------------------------------------------------- */ DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name) @@ -1770,17 +1744,16 @@ DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name) { } -void DatatypeConstructorDecl::addSelector(const DatatypeSelectorDecl& stor) +void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort) { - CVC4::Type t = *stor.d_sort.d_type; - if (t.isNull()) - { - d_ctor->addArg(stor.d_name, DatatypeSelfType()); - } - else - { - d_ctor->addArg(stor.d_name, t); - } + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) + << "non-null range sort for selector"; + d_ctor->addArg(name, *sort.d_type); +} + +void DatatypeConstructorDecl::addSelectorSelf(const std::string& name) +{ + d_ctor->addArg(name, DatatypeSelfType()); } std::string DatatypeConstructorDecl::toString() const @@ -1890,10 +1863,9 @@ bool DatatypeDecl::isNull() const { return isNullHelper(); } // to the new API. !!! CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } -std::ostream& operator<<(std::ostream& out, - const DatatypeSelectorDecl& stordecl) +std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) { - out << stordecl.toString(); + out << dtdecl.toString(); return out; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index dcf787b8e..7ccb73bc3 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -189,7 +189,6 @@ class CVC4_PUBLIC Sort { friend class DatatypeConstructorDecl; friend class DatatypeDecl; - friend class DatatypeSelectorDecl; friend class Op; friend class Solver; friend struct SortHashFunction; @@ -1138,51 +1137,6 @@ class DatatypeConstructorIterator; class DatatypeIterator; /** - * A place-holder sort to allow a DatatypeDecl to refer to itself. - * Self-sorted fields of DatatypeDecls will be properly sorted when a Sort is - * created for the DatatypeDecl. - */ -class CVC4_PUBLIC DatatypeDeclSelfSort -{ -}; - -/** - * A CVC4 datatype selector declaration. - */ -class CVC4_PUBLIC DatatypeSelectorDecl -{ - friend class DatatypeConstructorDecl; - - public: - /** - * Constructor. - * @param name the name of the datatype selector - * @param sort the sort of the datatype selector - * @return the DatatypeSelectorDecl - */ - DatatypeSelectorDecl(const std::string& name, Sort sort); - - /** - * Constructor. - * @param name the name of the datatype selector - * @param sort the sort of the datatype selector - * @return the DAtatypeSelectorDecl - */ - DatatypeSelectorDecl(const std::string& name, DatatypeDeclSelfSort sort); - - /** - * @return a string representation of this datatype selector - */ - std::string toString() const; - - private: - /* The name of the datatype selector. */ - std::string d_name; - /* The sort of the datatype selector. */ - Sort d_sort; -}; - -/** * A CVC4 datatype constructor declaration. */ class CVC4_PUBLIC DatatypeConstructorDecl @@ -1199,9 +1153,15 @@ class CVC4_PUBLIC DatatypeConstructorDecl /** * Add datatype selector declaration. - * @param stor the datatype selector declaration to add + * @param name the name of the datatype selector declaration to add + * @param sort the range sort of the datatype selector declaration to add + */ + void addSelector(const std::string& name, Sort sort); + /** + * Add datatype selector declaration whose range type is the datatype itself. + * @param name the name of the datatype selector declaration to add */ - void addSelector(const DatatypeSelectorDecl& stor); + void addSelectorSelf(const std::string& name); /** * @return a string representation of this datatype constructor declaration @@ -1768,15 +1728,6 @@ std::ostream& operator<<(std::ostream& out, const std::vector<DatatypeConstructorDecl>& vector); /** - * Serialize a datatype selector declaration to given stream. - * @param out the output stream - * @param stordecl the datatype selector declaration to be serialized - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const DatatypeSelectorDecl& stordecl) CVC4_PUBLIC; - -/** * Serialize a datatype to given stream. * @param out the output stream * @param dtdecl the datatype to be serialized to given stream diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index b8bf009af..bbff6f58b 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -55,7 +55,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass DatatypeConstructorDecl: DatatypeConstructorDecl(const string& name) except + - void addSelector(const DatatypeSelectorDecl& stor) except + + void addSelector(const string& name, Sort sort) except + + void addSelectorSelf(const string& name) except + string toString() except + @@ -65,21 +66,11 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": string toString() except + - cdef cppclass DatatypeDeclSelfSort: - DatatypeDeclSelfSort() except + - - cdef cppclass DatatypeSelector: DatatypeSelector() except + string toString() except + - cdef cppclass DatatypeSelectorDecl: - DatatypeSelectorDecl(const string& name, Sort sort) except + - DatatypeSelectorDecl(const string& name, DatatypeDeclSelfSort sort) except + - string toString() except + - - cdef cppclass Op: Op() except + bint operator==(const Op&) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 7e0e2e3c8..d61fed0fc 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -11,9 +11,7 @@ from cvc4 cimport Datatype as c_Datatype from cvc4 cimport DatatypeConstructor as c_DatatypeConstructor from cvc4 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl from cvc4 cimport DatatypeDecl as c_DatatypeDecl -from cvc4 cimport DatatypeDeclSelfSort as c_DatatypeDeclSelfSort from cvc4 cimport DatatypeSelector as c_DatatypeSelector -from cvc4 cimport DatatypeSelectorDecl as c_DatatypeSelectorDecl from cvc4 cimport Result as c_Result from cvc4 cimport RoundingMode as c_RoundingMode from cvc4 cimport Op as c_Op @@ -131,8 +129,10 @@ cdef class DatatypeConstructorDecl: def __cinit__(self, str name): self.cddc = new c_DatatypeConstructorDecl(name.encode()) - def addSelector(self, DatatypeSelectorDecl stor): - self.cddc.addSelector(stor.cdsd[0]) + def addSelector(self, str name, Sort sort): + self.cddc.addSelector(name.encode(), sort.csort) + def addSelectorSelf(self, str name): + self.cddc.addSelectorSelf(name.encode()) def __str__(self): return self.cddc.toString().decode() @@ -159,12 +159,6 @@ cdef class DatatypeDecl: return self.cdd.toString().decode() -cdef class DatatypeDeclSelfSort: - cdef c_DatatypeDeclSelfSort cddss - def __cinit__(self): - self.cddss = c_DatatypeDeclSelfSort() - - cdef class DatatypeSelector: cdef c_DatatypeSelector cds def __cinit__(self): @@ -177,24 +171,6 @@ cdef class DatatypeSelector: return self.cds.toString().decode() -cdef class DatatypeSelectorDecl: - cdef c_DatatypeSelectorDecl* cdsd - def __cinit__(self, str name, sort): - if isinstance(sort, Sort): - self.cdsd = new c_DatatypeSelectorDecl( - <const string &> name.encode(), (<Sort?> sort).csort) - elif isinstance(sort, DatatypeDeclSelfSort): - self.cdsd = new c_DatatypeSelectorDecl( - <const string &> name.encode(), - (<DatatypeDeclSelfSort?> sort).cddss) - - def __str__(self): - return self.cdsd.toString().decode() - - def __repr__(self): - return self.cdsd.toString().decode() - - cdef class Op: cdef c_Op cop def __cinit__(self): |