Added extract.cpp example

diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index 1b3e0b0862f378afb8483149dadbf3e345e5f2f1..c76bf9d1e131d7ea6365ed1403c3627db3fcf4cf 100644 (file)
--- 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 (file)
index 0000000..fac242b
--- /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;
+}