From 7205a170a25960561078a0718441a7ec7714607b Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 26 Jul 2018 16:37:26 -0700
Subject: [PATCH] New C++ API: Enable examples. (#2222)

---
 examples/api/Makefile.am       | 51 ++++++++++++++++++++++++++++++++--
 examples/api/datatypes-new.cpp |  2 ++
 2 files changed, 51 insertions(+), 2 deletions(-)

diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index c76bf9d1e..6cde8b98d 100644
--- a/examples/api/Makefile.am
+++ b/examples/api/Makefile.am
@@ -7,14 +7,23 @@ AM_CFLAGS = -Wall
 
 noinst_PROGRAMS = \
 	bitvectors \
+	bitvectors-new \
 	bitvectors_and_arrays \
+	bitvectors_and_arrays-new \
 	combination \
+	combination-new \
 	datatypes \
-        extract \
+	datatypes-new \
+	extract \
+	extract-new \
 	helloworld \
+	helloworld-new \
 	linear_arith \
+	linear_arith-new \
 	sets \
-	strings
+	sets-new \
+	strings \
+	strings-new
 
 noinst_DATA =
 
@@ -22,26 +31,46 @@ bitvectors_SOURCES = \
 	bitvectors.cpp
 bitvectors_LDADD = \
 	@builddir@/../../src/libcvc4.la
+bitvectors_new_SOURCES = \
+	bitvectors-new.cpp
+bitvectors_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 bitvectors_and_arrays_SOURCES = \
 	bitvectors_and_arrays.cpp
 bitvectors_and_arrays_LDADD = \
 	@builddir@/../../src/libcvc4.la
+bitvectors_and_arrays_new_SOURCES = \
+	bitvectors_and_arrays-new.cpp
+bitvectors_and_arrays_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 combination_SOURCES = \
 	combination.cpp
 combination_LDADD = \
 	@builddir@/../../src/libcvc4.la
+combination_new_SOURCES = \
+	combination-new.cpp
+combination_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 datatypes_SOURCES = \
 	datatypes.cpp
 datatypes_LDADD = \
 	@builddir@/../../src/libcvc4.la
+datatypes_new_SOURCES = \
+	datatypes-new.cpp
+datatypes_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 extract_SOURCES = \
 	extract.cpp
 extract_LDADD = \
 	@builddir@/../../src/libcvc4.la
+extract_new_SOURCES = \
+	extract-new.cpp
+extract_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 helloworld_SOURCES = \
 	helloworld.cpp
@@ -49,21 +78,39 @@ helloworld_CXXFLAGS = \
 	-DCVC4_MAKE_EXAMPLES
 helloworld_LDADD = \
 	@builddir@/../../src/libcvc4.la
+helloworld_new_SOURCES = \
+	helloworld-new.cpp
+helloworld_new_CXXFLAGS = \
+	-DCVC4_MAKE_EXAMPLES
+helloworld_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 linear_arith_SOURCES = \
 	linear_arith.cpp
 linear_arith_LDADD = \
 	@builddir@/../../src/libcvc4.la
+linear_arith_new_SOURCES = \
+	linear_arith-new.cpp
+linear_arith_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 sets_SOURCES = \
 	sets.cpp
 sets_LDADD = \
 	@builddir@/../../src/libcvc4.la
+sets_new_SOURCES = \
+	sets-new.cpp
+sets_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 strings_SOURCES = \
 	strings.cpp
 strings_LDADD = \
 	@builddir@/../../src/libcvc4.la
+strings_new_SOURCES = \
+	strings-new.cpp
+strings_new_LDADD = \
+	@builddir@/../../src/libcvc4.la
 
 # for installation
 examplesdir = $(docdir)/$(subdir)
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 0989d3c48..b6a816db4 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -93,11 +93,13 @@ void test(Solver& slv, Sort& consListSort)
   Sort sort = slv.mkParamSort("T");
   DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name
   DatatypeConstructorDecl paramCons("cons");
+  DatatypeConstructorDecl paramNil("nil");
   DatatypeSelectorDecl paramHead("head", sort);
   DatatypeSelectorDecl paramTail("tail", DatatypeDeclSelfSort());
   paramCons.addSelector(paramHead);
   paramCons.addSelector(paramTail);
   paramConsListSpec.addConstructor(paramCons);
+  paramConsListSpec.addConstructor(paramNil);
 
   Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec);
   Sort paramConsIntListSort =
-- 
2.30.2