From 45229fd903afa592deb0499027375bc1d5562cbc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 30 Nov 2012 23:07:19 +0000 Subject: all API examples now have java versions too; bitvectors gets built; also updated old-style copyrights in the examples --- examples/api/Makefile.am | 10 +++- examples/api/bitvectors.cpp | 8 ++- examples/api/combination.cpp | 6 +-- examples/api/helloworld.cpp | 4 +- examples/api/java/BitVectors.java | 108 +++++++++++++++++++++++++++++++++++++ examples/api/java/Combination.java | 95 ++++++++++++++++++++++++++++++++ examples/api/java/HelloWorld.java | 29 ++++++++++ examples/api/java/LinearArith.java | 81 ++++++++++++++++++++++++++++ examples/api/java/Makefile | 4 ++ examples/api/java/Makefile.am | 29 ++++++++++ examples/api/linear_arith.cpp | 6 +-- 11 files changed, 363 insertions(+), 17 deletions(-) create mode 100644 examples/api/java/BitVectors.java create mode 100644 examples/api/java/Combination.java create mode 100644 examples/api/java/HelloWorld.java create mode 100644 examples/api/java/LinearArith.java create mode 100644 examples/api/java/Makefile create mode 100644 examples/api/java/Makefile.am (limited to 'examples/api') diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am index 9e4e4470e..33775fd2a 100644 --- a/examples/api/Makefile.am +++ b/examples/api/Makefile.am @@ -1,3 +1,5 @@ +SUBDIRS = . java + AM_CPPFLAGS = \ -I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall @@ -6,7 +8,8 @@ AM_CFLAGS = -Wall noinst_PROGRAMS = \ linear_arith \ helloworld \ - combination + combination \ + bitvectors noinst_DATA = @@ -27,6 +30,11 @@ helloworld_SOURCES = \ helloworld_LDADD = \ @builddir@/../../src/libcvc4.la +bitvectors_SOURCES = \ + bitvectors.cpp +bitvectors_LDADD = \ + @builddir@/../../src/libcvc4.la + # for installation examplesdir = $(docdir)/$(subdir) examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST) diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 080ddf243..364fdb69e 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -1,13 +1,11 @@ /********************* */ -/*! \file bitvector.cpp +/*! \file bitvectors.cpp ** \verbatim ** Original author: lianah ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** 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 ** @@ -66,7 +64,7 @@ int main() { // 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 exectuing code (1) or (2) + Expr new_x_ = em.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) // Encoding code (0) // new_x = x == a ? b : a; diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index e0e5a6e13..f986eb8f9 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -5,13 +5,11 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** 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 + ** \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. diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 26b081a79..324883f46 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -5,9 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** 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 ** 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 " $@; diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index 38a78b5ef..c23595a30 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -5,15 +5,13 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** 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 + ** A simple demonstration of the linear arithmetic solving capabilities and ** the push pop of CVC4. This also gives an example option. **/ -- cgit v1.2.3