api: Rename get(Selector|Constructor)Term() to getTerm(). (#8537)

[cvc5.git] / examples / api / java / Datatypes.java

diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index 0f70ce0dcf6bdea0dd1855bec7ba82af3e934f36..03c80c0a0818a01da2e5b1251cb27d7911774629 100644 (file)
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -35,22 +35,21 @@ public class Datatypes
     // "nil" is a constructor too, so it needs to be applied with
     // APPLY_CONSTRUCTOR, even though it has no arguments.
     Term t = slv.mkTerm(Kind.APPLY_CONSTRUCTOR,
-        consList.getConstructor("cons").getConstructorTerm(),
+        consList.getConstructor("cons").getTerm(),
         slv.mkInteger(0),
-        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm()));
+        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm()));
 
     System.out.println("t is " + t + "\n"
-        + "sort of cons is " + consList.getConstructor("cons").getConstructorTerm().getSort() + "\n"
-        + "sort of nil is " + consList.getConstructor("nil").getConstructorTerm().getSort());
+        + "sort of cons is " + consList.getConstructor("cons").getTerm().getSort() + "\n"
+        + "sort of nil is " + consList.getConstructor("nil").getTerm().getSort());
 
     // t2 = head(cons 0 nil), and of course this can be evaluated
     //
     // Here we first get the DatatypeConstructor for cons (with
     // consList["cons"]) in order to get the "head" selector symbol
     // to apply.
-    Term t2 = slv.mkTerm(Kind.APPLY_SELECTOR,
-        consList.getConstructor("cons").getSelector("head").getSelectorTerm(),
-        t);
+    Term t2 = slv.mkTerm(
+        Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getTerm(), t);
 
     System.out.println("t2 is " + t2 + "\n"
         + "simplify(t2) is " + slv.simplify(t2) + "\n");
@@ -124,12 +123,10 @@ public class Datatypes
     Term a = slv.mkConst(paramConsIntListSort, "a");
     System.out.println("term " + a + " is of sort " + a.getSort());
 
-    Term head_a = slv.mkTerm(Kind.APPLY_SELECTOR,
-        paramConsList.getConstructor("cons").getSelector("head").getSelectorTerm(),
-        a);
+    Term head_a = slv.mkTerm(
+        Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelector("head").getTerm(), a);
     System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n"
-        + "sort of cons is " + paramConsList.getConstructor("cons").getConstructorTerm().getSort()
-        + "\n");
+        + "sort of cons is " + paramConsList.getConstructor("cons").getTerm().getSort() + "\n");
     Term assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50));
     System.out.println("Assert " + assertion);
     slv.assertFormula(assertion);