updated examples

7 files changed, 170 insertions, 66 deletions

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index 4701bf8e3..a0c43142d 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -10,7 +10,7 @@
  ** information.\endverbatim
  **
  ** \brief A simple demonstration of the solving capabilities of the CVC4
- ** bit-vector solver. 
+ ** bit-vector solver.
  **
  **/
 
@@ -27,7 +27,7 @@ int main() {
   SmtEngine smt(&em);
   smt.setOption("incremental", true); // Enable incremental solving
   smt.setLogic("QF_BV");              // Set the logic
-  
+
   // The following example has been adapted from the book A Hacker's Delight by
   // Henry S. Warren.
   //
@@ -39,14 +39,14 @@ int main() {
   //    else x = a;
   //
   // Two more efficient yet equivalent methods are:
-  // 
-  //(1) x = a ⊕ b ⊕ x; 
+  //
+  //(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. 
-  
+  // equivalent by encoding the problem in the bit-vector theory.
+
   // Creating a bit-vector type of width 32
   Type bitvector32 = em.mkBitVectorType(32);
 
@@ -56,57 +56,57 @@ int main() {
   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_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); 
+  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) 
+  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); 
+  // 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)
-  cout << "Asserting " << assignment0 << " to CVC4 " << endl; 
+  cout << "Asserting " << assignment0 << " to CVC4 " << endl;
   smt.assertFormula(assignment0);
   cout << "Pushing a new context." << endl;
   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 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; 
-  cout << "Asserting " << assignment1 << " to CVC4 " << endl; 
+  // Assert encoding to CVC4 in current context;
+  cout << "Asserting " << assignment1 << " to CVC4 " << endl;
   smt.assertFormula(assignment1);
   Expr new_x_eq_new_x_ = em.mkExpr(kind::EQUAL, new_x, new_x_);
 
   cout << " Querying: " << new_x_eq_new_x_ << endl;
-  cout << " Expect valid. " << endl; 
-  cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; 
+  cout << " Expect valid. " << endl;
+  cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
   cout << " Popping context. " << endl;
   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 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; 
-  cout << "Asserting " << assignment2 << " to CVC4 " << endl; 
+
+  // Assert encoding to CVC4 in current context;
+  cout << "Asserting " << assignment2 << " to CVC4 " << endl;
   smt.assertFormula(assignment1);
 
   cout << " Querying: " << new_x_eq_new_x_ << endl;
-  cout << " Expect valid. " << endl; 
-  cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; 
-  
+  cout << " Expect valid. " << endl;
+  cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
+
   return 0;
 }
diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp
index cda5e9274..8363da46c 100644
--- a/examples/api/bitvectors_and_arrays.cpp
+++ b/examples/api/bitvectors_and_arrays.cpp
@@ -1,18 +1,16 @@
 /*********************                                                        */
-/*! \file bitvector.cpp
+/*! \file bitvectors_and_arrays.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
  **
  ** \brief A simple demonstration of the solving capabilities of the CVC4
- ** bit-vector and array solvers. 
+ ** bit-vector and array solvers.
  **
  **/
 
