diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-26 16:37:26 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-26 16:37:26 -0700 |
commit | 7205a170a25960561078a0718441a7ec7714607b (patch) | |
tree | 68d3696c3d2f9c586f2bef7fbade46da6baaaf80 /examples/api | |
parent | ae984827fea8fe627e0ef68849d63377b1fbfc03 (diff) |
New C++ API: Enable examples. (#2222)
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/Makefile.am | 51 | ||||
-rw-r--r-- | 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 = |