all API examples now have java versions too; bitvectors gets built; also updated old-style copyrights in the examples

16 files changed, 369 insertions, 33 deletions

diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 4f4d19f24..fcf1485af 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -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/SimpleVCCompat.java b/examples/SimpleVCCompat.java
index 65bc62f78..78ad8ae78 100644
--- a/examples/SimpleVCCompat.java
+++ b/examples/SimpleVCCompat.java
@@ -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/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.
  **/
 
diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c
index 28ec06054..0980e8dfa 100644
--- a/examples/simple_vc_compat_c.c
+++ b/examples/simple_vc_compat_c.c
@@ -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/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp
index 0cb99f4be..f0b378b21 100644
--- a/examples/simple_vc_compat_cxx.cpp
+++ b/examples/simple_vc_compat_cxx.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/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 56c5763a2..f016c5306 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -3,11 +3,9 @@
  ** \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
  **