summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-07-26 16:37:26 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2018-07-26 16:37:26 -0700
commit7205a170a25960561078a0718441a7ec7714607b (patch)
tree68d3696c3d2f9c586f2bef7fbade46da6baaaf80
parentae984827fea8fe627e0ef68849d63377b1fbfc03 (diff)
New C++ API: Enable examples. (#2222)
-rw-r--r--examples/api/Makefile.am51
-rw-r--r--examples/api/datatypes-new.cpp2
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 =
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback