Test Java API on CI

6 files changed, 391 insertions, 0 deletions

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>