cmake: Add support for CxxTest.

14 files changed, 113 insertions, 12 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index a7f1adc0d..a2f0ac3d8 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -112,13 +112,13 @@ macro(cvc4_link_library library)
 endmacro()
 
 macro(cvc4_option var description)
-  set(${var} AUTO CACHE STRING "${description}")
+  set(${var} IGNORE CACHE STRING "${description}")
   # Provide drop down menu options in cmake-gui
-  set_property(CACHE ${var} PROPERTY STRINGS AUTO ON OFF)
+  set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF)
 endmacro()
 
 macro(cvc4_set_option var value)
-  if(${var} STREQUAL "AUTO")
+  if(${var} STREQUAL "IGNORE")
     set(${var} ${value})
   endif()
 endmacro()
@@ -130,7 +130,7 @@ endmacro()
 option(ENABLE_GPL                "Enable GPL dependencies" OFF)
 
 # General build options
-# >> 3-valued: AUTO ON OFF, allows to detect if set by user
+# >> 3-valued: INGORE ON OFF, allows to detect if set by user
 #              this is only necessary for options set for build types!
 cvc4_option(ENABLE_ASSERTIONS    "Enable assertions")
 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
@@ -139,8 +139,9 @@ cvc4_option(ENABLE_MUZZLE        "Enable silencing CVC4; supress ALL non-result
 cvc4_option(ENABLE_OPTIMIZED     "Enable optimization")
 cvc4_option(ENABLE_PROOFS        "Enable proof support")
 cvc4_option(ENABLE_REPLAY        "Enable the replay feature")
-cvc4_option(ENABLE_TRACING       "Enable tracing")
 cvc4_option(ENABLE_STATISTICS    "Enable statistics")
+cvc4_option(ENABLE_TRACING       "Enable tracing")
+cvc4_option(ENABLE_UNIT_TESTING  "Enable unit testing")
 cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
 cvc4_option(ENABLE_SHARED        "Build as shared library")
 # >> 2-valued: ON OFF, for options where we don't need to detect if set by user
@@ -197,7 +198,7 @@ add_check_cxx_flag("-Wnon-virtual-dtor")
 # Build types
 
 if(NOT CMAKE_BUILD_TYPE)
-  set(CMAKE_BUILD_TYPE production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
+  set(CMAKE_BUILD_TYPE Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
   # Provide drop down menu options in cmake-gui
   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 endif()
@@ -264,6 +265,11 @@ if(ENABLE_TRACING)
   set(CVC4_TRACING 1)
 endif()
 
+if(ENABLE_UNIT_TESTING)
+	find_package(CxxTest REQUIRED)
+	enable_testing()
+endif()
+
 if(ENABLE_SHARED)
   set(BUILD_SHARED_LIBS ON)
 endif()
@@ -454,6 +460,12 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR})
 
 add_subdirectory(doc)
 add_subdirectory(src)
+add_subdirectory(test/java)
+add_subdirectory(test/regress)
+add_subdirectory(test/system)
+if(ENABLE_UNIT_TESTING)
+	add_subdirectory(test/unit)
+endif()
 
 if(ENABLE_PROOFS)
   add_subdirectory(proofs/signatures)
@@ -486,12 +498,16 @@ message("Tracing           : ${ENABLE_TRACING}")
 message("Dumping           : ${ENABLE_DUMPING}")
 message("Muzzle            : ${ENABLE_MUZZLE}")
 message("")
-#message("Unit tests   : ${support_unit_tests}")
-message("gcov support      : ${ENABLE_COVERAGE}")
-message("gprof support     : ${ENABLE_PROFILING}")
+message("Unit tests        : ${ENABLE_UNIT_TESTING}")
+message("Coverage (gcov)   : ${ENABLE_COVERAGE}")
+message("Profiling (gprof) : ${ENABLE_PROFILING}")
 message("")
 #message("Static libs  : ${enable_static}")
-message("Shared libs       : ${ENABLE_SHARED}")
+if(BUILD_SHARED_LIBS)
+	message("Shared libs       : ON")
+else()
+	message("Shared libs       : OFF")
+endif()
 #message("Static binary: ${enable_static_binary}")
 #message("Compat lib   : ${CVC4_BUILD_LIBCOMPAT}")
 #message("Bindings     : ${bindings_to_be_built}")
diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake
index a5148859c..a7c7cb961 100644
--- a/cmake/ConfigCompetition.cmake
+++ b/cmake/ConfigCompetition.cmake
@@ -27,3 +27,4 @@ cvc4_set_option(ENABLE_MUZZLE ON)
 cvc4_set_option(ENABLE_VALGRIND OFF)
 # enable_shared=no
 cvc4_set_option(ENABLE_SHARED OFF)
+cvc4_set_option(ENABLE_UNIT_TESTING OFF)
diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
index 8d6b6cb99..9decc07be 100644
--- a/cmake/ConfigDebug.cmake
+++ b/cmake/ConfigDebug.cmake
@@ -23,3 +23,4 @@ cvc4_set_option(ENABLE_DUMPING ON)
 # enable_muzzle=no
 cvc4_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=optional
+cvc4_set_option(ENABLE_UNIT_TESTING ON)
diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake
index 9e85188e6..3b9a1ce98 100644
--- a/cmake/ConfigProduction.cmake
+++ b/cmake/ConfigProduction.cmake
@@ -21,3 +21,4 @@ cvc4_set_option(ENABLE_DUMPING ON)
 cvc4_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=no
 cvc4_set_option(ENABLE_VALGRIND OFF)
+cvc4_set_option(ENABLE_UNIT_TESTING OFF)
diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake
index ad0049988..3b359af93 100644
--- a/cmake/ConfigTesting.cmake
+++ b/cmake/ConfigTesting.cmake
@@ -21,3 +21,4 @@ cvc4_set_option(ENABLE_DUMPING ON)
 cvc4_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=no
 cvc4_set_option(ENABLE_VALGRIND OFF)
+cvc4_set_option(ENABLE_UNIT_TESTING ON)
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index b49a28223..9d69abbcd 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -1,4 +1,6 @@
 set(libmain_src_files
+  command_executor.cpp
+  driver_unified.cpp
   interactive_shell.cpp
   interactive_shell.h
   main.h
@@ -14,8 +16,6 @@ if(USE_READLINE)
 endif()
 
 set(cvc4main_src_files
-  command_executor.cpp
-  driver_unified.cpp
   main.cpp
 )
 
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 3e2dde59b..089e26303 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -1,3 +1,30 @@
+include_directories(.)
+include_directories(${PROJECT_SOURCE_DIR}/src)
+include_directories(${PROJECT_SOURCE_DIR}/src/include)
+include_directories(${CMAKE_BINARY_DIR}/src)
+
+set(CVC4_CXXTEST_FLAGS_BLACK
+  -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
+	-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(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
+  target_link_libraries(${name} main)
+  target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
+  if(${is_white})
+    target_compile_options(${name} PRIVATE -fno-access-control)
+  endif()
+endmacro()
+
+macro(cvc4_add_unit_test_black name)
+  cvc4_add_unit_test(FALSE ${name})
+endmacro()
+macro(cvc4_add_unit_test_white name)
+  cvc4_add_unit_test(TRUE ${name})
+endmacro()
+
+add_subdirectory(base)
 add_subdirectory(context)
 add_subdirectory(expr)
 add_subdirectory(main)
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index e69de29bb..b332d7340 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -0,0 +1,7 @@
+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)
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index e69de29bb..ca5fcbe6d 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -0,0 +1,15 @@
+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)
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index e69de29bb..7b90f0ca4 100644
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -0,0 +1 @@
+cvc4_add_unit_test_black(interactive_shell_black)
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index e69de29bb..fd3227be3 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -0,0 +1,2 @@
+cvc4_add_unit_test_black(parser_black)
+cvc4_add_unit_test_black(parser_builder_black)
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index e69de29bb..c712d7277 100644
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -0,0 +1 @@
+cvc4_add_unit_test_white(cnf_stream_white)
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index e69de29bb..6dc627db9 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -0,0 +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)
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index e69de29bb..3763c72ce 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -0,0 +1,17 @@
+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)