Add ExprManager as argument to Datatype (#3535)

3 files changed, 8 insertions, 6 deletions

diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 9ff05ac0d..43f97796e 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -85,8 +85,9 @@ void test(Solver& slv, Sort& consListSort)
   // This example builds a simple parameterized list of sort T, with one
   // constructor "cons".
   Sort sort = slv.mkParamSort("T");
-  DatatypeDecl paramConsListSpec("paramlist",
-                                 sort);  // give the datatype a name
+  DatatypeDecl paramConsListSpec =
+      slv.mkDatatypeDecl("paramlist",
+                         sort);  // give the datatype a name
   DatatypeConstructorDecl paramCons("cons");
   DatatypeConstructorDecl paramNil("nil");
   DatatypeSelectorDecl paramHead("head", sort);
@@ -139,7 +140,8 @@ int main()
   // Second, it is "resolved" to an actual sort, at which point function
   // symbols are assigned to its constructors, selectors, and testers.
 
-  DatatypeDecl consListSpec("list");  // give the datatype a name
+  DatatypeDecl consListSpec =
+      slv.mkDatatypeDecl("list");  // give the datatype a name
   DatatypeConstructorDecl cons("cons");
   DatatypeSelectorDecl head("head", slv.getIntegerSort());
   DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index 34d440e3e..a749f0a0f 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -31,7 +31,7 @@ int main() {
   // is specified.  Second, it is "resolved"---at which point function
   // symbols are assigned to its constructors, selectors, and testers.
 
-  Datatype consListSpec("list"); // give the datatype a name
+  Datatype consListSpec(&em, "list");  // give the datatype a name
   DatatypeConstructor cons("cons");
   cons.addArg("head", em.integerType());
   cons.addArg("tail", DatatypeSelfType()); // a list
@@ -103,7 +103,7 @@ int main() {
   // This example builds a simple parameterized list of sort T, with one
   // constructor "cons".
   Type sort = em.mkSort("T", ExprManager::SORT_FLAG_PLACEHOLDER);
-  Datatype paramConsListSpec("list", std::vector<Type>{sort});
+  Datatype paramConsListSpec(&em, "list", std::vector<Type>{sort});
   DatatypeConstructor paramCons("cons");
   DatatypeConstructor paramNil("nil");
   paramCons.addArg("head", sort);
diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index 2c79bb75f..c5efe3d06 100644
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -31,7 +31,7 @@ public class Datatypes {
     // is specified.  Second, it is "resolved"---at which point function
     // symbols are assigned to its constructors, selectors, and testers.
 
-    Datatype consListSpec = new Datatype("list"); // give the datatype a name
+    Datatype consListSpec = new Datatype(em, "list"); // give a name
     DatatypeConstructor cons = new DatatypeConstructor("cons");
     cons.addArg("head", em.integerType());
     cons.addArg("tail", new DatatypeSelfType()); // a list