From 8f311f52037a9fb6a82d062342fec4b5396173c6 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 29 Aug 2018 08:20:31 -0700 Subject: cmake: Add options for specifying install directories for dependencies. --- CMakeLists.txt | 25 ++++++++++++++++++++++++- cmake/FindABC.cmake | 17 +++++++++++++---- cmake/FindANTLR.cmake | 31 ++++++++++++++++++++++--------- cmake/FindCaDiCaL.cmake | 20 ++++++++++++++++++-- cmake/FindCryptoMiniSat.cmake | 20 ++++++++++++++++++-- cmake/FindGLPK.cmake | 19 +++++++++++++++---- cmake/FindGMP.cmake | 24 ++++++++++++++++++++++-- cmake/FindLFSC.cmake | 20 ++++++++++++++++++-- cmake/FindSymFPU.cmake | 16 +++++++++++++++- 9 files changed, 165 insertions(+), 27 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3e0d394e5..69f56f0bf 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -161,6 +161,20 @@ 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") +# Custom install directories for dependencies +# If no directory is provided by the user, we first check if the dependency was +# installed via the corresponding contrib/get-* script and if not found, we +# check the intalled system version. If the user provides a directory we +# immediately fail if the dependency was not found at the specified location. +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(GLPK_DIR "" CACHE STRING "Set GLPK install directory") +set(GMP_DIR "" CACHE STRING "Set GMP install directory") +set(LFSC_DIR "" CACHE STRING "Set LFSC install directory") +set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") + # Supported language bindings option(BUILD_BINDINGS_JAVA "Build Java bindings" OFF) option(BUILD_BINDINGS_PYTHON "Build Python bindings" OFF) @@ -190,8 +204,11 @@ set(CVC4_GPL_DEPS 0) #-----------------------------------------------------------------------------# find_package(PythonInterp REQUIRED) + +set(ANTLR_HOME ${ANTLR_DIR}) find_package(ANTLR REQUIRED) +set(GMP_HOME ${GMP_DIR}) find_package(GMP REQUIRED) cvc4_link_library(${GMP_LIBRARIES}) include_directories(${GMP_INCLUDE_DIR}) @@ -342,6 +359,7 @@ if(ENABLE_VALGRIND) endif() if(USE_ABC) + set(ABC_HOME "${ABC_DIR}") find_package(ABC REQUIRED) cvc4_link_library(${ABC_LIBRARIES}) include_directories(${ABC_INCLUDE_DIR}) @@ -349,6 +367,7 @@ if(USE_ABC) endif() if(USE_CADICAL) + set(CaDiCaL_HOME ${CADICAL_DIR}) find_package(CaDiCaL REQUIRED) cvc4_link_library(${CaDiCaL_LIBRARIES}) include_directories(${CaDiCaL_INCLUDE_DIR}) @@ -374,6 +393,7 @@ if(USE_CRYPTOMINISAT) if(THREADS_HAVE_PTHREAD_ARG) add_c_cxx_flag(-pthread) endif() + set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR}) find_package(CryptoMiniSat REQUIRED) cvc4_link_library(${CryptoMiniSat_LIBRARIES}) include_directories(${CryptoMiniSat_INCLUDE_DIR}) @@ -382,6 +402,7 @@ endif() if(USE_GLPK) set(GPL_LIBS "${GPL_LIBS} glpk") + set(GLPK_HOME ${GLPK_DIR}) find_package(GLPK REQUIRED) cvc4_link_library(${GLPK_LIBRARIES}) include_directories(${GLPK_INCLUDE_DIR}) @@ -390,6 +411,7 @@ endif() if(USE_LFSC) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc) + set(LFSC_HOME ${LFSC_DIR}) find_package(LFSC REQUIRED) include_directories(${LFSC_INCLUDE_DIR}) add_definitions(-DCVC4_USE_LFSC) @@ -411,6 +433,7 @@ else() endif() if(USE_SYMFPU) + set(SymFPU_HOME ${SYMFPU_DIR}) find_package(SymFPU REQUIRED) include_directories(${SymFPU_INCLUDE_DIR}) add_definitions(-DCVC4_USE_SYMFPU) @@ -591,7 +614,7 @@ message("Portfolio : ${ENABLE_PORTFOLIO}") message("") message("ABC : ${USE_ABC}") message("CaDiCaL : ${USE_CADICAL}") -message("Cryptominisat : ${USE_CRYPTOMINISAT}") +message("CryptoMiniSat : ${USE_CRYPTOMINISAT}") message("GLPK : ${USE_GLPK}") message("LFSC : ${USE_LFSC}") #message("MP library : ${mplibrary}") diff --git a/cmake/FindABC.cmake b/cmake/FindABC.cmake index 406471c52..0a9cea950 100644 --- a/cmake/FindABC.cmake +++ b/cmake/FindABC.cmake @@ -4,17 +4,26 @@ # ABC_LIBRARIES - Libraries needed to use ABC # ABC_ARCH_FLAGS - Platform specific compile flags -set(ABC_DEFAULT_HOME "${PROJECT_SOURCE_DIR}/abc/alanmi-abc-53f39c11b58d") +# Check default location of ABC built with contrib/get-abc. +if(NOT ABC_HOME) + set(ABC_HOME ${PROJECT_SOURCE_DIR}/abc/alanmi-abc-53f39c11b58d) +endif() + +# Note: We don't check the system version since ABC does not provide a default +# install rule. find_path(ABC_INCLUDE_DIR NAMES base/abc/abc.h - PATHS ${ABC_DEFAULT_HOME}/src) + PATHS ${ABC_HOME}/src + NO_DEFAULT_PATH) find_library(ABC_LIBRARIES NAMES abc - PATHS ${ABC_DEFAULT_HOME}) + PATHS ${ABC_HOME} + NO_DEFAULT_PATH) find_program(ABC_ARCH_FLAGS_PROG NAMES arch_flags - PATHS ${ABC_DEFAULT_HOME}) + PATHS ${ABC_HOME} + NO_DEFAULT_PATH) if(ABC_ARCH_FLAGS_PROG) execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG} diff --git a/cmake/FindANTLR.cmake b/cmake/FindANTLR.cmake index e977ba88d..79d38854e 100644 --- a/cmake/FindANTLR.cmake +++ b/cmake/FindANTLR.cmake @@ -4,20 +4,33 @@ # ANTLR_INCLUDE_DIR - the ANTLR include directory # ANTLR_LIBRARIES - Libraries needed to use ANTLR + +# Check default location of ANTLR built with contrib/get-antlr-3.4. +# If the user provides a directory we will not search the default paths and +# fail if ANTLR was not found in the specified directory. +if(NOT ANTLR_HOME) + set(ANTLR_HOME ${PROJECT_SOURCE_DIR}/antlr-3.4) + set(CHECK_SYSTEM_VERSION TRUE) +endif() + find_program(ANTLR_BINARY NAMES antlr3 - PATHS "${PROJECT_SOURCE_DIR}/antlr-3.4/bin" - ) - + PATHS ${ANTLR_HOME}/bin + NO_DEFAULT_PATH) find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h - PATHS "${PROJECT_SOURCE_DIR}/antlr-3.4/include" - ) - + PATHS ${ANTLR_HOME}/include + NO_DEFAULT_PATH) find_library(ANTLR_LIBRARIES - NAMES antlr3c libantlr3c - PATHS "${PROJECT_SOURCE_DIR}/antlr-3.4/lib" - ) + NAMES antlr3c antlr3c-static + PATHS ${ANTLR_HOME}/lib + NO_DEFAULT_PATH) + +if(CHECK_SYSTEM_VERSION) + find_program(ANTLR_BINARY NAMES antlr3) + find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h) + find_library(ANTLR_LIBRARIES NAMES antlr3c) +endif() include(FindPackageHandleStandardArgs) find_package_handle_standard_args( diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index e3a045911..2976bb2bb 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -3,12 +3,28 @@ # CaDiCaL_INCLUDE_DIR - the CaDiCaL include directory # CaDiCaL_LIBRARIES - Libraries needed to use CaDiCaL + +# Check default location of CaDiCaL built with contrib/get-cadical. +# If the user provides a directory we will not search the default paths and +# fail if CaDiCaL was not found in the specified directory. +if(NOT CaDiCaL_HOME) + set(CaDiCaL_HOME ${PROJECT_SOURCE_DIR}/cadical) + set(CHECK_SYSTEM_VERSION TRUE) +endif() + find_path(CaDiCaL_INCLUDE_DIR NAMES cadical.hpp - PATHS "${PROJECT_SOURCE_DIR}/cadical/src") + PATHS ${CaDiCaL_HOME}/src + NO_DEFAULT_PATH) find_library(CaDiCaL_LIBRARIES NAMES cadical - PATHS "${PROJECT_SOURCE_DIR}/cadical/build") + PATHS ${CaDiCaL_HOME}/build + NO_DEFAULT_PATH) + +if(CHECK_SYSTEM_VERSION) + find_path(CaDiCaL_INCLUDE_DIR NAMES cadical.hpp) + find_library(CaDiCaL_LIBRARIES NAMES cadical) +endif() include(FindPackageHandleStandardArgs) find_package_handle_standard_args(CaDiCaL diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index 1706efb9c..aecd92226 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -3,12 +3,28 @@ # CryptoMiniSat_INCLUDE_DIR - the CryptoMiniSat include directory # CryptoMiniSat_LIBRARIES - Libraries needed to use CryptoMiniSat + +# Check default location of CryptoMiniSat built with contrib/get-cryptominisat. +# If the user provides a directory we will not search the default paths and +# fail if CryptoMiniSat was not found in the specified directory. +if(NOT CryptoMiniSat_HOME) + set(CryptoMiniSat_HOME ${PROJECT_SOURCE_DIR}/cryptominisat5/install) + set(CHECK_SYSTEM_VERSION TRUE) +endif() + find_path(CryptoMiniSat_INCLUDE_DIR NAMES cryptominisat5/cryptominisat.h - PATHS "${PROJECT_SOURCE_DIR}/cryptominisat5/install/include") + PATHS ${CryptoMiniSat_HOME}/include + NO_DEFAULT_PATH) find_library(CryptoMiniSat_LIBRARIES NAMES cryptominisat5 - PATHS "${PROJECT_SOURCE_DIR}/cryptominisat5/install/lib") + PATHS ${CryptoMiniSat_HOME}/lib + NO_DEFAULT_PATH) + +if(CHECK_SYSTEM_VERSION) + find_path(CryptoMiniSat_INCLUDE_DIR NAMES cryptominisat5/cryptominisat.h) + find_library(CryptoMiniSat_LIBRARIES NAMES cryptominisat5) +endif() include(FindPackageHandleStandardArgs) find_package_handle_standard_args(CryptoMiniSat diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake index 7d7c1954f..e2b07faff 100644 --- a/cmake/FindGLPK.cmake +++ b/cmake/FindGLPK.cmake @@ -3,19 +3,30 @@ # GLPK_INCLUDE_DIR - the GLPK include directory # GLPK_LIBRARIES - Libraries needed to use GLPK -set(GLPK_DEFAULT_HOME ${PROJECT_SOURCE_DIR}/glpk-cut-log) + +# Check default location of GLPK built with contrib/get-glpk-cut-log. +# If the user provides a directory we will not search the default paths and +# fail if GLPK was not found in the specified directory. +if(NOT GLPK_HOME) + set(GLPK_HOME ${PROJECT_SOURCE_DIR}/glpk-cut-log) + set(CHECK_SYSTEM_VERSION TRUE) +endif() find_path(GLPK_INCLUDE_DIR NAMES glpk.h - PATHS ${GLPK_DEFAULT_HOME}/include + PATHS ${GLPK_HOME}/include NO_DEFAULT_PATH) find_library(GLPK_LIBRARIES NAMES glpk - PATHS ${GLPK_DEFAULT_HOME}/lib + PATHS ${GLPK_HOME}/lib NO_DEFAULT_PATH) +if(CHECK_SYSTEM_VERSION) + find_path(GLPK_INCLUDE_DIR NAMES glpk.h) + find_library(GLPK_LIBRARIES NAMES glpk) +endif() -# Check if we really have GLPK-cut-log +# Check if we really have GLPK-cut-log. if(GLPK_INCLUDE_DIR) include(CheckSymbolExists) set(CMAKE_REQUIRED_INCLUDES ${GLPK_INCLUDE_DIR}) diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 2d7b9b64a..a835e2d5e 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -3,8 +3,28 @@ # GMP_INCLUDE_DIR - the GMP include directory # GMP_LIBRARIES - Libraries needed to use GMP -find_path(GMP_INCLUDE_DIR NAMES gmp.h) -find_library(GMP_LIBRARIES NAMES gmp libgmp) + +# Check default location of GMP built with contrib/get-gmp. +# If the user provides a directory we will not search the default paths and +# fail if GMP was not found in the specified directory. +if(NOT GMP_HOME) + set(GMP_HOME ${PROJECT_SOURCE_DIR}/gmp-6.1.2) + set(CHECK_SYSTEM_VERSION TRUE) +endif() + +find_path(GMP_INCLUDE_DIR + NAMES gmp.h gmpxx.h + PATHS ${GMP_HOME}/include + NO_DEFAULT_PATH) +find_library(GMP_LIBRARIES + NAMES gmp + PATHS ${GMP_HOME}/lib + NO_DEFAULT_PATH) + +if(CHECK_SYSTEM_VERSION) + find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h) + find_library(GMP_LIBRARIES NAMES gmp) +endif() include(FindPackageHandleStandardArgs) find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index 7176b2015..2e3118669 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -3,12 +3,28 @@ # LFSC_INCLUDE_DIR - the LFSC include directory # LFSC_LIBRARIES - Libraries needed to use LFSC + +# Check default location of LFSC built with contrib/get-lfsc. +# If the user provides a directory we will not search the default paths and +# fail if LFSC was not found in the specified directory. +if(NOT LFSC_HOME) + set(LFSC_HOME ${PROJECT_SOURCE_DIR}/lfsc-checker/install) + set(CHECK_SYSTEM_VERSION TRUE) +endif() + find_path(LFSC_INCLUDE_DIR NAMES lfscc.h - PATHS "${PROJECT_SOURCE_DIR}/lfsc-checker/install/include") + PATHS ${LFSC_HOME}/include + NO_DEFAULT_PATH) find_library(LFSC_LIBRARIES NAMES lfscc - PATHS "${PROJECT_SOURCE_DIR}/lfsc-checker/install/lib") + PATHS ${LFSC_HOME}/lib + NO_DEFAULT_PATH) + +if(CHECK_SYSTEM_VERSION) + find_path(LFSC_INCLUDE_DIR NAMES lfscc.h) + find_library(LFSC_LIBRARIES NAMES lfscc) +endif() include(FindPackageHandleStandardArgs) find_package_handle_standard_args(LFSC diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake index 6d165e16a..f0f9ebf0f 100644 --- a/cmake/FindSymFPU.cmake +++ b/cmake/FindSymFPU.cmake @@ -2,9 +2,23 @@ # SymFPU_FOUND - system has SymFPU lib # SymFPU_INCLUDE_DIR - the SymFPU include directory + +# Check default location of SymFPU built with contrib/get-symfpu. +# If the user provides a directory we will not search the default paths and +# fail if SymFPU was not found in the specified directory. +if(NOT SymFPU_HOME) + set(SymFPU_HOME ${PROJECT_SOURCE_DIR}/symfpu-CVC4) + set(CHECK_SYSTEM_VERSION TRUE) +endif() + find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h - PATHS "${PROJECT_SOURCE_DIR}/symfpu-CVC4") + PATHS ${SymFPU_HOME} + NO_DEFAULT_PATH) + +if(CHECK_SYSTEM_VERSION) + find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h) +endif() include(FindPackageHandleStandardArgs) find_package_handle_standard_args(SymFPU DEFAULT_MSG SymFPU_INCLUDE_DIR) -- cgit v1.2.3