cmake: Add options for specifying install directories for dependencies.

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)