diff options
Diffstat (limited to 'CMakeLists.txt')
| -rw-r--r-- | CMakeLists.txt | 40 |
1 files changed, 1 insertions, 39 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 1bbe6d288..7d0c98be2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -70,9 +70,6 @@ endif() if(CRYPTOMINISAT_DIR) list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}") endif() -if(DRAT2ER_DIR) - list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}") -endif() if(GLPK_DIR) list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}") endif() @@ -82,9 +79,6 @@ endif() if(KISSAT_DIR) list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}") endif() -if(LFSC_DIR) - list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}") -endif() if(POLY_DIR) list(APPEND CMAKE_PREFIX_PATH "${POLY_DIR}") endif() @@ -119,7 +113,6 @@ cvc4_option(ENABLE_COMP_INC_TRACK cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") cvc4_option(ENABLE_DUMPING "Enable dumping") cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") -cvc4_option(ENABLE_PROOFS "Enable proof support") cvc4_option(ENABLE_STATISTICS "Enable statistics") cvc4_option(ENABLE_TRACING "Enable tracing") cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing") @@ -148,8 +141,6 @@ cvc4_option(USE_KISSAT "Use Kissat SAT solver") cvc4_option(USE_EDITLINE "Use Editline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) -option(USE_DRAT2ER "Include drat2er for making eager BV proofs") -option(USE_LFSC "Use LFSC proof checker") option(USE_POLY "Use LibPoly for polynomial arithmetic") option(USE_SYMFPU "Use SymFPU for floating point support") option(USE_PYTHON2 "Force Python 2 (deprecated)") @@ -163,11 +154,9 @@ 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(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") set(KISSAT_DIR "" CACHE STRING "Set Kissat install directory") -set(LFSC_DIR "" CACHE STRING "Set LFSC install directory") set(POLY_DIR "" CACHE STRING "Set LibPoly install directory") set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") @@ -429,10 +418,6 @@ if(ENABLE_PROFILING) add_check_c_cxx_flag("-pg") endif() -if(ENABLE_PROOFS) - add_definitions(-DCVC4_PROOF) -endif() - if(ENABLE_TRACING) add_definitions(-DCVC4_TRACING) endif() @@ -477,11 +462,6 @@ if(USE_CRYPTOMINISAT) add_definitions(-DCVC4_USE_CRYPTOMINISAT) endif() -if(USE_DRAT2ER) - find_package(Drat2Er REQUIRED) - add_definitions(-DCVC4_USE_DRAT2ER) -endif() - if(USE_GLPK) set(GPL_LIBS "${GPL_LIBS} glpk") find_package(GLPK REQUIRED) @@ -493,11 +473,6 @@ if(USE_KISSAT) add_definitions(-DCVC4_USE_KISSAT) endif() -if(USE_LFSC) - find_package(LFSC REQUIRED) - add_definitions(-DCVC4_USE_LFSC) -endif() - if(USE_POLY) find_package(Poly REQUIRED) add_definitions(-DCVC4_USE_POLY) @@ -550,11 +525,6 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR}) #-----------------------------------------------------------------------------# # Add subdirectories -# signatures needs to come before src since it adds source files to libcvc4. -if(ENABLE_PROOFS) - add_subdirectory(proofs/signatures) -endif() - add_subdirectory(doc) add_subdirectory(src) add_subdirectory(test) @@ -580,7 +550,7 @@ include(CMakePackageConfigHelpers) # libraries from deps/install/lib, we need to be cautious. Changing these # shared libraries from deps/install/lib most probably breaks the binary. # We only allow such an installation for custom installation prefixes -# (in the assumption that only reasonably experienced users use this and +# (in the assumption that only reasonably experienced users use this and # also that custom installation prefixes are not used for longer periods of # time anyway). Also, we print a big warning with further instructions. if(NOT ENABLE_STATIC_BINARY) @@ -695,10 +665,8 @@ message("") print_config("ABC :" USE_ABC) print_config("CaDiCaL :" USE_CADICAL) print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) -print_config("drat2er :" USE_DRAT2ER) print_config("GLPK :" USE_GLPK) print_config("Kissat :" USE_KISSAT) -print_config("LFSC :" USE_LFSC) print_config("LibPoly :" USE_POLY) message("") print_config("Build libcvc4 only :" BUILD_LIB_ONLY) @@ -723,9 +691,6 @@ endif() if(CRYPTOMINISAT_DIR) message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") endif() -if(DRAT2ER_DIR) - message("DRAT2ER dir : ${DRAT2ER_DIR}") -endif() if(GLPK_DIR) message("GLPK dir : ${GLPK_DIR}") endif() @@ -735,9 +700,6 @@ endif() if(KISSAT_DIR) message("KISSAT dir : ${KISSAT_DIR}") endif() -if(LFSC_DIR) - message("LFSC dir : ${LFSC_DIR}") -endif() if(POLY_DIR) message("LibPoly dir : ${POLY_DIR}") endif() |