cmake: Add module finder for readline.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 803d028c8f5fcac393c5013811816ab9fc76a0a0..ade953fcda5e820b51b96e6330a25a4be868e4af 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -147,6 +147,7 @@ option(USE_CADICAL           "Use CaDiCaL SAT solver" OFF)
 option(USE_CLN               "Use CLN instead of GMP" OFF)
 option(USE_CRYPTOMINISAT     "Use CryptoMiniSat SAT solver" OFF)
 option(USE_LFSC              "Use LFSC proof checker" OFF)
+option(USE_READLINE          "Use readline for better interactive support" OFF)
 option(USE_SYMFPU            "Use SymFPU for floating point support" OFF)
 
 set(OPTIMIZATION_LEVEL 0)
@@ -291,6 +292,18 @@ else()
   set(CVC4_USE_LFSC 0)
 endif()
 
+if(USE_READLINE)
+  find_package(Readline REQUIRED)
+  set(HAVE_LIBREADLINE 1)
+  if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
+    set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
+  else()
+    set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 0)
+  endif()
+else()
+  set(HAVE_LIBREADLINE 0)
+endif()
+
 if(USE_SYMFPU)
   find_package(SymFPU REQUIRED)
   include_directories(${SymFPU_INCLUDE_DIR})
@@ -335,9 +348,9 @@ include(ConfigureCVC4)
 # Define to 1 if Boost threading library has support for thread attributes
 set(BOOST_HAS_THREAD_ATTR 0)
 # Defined if using the CLN multi-precision arithmetic library.
-set(CVC4_CLN_IMP 0)
+set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
 # Defined if using the GMP multi-precision arithmetic library.
-set(CVC4_GMP_IMP 1)
+set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
 # Whether CVC4 is built with the (optional) GPLed library dependences.
 set(CVC4_GPL_DEPS 0)
 # Defined if the requested minimum BOOST version is satisfied
@@ -370,7 +383,7 @@ set(HAVE_LIBGMP 1)
 ## Define to 1 if you have the `profiler' library (-lprofiler).
 #set(HAVE_LIBPROFILER 0)
 # Define to 1 to use libreadline
-set(HAVE_LIBREADLINE 0)
+#set(HAVE_LIBREADLINE 0)
 ## Define to 1 if you have the `tcmalloc' library (-ltcmalloc).
 #set(HAVE_LIBTCMALLOC 0)
 # Define to 1 if you have the <memory.h> header file.
@@ -397,9 +410,6 @@ set(HAVE_SYS_TYPES_H 1)
 set(HAVE_UNISTD_H 1)
 ## Define to the sub-directory where libtool stores uninstalled libraries.
 #set(LT_OBJDIR ".libs/")
-# Define to 1 if rl_completion_entry_function is declared to return pointer
-# to char
-set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 0)
 ## Define to 1 if you have the ANSI C header files.
 #set(STDC_HEADERS 1)
 # Define to 1 if strerror_r returns char *.
@@ -462,7 +472,7 @@ message("Cryptominisat     : ${USE_CRYPTOMINISAT}")
 #message("GLPK              : ${USE_GLPK}")
 message("LFSC              : ${USE_LFSC}")
 #message("MP library   : ${mplibrary}")
-#message("Readline     : ${with_readline}")
+message("Readline          : ${USE_READLINE}")
 message("SymFPU            : ${USE_SYMFPU}")
 message("")
 #message("CPPFLAGS     : ${CPPFLAGS}")

diff --git a/cmake/FindReadline.cmake b/cmake/FindReadline.cmake
new file mode 100644 (file)
index 0000000..2448f73
--- /dev/null
+++ b/cmake/FindReadline.cmake
@@ -0,0 +1,31 @@
+# Find Readline
+# Readline_FOUND - system has Readline lib
+# Readline_INCLUDE_DIR - the Readline include directory
+# Readline_LIBRARIES - Libraries needed to use Readline
+
+find_path(Readline_INCLUDE_DIR NAMES readline/readline.h)
+find_library(Readline_LIBRARIES NAMES readline)
+
+# Check which standard of readline is installed on the system.
+# https://github.com/CVC4/CVC4/issues/702
+if(Readline_INCLUDE_DIR)
+  include(CheckCXXSourceCompiles)
+  set(CMAKE_REQUIRED_QUIET TRUE)
+  set(CMAKE_REQUIRED_LIBRARIES readline)
+  check_cxx_source_compiles(
+    "#include <stdio.h>
+     #include <readline/readline.h>
+     char* foo(const char*, int) { return (char*)0; }
+     int main() { rl_completion_entry_function = foo; return 0; }"
+     Readline_COMPENTRY_FUNC_RETURNS_CHARPTR
+  )
+endif()
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(Readline
+  DEFAULT_MSG Readline_INCLUDE_DIR Readline_LIBRARIES)
+mark_as_advanced(
+  Readline_INCLUDE_DIR
+  Readline_LIBRARIES
+  Readline_COMPENTRY_FUNC_RETURNS_CHARPTR
+)

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 023d02cbe8d9e0e8d04c11003a3c49960af56585..7ac8b1194547811a7d480fe6f9be2ee5bf32eb70 100644 (file)
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -8,6 +8,10 @@ set(libmain_src_files
 add_library(main ${libmain_src_files})
 target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER)
 target_link_libraries(main cvc4 cvc4parser)
+if(USE_READLINE)
+  target_link_libraries(main ${Readline_LIBRARIES})
+  target_include_directories(main PRIVATE ${Readline_INCLUDE_DIR})
+endif()
 
 set(cvc4main_src_files
   command_executor.cpp