diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/api/Makefile.am | 6 | ||||
| -rw-r--r-- | examples/api/extract.cpp | 56 |
2 files changed, 62 insertions, 0 deletions
diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am index 1b3e0b086..c76bf9d1e 100644 --- a/examples/api/Makefile.am +++ b/examples/api/Makefile.am @@ -10,6 +10,7 @@ noinst_PROGRAMS = \ bitvectors_and_arrays \ combination \ datatypes \ + extract \ helloworld \ linear_arith \ sets \ @@ -37,6 +38,11 @@ datatypes_SOURCES = \ datatypes_LDADD = \ @builddir@/../../src/libcvc4.la +extract_SOURCES = \ + extract.cpp +extract_LDADD = \ + @builddir@/../../src/libcvc4.la + helloworld_SOURCES = \ helloworld.cpp helloworld_CXXFLAGS = \ diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp new file mode 100644 index 000000000..fac242b76 --- /dev/null +++ b/examples/api/extract.cpp @@ -0,0 +1,56 @@ +/********************* */ +/*! \file bitvectors.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 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 solver. + ** + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // 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.setLogic("QF_BV"); // Set the logic + + Type bitvector32 = em.mkBitVectorType(32); + + Expr x = em.mkVar("a", bitvector32); + + Expr ext_31_1 = em.mkConst(CVC4::BitVectorExtract(31,1)); + Expr x_31_1 = em.mkExpr(ext_31_1, x); + + Expr ext_30_0 = em.mkConst(CVC4::BitVectorExtract(30,0)); + Expr x_30_0 = em.mkExpr(ext_30_0, x); + + Expr ext_31_31 = em.mkConst(CVC4::BitVectorExtract(31,31)); + Expr x_31_31 = em.mkExpr(ext_31_31, x); + + Expr ext_0_0 = em.mkConst(CVC4::BitVectorExtract(0,0)); + Expr x_0_0 = em.mkExpr(ext_0_0, x); + + Expr eq = em.mkExpr(kind::EQUAL, x_31_1, x_30_0); + cout << " Asserting: " << eq << endl; + smt.assertFormula(eq); + + Expr eq2 = em.mkExpr(kind::EQUAL, x_31_31, x_0_0); + cout << " Querying: " << eq2 << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << smt.query(eq2) << endl; + + return 0; +} |