Fix compile errors with java examples (#7646)

Fix compile errors with java examples

7 files changed, 104 insertions, 112 deletions

diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 0ae1b4a51..de00781d6 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -14,48 +14,45 @@
  *
  * To run the resulting class file, you need to do something like the
  * following:
- *
+ *   javac  "-cp" "../build/src/api/java/cvc5.jar" SimpleVC.java
  *   java \
- *     -cp path/to/CVC4.jar:SimpleVC.jar \
- *     -Djava.library.path=/dir/containing/libcvc4jni.so \
+ *     "-Djava.library.path=../build/src/api/java" "-cp" "../build/src/api/java/cvc5.jar:." \
  *     SimpleVC
- *
  */
 
-import edu.stanford.CVC4.*;
+import static io.github.cvc5.api.Kind.*;
 
-public class SimpleVC {
-  public static void main(String[] args) {
-    System.loadLibrary("cvc4jni");
+import io.github.cvc5.api.*;
 
-    ExprManager em = new ExprManager();
-    SmtEngine smt = new SmtEngine(em);
+public class SimpleVC
+{
+  public static void main(String[] args)
+  {
+    Solver slv = new Solver();
 
     // Prove that for integers x and y:
     //   x > 0 AND y > 0  =>  2x + y >= 3
 
-    Type integer = em.integerType();
+    Sort integer = slv.getIntegerSort();
 
-    Expr x = em.mkVar("x", integer);
-    Expr y = em.mkVar("y", integer);
-    Expr zero = em.mkConst(new Rational(0));
+    Term x = slv.mkConst(integer, "x");
+    Term y = slv.mkConst(integer, "y");
+    Term zero = slv.mkInteger(0);
 
-    Expr x_positive = em.mkExpr(Kind.GT, x, zero);
-    Expr y_positive = em.mkExpr(Kind.GT, y, zero);
+    Term x_positive = slv.mkTerm(Kind.GT, x, zero);
+    Term y_positive = slv.mkTerm(Kind.GT, y, zero);
 
-    Expr two = em.mkConst(new Rational(2));
-    Expr twox = em.mkExpr(Kind.MULT, two, x);
-    Expr twox_plus_y = em.mkExpr(Kind.PLUS, twox, y);
+    Term two = slv.mkInteger(2);
+    Term twox = slv.mkTerm(Kind.MULT, two, x);
+    Term twox_plus_y = slv.mkTerm(Kind.PLUS, twox, y);
 
-    Expr three = em.mkConst(new Rational(3));
-    Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
+    Term three = slv.mkInteger(3);
+    Term twox_plus_y_geq_3 = slv.mkTerm(Kind.GEQ, twox_plus_y, three);
 
-    Expr formula =
-        em.mkExpr(Kind.AND, x_positive, y_positive).impExpr(twox_plus_y_geq_3);
+    Term formula = slv.mkTerm(Kind.AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3);
 
-    System.out.println(
-        "Checking entailment of formula " + formula + " with CVC4.");
-    System.out.println("CVC4 should report ENTAILED.");
-    System.out.println("Result from CVC4 is: " + smt.checkEntailed(formula));
+    System.out.println("Checking entailment of formula " + formula + " with cvc5.");
+    System.out.println("cvc5 should report ENTAILED.");
+    System.out.println("Result from cvc5 is: " + slv.checkEntailed(formula));
   }
 }
diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java
index bc142571d..0ac1f628c 100644
--- a/examples/api/java/Exceptions.java
+++ b/examples/api/java/Exceptions.java
@@ -10,9 +10,9 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Catching CVC4 exceptions via the Java API.
+ * Catching cvc5 exceptions via the Java API.
  *
- * A simple demonstration of catching CVC4 execptions via the Java API.
+ * A simple demonstration of catching cvc5 execptions via the Java API.
  */
 
 import io.github.cvc5.api.*;
diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index fb082fc11..a3e2b2a7e 100644
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple demonstration of reasoning about relations with CVC4 via Java API.
+ * A simple demonstration of reasoning about relations with cvc5 via Java API.
  */
 
 import static io.github.cvc5.api.Kind.*;
@@ -20,47 +20,42 @@ import io.github.cvc5.api.*;
 /*
 This file uses the API to make a sat call equivalent to the following benchmark:
 (set-logic ALL)
+
 (set-option :finite-model-find true)
 (set-option :produce-models true)
 (set-option :sets-ext true)
-(set-option :output-language "smt2")
+
 (declare-sort Person 0)
+
 (declare-fun people () (Set (Tuple Person)))
 (declare-fun males () (Set (Tuple Person)))
-(declare-fun females() (Set (Tuple Person)))
+(declare-fun females () (Set (Tuple Person)))
 (declare-fun father () (Set (Tuple Person Person)))
 (declare-fun mother () (Set (Tuple Person Person)))
 (declare-fun parent () (Set (Tuple Person Person)))
 (declare-fun ancestor () (Set (Tuple Person Person)))
 (declare-fun descendant () (Set (Tuple Person Person)))
 
-(assert (= people (as univset (Set (Tuple Person)))))
-(assert (not (= males (as emptyset (Set (Tuple Person))))))
-(assert (not (= females (as emptyset (Set (Tuple Person))))))
-(assert (= (intersection males females) (as emptyset (Set (Tuple Person)))))
-
+(assert (= people (as set.universe (Set (Tuple Person)))))
+(assert (not (= males (as set.empty (Set (Tuple Person))))))
+(assert (not (= females (as set.empty (Set (Tuple Person))))))
+(assert (= (set.inter males females) (as set.empty (Set (Tuple Person)))))
 ; father relation is not empty
-(assert (not (= father (as emptyset (Set (Tuple Person Person))))))
+(assert (not (= father (as set.empty (Set (Tuple Person Person))))))
 ; mother relation is not empty
-(assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
-
+(assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
 ; fathers are males
-(assert (subset (join father people) males))
+(assert (set.subset (rel.join father people) males))
 ; mothers are females
-(assert (subset (join mother people) females))
-
+(assert (set.subset (rel.join mother people) females))
 ; parent
-(assert (= parent (union father mother)))
-
+(assert (= parent (set.union father mother)))
 ; no self ancestor
-(assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
-
+(assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
 ; descendant
-(assert (= descendant (tclosure parent)))
-
+(assert (= descendant (rel.tclosure parent)))
 ; ancestor
-(assert (= ancestor (transpose descendant)))
-
+(assert (= ancestor (rel.transpose descendant)))
 (check-sat)
 (get-model)
  */
@@ -115,53 +110,53 @@ public class Relations
       Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
       Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
 
-      // (assert (= people (as univset (Set (Tuple Person)))))
+      // (assert (= people (as set.universe (Set (Tuple Person)))))
       Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
-      // (assert (not (= males (as emptyset (Set (Tuple Person))))))
+      // (assert (not (= males (as set.empty (Set (Tuple Person))))))
       Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
-      // (assert (not (= females (as emptyset (Set (Tuple Person))))))
+      // (assert (not (= females (as set.empty (Set (Tuple Person))))))
       Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
 
-      // (assert (= (intersection males females) (as emptyset (Set (Tuple
+      // (assert (= (set.inter males females) (as set.empty (Set (Tuple
       // Person)))))
-      Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females);
+      Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
       Term malesAndFemalesAreDisjoint =
           solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
 
-      // (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
-      // (assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
+      // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
+      // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
       Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
       Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
       Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);
       Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4);
 
       // fathers are males
