From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sat, 25 Aug 2018 06:14:32 +0000 (-0700)
Subject: cmake: Add module finder for GLPK-cut-log.
X-Git-Tag: cvc5-1.0.0~4582
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7be6be7dec00579cb7eaae32bed1217d6c35ee83;p=cvc5.git

cmake: Add module finder for GLPK-cut-log.
---

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)