diff options
| author | makaimann <makaim@stanford.edu> | 2020-02-19 13:54:17 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-19 15:54:17 -0600 |
| commit | c82720479efcf922136f0919f6fc26a502b2515a (patch) | |
| tree | f9007e124cfc07490e914ae1e1e05747e1e1ee11 /src/api/cvc4cpp.h | |
| parent | c6a9ab9da205df7cbf192edc142ee151404dcb1b (diff) | |
Add Python bindings using Cython -- see below for more details (#2879)
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index f7f16832a..79c02c031 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1096,6 +1096,11 @@ class CVC4_PUBLIC DatatypeDecl friend class Solver; public: /** + * Nullary constructor for Cython + */ + DatatypeDecl(); + + /** * Destructor. */ ~DatatypeDecl(); @@ -1112,6 +1117,8 @@ class CVC4_PUBLIC DatatypeDecl /** Is this Datatype declaration parametric? */ bool isParametric() const; + bool isNull() const; + /** * @return a string representation of this datatype declaration */ @@ -1158,6 +1165,10 @@ class CVC4_PUBLIC DatatypeDecl const std::string& name, const std::vector<Sort>& params, bool isCoDatatype = false); + + // helper for isNull() to avoid calling API functions from other API functions + bool isNullHelper() const; + /* The internal (intermediate) datatype wrapped by this datatype * declaration * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -1295,6 +1306,9 @@ class CVC4_PUBLIC DatatypeConstructor friend class DatatypeConstructor; // to access constructor public: + /** Nullary constructor (required for Cython). */ + const_iterator(); + /** * Assignment operator. * @param it the iterator to assign to @@ -1398,6 +1412,9 @@ class CVC4_PUBLIC Datatype */ Datatype(const CVC4::Datatype& dtype); + // Nullary constructor for Cython + Datatype(); + /** * Destructor. */ @@ -1447,6 +1464,9 @@ class CVC4_PUBLIC Datatype friend class Datatype; // to access constructor public: + /** Nullary constructor (required for Cython). */ + const_iterator(); + /** * Assignment operator. * @param it the iterator to assign to |