diff options
Diffstat (limited to 'examples/api/java')
-rw-r--r-- | examples/api/java/BitVectors.java | 108 | ||||
-rw-r--r-- | examples/api/java/Combination.java | 95 | ||||
-rw-r--r-- | examples/api/java/HelloWorld.java | 29 | ||||
-rw-r--r-- | examples/api/java/LinearArith.java | 81 | ||||
-rw-r--r-- | examples/api/java/Makefile | 4 | ||||
-rw-r--r-- | examples/api/java/Makefile.am | 29 |
6 files changed, 346 insertions, 0 deletions
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java new file mode 100644 index 000000000..ccaf3fbfa --- /dev/null +++ b/examples/api/java/BitVectors.java @@ -0,0 +1,108 @@ +/********************* */ +/*! \file BitVectors.java + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A simple demonstration of the solving capabilities of the CVC4 + ** bit-vector solver. + ** + **/ + +import edu.nyu.acsys.CVC4.*; + +public class BitVectors { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + smt.setOption("incremental", new SExpr(true)); // Enable incremental solving + + // 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) + System.out.println("Asserting " + assignment0 + " to CVC4 "); + smt.assertFormula(assignment0); + System.out.println("Pushing a new context."); + 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; + System.out.println("Asserting " + assignment1 + " to CVC4 "); + smt.assertFormula(assignment1); + Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_); + + System.out.println(" Querying: " + new_x_eq_new_x_); + System.out.println(" Expect valid. "); + System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_)); + System.out.println(" Popping context. "); + 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; + System.out.println("Asserting " + assignment2 + " to CVC4 "); + smt.assertFormula(assignment1); + + System.out.println(" Querying: " + new_x_eq_new_x_); + System.out.println(" Expect valid. "); + System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_)); + } +} diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java new file mode 100644 index 000000000..3f5826f12 --- /dev/null +++ b/examples/api/java/Combination.java @@ -0,0 +1,95 @@ +/********************* */ +/*! \file Combination.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A simple demonstration of the capabilities of CVC4 + ** + ** A simple demonstration of how to use uninterpreted functions, combining this + ** with arithmetic, and extracting a model at the end of a satisfiable query. + **/ + +import edu.nyu.acsys.CVC4.*; + +public class Combination { + private static void preFixPrintGetValue(SmtEngine smt, Expr e, int level) { + for(int i = 0; i < level; ++i) { System.out.print('-'); } + System.out.println("smt.getValue(" + e + ") -> " + smt.getValue(e)); + + if(e.hasOperator()) { + preFixPrintGetValue(smt, e.getOperator(), level + 1); + } + + for(int i = 0; i < e.getNumChildren(); ++i) { + Expr curr = e.getChild(i); + preFixPrintGetValue(smt, curr, level + 1); + } + } + + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + smt.setOption("tlimit", new SExpr(100)); + smt.setOption("produce-models", new SExpr(true)); // Produce Models + smt.setOption("incremental", new SExpr(true)); // Enable Multiple Queries + smt.setOption("output-language", new SExpr("smtlib")); // output-language + smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output + + // 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); + + 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); + + System.out.println("Given the following assumptions:"); + System.out.println(assumptions); + System.out.println("Prove x /= y is valid. " + + "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) + "."); + + + System.out.println("Now we call checksat on a trivial query to show that"); + System.out.println("the assumptions are satisfiable: " + + smt.checkSat(em.mkConst(true)) + "."); + + System.out.println("Finally, after a SAT call, we use smt.getValue(...) to generate a model."); + preFixPrintGetValue(smt, assumptions, 0); + } +} diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java new file mode 100644 index 000000000..33f6740c8 --- /dev/null +++ b/examples/api/java/HelloWorld.java @@ -0,0 +1,29 @@ +/********************* */ +/*! \file HelloWorld.java + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A very simple CVC4 example + ** + ** A very simple CVC4 tutorial example. + **/ + +import edu.nyu.acsys.CVC4.*; + +public class HelloWorld { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + Expr helloworld = em.mkVar("Hello World!", em.booleanType()); + SmtEngine smt = new SmtEngine(em); + + System.out.println(helloworld + " is " + smt.query(helloworld)); + } +} diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java new file mode 100644 index 000000000..44d042489 --- /dev/null +++ b/examples/api/java/LinearArith.java @@ -0,0 +1,81 @@ +/********************* */ +/*! \file LinearArith.java + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 + ** + ** A simple demonstration of the linear arithmetic solving capabilities and + ** the push pop of CVC4. This also gives an example option. + **/ + +import edu.nyu.acsys.CVC4.*; + +public class LinearArith { + public static void main(String[] args) { + System.loadLibrary("cvc4jni"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + smt.setOption("incremental", new SExpr(true)); // Enable incremental solving + + // 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); + + System.out.println("Given the assumptions " + assumptions); + smt.assertFormula(assumptions); + + + smt.push(); + Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds); + System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4."); + System.out.println("CVC4 should report VALID."); + System.out.println("Result from CVC4 is: " + smt.query(diff_leq_two_thirds)); + smt.pop(); + + System.out.println(); + + smt.push(); + Expr diff_is_two_thirds = em.mkExpr(Kind.EQUAL, diff, two_thirds); + smt.assertFormula(diff_is_two_thirds); + System.out.println("Show that the asserts are consistent with "); + System.out.println(diff_is_two_thirds + " with CVC4."); + System.out.println("CVC4 should report SAT."); + System.out.println("Result from CVC4 is: " + smt.checkSat(em.mkConst(true))); + smt.pop(); + + System.out.println("Thus the maximum value of (y - x) is 2/3."); + } +} diff --git a/examples/api/java/Makefile b/examples/api/java/Makefile new file mode 100644 index 000000000..10a950e1c --- /dev/null +++ b/examples/api/java/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = examples/api/java + +include $(topdir)/Makefile.subdir diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am new file mode 100644 index 000000000..ff3d36e14 --- /dev/null +++ b/examples/api/java/Makefile.am @@ -0,0 +1,29 @@ +noinst_DATA = + +if CVC4_LANGUAGE_BINDING_JAVA +noinst_DATA += \ + BitVectors.class \ + Combination.class \ + HelloWorld.class \ + LinearArith.class +endif + +%.class: %.java + $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../../../src/bindings/CVC4.jar" -d "@builddir@" $< + +EXTRA_DIST = \ + BitVectors.java \ + Combination.java \ + HelloWorld.java \ + LinearArith.java + +# for installation +examplesdir = $(docdir)/$(subdir) +examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST) + +MOSTLYCLEANFILES = $(noinst_DATA) + +# for silent automake rules +AM_V_JAVAC = $(am__v_JAVAC_$(V)) +am__v_JAVAC_ = $(am__v_JAVAC_$(AM_DEFAULT_VERBOSITY)) +am__v_JAVAC_0 = @echo " JAVAC " $@; |