diff --git a/CMakeLists.txt b/CMakeLists.txt index 768e0d071..9925cde30 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -28,7 +28,6 @@ option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precom 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(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.") set(MSAT_ROOT "" CACHE STRING "The root directory of MathSAT (if available).") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") @@ -61,6 +60,7 @@ find_package(Gurobi) find_package(TBB) find_package(Threads REQUIRED) find_package(GMP) +find_package(Z3) # If the DEBUG option was turned on, we will target a debug version and a release version otherwise. if (STORM_DEBUG) @@ -82,12 +82,6 @@ else() set(ENABLE_CUDA ON) endif() -if ("${Z3_ROOT}" STREQUAL "") - set(ENABLE_Z3 OFF) -else() - set(ENABLE_Z3 ON) - set(Z3_LIB_NAME "z3") -endif() if ("${MSAT_ROOT}" STREQUAL "") set(ENABLE_MSAT OFF) @@ -142,10 +136,6 @@ elseif(MSVC) # since nobody cares at the moment add_definitions(/wd4250) - if(ENABLE_Z3) - set(Z3_LIB_NAME "libz3") - endif() - # MSVC does not do strict-aliasing, so no option needed else(CLANG) set(STORM_COMPILED_BY "Clang (LLVM)") @@ -209,11 +199,7 @@ message(STATUS "StoRM - Version information: ${STORM_CPP_VERSION_MAJOR}.${STORM_ # Base path for test files set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test") # Gurobi Defines -if (ENABLE_GUROBI) - set(STORM_CPP_GUROBI_DEF "define") -else() - set(STORM_CPP_GUROBI_DEF "undef") -endif() +set(STORM_HAVE_GUROBI ${ENABLE_GUROBI}) # CUDA Defines if (ENABLE_CUDA) @@ -223,24 +209,16 @@ else() endif() # glpk defines -set(STORM_CPP_GLPK_DEF "define") +set(STORM_HAVE_GLPK 1) # CUDA Defines set(STORM_CPP_CUDAFORSTORM_DEF "undef") # Z3 Defines -if (ENABLE_Z3) - set(STORM_CPP_Z3_DEF "define") -else() - set(STORM_CPP_Z3_DEF "undef") -endif() +set(STORM_HAVE_Z3 ${FOUND_Z3}) # MathSAT Defines -if (ENABLE_MSAT) - set(STORM_CPP_MSAT_DEF "define") -else() - set(STORM_CPP_MSAT_DEF "undef") -endif() +set(STORM_HAVE_MSAT ${ENABLE_MSAT}) # Intel TBB Defines if (TBB_FOUND AND STORM_USE_INTELTBB) @@ -474,9 +452,6 @@ if (ENABLE_GUROBI) endif() #link_directories("${GUROBI_ROOT}/lib") endif() -if (ENABLE_Z3) - link_directories("${Z3_ROOT}/bin") -endif() if (ENABLE_MSAT) link_directories("${MSAT_ROOT}/lib") endif() @@ -548,8 +523,6 @@ if (ENABLE_GUROBI) message (STATUS "StoRM - Linking with Gurobi (include: ${GUROBI_INCLUDE_DIRS})") include_directories(${GUROBI_INCLUDE_DIRS}) target_link_libraries(storm ${GUROBI_LIBRARY}) - target_link_libraries(storm-functional-tests ${GUROBI_LIBRARY}) - target_link_libraries(storm-performance-tests ${GUROBI_LIBRARY}) endif(ENABLE_GUROBI) ############################################################# @@ -559,11 +532,8 @@ endif(ENABLE_GUROBI) ############################################################# if (ENABLE_CUDA) message (STATUS "StoRM - Linking with CUDA") - target_link_libraries(storm ${STORM_CUDA_LIB_NAME}) - target_link_libraries(storm-functional-tests ${STORM_CUDA_LIB_NAME}) - target_link_libraries(storm-performance-tests ${STORM_CUDA_LIB_NAME}) - - include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") + target_link_libraries(storm ${STORM_CUDA_LIB_NAME}) + include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") endif(ENABLE_CUDA) ############################################################# @@ -589,11 +559,12 @@ include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk") ## Z3 (optional) ## ############################################################# -if (ENABLE_Z3) +if(STORM_HAVE_Z3) message (STATUS "StoRM - Linking with Z3") - include_directories("${Z3_ROOT}/include") - target_link_libraries(storm ${Z3_LIB_NAME}) -endif(ENABLE_Z3) + include_directories(${Z3_INCLUDE_DIRS}) + target_link_libraries(storm ${Z3_LIBRARIES}) +endif(STORM_HAVE_Z3) + ############################################################# ## @@ -605,8 +576,6 @@ if(STORM_HAVE_CARL) message(STATUS "StoRM - Linking with carl.") include_directories("${carl_INCLUDE_DIR}") target_link_libraries(storm lib_carl) - target_link_libraries(storm-functional-tests lib_carl) - target_link_libraries(storm-performance-tests lib_carl) endif() ############################################################# @@ -618,18 +587,12 @@ if (ENABLE_MSAT) message (STATUS "StoRM - Linking with MathSAT") include_directories("${MSAT_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) diff --git a/resources/cmake/FindZ3.cmake b/resources/cmake/FindZ3.cmake new file mode 100644 index 000000000..8b18ac133 --- /dev/null +++ b/resources/cmake/FindZ3.cmake @@ -0,0 +1,47 @@ +# - Try to find libz3 +# Once done this will define +# LIBZ3_FOUND - System has libz3 +# LIBZ3_INCLUDE_DIRS - The libz3 include directories +# LIBZ3_LIBRARIES - The libraries needed to use libz3 + +# dependencies +# -- TODO -- needed? + +# find include dir by searching for a concrete file, which definetely must be in it +find_path(Z3_INCLUDE_DIR + NAMES src/util/z3_exception.h #exemplary file, should only be available in z3 + PATHS ENV PATH INCLUDE + PATH_SUFFIXES z3 + ) + +# find library +find_library(Z3_LIBRARY + NAMES z3 + PATHS /usr/local/include/z3/build ENV PATH INCLUDE + ) + +find_program(Z3_EXEC + NAMES z3 + PATHS ENV PATH INCLUDE) + +# set up the final variables +set(Z3_LIBRARIES ${Z3_LIBRARY}) +set(Z3_INCLUDE_DIRS ${Z3_INCLUDE_DIR}/src/util) +set(Z3_SOLVER ${Z3_EXEC}) + +# set the LIBZ3_FOUND variable by utilizing the following macro +# (which also handles the REQUIRED and QUIET arguments) +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(z3 DEFAULT_MSG + Z3_LIBRARY Z3_INCLUDE_DIR) + +IF (NOT Z3_FIND_QUIETLY) + MESSAGE(STATUS "Found Z3: ${Z3_LIBRARY}") +ENDIF (NOT Z3_FIND_QUIETLY) + +# debug output to see if everything went well +#message(${Z3_INCLUDE_DIR}) +#message(${Z3_LIBRARY}) + +# make the set variables only visible in advanced mode +mark_as_advanced(Z3_LIBRARY Z3_INCLUDE_DIR Z3_SOLVER) \ No newline at end of file diff --git a/storm-config.h.in b/storm-config.h.in index 94de0014e..edab04fa6 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -15,22 +15,22 @@ #define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" // Whether Gurobi is available and to be used (define/undef) -#@STORM_CPP_GUROBI_DEF@ STORM_HAVE_GUROBI +#cmakedefine STORM_HAVE_GUROBI // Whether CUDA is available (define/undef) #@STORM_CPP_CUDA_DEF@ STORM_HAVE_CUDA // Whether GLPK is available and to be used (define/undef) -#@STORM_CPP_GLPK_DEF@ STORM_HAVE_GLPK +#cmakedefine STORM_HAVE_GLPK // Whether CudaForStorm is available and to be used (define/undef) #@STORM_CPP_CUDAFORSTORM_DEF@ STORM_HAVE_CUDAFORSTORM // Whether Z3 is available and to be used (define/undef) -#@STORM_CPP_Z3_DEF@ STORM_HAVE_Z3 +#cmakedefine STORM_HAVE_Z3 // Whether MathSAT is available and to be used (define/undef) -#@STORM_CPP_MSAT_DEF@ STORM_HAVE_MSAT +#cmakedefine STORM_HAVE_MSAT // Whether Intel Threading Building Blocks are available and to be used (define/undef) #@STORM_CPP_INTELTBB_DEF@ STORM_HAVE_INTELTBB