-      // (assert (subset (join father people) males))
-      Term fathers = solver.mkTerm(JOIN, father, people);
-      Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males);
+      // (assert (set.subset (rel.join father people) males))
+      Term fathers = solver.mkTerm(RELATION_JOIN, father, people);
+      Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males);
 
       // mothers are females
-      // (assert (subset (join mother people) females))
-      Term mothers = solver.mkTerm(JOIN, mother, people);
-      Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females);
+      // (assert (set.subset (rel.join mother people) females))
+      Term mothers = solver.mkTerm(RELATION_JOIN, mother, people);
+      Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females);
 
-      // (assert (= parent (union father mother)))
-      Term unionFatherMother = solver.mkTerm(UNION, father, mother);
+      // (assert (= parent (set.union father mother)))
+      Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother);
       Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
 
-      // (assert (= parent (union father mother)))
-      Term transitiveClosure = solver.mkTerm(TCLOSURE, parent);
+      // (assert (= descendant (rel.tclosure parent)))
+      Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent);
       Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure);
 
-      // (assert (= parent (union father mother)))
-      Term transpose = solver.mkTerm(TRANSPOSE, descendant);
+      // (assert (= ancestor (rel.transpose descendant)))
+      Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant);
       Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);
 
-      // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
+      // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor))))
       Term x = solver.mkVar(personSort, "x");
       DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
       Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x);
-      Term member = solver.mkTerm(MEMBER, xxTuple, ancestor);
+      Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
       Term notMember = solver.mkTerm(NOT, member);
 
       Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, x);
diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java
index 3edc49ae6..7eaa3a256 100644
--- a/examples/api/java/Sets.java
+++ b/examples/api/java/Sets.java
@@ -41,24 +41,24 @@ public class Sets
         Term B = slv.mkConst(set, "B");
         Term C = slv.mkConst(set, "C");
 
-        Term unionAB = slv.mkTerm(UNION, A, B);
-        Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
+        Term unionAB = slv.mkTerm(SET_UNION, A, B);
+        Term lhs = slv.mkTerm(SET_INTER, unionAB, C);
 
-        Term intersectionAC = slv.mkTerm(INTERSECTION, A, C);
-        Term intersectionBC = slv.mkTerm(INTERSECTION, B, C);
-        Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC);
+        Term intersectionAC = slv.mkTerm(SET_INTER, A, C);
+        Term intersectionBC = slv.mkTerm(SET_INTER, B, C);
+        Term rhs = slv.mkTerm(SET_UNION, intersectionAC, intersectionBC);
 
         Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
 
         System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + ".");
       }
 
