diff options
author | Pat Hawks <pat@pathawks.com> | 2017-08-24 17:31:09 -0500 |
---|---|---|
committer | Pat Hawks <pat@pathawks.com> | 2017-08-24 17:32:56 -0500 |
commit | 96b4329d58e7d13982e9fdcf458ab98ad0b6c07a (patch) | |
tree | 5db222f7375dad008138069abf21b82c81fc07c6 /test/java/Combination.java | |
parent | 27f0116e05c7448c14ba2527d1269806d32dd923 (diff) |
Test Java API on CI
Diffstat (limited to 'test/java/Combination.java')
-rw-r--r-- | test/java/Combination.java | 74 |
1 files changed, 74 insertions, 0 deletions
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() + ); + } +} |