From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 19 Sep 2018 00:57:56 +0000 (-0700)
Subject: cmake: Add target runexamples.
X-Git-Tag: cvc5-1.0.0~4537
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d78113d408d706d44c1d8cfc379fa86cd8e20460;p=cvc5.git

cmake: Add target runexamples.
---

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 493a7b3bb..920727e86 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -8,23 +8,68 @@ find_package(Boost)
 
 set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin/examples)
 
-# Create target examples. Add a dependency for each examples you add.
+# 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)
 
-add_executable(simple_vc_cxx EXCLUDE_FROM_ALL simple_vc_cxx.cpp)
-target_link_libraries(simple_vc_cxx cvc4 cvc4parser)
-add_dependencies(examples simple_vc_cxx)
+# 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_executable(simple_vc_quant_cxx EXCLUDE_FROM_ALL simple_vc_quant_cxx.cpp)
-target_link_libraries(simple_vc_quant_cxx cvc4 cvc4parser)
-add_dependencies(examples simple_vc_quant_cxx)
+# 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;...")
+# > ouput_dir: Determines the examples subdirectory and is empty (passed as
+#              empty string) for the examples root director (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 '<subdirs>/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 '<subdirs>/myexample.cpp'
+  #   we create test target 'example/<subdirs>/myexample'
+  #   and run it with 'ctest -R "example/<subdirs>/<example>"'.
+  if("${output_dir}" STREQUAL "")
+    set(example_test example/${name})
+    set(example_bin_dir ${EXAMPLES_BIN_DIR})
+  else()
+    set(example_test example/${output_dir}/${name})
+    set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir})
+  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()
 
-add_executable(translator EXCLUDE_FROM_ALL translator.cpp)
-target_link_libraries(translator cvc4 cvc4parser)
-add_dependencies(examples translator)
-
-set_target_properties(simple_vc_cxx simple_vc_quant_cxx translator
-  PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_BIN_DIR})
+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)
@@ -36,6 +81,15 @@ if(BUILD_BINDINGS_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)
diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
index 4e4d81ed3..c78c50466 100644
--- a/examples/api/CMakeLists.txt
+++ b/examples/api/CMakeLists.txt
@@ -1,5 +1,3 @@
-set(EXAMPLES_API_BIN_DIR ${EXAMPLES_BIN_DIR}/api)
-
 set(CVC4_EXAMPLES_API
   bitvectors
   bitvectors-new
@@ -21,12 +19,10 @@ set(CVC4_EXAMPLES_API
   strings-new
 )
 
+set(EXAMPLES_API_LINK_LIBS cvc4 cvc4parser)
 foreach(example ${CVC4_EXAMPLES_API})
-  add_executable(${example} EXCLUDE_FROM_ALL ${example}.cpp)
-  target_link_libraries(${example} cvc4)
-  set_target_properties(${example}
-    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_API_BIN_DIR})
-  add_dependencies(examples ${example})
+  cvc4_add_example(${example}
+    "" "${EXAMPLES_API_LINK_LIBS}" "api")
 endforeach()
 
 if(BUILD_BINDINGS_JAVA)
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index bb70ab054..76a55151e 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -1,76 +1,36 @@
-set(EXAMPLES_API_JAVA_BIN_DIR ${EXAMPLES_API_BIN_DIR}/java) 
+set(EXAMPLES_API_JAVA_BIN_DIR ${EXAMPLES_BIN_DIR}/api/java) 
 file(MAKE_DIRECTORY ${EXAMPLES_API_JAVA_BIN_DIR})
 
