9 files changed, 248 insertions, 1 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
new file mode 100644
index 000000000..33d341ac8
--- /dev/null
+++ b/examples/CMakeLists.txt
@@ -0,0 +1,98 @@
+include_directories(${PROJECT_SOURCE_DIR}/src)
+include_directories(${PROJECT_SOURCE_DIR}/src/include)
+include_directories(${CMAKE_BINARY_DIR}/src)
+
+# Some of the examples require boost. Enable these examples if boost is
+# installed.
+find_package(Boost)
+
+set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin/examples)
+
+# Create target examples.
+#
+# Only builds the examples, but does not run them. To run and build all
+# examples, use target runexamples (below).
+# Use macro cvc4_add_example to add examples.
+add_custom_target(examples)
+
+# Create target runexamples.
+# Builds and runs all examples.
+add_custom_target(runexamples
+  COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $(ARGS)
+  DEPENDS examples)
+
+# Add example target and create test to run example with ctest.
+#
+# > name: The name of the example
+# > src_files: The list of source files passed as string "src1 src2 ..."
+#              (alternative: "src1;src2;...").  If empty, <name>.cpp is assumed.
+# > libs: The list of libraries to link the example against, passed as either
+#           - a list variable: set(<list name> <libs1> <libs2> ...) and pass
+#                              as "${<list name>}"
+#           - a string: pass as "lib1 lib2 ..." (alternative: "lib1;lib2;...")
+# > output_dir: Determines the examples subdirectory and is empty (passed as
+#               empty string) for the examples root directory (this)
+# > ARGN: Any additional arguments passed to the macro are interpreted as
+#         as arguments to the test executable.
+macro(cvc4_add_example name src_files libs output_dir)
+  # The build target is created without the path prefix (not supported),
+  # e.g., for '<output_dir>/myexample.cpp'
+  #   we create build target 'myexample'
+  #   and build it with 'make myexample'.
+  # As a consequence, all build target names must be globally unique.
+  if("${src_files}" STREQUAL "")
+    set(src_files_list ${name}.cpp)
+  else()
+    string(REPLACE " " ";" src_files_list "${src_files}")
+  endif()
+  add_executable(${name} EXCLUDE_FROM_ALL ${src_files_list})
+  string(REPLACE " " ";" libs_list "${libs_list}")
+  target_link_libraries(${name} ${libs})
+  add_dependencies(examples ${name})
+  # The test target is prefixed with test identifier 'example/' and the path,
+  # e.g., for '<output_dir>/myexample.cpp'
+  #   we create test target 'example/<output_dir>/myexample'
+  #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+  set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir})
+  if("${output_dir}" STREQUAL "")
+    set(example_test example/${name})
+  else()
+    set(example_test example/${output_dir}/${name})
+  endif()
+  set_target_properties(${name}
+    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${example_bin_dir})
+  add_test(${example_test} ${example_bin_dir}/${name} ${ARGN})
+  set_tests_properties(${example_test} PROPERTIES LABELS "example")
+endmacro()
+
+set(EXAMPLES_LINK_LIBS cvc4 cvc4parser)
+cvc4_add_example(simple_vc_cxx "" "${EXAMPLES_LINK_LIBS}" "")
+cvc4_add_example(simple_vc_quant_cxx "" "${EXAMPLES_LINK_LIBS}" "")
+cvc4_add_example(translator "" "${EXAMPLES_LINK_LIBS}" "")
+
+if(BUILD_BINDINGS_JAVA)
+  find_package(Java REQUIRED)
+  set(EXAMPLES_JAVA_CLASSPATH "${CMAKE_BINARY_DIR}/src/bindings/java/CVC4.jar")
+  add_custom_target(SimpleVCjava
+    COMMAND
+      ${Java_JAVAC_EXECUTABLE}
+        -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/SimpleVC.java
+        -d ${CMAKE_BINARY_DIR}/bin/examples
+    DEPENDS cvc4jar)
+  add_dependencies(examples SimpleVCjava)
+  add_test(
+    NAME example/SimpleVCjava
+    COMMAND
+      ${Java_JAVA_EXECUTABLE}
+        -Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/
+        -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/"
+        SimpleVC
+  )
+  set_tests_properties(example/SimpleVCjava PROPERTIES LABELS "example")
+endif()
+
+add_subdirectory(api)
+add_subdirectory(hashsmt)
+add_subdirectory(nra-translate)
+add_subdirectory(sets-translate)
+
diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
new file mode 100644
index 000000000..c78c50466
--- /dev/null
+++ b/examples/api/CMakeLists.txt
@@ -0,0 +1,30 @@
+set(CVC4_EXAMPLES_API
+  bitvectors
+  bitvectors-new
+  bitvectors_and_arrays
+  bitvectors_and_arrays-new
+  combination
+  combination-new
+  datatypes
+  datatypes-new
+  extract
+  extract-new
+  helloworld
+  helloworld-new
+  linear_arith
+  linear_arith-new
+  sets
+  sets-new
+  strings
+  strings-new
+)
+
+set(EXAMPLES_API_LINK_LIBS cvc4 cvc4parser)
+foreach(example ${CVC4_EXAMPLES_API})
+  cvc4_add_example(${example}
+    "" "${EXAMPLES_API_LINK_LIBS}" "api")
+endforeach()
+
+if(BUILD_BINDINGS_JAVA)
+  add_subdirectory(java)
+endif()
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
new file mode 100644
index 000000000..76a55151e
--- /dev/null
+++ b/examples/api/java/CMakeLists.txt
@@ -0,0 +1,36 @@
+set(EXAMPLES_API_JAVA_BIN_DIR ${EXAMPLES_BIN_DIR}/api/java) 
+file(MAKE_DIRECTORY ${EXAMPLES_API_JAVA_BIN_DIR})
+
+set(EXAMPLES_API_JAVA
+  BitVectors
+  BitVectorsAndArrays
+  ## disabled until bindings for the new API are in place (issue #2284)
+  #CVC4Streams
+  Combination
+  Datatypes
+  HelloWorld
+  LinearArith
+  ## disabled until bindings for the new API are in place (issue #2284)
+  #PipedInput
+  Strings
+)
+
+foreach(example ${EXAMPLES_API_JAVA})
+  add_custom_target(${example}
+    COMMAND
+      ${Java_JAVAC_EXECUTABLE}
+        -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/${example}.java
+        -d ${EXAMPLES_API_JAVA_BIN_DIR}
+    DEPENDS cvc4jar)
+  add_dependencies(examples ${example})
+  set(example_test example/api/java/${example})
+  add_test(
+    NAME ${example_test}
+    COMMAND
+      ${Java_JAVA_EXECUTABLE}
+        -Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/
+        -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/api/java/"
+        ${example}
+  )
+  set_tests_properties(${example_test} PROPERTIES LABELS "example")
+endforeach()
diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt
new file mode 100644
index 000000000..ff696b403
--- /dev/null
+++ b/examples/hashsmt/CMakeLists.txt
@@ -0,0 +1,13 @@
+include_directories(.)
+
+set(EXAMPLES_HASHSMT_LINK_LIBS cvc4)
+
+if(Boost_FOUND)
+   cvc4_add_example(sha1_inversion
+     "sha1_inversion.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
+     "a" "sha1_inversion.outfile")  # arguments to binary (for testing)
+endif()
+
+cvc4_add_example(sha1_collision
+  "sha1_collision.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
+  "1" "1" "sha1_collision.outfile")  # arguments to binary (for testing)
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index 49e028614..352707455 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -22,7 +22,6 @@
  *      Author: dejan
  */
 
