From e39b94aa9425123420635c298fa6bb8a2ee4f048 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Sat, 1 Dec 2012 00:37:22 +0000 Subject: [PATCH] added a new example for the combination of bit-vectors and arrays (includes model generation) and set the logic for the bitvector example --- examples/api/Makefile.am | 7 +- examples/api/bitvectors.cpp | 3 +- examples/api/bitvectors_and_arrays.cpp | 97 ++++++++++++++++++++++++++ 3 files changed, 105 insertions(+), 2 deletions(-) create mode 100644 examples/api/bitvectors_and_arrays.cpp diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am index 33775fd2a..6dba17b05 100644 --- a/examples/api/Makefile.am +++ b/examples/api/Makefile.am @@ -9,7 +9,8 @@ noinst_PROGRAMS = \ linear_arith \ helloworld \ combination \ - bitvectors + bitvectors \ + bitvectors_and_arrays noinst_DATA = @@ -19,6 +20,10 @@ linear_arith_SOURCES = \ linear_arith_LDADD = \ @builddir@/../../src/libcvc4.la +bitvectors_and_arrays_SOURCES = \ + bitvectors_and_arrays.cpp +bitvectors_and_arrays_LDADD = \ + @builddir@/../../src/libcvc4.la combination_SOURCES = \ combination.cpp diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 364fdb69e..4701bf8e3 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -26,7 +26,8 @@ int main() { ExprManager em; 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. // diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp new file mode 100644 index 000000000..cda5e9274 --- /dev/null +++ b/examples/api/bitvectors_and_arrays.cpp @@ -0,0 +1,97 @@ +/********************* */ +/*! \file bitvector.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 + ** 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. + ** + **/ + +#include +#include +// #include // use this after CVC4 is properly installed +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + smt.setOption("produce-models", true); // Produce Models + smt.setOption("output-language", "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 + unsigned k = 4; // number of unrollings (should be a power of 2) + unsigned 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(BitVector(index_size, 0u)); + + // 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(BitVector(32, 0u))); + smt.assertFormula(current_array0_gt_0); + + // 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; + 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_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.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; + smt.assertFormula(query); + cout << "Expect sat. " << endl; + cout << "CVC4: " << smt.checkSat(em.mkConst(true)) << endl; + + // 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; + return 0; +} -- 2.30.2