cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.

Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 920727e865ba54c6a45527fbad3c83df054f7944..a37cb9276c075e891914f85bb53e0666f43263f3 100644 (file)
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -36,7 +36,7 @@ add_custom_target(runexamples
 #         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'
+  # 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.
@@ -50,15 +50,14 @@ macro(cvc4_add_example name src_files libs output_dir)
   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>"'.
+  # 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})
-    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})

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 5e45654a911e4892368d84446a4641c152f6b64e..3e90fb33371f0f021011ac4d505d4cb74ad2d30d 100644 (file)
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -15,15 +15,29 @@ set(CVC4_CXXTEST_FLAGS_BLACK
   -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
 set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
 
-macro(cvc4_add_unit_test is_white name)
-  # cxxtest_add_test generates the unit test executables into directory
-  # CMAKE_BINARY_DIR/test/unit by default and does not allow to change this
-  # location (it's possible to set corresponding target properties with
-  # set_target_properties, but then the test environment does not find them).
-  # Hence, these are the only executables that are not generated into our
-  # default directory for executables (CMAKE_BINARY_DIR/bin).
-  cxxtest_add_test(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
-  set_tests_properties(${name} PROPERTIES LABELS "unit")
+# Generate and add unit test.
+# Note: we do not use cxxtest_add_test from the FindCxxTest module since it
+#       does not allow test names containing '/'.
+macro(cvc4_add_unit_test is_white name output_dir)
+  # generate the test sources
+  set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp)
+  set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
+  add_custom_command(
+      OUTPUT  ${test_src}
+      DEPENDS ${test_header}
+      COMMAND
+        ${CXXTEST_TESTGEN_INTERPRETER}
+          ${CXXTEST_TESTGEN_EXECUTABLE}
+          ${CXXTEST_TESTGEN_ARGS} -o ${test_src} ${test_header}
+  )
+  set_source_files_properties(${test_src} PROPERTIES GENERATED true)
+  # The build target is created without the path prefix (not supported),
+  # e.g., for '<output_dir>/myunittest.h'
+  #   we generate '${CMAKE_BINAR_DIR}/test/unit/<output_dir>/myunittest.cpp',
+  #   create build target 'myunittest'
+  #   and build it with 'make myunittest'.
+  # As a consequence, all build target names must be globally unique.
+  add_executable(${name} ${test_src} ${test_header})
   target_link_libraries(${name} main-test)
   target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
   if(${is_white})
@@ -33,16 +47,31 @@ macro(cvc4_add_unit_test is_white name)
   # code that does not properly add the override keyword to runTest().
   target_compile_options(${name} PRIVATE -Wno-suggest-override)
   add_dependencies(units ${name})
+  # Generate into bin/test/unit/<output_dir>.
+  set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})
+  set_target_properties(${name}
+    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
+  # The test target is prefixed with test identifier 'unit/' and the path,
+  # e.g., for '<output_dir>/myunittest.h'
+  #   we create test target 'unit/<output_dir>/myunittest'
+  #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+  if("${output_dir}" STREQUAL "")
+    set(test_name unit/${name})
+  else()
+    set(test_name unit/${output_dir}/${name})
+  endif()
+  add_test(${test_name} ${test_bin_dir}/${name})
+  set_tests_properties(${test_name} PROPERTIES LABELS "unit")
   if(ENABLE_COVERAGE)
     add_dependencies(coverage ${name})
   endif()
 endmacro()
 
-macro(cvc4_add_unit_test_black name)
-  cvc4_add_unit_test(FALSE ${name})
+macro(cvc4_add_unit_test_black name output_dir)
+  cvc4_add_unit_test(FALSE ${name} ${output_dir})
 endmacro()
-macro(cvc4_add_unit_test_white name)
-  cvc4_add_unit_test(TRUE ${name})
+macro(cvc4_add_unit_test_white name output_dir)
+  cvc4_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
 add_subdirectory(base)

diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt
index 139d6d5771e33466cbb94d28b64de995a3cf387e..0a308b7a94c23f25f75d65eb4b29ccf47b12ab19 100644 (file)
--- a/test/unit/base/CMakeLists.txt
+++ b/test/unit/base/CMakeLists.txt
@@ -1,4 +1,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(map_util_black)
+cvc4_add_unit_test_black(map_util_black base)

diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index 3d556ff6dedd49415cefb9ae46dea78e2359eed6..f089ac5f39f5d4db31b56f651cf517aa64cd94cb 100644 (file)
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -1,10 +1,10 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(cdlist_black)
-cvc4_add_unit_test_black(cdmap_black)
-cvc4_add_unit_test_white(cdmap_white)
-cvc4_add_unit_test_black(cdo_black)
-cvc4_add_unit_test_black(context_black)
-cvc4_add_unit_test_black(context_mm_black)
-cvc4_add_unit_test_white(context_white)
+cvc4_add_unit_test_black(cdlist_black context)
+cvc4_add_unit_test_black(cdmap_black context)
+cvc4_add_unit_test_white(cdmap_white context)
+cvc4_add_unit_test_black(cdo_black context)
+cvc4_add_unit_test_black(context_black context)
+cvc4_add_unit_test_black(context_mm_black context)
+cvc4_add_unit_test_white(context_white context)

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 816d3bd7189c2080462469e17fb6471aff854046..575268cae758e35fa11595cd228543ff6518c094 100644 (file)
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -1,18 +1,18 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(attribute_black)
-cvc4_add_unit_test_white(attribute_white)
-cvc4_add_unit_test_black(expr_manager_public)
-cvc4_add_unit_test_black(expr_public)
-cvc4_add_unit_test_black(kind_black)
-cvc4_add_unit_test_black(kind_map_black)
-cvc4_add_unit_test_black(node_black)
-cvc4_add_unit_test_black(node_builder_black)
-cvc4_add_unit_test_black(node_manager_black)
-cvc4_add_unit_test_white(node_manager_white)
-cvc4_add_unit_test_black(node_self_iterator_black)
-cvc4_add_unit_test_white(node_white)
-cvc4_add_unit_test_black(symbol_table_black)
-cvc4_add_unit_test_black(type_cardinality_public)
-cvc4_add_unit_test_white(type_node_white)
+cvc4_add_unit_test_black(attribute_black expr)
+cvc4_add_unit_test_white(attribute_white expr)
+cvc4_add_unit_test_black(expr_manager_public expr)
+cvc4_add_unit_test_black(expr_public expr)
+cvc4_add_unit_test_black(kind_black expr)
+cvc4_add_unit_test_black(kind_map_black expr)
+cvc4_add_unit_test_black(node_black expr)
+cvc4_add_unit_test_black(node_builder_black expr)
+cvc4_add_unit_test_black(node_manager_black expr)
+cvc4_add_unit_test_white(node_manager_white expr)
+cvc4_add_unit_test_black(node_self_iterator_black expr)
+cvc4_add_unit_test_white(node_white expr)
+cvc4_add_unit_test_black(symbol_table_black expr)
+cvc4_add_unit_test_black(type_cardinality_public expr)
+cvc4_add_unit_test_white(type_node_white expr)

diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index 2b2497a4b36788870052d338d66c5490035f47b4..7dbd01bd27298899cd0e125bfaba331831a8accf 100644 (file)
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -1,4 +1,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(interactive_shell_black)
+cvc4_add_unit_test_black(interactive_shell_black main)

diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index debe8a4cee1e25b7693068e51ee07f06e45d89bd..37204f0c32d0a965cd786d1fe59bf532eaa75578 100644 (file)
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -1,5 +1,5 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(parser_black)
-cvc4_add_unit_test_black(parser_builder_black)
+cvc4_add_unit_test_black(parser_black parser)
+cvc4_add_unit_test_black(parser_builder_black parser)

diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index 9904224456390511bb08b4879348b31f78937b11..dbb6de01d19026ed411be0711a8e9c1a55771eff 100644 (file)
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -1,4 +1,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(cnf_stream_white)
+cvc4_add_unit_test_white(cnf_stream_white prop)

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 6dc627db96e892bf8915a30ff1fbf48ec5e7322e..a5a67cfa29c0658b1c651770901fae5895b6239e 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -1,11 +1,11 @@
-cvc4_add_unit_test_white(evaluator_white)
-cvc4_add_unit_test_white(logic_info_white)
-cvc4_add_unit_test_white(theory_arith_white)
-cvc4_add_unit_test_black(theory_black)
-cvc4_add_unit_test_white(theory_bv_white)
-cvc4_add_unit_test_white(theory_engine_white)
-cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white)
-cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white)
-cvc4_add_unit_test_white(theory_strings_rewriter_white)
-cvc4_add_unit_test_white(theory_white)
-cvc4_add_unit_test_white(type_enumerator_white)
+cvc4_add_unit_test_white(evaluator_white theory)
+cvc4_add_unit_test_white(logic_info_white theory)
+cvc4_add_unit_test_white(theory_arith_white theory)
+cvc4_add_unit_test_black(theory_black theory)
+cvc4_add_unit_test_white(theory_bv_white theory)
+cvc4_add_unit_test_white(theory_engine_white theory)
+cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
+cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc4_add_unit_test_white(theory_strings_rewriter_white theory)
+cvc4_add_unit_test_white(theory_white theory)
+cvc4_add_unit_test_white(type_enumerator_white theory)

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 79e5e78ff71e46c887e2b4fed77e8ac353381f26..0748e1059fb1155ba46075bed75f4e3415873af0 100644 (file)
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -1,20 +1,20 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(array_store_all_black)
-cvc4_add_unit_test_white(assert_white)
-cvc4_add_unit_test_black(binary_heap_black)
-cvc4_add_unit_test_black(bitvector_black)
-cvc4_add_unit_test_black(boolean_simplification_black)
-cvc4_add_unit_test_black(cardinality_public)
-cvc4_add_unit_test_white(check_white)
-cvc4_add_unit_test_black(configuration_black)
-cvc4_add_unit_test_black(datatype_black)
-cvc4_add_unit_test_black(exception_black)
-cvc4_add_unit_test_black(integer_black)
-cvc4_add_unit_test_white(integer_white)
-cvc4_add_unit_test_black(listener_black)
-cvc4_add_unit_test_black(output_black)
-cvc4_add_unit_test_black(rational_black)
-cvc4_add_unit_test_white(rational_white)
-cvc4_add_unit_test_black(stats_black)
+cvc4_add_unit_test_black(array_store_all_black util)
+cvc4_add_unit_test_white(assert_white util)
+cvc4_add_unit_test_black(binary_heap_black util)
+cvc4_add_unit_test_black(bitvector_black util)
+cvc4_add_unit_test_black(boolean_simplification_black util)
+cvc4_add_unit_test_black(cardinality_public util)
+cvc4_add_unit_test_white(check_white util)
+cvc4_add_unit_test_black(configuration_black util)
+cvc4_add_unit_test_black(datatype_black util)
+cvc4_add_unit_test_black(exception_black util)
+cvc4_add_unit_test_black(integer_black util)
+cvc4_add_unit_test_white(integer_white util)
+cvc4_add_unit_test_black(listener_black util)
+cvc4_add_unit_test_black(output_black util)
+cvc4_add_unit_test_black(rational_black util)
+cvc4_add_unit_test_white(rational_white util)
+cvc4_add_unit_test_black(stats_black util)