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.

4 files changed, 47 insertions, 3 deletions

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