-#include <boost/uuid/sha1.hpp>
 #include <fstream>
 #include <iostream>
 #include <sstream>
diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt
new file mode 100644
index 000000000..b719ac2a4
--- /dev/null
+++ b/examples/nra-translate/CMakeLists.txt
@@ -0,0 +1,24 @@
+set(EXAMPLES_NRA_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/nra-translate)
+
+set(CVC4_EXAMPLES_NRA_TRANSLATE
+  normalize
+  smt2info
+  smt2todreal
+  smt2toisat
+  smt2tomathematica
+  smt2toqepcad
+  smt2toredlog
+)
+
+set(EXAMPLES_NRA_TRANSLATE_LINK_LIBS cvc4 cvc4parser)
+foreach(example ${CVC4_EXAMPLES_NRA_TRANSLATE})
+  cvc4_add_example(${example}
+    "" "${EXAMPLES_NRA_TRANSLATE_LINK_LIBS}" "nra-translate"
+    # arguments to binary (for testing)
+    # input file is required by all tests
+    ${CMAKE_CURRENT_SOURCE_DIR}/nra-translate-example-input.smt2
+    # This is a dummy argument for smt2toredlog (argument is only printed, can
+    # be anything for testing purposes). We pass this to all examples since the
+    # other examples ignore additional arguments.
+    "foo")
+endforeach()
diff --git a/examples/nra-translate/nra-translate-example-input.smt2 b/examples/nra-translate/nra-translate-example-input.smt2
new file mode 100644
index 000000000..229c46d4a
--- /dev/null
+++ b/examples/nra-translate/nra-translate-example-input.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status sat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (+ x n) 0))
+(assert (= (+ y n) 1))
+
+(check-sat)
diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt
new file mode 100644
index 000000000..1c34d3aaf
--- /dev/null
+++ b/examples/sets-translate/CMakeLists.txt
@@ -0,0 +1,14 @@
+if(Boost_FOUND)
+  set(EXAMPLES_SETS_TRANSLATE_LINK_LIBS cvc4 cvc4parser)
+  cvc4_add_example(sets2arrays
+    "sets_translate.cpp" "${EXAMPLES_SETS_TRANSLATE_LINK_LIBS}" "sets-translate"
+    # argument to binary (for testing)
+    ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
+
+  cvc4_add_example(sets2axioms
+    "sets_translate.cpp" "${EXAMPLES_SETS_TRANSLATE_LINK_LIBS}" "sets-translate"
+    # argument to binary (for testing)
+    ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
+  target_compile_definitions(sets2axioms PRIVATE -DENABLE_AXIOMS)
+endif()
+
diff --git a/examples/sets-translate/sets-translate-example-input.smt2 b/examples/sets-translate/sets-translate-example-input.smt2
new file mode 100644
index 000000000..3bf1a9b6a
--- /dev/null
+++ b/examples/sets-translate/sets-translate-example-input.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun k (Atom Atom) (Set Atom))
+
+(declare-fun t0 () Atom)
+(declare-fun t1 () Atom)
+(declare-fun t2 () Atom)
+(declare-fun v () Atom)
+(declare-fun b2 () Atom)
+
+(assert (forall ((b Atom)) (or 
+(member v (k t0 b))
+(member v (k t1 b))
+) ))
+
+(assert (not (member v (k t2 b2))))
+
+(check-sat)
+