diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-06 11:00:33 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-06 11:00:33 -0600 |
commit | c7c2d593674e3776ab0c720be1c0c759db8f9453 (patch) | |
tree | fc129a2f0453eb2944009249c4a83ba3bdbaf5a0 /src/api/cvc4cpp.h | |
parent | 499aa5641e2b830f60159c2ce1c791bf4d45aac1 (diff) |
Add ExprManager as argument to Datatype (#3535)
Diffstat (limited to 'src/api/cvc4cpp.h')
-rw-r--r-- | src/api/cvc4cpp.h | 103 |
1 files changed, 74 insertions, 29 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 8c9bdc10c..e05c228bc 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1093,6 +1093,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl std::shared_ptr<CVC4::DatatypeConstructor> d_ctor; }; +class Solver; /** * A CVC4 datatype declaration. */ @@ -1100,37 +1101,8 @@ class CVC4_PUBLIC DatatypeDecl { friend class DatatypeConstructorArg; friend class Solver; - public: /** - * Constructor. - * @param name the name of the datatype - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - DatatypeDecl(const std::string& name, bool isCoDatatype = false); - - /** - * Constructor for parameterized datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param param the sort parameter - * @param isCoDatatype true if a codatatype is to be constructed - */ - DatatypeDecl(const std::string& name, Sort param, bool isCoDatatype = false); - - /** - * Constructor for parameterized datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param params a list of sort parameters - * @param isCoDatatype true if a codatatype is to be constructed - */ - DatatypeDecl(const std::string& name, - const std::vector<Sort>& params, - bool isCoDatatype = false); - - /** * Destructor. */ ~DatatypeDecl(); @@ -1157,6 +1129,42 @@ class CVC4_PUBLIC DatatypeDecl const CVC4::Datatype& getDatatype(void) const; private: + /** + * Constructor. + * @param s the solver that created this datatype declaration + * @param name the name of the datatype + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + DatatypeDecl(const Solver* s, + const std::string& name, + bool isCoDatatype = false); + + /** + * Constructor for parameterized datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param s the solver that created this datatype declaration + * @param name the name of the datatype + * @param param the sort parameter + * @param isCoDatatype true if a codatatype is to be constructed + */ + DatatypeDecl(const Solver* s, + const std::string& name, + Sort param, + bool isCoDatatype = false); + + /** + * Constructor for parameterized datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param s the solver that created this datatype declaration + * @param name the name of the datatype + * @param params a list of sort parameters + * @param isCoDatatype true if a codatatype is to be constructed + */ + DatatypeDecl(const Solver* s, + const std::string& name, + const std::vector<Sort>& params, + bool isCoDatatype = false); /* The internal (intermediate) datatype wrapped by this datatype * declaration * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -2293,6 +2301,43 @@ class CVC4_PUBLIC Solver Term mkVar(Sort sort, const std::string& symbol = std::string()) const; /* .................................................................... */ + /* Create datatype declarations */ + /* .................................................................... */ + + /** + * Create a datatype declaration. + * @param name the name of the datatype + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + DatatypeDecl mkDatatypeDecl(const std::string& name, + bool isCoDatatype = false); + + /** + * Create a datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param param the sort parameter + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + DatatypeDecl mkDatatypeDecl(const std::string& name, + Sort param, + bool isCoDatatype = false); + + /** + * Create a datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param params a list of sort parameters + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + DatatypeDecl mkDatatypeDecl(const std::string& name, + const std::vector<Sort>& params, + bool isCoDatatype = false); + + /* .................................................................... */ /* Formula Handling */ /* .................................................................... */ |