From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 5 Jun 2020 00:27:33 +0000 (-0700)
Subject: Update Java tests to match changes in API (#4535)
X-Git-Tag: cvc5-1.0.0~3255
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=67678d6c8a28e71483d8171311725e9e1a86775c;p=cvc5.git

Update Java tests to match changes in API (#4535)

Commit cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 renamed
`Result::Validity` and `SmtEngine::query()` to `Result::Entailment` and
`SmtEngine::checkEntailed()`, respectively. The commit did not update
the Java tests which lead to issues in debug builds with Java bindings.
The commit also adds a corresponding `NEWS` entry.
---

diff --git a/NEWS b/NEWS
index b25f4517a..0a8ad8eaa 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,9 @@ Changes since 1.7
 =================
 
 Changes:
+* API change: `SmtEngine::query()` has been renamed to
+  `SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to
+  `Result::Entailment` along with corresponding changes to the enum values.
 * Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
   instead of `edu.nyu.acsys.CVC4`.
 
diff --git a/test/java/BitVectors.java b/test/java/BitVectors.java
index 1a750ff23..0d940dc69 100644
--- a/test/java/BitVectors.java
+++ b/test/java/BitVectors.java
@@ -16,11 +16,11 @@
  **/
 
 import static org.junit.Assert.assertEquals;
+
+import edu.stanford.CVC4.*;
 import org.junit.Before;
 import org.junit.Test;
 
-import edu.nyu.acsys.CVC4.*;
-
 public class BitVectors {
   static {
     System.loadLibrary("cvc4jni");
@@ -36,7 +36,7 @@ public class BitVectors {
 
   @Test
   public void evaluatesExpression() {
-    Result.Validity expect, actual;
+    Result.Entailment expect, actual;
     smt.setLogic("QF_BV"); // Set the logic
 
     // The following example has been adapted from the book A Hacker's Delight by
@@ -96,8 +96,8 @@ public class BitVectors {
     smt.assertFormula(assignment1);
     Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_);
 
-    expect = Result.Validity.VALID;
-    actual = smt.query(new_x_eq_new_x_).isValid();
+    expect = Result.Entailment.ENTAILED;
+    actual = smt.checkEntailed(new_x_eq_new_x_).isEntailed();
     assertEquals(expect, actual);
     smt.pop();
 
@@ -110,8 +110,8 @@ public class BitVectors {
     // Assert encoding to CVC4 in current context;
     smt.assertFormula(assignment2);
 
-    expect = Result.Validity.VALID;
-    actual = smt.query(new_x_eq_new_x_).isValid();
+    expect = Result.Entailment.ENTAILED;
+    actual = smt.checkEntailed(new_x_eq_new_x_).isEntailed();
     assertEquals(expect, actual);
   }
 }
diff --git a/test/java/BitVectorsAndArrays.java b/test/java/BitVectorsAndArrays.java
index de016a2cc..aed3c1007 100644
--- a/test/java/BitVectorsAndArrays.java
+++ b/test/java/BitVectorsAndArrays.java
@@ -16,11 +16,11 @@
  **/
 
 import static org.junit.Assert.assertEquals;
+
+import edu.stanford.CVC4.*;
 import org.junit.Before;
 import org.junit.Test;
 
-import edu.nyu.acsys.CVC4.*;
-
 public class BitVectorsAndArrays {
   static {
     System.loadLibrary("cvc4jni");
@@ -78,7 +78,8 @@ public class BitVectorsAndArrays {
 
     vectorExpr assertions = new vectorExpr();
     for (int i = 1; i < k; ++i) {
-      index = em.mkConst(new BitVector(index_size, new edu.nyu.acsys.CVC4.Integer(i)));
+      index = em.mkConst(
+          new BitVector(index_size, new edu.stanford.CVC4.Integer(i)));
       Expr new_current = em.mkExpr(Kind.BITVECTOR_MULT, two, old_current);
       // current[i] = 2 * current[i-1]
       current_array = em.mkExpr(Kind.STORE, current_array, index, new_current);
diff --git a/test/java/Combination.java b/test/java/Combination.java
index b710bf0d9..ead3fd617 100644
--- a/test/java/Combination.java
+++ b/test/java/Combination.java
@@ -16,11 +16,11 @@
  **/
 
 import static org.junit.Assert.assertEquals;
+
+import edu.stanford.CVC4.*;
 import org.junit.Before;
 import org.junit.Test;
 
-import edu.nyu.acsys.CVC4.*;
-
 public class Combination {
   static {
     System.loadLibrary("cvc4jni");
@@ -78,10 +78,8 @@ public class Combination {
                 p_f_y);                         // p(f(y))
     smt.assertFormula(assumptions);
 
-    assertEquals(
-        Result.Validity.VALID,
-        smt.query(em.mkExpr(Kind.DISTINCT, x, y)).isValid()
-    );
+    assertEquals(Result.Entailment.ENTAILED,
+        smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y)).isEntailed());
 
     assertEquals(
         Result.Sat.SAT,
diff --git a/test/java/HelloWorld.java b/test/java/HelloWorld.java
index f1e0768e2..ee2cb65a1 100644
--- a/test/java/HelloWorld.java
+++ b/test/java/HelloWorld.java
@@ -16,11 +16,11 @@
  **/
 
 import static org.junit.Assert.assertEquals;
+
+import edu.stanford.CVC4.*;
 import org.junit.Before;
 import org.junit.Test;
 
-import edu.nyu.acsys.CVC4.*;
-
 public class HelloWorld {
   static {
     System.loadLibrary("cvc4jni");
@@ -37,8 +37,8 @@ public class HelloWorld {
   @Test
   public void evaluatesExpression() {
     Expr helloworld = em.mkVar("Hello World!", em.booleanType());
-    Result.Validity expect = Result.Validity.INVALID;
-    Result.Validity actual = smt.query(helloworld).isValid();
+    Result.Entailment expect = Result.Entailment.NOT_ENTAILED;
+    Result.Entailment actual = smt.checkEntailed(helloworld).isEntailed();
     assertEquals(actual, expect);
   }
 }
diff --git a/test/java/LinearArith.java b/test/java/LinearArith.java
index 8f90b4a6d..5056b7fc6 100644
--- a/test/java/LinearArith.java
+++ b/test/java/LinearArith.java
@@ -16,11 +16,11 @@
  **/
 
 import static org.junit.Assert.assertEquals;
+
+import edu.stanford.CVC4.*;
 import org.junit.Before;
 import org.junit.Test;
 
-import edu.nyu.acsys.CVC4.*;
-
 public class LinearArith {
   static {
     System.loadLibrary("cvc4jni");
@@ -69,10 +69,8 @@ public class LinearArith {
     smt.push();
     Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds);
 
-    assertEquals(
-        Result.Validity.VALID,
-        smt.query(diff_leq_two_thirds).isValid()
-    );
+    assertEquals(Result.Entailment.ENTAILED,
+        smt.checkEntailed(diff_leq_two_thirds).isEntailed());
 
     smt.pop();