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 | |
parent | 499aa5641e2b830f60159c2ce1c791bf4d45aac1 (diff) |
Add ExprManager as argument to Datatype (#3535)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 44 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 103 |
2 files changed, 110 insertions, 37 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 7a3577e0d..f7ffe850a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1680,20 +1680,26 @@ std::ostream& operator<<(std::ostream& out, /* DatatypeDecl ------------------------------------------------------------- */ -DatatypeDecl::DatatypeDecl(const std::string& name, bool isCoDatatype) - : d_dtype(new CVC4::Datatype(name, isCoDatatype)) +DatatypeDecl::DatatypeDecl(const Solver* s, + const std::string& name, + bool isCoDatatype) + : d_dtype(new CVC4::Datatype(s->getExprManager(), name, isCoDatatype)) { } -DatatypeDecl::DatatypeDecl(const std::string& name, +DatatypeDecl::DatatypeDecl(const Solver* s, + const std::string& name, Sort param, bool isCoDatatype) - : d_dtype(new CVC4::Datatype( - name, std::vector<Type>{*param.d_type}, isCoDatatype)) + : d_dtype(new CVC4::Datatype(s->getExprManager(), + name, + std::vector<Type>{*param.d_type}, + isCoDatatype)) { } -DatatypeDecl::DatatypeDecl(const std::string& name, +DatatypeDecl::DatatypeDecl(const Solver* s, + const std::string& name, const std::vector<Sort>& params, bool isCoDatatype) { @@ -1703,7 +1709,7 @@ DatatypeDecl::DatatypeDecl(const std::string& name, tparams.push_back(*s.d_type); } d_dtype = std::shared_ptr<CVC4::Datatype>( - new CVC4::Datatype(name, tparams, isCoDatatype)); + new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype)); } DatatypeDecl::~DatatypeDecl() {} @@ -2867,6 +2873,28 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const CVC4_API_SOLVER_TRY_CATCH_END; } +/* Create datatype declarations */ +/* -------------------------------------------------------------------------- */ + +DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) +{ + return DatatypeDecl(this, name, isCoDatatype); +} + +DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, + Sort param, + bool isCoDatatype) +{ + return DatatypeDecl(this, name, param, isCoDatatype); +} + +DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, + const std::vector<Sort>& params, + bool isCoDatatype) +{ + return DatatypeDecl(this, name, params, isCoDatatype); +} + /* Create terms */ /* -------------------------------------------------------------------------- */ @@ -3409,7 +3437,7 @@ Sort Solver::declareDatatype( { CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors) << "a datatype declaration with at least one constructor"; - DatatypeDecl dtdecl(symbol); + DatatypeDecl dtdecl(this, symbol); for (const DatatypeConstructorDecl& ctor : ctors) { dtdecl.addConstructor(ctor); 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 */ /* .................................................................... */ |