** information.\endverbatim
**
** \brief A simple demonstration of the solving capabilities of the CVC4
- ** bit-vector solver.
+ ** bit-vector solver.
**
**/
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.
//
// 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);
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;
}
/********************* */
-/*! \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.
**
**/
// 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
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;
}
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.
--- /dev/null
+/********************* */
+/*! \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));
+ }
+}
**
** 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);
}
}
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");
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)
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);
}
}
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
if CVC4_LANGUAGE_BINDING_JAVA
noinst_DATA += \
BitVectors.class \
+ BitVectorsAndArrays.class \
Combination.class \
HelloWorld.class \
LinearArith.class
EXTRA_DIST = \
BitVectors.java \
+ BitVectorsAndArrays.java \
Combination.java \
HelloWorld.java \
LinearArith.java
projects / cvc5.git / commitdiff