sudo apt-get install -y \
build-essential \
ccache \
- cxxtest \
libcln-dev \
libgmp-dev \
libgtest-dev \
run: |
brew install \
ccache \
- cxxtest \
cln \
gmp \
pkgconfig \
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()
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")
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
+++ /dev/null
-#####################
-## 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)
--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
cadical_dir=default
cryptominisat_dir=default
drat2er_dir=default
-cxxtest_dir=default
glpk_dir=default
gmp_dir=default
kissat_dir=default
--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##*=} ;;
&& 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 ] \
## 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)
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)
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()
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)
#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"
** Black box testing of CVC4::SymbolTable.
**/
-#include <cxxtest/TestSuite.h>
-
#include <sstream>
#include <string>
+++ /dev/null
-/********************* */
-/*! \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)
#include "expr/expr.h"
#include "expr/type.h"
#include "test_smt.h"
-#include "test_utils.h"
namespace CVC4 {
namespace test {
projects / cvc5.git / commitdiff