Remove obsolete dependency on CxxTest. (#6038)

10 files changed, 0 insertions, 214 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index abd47ec97..eb95a7bef 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -64,7 +64,6 @@ jobs:
         sudo apt-get install -y \
           build-essential \
           ccache \
-          cxxtest \
           libcln-dev \
           libgmp-dev \
           libgtest-dev \
@@ -87,7 +86,6 @@ jobs:
       run: |
         brew install \
           ccache \
-          cxxtest \
           cln \
           gmp \
           pkgconfig \
diff --git a/CMakeLists.txt b/CMakeLists.txt
index b48974cc3..060753864 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -68,9 +68,6 @@ endif()
 if(CRYPTOMINISAT_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}")
 endif()
-if(CXXTEST_DIR)
-  list(APPEND CMAKE_PREFIX_PATH "${CXXTEST_DIR}")
-endif()
 if(DRAT2ER_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}")
 endif()
@@ -164,7 +161,6 @@ set(ABC_DIR           "" CACHE STRING "Set ABC install directory")
 set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
-set(CXXTEST_DIR       "" CACHE STRING "Set CxxTest install directory")
 set(DRAT2ER_DIR       "" CACHE STRING "Set drat2er install directory")
 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
diff --git a/INSTALL.md b/INSTALL.md
index fc19dc946..635118f1d 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -189,13 +189,6 @@ for a package named "libedit-dev" or "libedit-devel" or similar.
 The [Boost](http://www.boost.org) C++ base library is needed for some examples
 provided with CVC4.
 
-### CxxTest Unit Testing Framework (Unit Tests)
-
-[CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests
-(included with the distribution). 
-See [Testing CVC4](#Testing-CVC4) below for more details.
-
-
 ### Google Test Unit Testing Framework (Unit Tests)
 
 [Google Test](https://github.com/google/googletest) is required to optionally
diff --git a/cmake/FindCxxTest.cmake b/cmake/FindCxxTest.cmake
deleted file mode 100644
index f21a4fe0d..000000000
--- a/cmake/FindCxxTest.cmake
+++ /dev/null
@@ -1,60 +0,0 @@
-#####################
-## FindCxxTest.cmake
-## Top contributors (to current version):
-##   Mathias Preiner, Alex Ozdemir, Andrew Reynolds
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
-## in the top-level source directory and their institutional affiliations.
-## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.
-##
-# Find CxxTest
-# CxxTest_FOUND - system has CxxTest lib
-# CxxTest_INCLUDE_DIR - the CxxTest include directory
-# CxxTest_TESTGEN_EXECUTABLE - CxxTest excecutable
-# CxxTest_TESTGEN_INTERPRETER - Python/Perl interpreter for running executable
-
-find_package(PythonInterp QUIET)
-find_package(Perl QUIET)
-
-find_path(CxxTest_INCLUDE_DIR cxxtest/TestSuite.h
-          PATHS ${CxxTest_HOME}
-          NO_DEFAULT_PATH)
-find_program(CxxTest_PYTHON_TESTGEN_EXECUTABLE
-             NAMES cxxtestgen cxxtestgen.py
-             PATHS ${CxxTest_HOME}/bin
-             NO_DEFAULT_PATH)
-find_program(CxxTest_PERL_TESTGEN_EXECUTABLE cxxtestgen.pl
-             PATHS ${CxxTest_HOME}/bin
-             NO_DEFAULT_PATH)
-
-if(NOT CxxTest_HOME)
-  find_path(CxxTest_INCLUDE_DIR cxxtest/TestSuite.h)
-  find_program(CxxTest_PYTHON_TESTGEN_EXECUTABLE NAMES cxxtestgen.py)
-  find_program(CxxTest_SHEBANG_TESTGEN_EXECUTABLE NAMES cxxtestgen)
-  find_program(CxxTest_PERL_TESTGEN_EXECUTABLE cxxtestgen.pl)
-endif()
-
-
-if(CxxTest_SHEBANG_TESTGEN_EXECUTABLE)
-  set(CxxTest_USE_SHEBANG ON)
-  set(CxxTest_TESTGEN_EXECUTABLE ${CxxTest_SHEBANG_TESTGEN_EXECUTABLE})
-elseif(PYTHONINTERP_FOUND AND CxxTest_PYTHON_TESTGEN_EXECUTABLE)
-  set(CxxTest_TESTGEN_EXECUTABLE ${CxxTest_PYTHON_TESTGEN_EXECUTABLE})
-  set(CxxTest_TESTGEN_INTERPRETER ${PYTHON_EXECUTABLE})
-elseif(PERL_FOUND AND CxxTest_PERL_TESTGEN_EXECUTABLE)
-  set(CxxTest_TESTGEN_EXECUTABLE ${CxxTest_PERL_TESTGEN_EXECUTABLE})
-  set(CxxTest_TESTGEN_INTERPRETER ${PERL_EXECUTABLE})
-elseif(NOT PYTHONINTERP_FOUND AND NOT PERL_FOUND AND CxxTest_FIND_REQUIRED)
-  message(FATAL_ERROR "Neither Python nor Perl found, cannot use CxxTest.")
-endif()
-
-if(NOT DEFINED CxxTest_TESTGEN_ARGS)
-  set(CxxTest_TESTGEN_ARGS --error-printer)
-endif()
-
-include(FindPackageHandleStandardArgs)
-find_package_handle_standard_args(
-  CxxTest DEFAULT_MSG CxxTest_INCLUDE_DIR CxxTest_TESTGEN_EXECUTABLE)
-
-mark_as_advanced(CxxTest_INCLUDE_DIR CxxTest_TESTGEN_EXECUTABLE)
diff --git a/configure.sh b/configure.sh
index e7a858486..f583b008a 100755
--- a/configure.sh
+++ b/configure.sh
@@ -74,7 +74,6 @@ Optional Path to Optional Packages:
   --cadical-dir=PATH       path to top level of CaDiCaL source tree
   --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
   --drat2er-dir=PATH       path to the top level of the drat2er installation
-  --cxxtest-dir=PATH       path to CxxTest installation
   --glpk-dir=PATH          path to top level of GLPK installation
   --gmp-dir=PATH           path to top level of GMP installation
   --kissat-dir=PATH        path to top level of Kissat source tree
@@ -160,7 +159,6 @@ antlr_dir=default
 cadical_dir=default
 cryptominisat_dir=default
 drat2er_dir=default
-cxxtest_dir=default
 glpk_dir=default
 gmp_dir=default
 kissat_dir=default
@@ -319,9 +317,6 @@ do
     --cryptominisat-dir) die "missing argument to $1 (try -h)" ;;
     --cryptominisat-dir=*) cryptominisat_dir=${1##*=} ;;
 
-    --cxxtest-dir) die "missing argument to $1 (try -h)" ;;
-    --cxxtest-dir=*) cxxtest_dir=${1##*=} ;;
-
     --drat2er-dir) die "missing argument to $1 (try -h)" ;;
     --drat2er-dir=*) drat2er_dir=${1##*=} ;;
 
@@ -469,8 +464,6 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir"
 [ "$cryptominisat_dir" != default ] \
   && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
-[ "$cxxtest_dir" != default ] \
-  && cmake_opts="$cmake_opts -DCXXTEST_DIR=$cxxtest_dir"
 [ "$drat2er_dir" != default ] \
   && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir"
 [ "$glpk_dir" != default ] \
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 46ff346e0..fda403e84 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -8,11 +8,6 @@
 ## All rights reserved.  See the file COPYING in the top-level source
 ## directory for licensing information.
 ##
-# Note: We use our custom CxxTest finder here to specify custom directories and
-# fail if it is not found in the specified directory (similar to the other
-# custom finder modules).
-set(CxxTest_HOME ${CXXTEST_DIR})
-find_package(CxxTest REQUIRED)
 find_package(GTest REQUIRED)
 include(GoogleTest)
 
@@ -35,7 +30,6 @@ add_custom_target(units
 set(CVC4_UNIT_TEST_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_UNIT_TEST_FLAGS_BLACK})
 
 # Generate and add unit test.
 macro(cvc4_add_unit_test is_white name output_dir)
@@ -80,84 +74,6 @@ macro(cvc4_add_unit_test is_white name output_dir)
   set_tests_properties(${test_name} PROPERTIES LABELS "unit")
 endmacro()
 
-# 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 '/'.
-# !! This macro will be removed when all unit tests are migrated to Google Test.
-macro(cvc4_add_cxx_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)
-  if (CxxTest_USE_SHEBANG)
-    add_custom_command(
-        OUTPUT  ${test_src}
-        DEPENDS ${test_header}
-        COMMAND
-          ${CxxTest_TESTGEN_EXECUTABLE}
-            ${CxxTest_TESTGEN_ARGS} -o ${test_src} ${test_header}
-    )
-  else()
-    add_custom_command(
-        OUTPUT  ${test_src}
-        DEPENDS ${test_header}
-        COMMAND
-          ${CxxTest_TESTGEN_INTERPRETER}
-            ${CxxTest_TESTGEN_EXECUTABLE}
-            ${CxxTest_TESTGEN_ARGS} -o ${test_src} ${test_header}
-    )
-  endif()
-  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_include_directories(${name} PRIVATE ${CxxTest_INCLUDE_DIR})
-  target_compile_definitions(${name} PRIVATE ${CVC4_UNIT_TEST_FLAGS_BLACK})
-  if(USE_LFSC)
-    # We don't link against LFSC, because CVC4 is already linked against it.
-    target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
-  endif()
-  if(USE_POLY)
-    # We don't link against libpoly, because CVC4 is already linked against it.
-    target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
-  endif()
-  if(${is_white})
-    target_compile_options(${name} PRIVATE -fno-access-control)
-  endif()
-  # Disable the Wsuggest-override warnings for the unit tests. CxxTest generates
-  # code that does not properly add the override keyword to runTest().
-  check_cxx_compiler_flag("-Wno-suggest-override" HAVE_FLAGWno_suggest_override)
-  if(HAVE_FLAGWno_suggest_override)
-    target_compile_options(${name} PRIVATE -Wno-suggest-override)
-  endif()
-  # Disable the Wunused-comparison warnings for the unit tests.
-  check_cxx_compiler_flag("-Wno-unused-comparison" HAVE_FLAGWno_unused_comparison)
-  if(HAVE_FLAGWno_unused_comparison)
-    target_compile_options(${name} PRIVATE -Wno-unused-comparison)
-  endif()
-
-  add_dependencies(build-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")
-endmacro()
-
 macro(cvc4_add_unit_test_black name output_dir)
   cvc4_add_unit_test(FALSE ${name} ${output_dir})
 endmacro()
@@ -165,15 +81,6 @@ macro(cvc4_add_unit_test_white name output_dir)
   cvc4_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
-# !! Will be removed when all unit tests are migrated to Google Test.
-macro(cvc4_add_cxx_unit_test_black name output_dir)
-  cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir})
-endmacro()
-# !! Will be removed when all unit tests are migrated to Google Test.
-macro(cvc4_add_cxx_unit_test_white name output_dir)
-  cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir})
-endmacro()
-
 add_subdirectory(api)
 add_subdirectory(base)
 add_subdirectory(context)
