** 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
**
** 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
**
+SUBDIRS = . java
+
AM_CPPFLAGS = \
-I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall
noinst_PROGRAMS = \
linear_arith \
helloworld \
- combination
+ combination \
+ bitvectors
noinst_DATA =
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)
/********************* */
-/*! \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
**
// 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;
** 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.
** 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
**
--- /dev/null
+/********************* */
+/*! \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_));
+ }
+}
--- /dev/null
+/********************* */
+/*! \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);
+ }
+}
--- /dev/null
+/********************* */
+/*! \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));
+ }
+}
--- /dev/null
+/********************* */
+/*! \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.");
+ }
+}
--- /dev/null
+topdir = ../../..
+srcdir = examples/api/java
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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 " $@;
** 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.
**/
** 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
**
** 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
**
** \verbatim
** Original author: mdeters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
** 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
**
projects / cvc5.git / commitdiff