From 2e92d66bf34568a242f13c7cab304b77ab916291 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Wed, 29 Oct 2014 17:00:58 +0100 Subject: [PATCH] Cmake scripts for linking mathsat and gmp or mpir which is required by mathsat Former-commit-id: b13b68115aab80d6045df9c22ae05d084b0ae6b3 --- CMakeLists.txt | 52 +++++++++++++++++++++++++++++++++ resources/cmake/FindGMP.cmake | 54 +++++++++++++++++++++++++++++++++++ storm-config.h.in | 3 ++ 3 files changed, 109 insertions(+) create mode 100644 resources/cmake/FindGMP.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index c6d62bdde..a127d5bc1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -30,6 +30,7 @@ option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).") set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).") +set(MathSAT_ROOT "" CACHE STRING "The root directory of MathSAT (if available).") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.") @@ -60,6 +61,7 @@ find_package(Boost REQUIRED) find_package(Doxygen REQUIRED) find_package(TBB) find_package(Threads REQUIRED) +find_package(GMP) # If the DEBUG option was turned on, we will target a debug version and a release version otherwise if (STORM_DEBUG) @@ -82,6 +84,12 @@ else() set(Z3_LIB_NAME "z3") endif() +if ("${MathSAT_ROOT}" STREQUAL "") + set(ENABLE_MathSAT OFF) +else() + set(ENABLE_MathSAT ON) +endif() + message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}") message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") @@ -207,6 +215,13 @@ else() set(STORM_CPP_Z3_DEF "undef") endif() +# MathSAT Defines +if (ENABLE_MathSAT) + set(STORM_CPP_MathSAT_DEF "define") +else() + set(STORM_CPP_MathSAT_DEF "undef") +endif() + # Intel TBB Defines if (TBB_FOUND AND STORM_USE_INTELTBB) set(STORM_CPP_INTELTBB_DEF "define") @@ -311,6 +326,17 @@ endif() if (ENABLE_Z3) link_directories("${Z3_ROOT}/bin") endif() +if (ENABLE_MathSAT) + link_directories("${MathSAT_ROOT}/lib") +endif() +if(GMP_FOUND) + link_directories(${GMP_LIBRARY_DIR}) +elseif(MPIR_FOUND) + link_directories(${GMP_MPIR_LIBRARY_DIR} ${GMP_MPIRXX_LIBRARY_DIR}) +else(GMP_FOUND) + message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") +endif(GMP_FOUND) + if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") endif () @@ -408,6 +434,32 @@ if (ENABLE_Z3) target_link_libraries(storm-performance-tests ${Z3_LIB_NAME}) endif(ENABLE_Z3) +############################################################# +## +## MathSAT (optional) +## +############################################################# +if (ENABLE_MathSAT) + message (STATUS "StoRM - Linking with MathSAT") + include_directories("${MathSAT_ROOT}/include") + target_link_libraries(storm "mathsat") + target_link_libraries(storm-functional-tests "mathsat") + target_link_libraries(storm-performance-tests "mathsat") + if(GMP_FOUND) + include_directories("${GMP_INCLUDE_DIR}") + target_link_libraries(storm "gmp") + target_link_libraries(storm-functional-tests "gmp") + target_link_libraries(storm-performance-tests "gmp") + elseif(MPIR_FOUND) + include_directories("${GMP_INCLUDE_DIR}") + target_link_libraries(storm "mpir" "mpirxx") + target_link_libraries(storm-functional-tests "mpir" "mpirxx") + target_link_libraries(storm-performance-tests "mpir" "mpirxx") + else(GMP_FOUND) + message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") + endif(GMP_FOUND) +endif(ENABLE_MathSAT) + ############################################################# ## ## Google Test gtest diff --git a/resources/cmake/FindGMP.cmake b/resources/cmake/FindGMP.cmake new file mode 100644 index 000000000..bec3d9a90 --- /dev/null +++ b/resources/cmake/FindGMP.cmake @@ -0,0 +1,54 @@ +# FindGMP.cmake can be found at https://code.google.com/p/origin/source/browse/trunk/cmake/FindGMP.cmake +# Copyright (c) 2008-2010 Kent State University +# Copyright (c) 2011-2012 Texas A&M University +# +# This file is distributed under the MIT License. See the accompanying file +# LICENSE.txt or http://www.opensource.org/licenses/mit-license.php for terms +# and conditions. +# Modified by David Korzeniewski to also find MPIR as an alternative. + +# FIXME: How do I find the version of GMP that I want to use? +# What versions are available? + +# NOTE: GMP prefix is understood to be the path to the root of the GMP +# installation library. +set(GMP_PREFIX "" CACHE PATH "The path to the prefix of a GMP installation") + + +find_path(GMP_INCLUDE_DIR gmp.h + PATHS ${GMP_PREFIX}/include /usr/include /usr/local/include) + +find_library(GMP_LIBRARY NAMES gmp + PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib) + +find_library(GMP_MPIR_LIBRARY NAMES mpir + PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib) + +find_library(GMP_MPIRXX_LIBRARY NAMES mpirxx + PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib) + + +if(GMP_INCLUDE_DIR AND GMP_LIBRARY) + get_filename_component(GMP_LIBRARY_DIR ${GMP_LIBRARY} PATH) + set(GMP_FOUND TRUE) +endif() + +if(GMP_INCLUDE_DIR AND GMP_MPIR_LIBRARY AND GMP_MPIRXX_LIBRARY) + get_filename_component(GMP_MPIR_LIBRARY_DIR ${GMP_MPIR_LIBRARY} PATH) + get_filename_component(GMP_MPIRXX_LIBRARY_DIR ${GMP_MPIRXX_LIBRARY} PATH) + set(MPIR_FOUND TRUE) +endif() + +if(GMP_FOUND) + if(NOT GMP_FIND_QUIETLY) + MESSAGE(STATUS "Found GMP: ${GMP_LIBRARY}") + endif() +elseif(MPIR_FOUND) + if(NOT GMP_FIND_QUIETLY) + MESSAGE(STATUS "Found GMP alternative MPIR: ${MPIR_LIBRARY} and ${MPIRXX_LIBRARY}") + endif() +elseif(GMP_FOUND) + if(GMP_FIND_REQUIRED) + message(FATAL_ERROR "Could not find GMP") + endif() +endif() \ No newline at end of file diff --git a/storm-config.h.in b/storm-config.h.in index cb90e5af6..dd19cc6df 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -23,6 +23,9 @@ // Whether Z3 is available and to be used (define/undef) #@STORM_CPP_Z3_DEF@ STORM_HAVE_Z3 +// Whether MathSAT is available and to be used (define/undef) +#@STORM_CPP_MathSAT_DEF@ STORM_HAVE_MSAT + // Whether Intel Threading Building Blocks are available and to be used (define/undef) #@STORM_CPP_INTELTBB_DEF@ STORM_HAVE_INTELTBB