cmake: Add module finder for SymFPU.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9d5e4da5456d588e8e9b6635f9d2ab0e8f160c8a..624644fc4aafd7aef13d383dad4a4002a54d79ed 100644 (file)
--- 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 (file)
index 0000000..6d165e1
--- /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 92a5ba335af486dd374c2ed1aa6a71f0572efd66..f8c9752f0fe1d12bb909f1b6793ede8855959c3e 100644 (file)
--- 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})