From 96b4329d58e7d13982e9fdcf458ab98ad0b6c07a Mon Sep 17 00:00:00 2001 From: Pat Hawks Date: Thu, 24 Aug 2017 17:31:09 -0500 Subject: Test Java API on CI --- test/java/BitVectors.java | 100 +++++++++++++++++++++++++++++++++++++ test/java/BitVectorsAndArrays.java | 86 +++++++++++++++++++++++++++++++ test/java/Combination.java | 74 +++++++++++++++++++++++++++ test/java/HelloWorld.java | 27 ++++++++++ test/java/LinearArith.java | 73 +++++++++++++++++++++++++++ test/java/build.xml | 31 ++++++++++++ 6 files changed, 391 insertions(+) create mode 100644 test/java/BitVectors.java create mode 100644 test/java/BitVectorsAndArrays.java create mode 100644 test/java/Combination.java create mode 100644 test/java/HelloWorld.java create mode 100644 test/java/LinearArith.java create mode 100644 test/java/build.xml (limited to 'test') diff --git a/test/java/BitVectors.java b/test/java/BitVectors.java new file mode 100644 index 000000000..d5020ca69 --- /dev/null +++ b/test/java/BitVectors.java @@ -0,0 +1,100 @@ +import static org.junit.Assert.assertEquals; +import org.junit.Before; +import org.junit.Test; + +import edu.nyu.acsys.CVC4.*; + +public class BitVectors { + static { + System.loadLibrary("cvc4jni"); + } + ExprManager em; + SmtEngine smt; + + @Before + public void initialize() { + em = new ExprManager(); + smt = new SmtEngine(em); + } + + @Test + public void evaluatesExpression() { + Result.Validity expect, actual; + smt.setLogic("QF_BV"); // Set the logic + + // The following example has been adapted from the book A Hacker's Delight by + // Henry S. Warren. + // + // Given a variable x that can only have two values, a or b. We want to + // assign to x a value other than the current one. The straightforward code + // to do that is: + // + //(0) if (x == a ) x = b; + // else x = a; + // + // Two more efficient yet equivalent methods are: + // + //(1) x = a ⊕ b ⊕ x; + // + //(2) x = a + b - x; + // + // We will use CVC4 to prove that the three pieces of code above are all + // equivalent by encoding the problem in the bit-vector theory. + + // Creating a bit-vector type of width 32 + Type bitvector32 = em.mkBitVectorType(32); + + // Variables + Expr x = em.mkVar("x", bitvector32); + Expr a = em.mkVar("a", bitvector32); + Expr b = em.mkVar("b", bitvector32); + + // First encode the assumption that x must be equal to a or b + Expr x_eq_a = em.mkExpr(Kind.EQUAL, x, a); + Expr x_eq_b = em.mkExpr(Kind.EQUAL, x, b); + Expr assumption = em.mkExpr(Kind.OR, x_eq_a, x_eq_b); + + // Assert the assumption + smt.assertFormula(assumption); + + // Introduce a new variable for the new value of x after assignment. + Expr new_x = em.mkVar("new_x", bitvector32); // x after executing code (0) + Expr new_x_ = em.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) + + // Encoding code (0) + // new_x = x == a ? b : a; + Expr ite = em.mkExpr(Kind.ITE, x_eq_a, b, a); + Expr assignment0 = em.mkExpr(Kind.EQUAL, new_x, ite); + + // Assert the encoding of code (0) + smt.assertFormula(assignment0); + smt.push(); + + // Encoding code (1) + // new_x_ = a xor b xor x + Expr a_xor_b_xor_x = em.mkExpr(Kind.BITVECTOR_XOR, a, b, x); + Expr assignment1 = em.mkExpr(Kind.EQUAL, new_x_, a_xor_b_xor_x); + + // Assert encoding to CVC4 in current context; + 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(); + assertEquals(expect, actual); + smt.pop(); + + // Encoding code (2) + // new_x_ = a + b - x + Expr a_plus_b = em.mkExpr(Kind.BITVECTOR_PLUS, a, b); + Expr a_plus_b_minus_x = em.mkExpr(Kind.BITVECTOR_SUB, a_plus_b, x); + Expr assignment2 = em.mkExpr(Kind.EQUAL, new_x_, a_plus_b_minus_x); + + // Assert encoding to CVC4 in current context; + smt.assertFormula(assignment2); + + expect = Result.Validity.VALID; + actual = smt.query(new_x_eq_new_x_).isValid(); + assertEquals(expect, actual); + } +} diff --git a/test/java/BitVectorsAndArrays.java b/test/java/BitVectorsAndArrays.java new file mode 100644 index 000000000..b66d48b9d --- /dev/null +++ b/test/java/BitVectorsAndArrays.java @@ -0,0 +1,86 @@ +import static org.junit.Assert.assertEquals; +import org.junit.Before; +import org.junit.Test; + +import edu.nyu.acsys.CVC4.*; + +public class BitVectorsAndArrays { + static { + System.loadLibrary("cvc4jni"); + } + ExprManager em; + SmtEngine smt; + + @Before + public void initialize() { + em = new ExprManager(); + smt = new SmtEngine(em); + } + + @Test + public void evaluatesExpression() { + smt.setOption("produce-models", new SExpr(true)); // Produce Models + smt.setOption("output-language", new SExpr("smtlib")); // output-language + smt.setLogic("QF_AUFBV"); // Set the logic + + // Consider the following code (where size is some previously defined constant): + // + // Assert (current_array[0] > 0); + // for (unsigned i = 1; i < k; ++i) { + // current_array[i] = 2 * current_array[i - 1]; + // Assert (current_array[i-1] < current_array[i]); + // } + // + // We want to check whether the assertion in the body of the for loop holds + // throughout the loop. + + // Setting up the problem parameters + int k = 4; // number of unrollings (should be a power of 2) + int index_size = log2(k); // size of the index + + // Types + Type elementType = em.mkBitVectorType(32); + Type indexType = em.mkBitVectorType(index_size); + Type arrayType = em.mkArrayType(indexType, elementType); + + // Variables + Expr current_array = em.mkVar("current_array", arrayType); + + // Making a bit-vector constant + Expr zero = em.mkConst(new BitVector(index_size, 0)); + + // Asserting that current_array[0] > 0 + Expr current_array0 = em.mkExpr(Kind.SELECT, current_array, zero); + Expr current_array0_gt_0 = em.mkExpr(Kind.BITVECTOR_SGT, current_array0, em.mkConst(new BitVector(32, 0))); + smt.assertFormula(current_array0_gt_0); + + // Building the assertions in the loop unrolling + Expr index = em.mkConst(new BitVector(index_size, 0)); + Expr old_current = em.mkExpr(Kind.SELECT, current_array, index); + Expr two = em.mkConst(new BitVector(32, 2)); + + 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))); + 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); + // current[i-1] < current [i] + Expr current_slt_new_current = em.mkExpr(Kind.BITVECTOR_SLT, old_current, new_current); + assertions.add(current_slt_new_current); + + old_current = em.mkExpr(Kind.SELECT, current_array, index); + } + + Expr query = em.mkExpr(Kind.NOT, em.mkExpr(Kind.AND, assertions)); + smt.assertFormula(query); + + Result.Sat expect = Result.Sat.SAT; + Result.Sat actual = smt.checkSat(em.mkConst(true)).isSat(); + assertEquals(expect, actual); + } + + private static int log2(int n) { + return (int) Math.round(Math.log(n) / Math.log(2)); + } +} diff --git a/test/java/Combination.java b/test/java/Combination.java new file mode 100644 index 000000000..a30c46d09 --- /dev/null +++ b/test/java/Combination.java @@ -0,0 +1,74 @@ +import static org.junit.Assert.assertEquals; +import org.junit.Before; +import org.junit.Test; + +import edu.nyu.acsys.CVC4.*; + +public class Combination { + static { + System.loadLibrary("cvc4jni"); + } + ExprManager em; + SmtEngine smt; + + @Before + public void initialize() { + em = new ExprManager(); + smt = new SmtEngine(em); + } + + @Test + public void evaluatesExpression() { + smt.setOption("tlimit", new SExpr(100)); + smt.setOption("produce-models", new SExpr(true)); // Produce Models + smt.setOption("output-language", new SExpr("cvc4")); // output-language + smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output + smt.setLogic("QF_UFLIRA"); + + // Sorts + SortType u = em.mkSort("u"); + Type integer = em.integerType(); + Type booleanType = em.booleanType(); + Type uToInt = em.mkFunctionType(u, integer); + Type intPred = em.mkFunctionType(integer, booleanType); + + // Variables + Expr x = em.mkVar("x", u); + Expr y = em.mkVar("y", u); + + // Functions + Expr f = em.mkVar("f", uToInt); + Expr p = em.mkVar("p", intPred); + + // Constants + Expr zero = em.mkConst(new Rational(0)); + Expr one = em.mkConst(new Rational(1)); + + // Terms + Expr f_x = em.mkExpr(Kind.APPLY_UF, f, x); + Expr f_y = em.mkExpr(Kind.APPLY_UF, f, y); + Expr sum = em.mkExpr(Kind.PLUS, f_x, f_y); + Expr p_0 = em.mkExpr(Kind.APPLY_UF, p, zero); + Expr p_f_y = em.mkExpr(Kind.APPLY_UF, p, f_y); + + // Construct the assumptions + Expr assumptions = + em.mkExpr(Kind.AND, + em.mkExpr(Kind.LEQ, zero, f_x), // 0 <= f(x) + em.mkExpr(Kind.LEQ, zero, f_y), // 0 <= f(y) + em.mkExpr(Kind.LEQ, sum, one), // f(x) + f(y) <= 1 + p_0.notExpr(), // not p(0) + p_f_y); // p(f(y)) + smt.assertFormula(assumptions); + + assertEquals( + Result.Validity.VALID, + smt.query(em.mkExpr(Kind.DISTINCT, x, y)).isValid() + ); + + assertEquals( + Result.Sat.SAT, + smt.checkSat(em.mkConst(true)).isSat() + ); + } +} diff --git a/test/java/HelloWorld.java b/test/java/HelloWorld.java new file mode 100644 index 000000000..735f947e6 --- /dev/null +++ b/test/java/HelloWorld.java @@ -0,0 +1,27 @@ +import static org.junit.Assert.assertEquals; +import org.junit.Before; +import org.junit.Test; + +import edu.nyu.acsys.CVC4.*; + +public class HelloWorld { + static { + System.loadLibrary("cvc4jni"); + } + ExprManager em; + SmtEngine smt; + + @Before + public void initialize() { + em = new ExprManager(); + smt = new SmtEngine(em); + } + + @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(); + assertEquals(actual, expect); + } +} diff --git a/test/java/LinearArith.java b/test/java/LinearArith.java new file mode 100644 index 000000000..9e745b663 --- /dev/null +++ b/test/java/LinearArith.java @@ -0,0 +1,73 @@ +import static org.junit.Assert.assertEquals; +import org.junit.Before; +import org.junit.Test; + +import edu.nyu.acsys.CVC4.*; + +public class LinearArith { + static { + System.loadLibrary("cvc4jni"); + } + ExprManager em; + SmtEngine smt; + + @Before + public void initialize() { + em = new ExprManager(); + smt = new SmtEngine(em); + } + + @Test + public void evaluatesExpression() { + smt.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(); + + // Variables + Expr x = em.mkVar("x", integer); + Expr y = em.mkVar("y", real); + + // Constants + Expr three = em.mkConst(new Rational(3)); + Expr neg2 = em.mkConst(new Rational(-2)); + Expr two_thirds = em.mkConst(new Rational(2,3)); + + // Terms + Expr three_y = em.mkExpr(Kind.MULT, three, y); + Expr diff = em.mkExpr(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); + smt.assertFormula(assumptions); + 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() + ); + + smt.pop(); + + smt.push(); + Expr diff_is_two_thirds = em.mkExpr(Kind.EQUAL, diff, two_thirds); + smt.assertFormula(diff_is_two_thirds); + + assertEquals( + Result.Sat.SAT, + smt.checkSat(em.mkConst(true)).isSat() + ); + + smt.pop(); + } +} diff --git a/test/java/build.xml b/test/java/build.xml new file mode 100644 index 000000000..d8973cedc --- /dev/null +++ b/test/java/build.xml @@ -0,0 +1,31 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + -- cgit v1.2.3