diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-13 15:24:46 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
| commit | 1d8989a959c2a555f106022fd9a017f5b640eda9 (patch) | |
| tree | 5da1252cfce0cbdd7fcf78ef075a479bf9575525 | |
| parent | 013a0fb7fe918d707604690a96ef6c0559af7440 (diff) | |
cmake: Add module finder for SymFPU.
| -rw-r--r-- | CMakeLists.txt | 39 | ||||
| -rw-r--r-- | cmake/FindSymFPU.cmake | 12 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 2 |
3 files changed, 40 insertions, 13 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 9d5e4da54..624644fc4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -81,6 +81,10 @@ macro(add_check_c_cxx_flag flag) message(STATUS "Configure with flag '${flag}'") endmacro() +macro(cvc4_link_library library) + set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${library}) +endmacro() + #-----------------------------------------------------------------------------# set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) @@ -102,27 +106,31 @@ message(STATUS "Building ${CMAKE_BUILD_TYPE} build") #-----------------------------------------------------------------------------# -option(USE_CLN "Use CLN instead of GMP" OFF) +option(USE_CLN "Use CLN instead of GMP" OFF) +option(ENABLE_PROOFS "Enable proof support" OFF) +option(USE_SYMFPU "Use SymFPU for floating point support" OFF) #-----------------------------------------------------------------------------# find_package(PythonInterp REQUIRED) find_package(GMP REQUIRED) -set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES}) +cvc4_link_library(${GMP_LIBRARIES}) include_directories(${GMP_INCLUDE_DIR}) if(USE_CLN) find_package(CLN 1.2.2 REQUIRED) - if(CLN_FOUND) - set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES}) - include_directories(${GMP_INCLUDE_DIR}) - endif() + cvc4_link_library(${CLN_LIBRARIES}) + include_directories(${CLN_INCLUDE_DIR}) +endif() + +if(USE_SYMFPU) + find_package(SymFPU REQUIRED) + include_directories(${SymFPU_INCLUDE_DIR}) endif() find_package(ANTLR REQUIRED) -message(STATUS "Found ANTLR headers: ${ANTLR_INCLUDE_DIR}") -set(LIBRARIES ${LIBRARIES} ${ANTLR_LIBRARIES}) +cvc4_link_library(${ANTLR_LIBRARIES}) include_directories(${ANTLR_INCLUDE_DIR}) #-----------------------------------------------------------------------------# @@ -240,16 +248,23 @@ else() set(CVC4_USE_GMP_IMP 1) endif() -set(CVC4_USE_SYMFPU 0) +if(USE_SYMFPU) + add_definitions(-DCVC4_USE_SYMFPU) + set(CVC4_USE_SYMFPU 1) +else() + set(CVC4_USE_SYMFPU 0) +endif() -set(CVC4_PROOF 0) +if(ENABLE_PROOFS) + add_definitions(-DCVC4_PROOF) +endif() #-----------------------------------------------------------------------------# add_subdirectory(doc) add_subdirectory(src) -if(CVC4_PROOF) +if(ENABLE_PROOFS) add_subdirectory(proofs/signatures) - set(LIBRARIES ${LIBRARIES} signatures) + cvc4_link_library(signatures) endif() diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake new file mode 100644 index 000000000..6d165e16a --- /dev/null +++ b/cmake/FindSymFPU.cmake @@ -0,0 +1,12 @@ +# Find SymFPU +# SymFPU_FOUND - system has SymFPU lib +# SymFPU_INCLUDE_DIR - the SymFPU include directory + +find_path(SymFPU_INCLUDE_DIR + NAMES symfpu/core/unpackedFloat.h + PATHS "${PROJECT_SOURCE_DIR}/symfpu-CVC4") + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(SymFPU DEFAULT_MSG SymFPU_INCLUDE_DIR) + +mark_as_advanced(SymFPU_INCLUDE_DIR) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 92a5ba335..f8c9752f0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -577,7 +577,7 @@ set_target_properties(cvc4 add_dependencies(cvc4 gen-theory-files) target_link_libraries(cvc4 base bvminisat expr minisat options smtutil util replacements - ${LIBRARIES} + ${CVC4_LIBRARIES} ) include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) |