@@ -34,23 +32,23 @@ int main() {
   // Consider the following code (where size is some previously defined constant):
   //
   //
-  //   Assert (current_array[0] > 0); 
+  //   Assert (current_array[0] > 0);
   //   for (unsigned i = 1; i < k; ++i) {
   //     current_array[i] = 2 * current_array[i - 1];
-  //     Assert (current_array[i-1] < current_array[i]); 
+  //     Assert (current_array[i-1] < current_array[i]);
   //     }
   //
   // We want to check whether the assertion in the body of the for loop holds
-  // throughout the loop. 
-  
+  // throughout the loop.
+
   // Setting up the problem parameters
   unsigned k = 4;                // number of unrollings (should be a power of 2)
-  unsigned index_size = log2(k); // size of the index 
-    
+  unsigned index_size = log2(k); // size of the index
+
 
   // Types
   Type elementType = em.mkBitVectorType(32);
-  Type indexType = em.mkBitVectorType(index_size); 
+  Type indexType = em.mkBitVectorType(index_size);
   Type arrayType = em.mkArrayType(indexType, elementType);
 
   // Variables
@@ -60,38 +58,38 @@ int main() {
   Expr zero = em.mkConst(BitVector(index_size, 0u));
 
   // Asserting that current_array[0] > 0
-  Expr current_array0 = em.mkExpr(kind::SELECT, current_array, zero); 
+  Expr current_array0 = em.mkExpr(kind::SELECT, current_array, zero);
   Expr current_array0_gt_0 = em.mkExpr(kind::BITVECTOR_SGT, current_array0, em.mkConst(BitVector(32, 0u)));
   smt.assertFormula(current_array0_gt_0);
 
-  // Building the assertions in the loop unrolling 
-  Expr index = em.mkConst(BitVector(index_size, 0u)); 
+  // Building the assertions in the loop unrolling
+  Expr index = em.mkConst(BitVector(index_size, 0u));
   Expr old_current = em.mkExpr(kind::SELECT, current_array, index);
-  Expr two = em.mkConst(BitVector(32, 2u)); 
-  
-  std::vector<Expr> assertions; 
+  Expr two = em.mkConst(BitVector(32, 2u));
+
+  std::vector<Expr> assertions;
   for (unsigned i = 1; i < k; ++i) {
     index = em.mkConst(BitVector(index_size, Integer(i)));
     Expr new_current = em.mkExpr(kind::BITVECTOR_MULT, two, old_current);
-    // current[i] = 2 * current[i-1] 
+    // current[i] = 2 * current[i-1]
     current_array = em.mkExpr(kind::STORE, current_array, index, new_current);
     // current[i-1] < current [i]
-    Expr current_slt_new_current = em.mkExpr(kind::BITVECTOR_SLT, old_current, new_current); 
+    Expr current_slt_new_current = em.mkExpr(kind::BITVECTOR_SLT, old_current, new_current);
     assertions.push_back(current_slt_new_current);
-  
+
     old_current = em.mkExpr(kind::SELECT, current_array, index);
   }
 
   Expr query = em.mkExpr(kind::NOT, em.mkExpr(kind::AND, assertions));
-  
-  cout << "Asserting " << query << " to CVC4 " << endl; 
+
+  cout << "Asserting " << query << " to CVC4 " << endl;
   smt.assertFormula(query);
   cout << "Expect sat. " << endl;
   cout << "CVC4: " << smt.checkSat(em.mkConst(true)) << endl;
 
-  // Getting the model 
+  // Getting the model
   cout << "The satisfying model is: " << endl;
-  cout << "  current_array = " << smt.getValue(current_array) << endl; 
-  cout << "  current_array[0] = " << smt.getValue(current_array0) << endl;   
+  cout << "  current_array = " << smt.getValue(current_array) << endl;
+  cout << "  current_array[0] = " << smt.getValue(current_array0) << endl;
   return 0;
 }
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index ccaf3fbfa..db236475d 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -24,6 +24,7 @@ public class BitVectors {
     SmtEngine smt = new SmtEngine(em);
 
     smt.setOption("incremental", new SExpr(true)); // Enable incremental solving
+    smt.setLogic("QF_BV");                         // Set the logic
 
     // The following example has been adapted from the book A Hacker's Delight by
     // Henry S. Warren.
diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java
new file mode 100644
index 000000000..23009428c
--- /dev/null
+++ b/examples/api/java/BitVectorsAndArrays.java
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file BitVectorsAndArrays.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 and array solvers.
+ **
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.util.*;
+
+public class BitVectorsAndArrays {
+  private static int log2(int n) {
+    return (int) Math.round(Math.log(n) / Math.log(2));
+  }
+
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+    smt.setOption("produce-models", new SExpr(true));      // Produce Models
+    smt.setOption("output-language", new SExpr("smtlib")); // output-language
+    smt.setLogic("QF_AUFBV");                              // Set the logic
+
+    // Consider the following code (where size is some previously defined constant):
+    //
+    //
+    //   Assert (current_array[0] > 0);
+    //   for (unsigned i = 1; i < k; ++i) {
+    //     current_array[i] = 2 * current_array[i - 1];
+    //     Assert (current_array[i-1] < current_array[i]);
+    //     }
+    //
+    // We want to check whether the assertion in the body of the for loop holds
+    // throughout the loop.
+
+    // Setting up the problem parameters
+    int k = 4;                // number of unrollings (should be a power of 2)
+    int index_size = log2(k); // size of the index
+
+
+    // Types
+    Type elementType = em.mkBitVectorType(32);
+    Type indexType = em.mkBitVectorType(index_size);
+    Type arrayType = em.mkArrayType(indexType, elementType);
+
+    // Variables
+    Expr current_array = em.mkVar("current_array", arrayType);
+
+    // Making a bit-vector constant
+    Expr zero = em.mkConst(new BitVector(index_size, 0));
+
+    // Asserting that current_array[0] > 0
+    Expr current_array0 = em.mkExpr(Kind.SELECT, current_array, zero);
+    Expr current_array0_gt_0 = em.mkExpr(Kind.BITVECTOR_SGT, current_array0, em.mkConst(new BitVector(32, 0)));
+    smt.assertFormula(current_array0_gt_0);
+
+    // Building the assertions in the loop unrolling
+    Expr index = em.mkConst(new BitVector(index_size, 0));
+    Expr old_current = em.mkExpr(Kind.SELECT, current_array, index);
+    Expr two = em.mkConst(new BitVector(32, 2));
+
+    vectorExpr assertions = new vectorExpr();
+    for (int i = 1; i < k; ++i) {
+      index = em.mkConst(new BitVector(index_size, new edu.nyu.acsys.CVC4.Integer(i)));
+      Expr new_current = em.mkExpr(Kind.BITVECTOR_MULT, two, old_current);
+      // current[i] = 2 * current[i-1]
+      current_array = em.mkExpr(Kind.STORE, current_array, index, new_current);
+      // current[i-1] < current [i]
+      Expr current_slt_new_current = em.mkExpr(Kind.BITVECTOR_SLT, old_current, new_current);
+      assertions.add(current_slt_new_current);
+
+      old_current = em.mkExpr(Kind.SELECT, current_array, index);
+    }
+
+    Expr query = em.mkExpr(Kind.NOT, em.mkExpr(Kind.AND, assertions));
+
+    System.out.println("Asserting " + query + " to CVC4 ");
+    smt.assertFormula(query);
+    System.out.println("Expect sat. ");
+    System.out.println("CVC4: " + smt.checkSat(em.mkConst(true)));
+
+    // Getting the model
+    System.out.println("The satisfying model is: ");
+    System.out.println("  current_array = " + smt.getValue(current_array));
+    System.out.println("  current_array[0] = " + smt.getValue(current_array0));
+  }
+}
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 3f5826f12..d45a8ad16 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -13,22 +13,23 @@
  **
  ** A simple demonstration of how to use uninterpreted functions, combining this
  ** with arithmetic, and extracting a model at the end of a satisfiable query.
+ ** The model is displayed using getValue().
  **/
 
 import edu.nyu.acsys.CVC4.*;
 
 public class Combination {
-  private static void preFixPrintGetValue(SmtEngine smt, Expr e, int level) {
+  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);
+      prefixPrintGetValue(smt, e.getOperator(), level + 1);
     }
 
     for(int i = 0; i < e.getNumChildren(); ++i) {
       Expr curr = e.getChild(i);
-      preFixPrintGetValue(smt, curr, level + 1);
+      prefixPrintGetValue(smt, curr, level + 1);
     }
   }
 