-      // Verify emptset is a subset of any set
+      // Verify set.empty is a subset of any set
       {
         Term A = slv.mkConst(set, "A");
         Term emptyset = slv.mkEmptySet(set);
 
-        Term theorem = slv.mkTerm(SUBSET, emptyset, A);
+        Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A);
 
         System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + ".");
       }
@@ -69,16 +69,16 @@ public class Sets
         Term two = slv.mkInteger(2);
         Term three = slv.mkInteger(3);
 
-        Term singleton_one = slv.mkTerm(SINGLETON, one);
-        Term singleton_two = slv.mkTerm(SINGLETON, two);
-        Term singleton_three = slv.mkTerm(SINGLETON, three);
-        Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
-        Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
-        Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
+        Term singleton_one = slv.mkTerm(SET_SINGLETON, one);
+        Term singleton_two = slv.mkTerm(SET_SINGLETON, two);
+        Term singleton_three = slv.mkTerm(SET_SINGLETON, three);
+        Term one_two = slv.mkTerm(SET_UNION, singleton_one, singleton_two);
+        Term two_three = slv.mkTerm(SET_UNION, singleton_two, singleton_three);
+        Term intersection = slv.mkTerm(SET_INTER, one_two, two_three);
 
         Term x = slv.mkConst(integer, "x");
 
-        Term e = slv.mkTerm(MEMBER, x, intersection);
+        Term e = slv.mkTerm(SET_MEMBER, x, intersection);
 
         Result result = slv.checkSatAssuming(e);
         System.out.println("cvc5 reports: " + e + " is " + result + ".");
diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java
index 7db7cc4f3..635be65f6 100644
--- a/examples/api/java/Statistics.java
+++ b/examples/api/java/Statistics.java
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * An example of accessing CVC4's statistics using the Java API.
+ * An example of accessing cvc5's statistics using the Java API.
  */
 
 import static io.github.cvc5.api.Kind.*;
@@ -158,52 +158,52 @@ public class Statistics
     Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
     Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
 
-    // (assert (= people (as univset (Set (Tuple Person)))))
+    // (assert (= people (as set.universe (Set (Tuple Person)))))
     Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
-    // (assert (not (= males (as emptyset (Set (Tuple Person))))))
+    // (assert (not (= males (as set.empty (Set (Tuple Person))))))
     Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
-    // (assert (not (= females (as emptyset (Set (Tuple Person))))))
+    // (assert (not (= females (as set.empty (Set (Tuple Person))))))
     Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
 
-    // (assert (= (intersection males females) (as emptyset (Set (Tuple
+    // (assert (= (set.inter males females) (as set.empty (Set (Tuple
     // Person)))))
-    Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females);
+    Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
     Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
 
-    // (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
-    // (assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
+    // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
+    // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
     Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
     Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
     Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);
     Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4);
 
     // fathers are males
-    // (assert (subset (join father people) males))
-    Term fathers = solver.mkTerm(JOIN, father, people);
-    Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males);
+    // (assert (set.subset (rel.join father people) males))
+    Term fathers = solver.mkTerm(RELATION_JOIN, father, people);
+    Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males);
 
     // mothers are females
-    // (assert (subset (join mother people) females))
-    Term mothers = solver.mkTerm(JOIN, mother, people);
-    Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females);
+    // (assert (set.subset (rel.join mother people) females))
+    Term mothers = solver.mkTerm(RELATION_JOIN, mother, people);
+    Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females);
 
-    // (assert (= parent (union father mother)))
-    Term unionFatherMother = solver.mkTerm(UNION, father, mother);
+    // (assert (= parent (set.union father mother)))
+    Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother);
     Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
 
-    // (assert (= parent (union father mother)))
-    Term transitiveClosure = solver.mkTerm(TCLOSURE, parent);
+    // (assert (= descendant (rel.tclosure parent)))
+    Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent);
     Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure);
 
-    // (assert (= parent (union father mother)))
-    Term transpose = solver.mkTerm(TRANSPOSE, descendant);
+    // (assert (= ancestor (rel.transpose descendant)))
+    Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant);
     Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);
 
-    // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
+    // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor))))
     Term var = solver.mkVar(personSort, "x");
     DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
     Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), var, var);
-    Term member = solver.mkTerm(MEMBER, xxTuple, ancestor);
+    Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
     Term notMember = solver.mkTerm(NOT, member);
 
     Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, var);
diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java
index feec35dbd..b91a94ab7 100644
--- a/examples/api/java/UnsatCores.java
+++ b/examples/api/java/UnsatCores.java
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * An example of interacting with unsat cores using CVC4's Java API.
+ * An example of interacting with unsat cores using cvc5's Java API.
  */
 
 import io.github.cvc5.api.*;
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 026665561..1c0663a00 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -47,10 +47,10 @@ int main() {
   Term formula =
       slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3);
 
-  std::cout << "Checking entailment of formula " << formula << " with CVC4."
+  std::cout << "Checking entailment of formula " << formula << " with cvc5."
             << std::endl;
-  std::cout << "CVC4 should report ENTAILED." << std::endl;
-  std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula)
+  std::cout << "cvc5 should report ENTAILED." << std::endl;
+  std::cout << "Result from cvc5 is: " << slv.checkEntailed(formula)
             << std::endl;
 
   return 0;