-add_custom_target(BitVectorsjava
-  COMMAND
-    ${Java_JAVAC_EXECUTABLE}
-      -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/BitVectors.java
-      -d ${EXAMPLES_API_JAVA_BIN_DIR}
-  DEPENDS cvc4jar)
-add_dependencies(examples BitVectorsjava)
-
-add_custom_target(BitVectorsAndArraysjava
-  COMMAND
-    ${Java_JAVAC_EXECUTABLE}
-      -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/BitVectorsAndArrays.java
-      -d ${EXAMPLES_API_JAVA_BIN_DIR}
-  DEPENDS cvc4jar)
-add_dependencies(examples BitVectorsAndArraysjava)
-
-## disabled until bindings for the new API are in place (issue #2284)
-#  add_custom_target(CVC4Streamsjava
-#    COMMAND
-#      ${Java_JAVAC_EXECUTABLE}
-#        -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/CVC4Streams.java
-#        -d ${CMAKE_BINARY_DIR}/bin/examples/api/java
-#    DEPENDS cvc4jar)
-#  add_dependencies(examples CVC4Streamsjava)
-
-add_custom_target(Combinationjava
-  COMMAND
-    ${Java_JAVAC_EXECUTABLE}
-      -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/Combination.java
-      -d ${EXAMPLES_API_JAVA_BIN_DIR}
-  DEPENDS cvc4jar)
-add_dependencies(examples Combinationjava)
-
-add_custom_target(Datatypesjava
-  COMMAND
-    ${Java_JAVAC_EXECUTABLE}
-      -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/Datatypes.java
-      -d ${EXAMPLES_API_JAVA_BIN_DIR}
-  DEPENDS cvc4jar)
-add_dependencies(examples Datatypesjava)
-
-add_custom_target(HelloWorldjava
-  COMMAND
-    ${Java_JAVAC_EXECUTABLE}
-      -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/HelloWorld.java
-      -d ${EXAMPLES_API_JAVA_BIN_DIR}
-  DEPENDS cvc4jar)
-add_dependencies(examples HelloWorldjava)
-
-add_custom_target(LinearArithjava
-  COMMAND
-    ${Java_JAVAC_EXECUTABLE}
-      -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/LinearArith.java
-      -d ${EXAMPLES_API_JAVA_BIN_DIR}
-  DEPENDS cvc4jar)
-add_dependencies(examples LinearArithjava)
-
-## disabled until bindings for the new API are in place (issue #2284)
-#  add_custom_target(PipedInputjava
-#    COMMAND
-#      ${Java_JAVAC_EXECUTABLE}
-#        -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/PipedInput.java
-#        -d ${EXAMPLES_API_JAVA_BIN_DIR}
-#    DEPENDS cvc4jar)
-#  add_dependencies(examples PipedInputjava)
-
-add_custom_target(Stringsjava
-  COMMAND
-    ${Java_JAVAC_EXECUTABLE}
-      -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/Strings.java
-      -d ${EXAMPLES_API_JAVA_BIN_DIR}
-  DEPENDS cvc4jar)
-add_dependencies(examples Stringsjava)
+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
index bf7c910b9..ff696b403 100644
--- a/examples/hashsmt/CMakeLists.txt
+++ b/examples/hashsmt/CMakeLists.txt
@@ -1,18 +1,13 @@
 include_directories(.)
 
-set(EXAMPLES_HASHSMT_BIN_DIR ${EXAMPLES_BIN_DIR}/hashsmt)
+set(EXAMPLES_HASHSMT_LINK_LIBS cvc4)
 
 if(Boost_FOUND)
-  add_executable(sha1_inversion EXCLUDE_FROM_ALL sha1_inversion.cpp word.cpp)
-  target_link_libraries(sha1_inversion cvc4)
-  add_dependencies(examples sha1_inversion)
-  set_target_properties(sha1_inversion
-    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_HASHSMT_BIN_DIR})
+   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()
 
-add_executable(sha1_collision EXCLUDE_FROM_ALL sha1_collision.cpp word.cpp)
-target_link_libraries(sha1_collision cvc4)
-add_dependencies(examples sha1_collision)
-
-set_target_properties(sha1_collision
-  PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_HASHSMT_BIN_DIR})
+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/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt
index 19317604c..b719ac2a4 100644
--- a/examples/nra-translate/CMakeLists.txt
+++ b/examples/nra-translate/CMakeLists.txt
@@ -10,10 +10,15 @@ set(CVC4_EXAMPLES_NRA_TRANSLATE
   smt2toredlog
 )
 
+set(EXAMPLES_NRA_TRANSLATE_LINK_LIBS cvc4 cvc4parser)
 foreach(example ${CVC4_EXAMPLES_NRA_TRANSLATE})
-  add_executable(${example} EXCLUDE_FROM_ALL ${example}.cpp)
-  target_link_libraries(${example} cvc4 cvc4parser)
-  set_target_properties(${example}
-    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_NRA_TRANSLATE_BIN_DIR})
-  add_dependencies(examples ${example})
+  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
index bcf220f32..1c34d3aaf 100644
--- a/examples/sets-translate/CMakeLists.txt
+++ b/examples/sets-translate/CMakeLists.txt
@@ -1,16 +1,14 @@
-set(EXAMPLES_SETS_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/sets-translate)
-
 if(Boost_FOUND)
-  add_executable(sets2arrays EXCLUDE_FROM_ALL sets_translate.cpp)
-  target_link_libraries(sets2arrays cvc4 cvc4parser)
-  add_dependencies(examples sets2arrays)
-
-  add_executable(sets2axioms EXCLUDE_FROM_ALL sets_translate.cpp)
+  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)
-  target_link_libraries(sets2axioms cvc4 cvc4parser)
-  add_dependencies(examples sets2axioms)
-
-  set_target_properties(sets2arrays sets2axioms
-    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_SETS_TRANSLATE_BIN_DIR})
 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)
+