@@ -41,8 +42,9 @@ public class Combination {
     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("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");
@@ -70,6 +72,7 @@ public class Combination {
     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)
@@ -81,15 +84,17 @@ public class Combination {
 
     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("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("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);
+    System.out.println("Finally, after a SAT call, we recursively call smt.getValue(...) on" +
+                       "all of the assumptions to see what the satisfying model looks like.");
+    prefixPrintGetValue(smt, assumptions, 0);
   }
 }
diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index 44d042489..8b09bd688 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -25,6 +25,7 @@ public class LinearArith {
     SmtEngine smt = new SmtEngine(em);
 
     smt.setOption("incremental", new SExpr(true)); // Enable incremental solving
+    smt.setLogic("QF_LIRA");                       // Set the logic
 
     // Prove that if given x (Integer) and y (Real) then
     // the maximum value of y - x is 2/3
diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index ff3d36e14..55f637604 100644
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -3,6 +3,7 @@ noinst_DATA =
 if CVC4_LANGUAGE_BINDING_JAVA
 noinst_DATA += \
 	BitVectors.class \
+	BitVectorsAndArrays.class \
 	Combination.class \
 	HelloWorld.class \
 	LinearArith.class
@@ -13,6 +14,7 @@ endif
 
 EXTRA_DIST = \
 	BitVectors.java \
+	BitVectorsAndArrays.java \
 	Combination.java \
 	HelloWorld.java \
 	LinearArith.java