From 9c672a9d1459fd8d9a5bd9b8b1a665620168a4e0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 24 Nov 2021 09:53:29 -0800 Subject: [PATCH] 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. --- examples/api/java/Datatypes.java | 17 +++++++++++++++-- 1 file 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()); -- 2.30.2