diff --git a/test/unit/expr/node_manager_black.cpp b/test/unit/expr/node_manager_black.cpp
index 4b72f0418..d9a236a64 100644
--- a/test/unit/expr/node_manager_black.cpp
+++ b/test/unit/expr/node_manager_black.cpp
@@ -21,7 +21,6 @@
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
 #include "test_node.h"
-#include "test_utils.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
diff --git a/test/unit/expr/symbol_table_black.cpp b/test/unit/expr/symbol_table_black.cpp
index 2897a5588..4ca26ba7b 100644
--- a/test/unit/expr/symbol_table_black.cpp
+++ b/test/unit/expr/symbol_table_black.cpp
@@ -14,8 +14,6 @@
  ** Black box testing of CVC4::SymbolTable.
  **/
 
-#include <cxxtest/TestSuite.h>
-
 #include <sstream>
 #include <string>
 
diff --git a/test/unit/test_utils.h b/test/unit/test_utils.h
deleted file mode 100644
index 155d923ed..000000000
--- a/test/unit/test_utils.h
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file test_utils.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utilities for testing.
- **
- **/
-
-#include <sys/wait.h>
-#include <unistd.h>
-
-/**
- * Use TS_UTILS_EXPECT_ABORT if you expect the expression to abort() when a
- * AlwaysAssert or Assert is triggered.
- */
-#define TS_UTILS_EXPECT_ABORT(expr) \
-  do                                \
-  {                                 \
-    int32_t status;                 \
-    if (fork())                     \
-    {                               \
-      wait(&status);                \
-    }                               \
-    else                            \
-    {                               \
-      expr;                         \
-      exit(EXIT_SUCCESS);           \
-    }                               \
-    TS_ASSERT(WIFSIGNALED(status)); \
-  } while (0)
diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
index a0a954008..74dace3fd 100644
--- a/test/unit/util/array_store_all_white.cpp
+++ b/test/unit/util/array_store_all_white.cpp
@@ -18,7 +18,6 @@
 #include "expr/expr.h"
 #include "expr/type.h"
 #include "test_smt.h"
-#include "test_utils.h"
 
 namespace CVC4 {
 namespace test {