diff options
Diffstat (limited to 'examples/api/bitvectors_and_arrays.cpp')
-rw-r--r-- | examples/api/bitvectors_and_arrays.cpp | 50 |
1 files changed, 24 insertions, 26 deletions
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; } |