cmake: Added target check

Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.

5 files changed, 53 insertions, 15 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index b72d097b8..53c7466c5 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -352,9 +352,12 @@ endif()
 #-----------------------------------------------------------------------------#
 # Enable the ctest testing framework
 
+# This needs to be enabled here rather than in subdirectory test in order to
+# allow calling ctest from the root build directory.
 enable_testing()
 
 #-----------------------------------------------------------------------------#
+# Check options, find packages and configure build.
 
 if(USE_PYTHON2)
   find_package(PythonInterp 2.7 REQUIRED)
@@ -590,24 +593,15 @@ endif()
 
 add_subdirectory(doc)
 add_subdirectory(src)
+add_subdirectory(test)
 
 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
   add_subdirectory(src/bindings)
 endif()
 
-if(BUILD_BINDINGS_JAVA)
-  add_subdirectory(test/java)
-endif()
-
-add_subdirectory(test/regress)
-add_subdirectory(test/system)
-
-if(ENABLE_UNIT_TESTING)
-	add_subdirectory(test/unit)
-endif()
-
 #-----------------------------------------------------------------------------#
 # Print build configuration
+
 if(CVC4_BUILD_PROFILE_PRODUCTION)
   set(CVC4_BUILD_PROFILE_STRING "production")
 elseif(CVC4_BUILD_PROFILE_DEBUG)
@@ -622,7 +616,7 @@ endif()
 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 
-# Print configuration of 2/3-valued option 'var' with prefix 'str'
+# Print configuration of 2-valued or 3-valued option 'var' with prefix 'str'
 macro(print_config str var)
   if(${var} STREQUAL "ON")
     set(OPT_VAL_STR "on")
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
new file mode 100644
index 000000000..2e062bd85
--- /dev/null
+++ b/test/CMakeLists.txt
@@ -0,0 +1,30 @@
+# Determine number of threads available, used to configure (default) parallel
+# execution of custom test targets (can be overriden with ARGS=-jN).
+include(ProcessorCount)
+ProcessorCount(NTHREADS)
+if(NTHREADS EQUAL 0)
+  set(NTHREADS 1)
+endif()
+
+#-----------------------------------------------------------------------------#
+# Add subdirectories
+
+add_subdirectory(regress)
+add_subdirectory(system)
+
+if(BUILD_BINDINGS_JAVA)
+  add_subdirectory(java)
+endif()
+
+if(ENABLE_UNIT_TESTING)
+	add_subdirectory(unit)
+endif()
+
+#-----------------------------------------------------------------------------#
+# Add target 'check', builds and runs
+# > unit tests
+# > regression tests of levels 0 and 1
+# > system tests
+
+add_custom_target(check
+  COMMAND ctest --output-on-failure -LE "regress[2-4]" -j${NTHREADS} $(ARGS))
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c4ba87489..9ecb218d8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2050,11 +2050,15 @@ set(regression_disabled_tests
   regress2/xs-11-20-5-2-5-3.smt2
 )
 
+#-----------------------------------------------------------------------------#
+# Add target 'regress', builds and runs
+# > regression tests of levels 0 and 1
+
 get_target_property(path_to_cvc4 cvc4-bin RUNTIME_OUTPUT_DIRECTORY)
 set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_regression.py)
 
 add_custom_target(regress
-  COMMAND ctest --output-on-failure -L "regress[0-1]" $(ARGS)
+  COMMAND ctest --output-on-failure -L "regress[0-1]" -j${NTHREADS} $(ARGS)
   DEPENDS cvc4-bin)
 
 macro(cvc4_add_regression_test level file)
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index faaf53ae4..01b4a384d 100644
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -3,7 +3,12 @@ include_directories(${PROJECT_SOURCE_DIR}/src)
 include_directories(${PROJECT_SOURCE_DIR}/src/include)
 include_directories(${CMAKE_BINARY_DIR}/src)
 
-add_custom_target(systemtests COMMAND ctest --output-on-failure -L "system" $(ARGS))
+#-----------------------------------------------------------------------------#
+# Add target 'systemtests', builds and runs
+# > system tests
+
+add_custom_target(systemtests
+  COMMAND ctest --output-on-failure -L "system" -j${NTHREADS} $(ARGS))
 
 set(CVC4_SYSTEM_TEST_FLAGS
   -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 3d2a08385..0123ae7ff 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -3,7 +3,12 @@ include_directories(${PROJECT_SOURCE_DIR}/src)
 include_directories(${PROJECT_SOURCE_DIR}/src/include)
 include_directories(${CMAKE_BINARY_DIR}/src)
 
-add_custom_target(units COMMAND ctest -L "unit" $(ARGS))
+#-----------------------------------------------------------------------------#
+# Add target 'units', builds and runs
+# > unit tests
+
+add_custom_target(units
+  COMMAND ctest --output-on-failure -L "unit" -j${NTHREADS} $(ARGS))
 
 set(CVC4_CXXTEST_FLAGS_BLACK
   -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST