Finding z3 in system, cleaned some cmakelists.

Former-commit-id: 67ab9f7a0c

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)
 
 #############################################################
@@ -560,9 +533,6 @@ 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/")
 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)

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)

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