diff options
| -rw-r--r-- | NEWS | 3 | ||||
| -rw-r--r-- | test/java/BitVectors.java | 14 | ||||
| -rw-r--r-- | test/java/BitVectorsAndArrays.java | 7 | ||||
| -rw-r--r-- | test/java/Combination.java | 10 | ||||
| -rw-r--r-- | test/java/HelloWorld.java | 8 | ||||
| -rw-r--r-- | test/java/LinearArith.java | 10 |
6 files changed, 26 insertions, 26 deletions
@@ -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(); |