diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-11-24 09:53:29 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-24 17:53:29 +0000 |
commit | 9c672a9d1459fd8d9a5bd9b8b1a665620168a4e0 (patch) | |
tree | 3d2647237cd181c1797ff56c8dbc797a0cea9553 | |
parent | 01ff626de4261af83f69552eaba038399c428882 (diff) |
examples: Update Java datatypes example with recent extensions. (#7693)
The C++ datatypes example was extended in #7689. This updates the Java
API datatypes example accordingly.
-rw-r--r-- | examples/api/java/Datatypes.java | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index b29419165..77cfea040 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -66,7 +66,7 @@ public class Datatypes System.out.println(" + arg: " + j.next()); } } - System.out.println("\n"); + System.out.println(); // Alternatively, you can use for each loops. for (DatatypeConstructor c : consList) @@ -79,6 +79,19 @@ public class Datatypes } System.out.println(); + // You can also define a tester term for constructor 'cons': (_ is cons) + Term t_is_cons = + slv.mkTerm(Kind.APPLY_TESTER, consList.getConstructor("cons").getTesterTerm(), t); + System.out.println("t_is_cons is " + t_is_cons + "\n"); + slv.assertFormula(t_is_cons); + // Updating t at 'head' with value 1 is defined as follows: + Term t_updated = slv.mkTerm(Kind.APPLY_UPDATER, + consList.getConstructor("cons").getSelector("head").getUpdaterTerm(), + t, + slv.mkInteger(1)); + System.out.println("t_updated is " + t_updated + "\n"); + slv.assertFormula(slv.mkTerm(Kind.DISTINCT, t, t_updated)); + // You can also define parameterized datatypes. // This example builds a simple parameterized list of sort T, with one // constructor "cons". @@ -156,7 +169,7 @@ public class Datatypes System.out.println("\n" + ">>> Alternatively, use declareDatatype"); - System.out.println("\n"); + System.out.println(); DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons"); cons2.addSelector("head", slv.getIntegerSort()); |