diff options
-rw-r--r-- | .travis.yml | 12 | ||||
-rw-r--r-- | test/java/BitVectors.java | 100 | ||||
-rw-r--r-- | test/java/BitVectorsAndArrays.java | 86 | ||||
-rw-r--r-- | test/java/Combination.java | 74 | ||||
-rw-r--r-- | test/java/HelloWorld.java | 27 | ||||
-rw-r--r-- | test/java/LinearArith.java | 73 | ||||
-rw-r--r-- | test/java/build.xml | 31 |
7 files changed, 401 insertions, 2 deletions
diff --git a/.travis.yml b/.travis.yml index 47fc617c2..65b9dcd25 100644 --- a/.travis.yml +++ b/.travis.yml @@ -17,8 +17,8 @@ env: - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ=" - TEST_GROUPS=2 matrix: - - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio' - - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=0 + - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio' + - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_JAVA_API_TEST=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=0 - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=1 - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof' - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes TRAVIS_CVC4_CONFIG='--enable-proof' @@ -37,6 +37,7 @@ addons: - openjdk-7-jdk - antlr3 - libantlr3c-dev + - ant-optional install: # Download and cache a copy of cxxtest until it appears officially in quantal. - wget http://sourceforge.net/projects/cxxtest/files/cxxtest/4.3/cxxtest-4.3.tar.gz @@ -73,6 +74,12 @@ script: make V=1 -j2 check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= || error "PORTFOLIO TEST FAILED"; } + JavaApiTest() { + pushd test/java + local status=${ant} + popd + return $status + } makeExamples() { make V=1 -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}"; } @@ -102,6 +109,7 @@ script: [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_DISTCHECK" ] && run makeDistcheck [ -n "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_CVC4_DISTCHECK" ] && run makeCheck && run makeExamples [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_CHECK_PORTFOLIO" ] && run makeCheckPortfolio + [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_CVC4_JAVA_API_TEST" ] && run JavaApiTest [ -n "$TRAVIS_LFSC" ] && run LFSCchecks [ -n "$TRAVIS_COVERITY" ] && echo "Running coverity. Skipping the normal build." [ -z "$TRAVIS_CVC4" ] && [ -z "$TRAVIS_LFSC" ] && [ -z "$TRAVIS_COVERITY" ] && error "Unknown Travis-CI configuration" 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 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project name="CVC4" default="test" basedir="."> + <property name="class-dir" value="classes" /> + <path id="classpath"> + <fileset dir="local-lib" includes="**/*.jar" /> + <fileset dir="../../builds" includes="**/*.jar" /> + </path> + + <path id="testpath"> + <path refid="classpath" /> + <pathelement location="${class-dir}" /> + </path> + + <dirset id="lib-dirs" dir="../.." includes="builds/**/*/src/bindings/java/.libs" /> + <pathconvert property="lib-path" refid="lib-dirs" /> + + <target name="compile"> + <mkdir dir="${class-dir}" /> + <javac srcdir="." destdir="${class-dir}" classpathref="classpath" includeantruntime="false" /> + </target> + + <target name="test" depends="compile"> + <junit printsummary="withOutAndErr" haltonfailure="yes" fork="yes"> + <jvmarg value='-Djava.library.path=${lib-path}'/> + <classpath refid="testpath" /> + <batchtest> + <fileset dir="${class-dir}" includes="**/*.class"/> + </batchtest> + </junit> + </target> +</project> |