From 8953b603bd6960eb59ccb41a63d4742096da1c4a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 1 Dec 2012 01:43:08 +0000 Subject: [PATCH] updated examples --- examples/api/bitvectors.cpp | 60 ++++++------- examples/api/bitvectors_and_arrays.cpp | 50 ++++++----- examples/api/java/BitVectors.java | 1 + examples/api/java/BitVectorsAndArrays.java | 97 ++++++++++++++++++++++ examples/api/java/Combination.java | 25 +++--- examples/api/java/LinearArith.java | 1 + examples/api/java/Makefile.am | 2 + 7 files changed, 170 insertions(+), 66 deletions(-) create mode 100644 examples/api/java/BitVectorsAndArrays.java 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 assertions; + Expr two = em.mkConst(BitVector(32, 2u)); + + std::vector 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 -- 2.30.2