diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-15 12:53:43 -0700 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
commit | 48596d14f3aa3946fb53c632ca0f38827097951a (patch) | |
tree | 55cb93b95250fb2a8f0b638e95176ca622d2b710 | |
parent | 52b9d01f4c3cc0b34daa4759e1004fc315f3f30e (diff) |
cmake: Add module finder for readline.
-rw-r--r-- | CMakeLists.txt | 24 | ||||
-rw-r--r-- | cmake/FindReadline.cmake | 31 | ||||
-rw-r--r-- | src/main/CMakeLists.txt | 4 |
3 files changed, 52 insertions, 7 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 803d028c8..ade953fcd 100644 --- 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 index 000000000..2448f73cb --- /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 023d02cbe..7ac8b1194 100644 --- 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 |