From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 13 Aug 2018 22:24:46 +0000 (-0700)
Subject: cmake: Add module finder for SymFPU.
X-Git-Tag: cvc5-1.0.0~4613
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d8989a959c2a555f106022fd9a017f5b640eda9;p=cvc5.git

cmake: Add module finder for SymFPU.
---

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})