moves-rwth · volkm · Jan 16, 2025 · Jan 16, 2025 · Jan 16, 2025 · Jan 17, 2025
diff --git a/.github/workflows/Dockerfile.archlinux b/.github/workflows/Dockerfile.archlinux
@@ -16,6 +16,7 @@ ARG no_threads=1
 
 # Specify Storm configuration (ON/OFF)
 ARG gurobi_support="ON"
+ARG mathsat_support="ON"
 ARG soplex_support="ON"
 ARG spot_support="ON"
 ARG developer="OFF"
@@ -51,6 +52,7 @@ WORKDIR /opt/storm/build
 RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \
              -DSTORM_PORTABLE=ON \
              -DSTORM_USE_GUROBI=$gurobi_support \
+             -DSTORM_USE_MATHSAT=$mathsat_support \
              -DSTORM_USE_SOPLEX=$soplex_support \
              -DSTORM_USE_SPOT_SYSTEM=$spot_support \
              -DSTORM_DEVELOPER=$developer \

diff --git a/.github/workflows/Dockerfile.doxygen b/.github/workflows/Dockerfile.doxygen
@@ -36,6 +36,7 @@ WORKDIR /opt/storm/build
 RUN cmake .. -DCMAKE_BUILD_TYPE=Release \
              -DSTORM_PORTABLE=ON \
              -DSTORM_USE_GUROBI=ON \
+             -DSTORM_USE_MATHSAT=ON \
              -DSTORM_USE_SOPLEX=ON \
              -DSTORM_USE_SPOT_SYSTEM=ON
 

diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml
@@ -26,61 +26,66 @@ jobs:
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "ON",
+             Mathsat: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "OFF",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5"
+             cmakeArgs: ""
             }
           - {name: "CLN exact; GMP rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "ON",
+             Mathsat: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
              ClnExact: "ON",
              ClnRatfunc: "OFF",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5"
+             cmakeArgs: ""
             }
           - {name: "CLN exact; CLN rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "ON",
+             Mathsat: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
              ClnExact: "ON",
              ClnRatfunc: "ON",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5"
+             cmakeArgs: ""
             }
           - {name: "GMP exact; CLN rational functions; No dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "ON",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT="
+             cmakeArgs: ""
             }
           - {name: "Minimal dependencies",
             baseImg: "storm-basesystem:minimal_dependencies",
             buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "ON",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT="
+             cmakeArgs: ""
             }
     steps:
       - name: Git clone
@@ -91,6 +96,7 @@ jobs:
             --build-arg BASE_IMG=movesrwth/${{ matrix.config.baseImg }} \
             --build-arg build_type="${{ matrix.config.buildType }}" \
             --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \
+            --build-arg mathsat_support="${{ matrix.config.Mathsat }}" \
             --build-arg soplex_support="${{ matrix.config.Soplex }}" \
             --build-arg spot_support="${{ matrix.config.Spot }}" \
             --build-arg developer="${{ matrix.config.Developer }}" \
@@ -129,6 +135,7 @@ jobs:
           - {name: "GCC",
              buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
@@ -138,6 +145,7 @@ jobs:
           - {name: "Clang",
              buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
@@ -154,6 +162,7 @@ jobs:
           docker build -t movesrwth/storm:ci . \
             --build-arg build_type="${{ matrix.config.buildType }}" \
             --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \
+            --build-arg mathsat_support="${{ matrix.config.Mathsat }}" \
             --build-arg soplex_support="${{ matrix.config.Soplex }}" \
             --build-arg spot_support="${{ matrix.config.Spot }}" \
             --build-arg developer="${{ matrix.config.Developer }}" \
@@ -196,6 +205,7 @@ jobs:
             --build-arg BASE_IMG=movesrwth/storm-basesystem:${{ matrix.distro }} \
             --build-arg build_type="${{ matrix.buildType }}" \
             --build-arg gurobi_support="OFF" \
+            --build-arg mathsat_support="OFF" \
             --build-arg soplex_support="OFF" \
             --build-arg spot_support="OFF" \
             --build-arg no_threads=${NR_JOBS}
@@ -251,7 +261,7 @@ jobs:
             --build-arg developer="${{ matrix.buildType.Developer }}" \
             --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \
             --build-arg no_threads=${NR_JOBS}
-            # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
+            # Omitting arguments gurobi_support, mathsat_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
       - name: Run Docker
         run: docker run -d -it --name ci movesrwth/storm:${{ matrix.buildType.dockerTag }}
 

diff --git a/.github/workflows/release_docker.yml b/.github/workflows/release_docker.yml
@@ -39,7 +39,7 @@ jobs:
             --build-arg developer="${{ matrix.buildType.Developer }}" \
             --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \
             --build-arg no_threads=${NR_JOBS}
-            # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
+            # Omitting arguments gurobi_support, mathsat_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
       - name: Login to Docker Hub
         # Only login if using original repo
         if: github.repository_owner == 'moves-rwth'

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -23,66 +23,80 @@ include(ProcessorCount)
 ##	CMake options of Storm
 ##
 #############################################################
+# Build options
 option(STORM_DEVELOPER "Sets whether the development mode is used." OFF)
+option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF)
 option(STORM_ALLWARNINGS "Compile with even more warnings" OFF)
+option(STORM_EXCLUDE_TESTS_FROM_ALL "If set, tests will not be compiled by default" OFF )
+export_option(STORM_EXCLUDE_TESTS_FROM_ALL)
+MARK_AS_ADVANCED(STORM_EXCLUDE_TESTS_FROM_ALL)
+option(STORM_PORTABLE "Sets whether a build needs to be portable." OFF)
+MARK_AS_ADVANCED(STORM_PORTABLE)
+# Force POPCNT is helpful for portable code targeting platforms with SSE4.2 operation support.
+option(STORM_FORCE_POPCNT "Sets whether the popcnt instruction is forced to be used." OFF)
+MARK_AS_ADVANCED(STORM_FORCE_POPCNT)
+option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF)
+option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON)
+mark_as_advanced(STORM_COMPILE_WITH_CCACHE)
 option(STORM_USE_LTO "Sets whether link-time optimizations are enabled." ON)
 MARK_AS_ADVANCED(STORM_USE_LTO)
 option(STORM_USE_THIN_LTO "Sets whether thin link-time optimizations are enabled (faster compile times than normal LTO)." OFF)
 MARK_AS_ADVANCED(STORM_USE_THIN_LTO)
-option(STORM_PORTABLE "Sets whether a build needs to be portable." OFF)
-MARK_AS_ADVANCED(STORM_PORTABLE)
-# Force POPCNT is helpful for portable code targetting platforms with SSE4.2 operation support.
-option(STORM_FORCE_POPCNT "Sets whether the popcnt instruction is forced to be used (advanced)." OFF)
-MARK_AS_ADVANCED(STORM_FORCE_POPCNT)
-option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF)
-option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF)
-option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF)
-option(STORM_USE_SOPLEX "Sets whether Soplex should be used." OFF)
-set(STORM_CARL_DIR_HINT "" CACHE STRING "A hint where the preferred CArL version can be found. If CArL cannot be found there, it is searched in the OS's default paths.")
-option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of carl is to be used no matter whether carl is found or not." OFF)
-MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL)
-option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF)
-mark_as_advanced(USE_SMTRAT)
-option(STORM_USE_SPOT_SYSTEM "Sets whether the system version of Spot should be included (if found)." ON)
-option(STORM_USE_SPOT_SHIPPED "Sets whether Spot should be downloaded and installed (if system version is not available or not used)." OFF)
-option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON)
+option(STORM_COMPILE_WITH_ADDRESS_SANITIZER "Sets whether to compile with AddressSanitizer enabled" OFF)
+option(STORM_COMPILE_WITH_ALL_SANITIZERS "Sets whether to compile with all sanitizers enabled" OFF)
+option(STORM_COMPILE_WITH_COMPILATION_PROFILING "Compile with output to profile compilation process" OFF)
+MARK_AS_ADVANCED(STORM_COMPILE_WITH_COMPILATION_PROFILING)
 option(FORCE_COLOR "Force color output" OFF)
 mark_as_advanced(FORCE_COLOR)
-option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON)
-mark_as_advanced(STORM_COMPILE_WITH_CCACHE)
-option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF)
+
+# Configuration options
 option(STORM_USE_CLN_EA "Sets whether CLN instead of GMP numbers should be used for exact arithmetic." OFF)
 export_option(STORM_USE_CLN_EA)
 option(STORM_USE_CLN_RF "Sets whether CLN instead of GMP numbers should be used for rational functions." ON)
 export_option(STORM_USE_CLN_RF)
-option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF)
+
+# Dependencies
+set(STORM_CARL_DIR_HINT "" CACHE STRING "A hint where the preferred CArL version can be found. If CArL cannot be found there, it is searched in the OS's default paths.")
+option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of CArL is to be used no matter whether CArL is found or not." OFF)
+MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL)
+option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF)
+set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).")
+MARK_AS_ADVANCED(BOOST_ROOT)
 option(STORM_DEBUG_CUDD "Build CUDD in debug mode." OFF)
 MARK_AS_ADVANCED(STORM_DEBUG_CUDD)
-option(STORM_EXCLUDE_TESTS_FROM_ALL "If set, tests will not be compiled by default" OFF )
-export_option(STORM_EXCLUDE_TESTS_FROM_ALL)
-MARK_AS_ADVANCED(STORM_EXCLUDE_TESTS_FROM_ALL)
-set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).")
+# CUDD is shipped
+# ExprTk is shipped
+# GLPK is shipped
+option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF)
 set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).")
