diff options
| -rw-r--r-- | CMakeLists.txt | 16 | ||||
| -rw-r--r-- | cmake/FindGLPK.cmake | 35 |
2 files changed, 45 insertions, 6 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 9a2f8ed8a..3e0d394e5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -156,6 +156,7 @@ option(USE_ABC "Use ABC for AIG bit-blasting") option(USE_CADICAL "Use CaDiCaL SAT solver") option(USE_CLN "Use CLN instead of GMP") option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") +option(USE_GLPK "Use GLPK simplex solver") option(USE_LFSC "Use LFSC proof checker") option(USE_READLINE "Use readline for better interactive support") option(USE_SYMFPU "Use SymFPU for floating point support") @@ -356,11 +357,6 @@ endif() if(USE_CLN) set(GPL_LIBS "${GPL_LIBS} cln") - if(NOT ENABLE_GPL) - message(FATAL_ERROR - "Bad configuration detected: BSD-licensed code only, but also requested " - "GPLed libraries: ${GPL_LIBS}") - endif() find_package(CLN 1.2.2 REQUIRED) cvc4_link_library(${CLN_LIBRARIES}) include_directories(${CLN_INCLUDE_DIR}) @@ -384,6 +380,14 @@ if(USE_CRYPTOMINISAT) add_definitions(-DCVC4_USE_CRYPTOMINISAT) endif() +if(USE_GLPK) + set(GPL_LIBS "${GPL_LIBS} glpk") + find_package(GLPK REQUIRED) + cvc4_link_library(${GLPK_LIBRARIES}) + include_directories(${GLPK_INCLUDE_DIR}) + add_definitions(-DCVC4_USE_GLPK) +endif() + if(USE_LFSC) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc) find_package(LFSC REQUIRED) @@ -588,7 +592,7 @@ message("") message("ABC : ${USE_ABC}") message("CaDiCaL : ${USE_CADICAL}") message("Cryptominisat : ${USE_CRYPTOMINISAT}") -#message("GLPK : ${USE_GLPK}") +message("GLPK : ${USE_GLPK}") message("LFSC : ${USE_LFSC}") #message("MP library : ${mplibrary}") message("Readline : ${USE_READLINE}") diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake new file mode 100644 index 000000000..7d7c1954f --- /dev/null +++ b/cmake/FindGLPK.cmake @@ -0,0 +1,35 @@ +# Find GLPK-cut-log +# GLPK_FOUND - system has GLPK lib +# GLPK_INCLUDE_DIR - the GLPK include directory +# GLPK_LIBRARIES - Libraries needed to use GLPK + +set(GLPK_DEFAULT_HOME ${PROJECT_SOURCE_DIR}/glpk-cut-log) + +find_path(GLPK_INCLUDE_DIR + NAMES glpk.h + PATHS ${GLPK_DEFAULT_HOME}/include + NO_DEFAULT_PATH) +find_library(GLPK_LIBRARIES + NAMES glpk + PATHS ${GLPK_DEFAULT_HOME}/lib + NO_DEFAULT_PATH) + + +# Check if we really have GLPK-cut-log +if(GLPK_INCLUDE_DIR) + include(CheckSymbolExists) + set(CMAKE_REQUIRED_INCLUDES ${GLPK_INCLUDE_DIR}) + set(CMAKE_REQUIRED_LIBRARIES ${GLPK_LIBRARIES} m) + check_symbol_exists(glp_ios_get_cut "glpk.h" HAVE_GLPK_CUT_LOG) + if(NOT HAVE_GLPK_CUT_LOG) + message(FATAL_ERROR "Could not link against GLPK-cut-log. " + "Did you forget to install GLPK-cut-log?") + endif() +endif() + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(GLPK + DEFAULT_MSG + GLPK_INCLUDE_DIR GLPK_LIBRARIES) + +mark_as_advanced(GLPK_INCLUDE_DIR GLPK_LIBRARIES) |