diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 47 |
1 files changed, 38 insertions, 9 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 87be7b74c..855ba4400 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1167,14 +1167,13 @@ class DatatypeIterator; class CVC4_PUBLIC DatatypeConstructorDecl { friend class DatatypeDecl; + friend class Solver; public: /** - * Constructor. - * @param name the name of the datatype constructor - * @return the DatatypeConstructorDecl + * Nullary constructor for Cython. */ - DatatypeConstructorDecl(const std::string& name); + DatatypeConstructorDecl(); /** * Add datatype selector declaration. @@ -1199,6 +1198,19 @@ class CVC4_PUBLIC DatatypeConstructorDecl private: /** + * Constructor. + * @param slv the associated solver object + * @param name the name of the datatype constructor + * @return the DatatypeConstructorDecl + */ + DatatypeConstructorDecl(const Solver* slv, const std::string& name); + + /** + * The associated solver object. + */ + const Solver* d_solver; + + /** * The internal (intermediate) datatype constructor wrapped by this * datatype constructor declaration. * This is a shared_ptr rather than a unique_ptr since @@ -1219,7 +1231,7 @@ class CVC4_PUBLIC DatatypeDecl public: /** - * Nullary constructor for Cython + * Nullary constructor for Cython. */ DatatypeDecl(); @@ -1240,6 +1252,9 @@ class CVC4_PUBLIC DatatypeDecl /** Is this Datatype declaration parametric? */ bool isParametric() const; + /** + * @return true if this DatatypeDecl is a null object + */ bool isNull() const; /** @@ -1257,7 +1272,7 @@ class CVC4_PUBLIC DatatypeDecl private: /** * Constructor. - * @param slv the solver that created this datatype declaration + * @param slv the associated solver object * @param name the name of the datatype * @param isCoDatatype true if a codatatype is to be constructed * @return the DatatypeDecl @@ -1269,7 +1284,7 @@ class CVC4_PUBLIC DatatypeDecl /** * Constructor for parameterized datatype declaration. * Create sorts parameter with Solver::mkParamSort(). - * @param slv the solver that created this datatype declaration + * @param slv the associated solver object * @param name the name of the datatype * @param param the sort parameter * @param isCoDatatype true if a codatatype is to be constructed @@ -1282,7 +1297,7 @@ class CVC4_PUBLIC DatatypeDecl /** * Constructor for parameterized datatype declaration. * Create sorts parameter with Solver::mkParamSort(). - * @param slv the solver that created this datatype declaration + * @param slv the associated solver object * @param name the name of the datatype * @param params a list of sort parameters * @param isCoDatatype true if a codatatype is to be constructed @@ -1292,9 +1307,17 @@ class CVC4_PUBLIC DatatypeDecl const std::vector<Sort>& params, bool isCoDatatype = false); - // helper for isNull() to avoid calling API functions from other API functions + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ bool isNullHelper() const; + /** + * The associated solver object. + */ + const Solver* d_solver; + /* The internal (intermediate) datatype wrapped by this datatype * declaration * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -2680,6 +2703,12 @@ class CVC4_PUBLIC Solver Term mkVar(Sort sort, const std::string& symbol = std::string()) const; /* .................................................................... */ + /* Create datatype constructor declarations */ + /* .................................................................... */ + + DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name); + + /* .................................................................... */ /* Create datatype declarations */ /* .................................................................... */ |