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 /examples | |
parent | 499aa5641e2b830f60159c2ce1c791bf4d45aac1 (diff) |
Add ExprManager as argument to Datatype (#3535)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/datatypes-new.cpp | 8 | ||||
-rw-r--r-- | examples/api/datatypes.cpp | 4 | ||||
-rw-r--r-- | examples/api/java/Datatypes.java | 2 |
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 |