updated examples

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;
 }

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;
 }

examples/api/java/BitVectors.java

@@ -24,6 +24,7 @@ public static void main(String[] args) {
     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.

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));
+  }
+}