Add ExprManager as argument to Datatype (#3535)

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                                                     */
   /* .................................................................... */