From 91673d6cefa63bc0f706101946e0c01fcd429071 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 28 Nov 2012 22:59:58 +0000
Subject: [PATCH] Adding the helloworld.cpp example.

---
 examples/Makefile.am                | 12 ++----------
 examples/api/Makefile.am            | 26 +++++++++++++++++++++++++
 examples/api/helloworld.cpp         | 30 +++++++++++++++++++++++++++++
 examples/{ => api}/linear_arith.cpp |  0
 4 files changed, 58 insertions(+), 10 deletions(-)
 create mode 100644 examples/api/Makefile.am
 create mode 100644 examples/api/helloworld.cpp
 rename examples/{ => api}/linear_arith.cpp (100%)

diff --git a/examples/Makefile.am b/examples/Makefile.am
index a36480af7..d5d8534f4 100644
--- a/examples/Makefile.am
+++ b/examples/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = nra-translate hashsmt .
+SUBDIRS = nra-translate hashsmt api .
 
 AM_CPPFLAGS = \
 	-I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES)
@@ -6,8 +6,7 @@ AM_CXXFLAGS = -Wall
 AM_CFLAGS = -Wall
 
 noinst_PROGRAMS = \
-	simple_vc_cxx \
-	linear_arith
+	simple_vc_cxx
 
 if CVC4_BUILD_LIBCOMPAT
 noinst_PROGRAMS += \
@@ -29,11 +28,6 @@ noinst_DATA += \
 endif
 endif
 
-linear_arith_SOURCES = \
-	linear_arith.cpp
-linear_arith_LDADD = \
-	@builddir@/../src/parser/libcvc4parser.la \
-	@builddir@/../src/libcvc4.la
 
 simple_vc_cxx_SOURCES = \
 	simple_vc_cxx.cpp
@@ -70,12 +64,10 @@ EXTRA_DIST = \
 	README
 
 if STATIC_BINARY
-linear_arith_LINK = $(CXXLINK) -all-static
 simple_vc_cxx_LINK = $(CXXLINK) -all-static
 simple_vc_compat_cxx_LINK = $(CXXLINK) -all-static
 simple_vc_compat_c_LINK = $(LINK) -all-static
 else
-linear_arith_LINK = $(CXXLINK)
 simple_vc_cxx_LINK = $(CXXLINK)
 simple_vc_compat_cxx_LINK = $(CXXLINK)
 simple_vc_compat_c_LINK = $(LINK)
diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
new file mode 100644
index 000000000..937a76d36
--- /dev/null
+++ b/examples/api/Makefile.am
@@ -0,0 +1,26 @@
+AM_CPPFLAGS = \
+	-I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES)
+AM_CXXFLAGS = -Wall
+AM_CFLAGS = -Wall
+
+noinst_PROGRAMS = \
+	linear_arith \
+	helloworld
+
+
+noinst_DATA =
+
+linear_arith_SOURCES = \
+	linear_arith.cpp
+linear_arith_LDADD = \
+	@builddir@/../../src/libcvc4.la
+
+
+helloworld_SOURCES = \
+	helloworld.cpp
+helloworld_LDADD = \
+	@builddir@/../../src/libcvc4.la
+
+# for installation
+examplesdir = $(docdir)/$(subdir)
+examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
new file mode 100644
index 000000000..26b081a79
--- /dev/null
+++ b/examples/api/helloworld.cpp
@@ -0,0 +1,30 @@
+/*********************                                                        */
+/*! \file helloworld.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** 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 very simple CVC4 example
+ **
+ ** A very simple CVC4 tutorial example.
+ **/
+
+#include <iostream>
+#warning "To use helloworld.cpp as given in the wiki, instead of make examples, change the following two includes lines."
+#include "smt/smt_engine.h" // for use with make examples
+//#include <cvc4/cvc4.h> // To follow the wiki
+using namespace CVC4;
+int main() {
+  ExprManager em;
+  Expr helloworld = em.mkVar("Hello World!", em.booleanType());
+  SmtEngine smt(&em);
+  std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;
+  return 0;
+}
diff --git a/examples/linear_arith.cpp b/examples/api/linear_arith.cpp
similarity index 100%
rename from examples/linear_arith.cpp
rename to examples/api/linear_arith.cpp
-- 
2.30.2