-set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
-set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).")
-set(SPOT_ROOT "" CACHE STRING "The hint to the root directory of Spot (optional).")
+MARK_AS_ADVANCED(GUROBI_ROOT)
+# Eigen is shipped
+option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF)
+option(STORM_USE_MATHSAT "Sets whether MathSAT should be used." OFF)
+set(MATHSAT_ROOT "" CACHE STRING "A hint to the root directory of MathSAT (optional).")
+MARK_AS_ADVANCED(MATHSAT_ROOT)
+option(STORM_USE_SMTRAT "Sets whether SMT-RAT should be included." OFF)
+mark_as_advanced(STORM_USE_SMTRAT)
+set(SMTRAT_ROOT "" CACHE STRING "A hint to the root directory of SMT-RAT (optional).")
+MARK_AS_ADVANCED(SMTRAT_ROOT)
+option(STORM_USE_SOPLEX "Sets whether Soplex should be used." OFF)
+set(SOPLEX_ROOT "" CACHE STRING "A hint to the root directory of Soplex (optional).")
+MARK_AS_ADVANCED(SOPLEX_ROOT)
+option(STORM_USE_SPOT_SYSTEM "Sets whether the system version of Spot should be included (if found)." ON)
+option(STORM_USE_SPOT_SHIPPED "Sets whether Spot should be downloaded and installed (if system version is not available or not used)." OFF)
+set(SPOT_ROOT "" CACHE STRING "A hint to the root directory of Spot (optional).")
 MARK_AS_ADVANCED(SPOT_ROOT)
+option(STORM_USE_XERCES "Sets whether Xerces should be included." ON)
+set(XERCESC_ROOT "" CACHE STRING "A hint to the root directory of Xerces (optional).")
+MARK_AS_ADVANCED(XERCESC_ROOT)
+set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
+MARK_AS_ADVANCED(Z3_ROOT)
 option(STORM_LOAD_QVBS "Sets whether the Quantitative Verification Benchmark Set (QVBS) should be downloaded." OFF)
 set(STORM_QVBS_ROOT "" CACHE STRING "The root directory of the Quantitative Verification Benchmark Set (QVBS) in case it should not be downloaded (optional).")
 MARK_AS_ADVANCED(STORM_QVBS_ROOT)
 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(USE_XERCESC ${XML_SUPPORT})
-mark_as_advanced(USE_XERCESC)
-option(STORM_COMPILE_WITH_ADDRESS_SANITIZER "Sets whether to compile with AddressSanitizer enabled" OFF)
-option(STORM_COMPILE_WITH_ALL_SANITIZERS "Sets whether to compile with all sanitizers enabled" OFF)
-option(STORM_COMPILE_WITH_COMPILATION_PROFILING "Compile with output to profile compilation process" OFF)
-MARK_AS_ADVANCED(STORM_COMPILE_WITH_COMPILATION_PROFILING)
-
 
-if (STORM_COMPILE_WITH_ALL_SANITIZERS)
-    set(STORM_COMPILE_WITH_ADDRESS_SANITIZER ON)
-endif()
 
 # Get an approximation of the number of available processors (used for parallel build of shipped resources)
 ProcessorCount(STORM_RESOURCES_BUILD_JOBCOUNT_DEFAULT)
@@ -333,6 +347,10 @@ else()
     message(STATUS "Storm - Disabling link-time optimizations.")
 endif()
 
+if (STORM_COMPILE_WITH_ALL_SANITIZERS)
+	set(STORM_COMPILE_WITH_ADDRESS_SANITIZER ON)
+endif()
+
 if (STORM_COMPILE_WITH_ADDRESS_SANITIZER)
     message(STATUS "Storm - Enabling AddressSanitizer")
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fsanitize=address")
@@ -390,7 +408,6 @@ if (STORM_DEVELOPER)
 			# Requires adapter for gmock
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-undef")
 
-
 			# Conflicts with warnings in gcc
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unreachable-code-return")
 
@@ -414,9 +431,6 @@ if (STORM_DEVELOPER)
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-documentation-unknown-command")
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-noreturn")
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-prototypes")
-
-
-
 		endif ()
 	else ()
 	    set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra")

diff --git a/Dockerfile b/Dockerfile
@@ -21,6 +21,7 @@ ARG no_threads=1
 
 # Specify Storm configuration (ON/OFF)
 ARG gurobi_support="ON"
+ARG mathsat_support="ON"
 ARG soplex_support="ON"
 ARG spot_support="ON"
 ARG developer="OFF"
@@ -48,6 +49,7 @@ WORKDIR /opt/storm/build
 RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \
              -DSTORM_PORTABLE=ON \
              -DSTORM_USE_GUROBI=$gurobi_support \
+             -DSTORM_USE_MATHSAT=$mathsat_support \
              -DSTORM_USE_SOPLEX=$soplex_support \
              -DSTORM_USE_SPOT_SYSTEM=$spot_support \
              -DSTORM_DEVELOPER=$developer \