From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 23 Dec 2015 16:56:15 +0000 (-0800)
Subject: Added extract.cpp example
X-Git-Tag: cvc5-1.0.0~6131
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0879991984ebc0687faec90b44c85f2389931207;p=cvc5.git

Added extract.cpp example
---

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;
+}