From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 24 Nov 2021 17:53:29 +0000 (-0800)
Subject: examples: Update Java datatypes example with recent extensions. (#7693)
X-Git-Tag: cvc5-1.0.0~773
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c672a9d1459fd8d9a5bd9b8b1a665620168a4e0;p=cvc5.git

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

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());