1 files changed, 40 insertions, 46 deletions

diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index 08f3792d6..0c728894a 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Morgan Deters, Tim King, Aina Niemetz
+ *   Aina Niemetz, Tim King, Mudathir Mohamed
  *
  * This file is part of the cvc5 project.
  *
@@ -11,71 +11,65 @@
  * ****************************************************************************
  *
  * A simple demonstration of the linear arithmetic solving capabilities and
- * the push pop of CVC4. This also gives an example option.
+ * the push pop of cvc5. This also gives an example option.
  */
 
-import edu.stanford.CVC4.*;
-
-public class LinearArith {
-  public static void main(String[] args) {
-    System.loadLibrary("cvc4jni");
-
-    ExprManager em = new ExprManager();
-    SmtEngine smt = new SmtEngine(em);
-
-    smt.setLogic("QF_LIRA"); // Set the logic
+import cvc5.*;
+public class LinearArith
+{
+  public static void main(String args[]) throws CVC5ApiException
+  {
+    Solver slv = new Solver();
+    slv.setLogic("QF_LIRA"); // Set the logic
 
     // Prove that if given x (Integer) and y (Real) then
     // the maximum value of y - x is 2/3
 
-    // Types
-    Type real = em.realType();
-    Type integer = em.integerType();
+    // Sorts
+    Sort real = slv.getRealSort();
+    Sort integer = slv.getIntegerSort();
 
     // Variables
-    Expr x = em.mkVar("x", integer);
-    Expr y = em.mkVar("y", real);
+    Term x = slv.mkConst(integer, "x");
+    Term y = slv.mkConst(real, "y");
 
     // Constants
-    Expr three = em.mkConst(new Rational(3));
-    Expr neg2 = em.mkConst(new Rational(-2));
-    Expr two_thirds = em.mkConst(new Rational(2,3));
+    Term three = slv.mkInteger(3);
+    Term neg2 = slv.mkInteger(-2);
+    Term two_thirds = slv.mkReal(2, 3);
 
     // Terms
-    Expr three_y = em.mkExpr(Kind.MULT, three, y);
-    Expr diff = em.mkExpr(Kind.MINUS, y, x);
+    Term three_y = slv.mkTerm(Kind.MULT, three, y);
+    Term diff = slv.mkTerm(Kind.MINUS, y, x);
 
     // Formulas
-    Expr x_geq_3y = em.mkExpr(Kind.GEQ, x, three_y);
-    Expr x_leq_y = em.mkExpr(Kind.LEQ, x, y);
-    Expr neg2_lt_x = em.mkExpr(Kind.LT, neg2, x);
-
-    Expr assumptions =
-      em.mkExpr(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x);
+    Term x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y);
+    Term x_leq_y = slv.mkTerm(Kind.LEQ, x, y);
+    Term neg2_lt_x = slv.mkTerm(Kind.LT, neg2, x);
 
-    System.out.println("Given the assumptions " + assumptions);
-    smt.assertFormula(assumptions);
+    Term assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x);
 
+    System.out.println("Given the assertions " + assertions);
+    slv.assertFormula(assertions);
 
-    smt.push();
-    Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds);
-    System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4.");
-    System.out.println("CVC4 should report ENTAILED.");
-    System.out.println(
-        "Result from CVC4 is: " + smt.checkEntailed(diff_leq_two_thirds));
-    smt.pop();
+    slv.push();
+    Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds);
+    System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5.");
+    System.out.println("cvc5 should report ENTAILED.");
+    System.out.println("Result from cvc5 is: " + slv.checkEntailed(diff_leq_two_thirds));
+    slv.pop();
 
     System.out.println();
 
-    smt.push();
-    Expr diff_is_two_thirds = em.mkExpr(Kind.EQUAL, diff, two_thirds);
-    smt.assertFormula(diff_is_two_thirds);
-    System.out.println("Show that the asserts are consistent with ");
-    System.out.println(diff_is_two_thirds + " with CVC4.");
-    System.out.println("CVC4 should report SAT.");
-    System.out.println("Result from CVC4 is: " + smt.checkSat(em.mkConst(true)));
-    smt.pop();
+    slv.push();
+    Term diff_is_two_thirds = slv.mkTerm(Kind.EQUAL, diff, two_thirds);
+    slv.assertFormula(diff_is_two_thirds);
+    System.out.println("Show that the assertions are consistent with ");
+    System.out.println(diff_is_two_thirds + " with cvc5.");
+    System.out.println("cvc5 should report SAT.");
+    System.out.println("Result from cvc5 is: " + slv.checkSat());
+    slv.pop();
 
     System.out.println("Thus the maximum value of (y - x) is 2/3.");
   }
-}
+}
\ No newline at end of file