New C++ API: Enable examples. (#2222)

diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index c76bf9d1e131d7ea6365ed1403c3627db3fcf4cf..6cde8b98d02ccaa6c04ab78c9a28111d93ee7fed 100644 (file)
--- 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 0989d3c480eefb4fc154a8d5a94488d442a3afe2..b6a816db481a69b88d53727d42a2f6d8994634e3 100644 (file)
--- 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 =