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 b25f4517ad15b9eb2991c37d556a2ddc44b2e2a7..0a8ad8eaa288cf39053c3a8daf2c084c5e96b295 100644 (file)
--- 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 1a750ff231674a1f68f7088b05b367e55095517c..0d940dc69c879f4eb620b7cbc8d7bd9ec1609649 100644 (file)
--- 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 de016a2cc63ac8e3c1d5afbfdc1733cb417034c6..aed3c100736f9c21f68b541704f65720a576f176 100644 (file)
--- 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 b710bf0d95daa8b08c30b9ce6fd5931eb0f41e68..ead3fd617baab56cbd09705ca7b51ec6c27bb680 100644 (file)
--- 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 f1e0768e2f9b30e8e26ed7c857c757c59d85d113..ee2cb65a12658eae73de718178cb54f4f4617cd3 100644 (file)
--- 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 8f90b4a6d06a318cb55fd9373bd243380e7c3eb4..5056b7fc68ea33bae242da58eaa7d2ea09b8a687 100644 (file)
--- 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();