diff --git a/CMakeLists.txt b/CMakeLists.txt index 57e94b8b8..73be3c249 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -43,7 +43,8 @@ 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) -option(STORM_USE_CLN_NUMBERS "Sets whether CLN or GMP numbers should be used" ON) +option(STORM_USE_CLN_EA "Sets whether CLN or GMP numbers should be used for exact arithmetic." OFF) +option(STORM_USE_CLN_RF "Sets whether CLN or GMP numbers should be used for rational functions." ON) option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF) set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).") set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index b468ae4b3..b8ce069b2 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -76,7 +76,7 @@ foreach(BOOSTLIB ${Boost_LIBRARIES}) list(APPEND STORM_DEP_TARGETS target-boost-${CNTVAR}_SHARED) MATH(EXPR CNTVAR "${CNTVAR}+1") endforeach() -message(STATUS "storm - Using boost ${Boost_VERSION} (library version ${Boost_LIB_VERSION}).") +message(STATUS "Storm - Using boost ${Boost_VERSION} (library version ${Boost_LIB_VERSION}).") # set the information for the config header set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}") @@ -87,7 +87,7 @@ set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}") ############################################################# # Use the shipped version of ExprTK -message (STATUS "storm - Including ExprTk.") +message (STATUS "Storm - Including ExprTk.") add_imported_library_interface(ExprTk "${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk") list(APPEND STORM_DEP_TARGETS ExprTk) @@ -98,7 +98,7 @@ list(APPEND STORM_DEP_TARGETS ExprTk) ############################################################# # Use the shipped version of Sparsepp -message (STATUS "storm - Including Sparsepp.") +message (STATUS "Storm - Including Sparsepp.") include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/sparsepp") # Add sparsepp.h to the headers that are copied to the include directory in thebuild directory. @@ -117,7 +117,7 @@ list(APPEND STORM_RESOURCES_HEADERS "${CMAKE_BINARY_DIR}/include/resources/3rdpa ############################################################# #use the shipped version of modernjson -message (STATUS "storm - Including ModernJSON.") +message (STATUS "Storm - Including ModernJSON.") add_imported_library_interface(ModernJSON "${PROJECT_SOURCE_DIR}/resources/3rdparty/modernjson/src/") list(APPEND STORM_DEP_TARGETS ModernJSON) @@ -148,9 +148,9 @@ if(Z3_FOUND) endif() if(STORM_HAVE_Z3_OPTIMIZE) - message (STATUS "storm - Linking with Z3. (Z3 version supports optimization)") + message (STATUS "Storm - Linking with Z3. (Z3 version supports optimization)") else() - message (STATUS "storm - Linking with Z3. (Z3 version does not support optimization)") + message (STATUS "Storm - Linking with Z3. (Z3 version does not support optimization)") endif() add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS}) @@ -175,7 +175,7 @@ if (STORM_USE_GUROBI) find_package(Gurobi QUIET REQUIRED) set(STORM_HAVE_GUROBI ${GUROBI_FOUND}) if (GUROBI_FOUND) - message (STATUS "storm - Linking with Gurobi.") + message (STATUS "Storm - Linking with Gurobi.") add_imported_library(Gurobi "" ${GUROBI_LIBRARY} ${GUROBI_INCLUDE_DIRS}) list(APPEND STORM_DEP_TARGETS Gurobi) endif() @@ -211,8 +211,8 @@ if(USE_CARL) if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) set(STORM_SHIPPED_CARL OFF) set(STORM_HAVE_CARL ON) - message(STATUS "storm - Use system version of carl.") - message(STATUS "storm - Linking with carl ${carl_VERSION} (CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}).") + message(STATUS "Storm - Use system version of carl.") + message(STATUS "Storm - Linking with carl ${carl_VERSION} (CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}).") set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) else() set(STORM_SHIPPED_CARL ON) @@ -220,7 +220,7 @@ if(USE_CARL) message("START CARL CONFIG PROCESS") file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) execute_process( - COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" + COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON" WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download OUTPUT_VARIABLE carlconfig_out RESULT_VARIABLE carlconfig_result) @@ -239,7 +239,7 @@ if(USE_CARL) endif() message("END CARL CONFIG PROCESS") - message(STATUS "storm - Using shipped version of carl.") + message(STATUS "Storm - Using shipped version of carl.") ExternalProject_Add( carl SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl @@ -262,8 +262,8 @@ if(USE_CARL) # install the carl dynamic library if we build it install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.1.0.0${DYNAMIC_EXT} DESTINATION lib) endif() - if(STORM_USE_CLN_NUMBERS AND NOT STORM_HAVE_CLN) - message(FATAL_ERROR "Cannot use CLN numbers if carl is build without") + if(STORM_USE_CLN_RF AND NOT STORM_HAVE_CLN) + message(FATAL_ERROR "Cannot use CLN numbers if carl is build without.") endif() list(APPEND STORM_DEP_IMP_TARGETS lib_carl) @@ -281,11 +281,11 @@ if(USE_SMTRAT) find_package(smtrat QUIET REQUIRED) if(smtrat_FOUND) set(STORM_HAVE_SMTRAT ON) - message(STATUS "storm - Linking with smtrat.") + message(STATUS "Storm - Linking with smtrat.") include_directories("${smtrat_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES}) else() - message(FATAL_ERROR "storm - SMT-RAT was requested but not found") + message(FATAL_ERROR "Storm - SMT-RAT was requested but not found") endif() endif() @@ -301,24 +301,39 @@ if(USE_HYPRO) find_package(hypro QUIET REQUIRED) if(hypro_FOUND) set(STORM_HAVE_HYPRO ON) - message(STATUS "storm - Linking with hypro.") + message(STATUS "Storm - Linking with hypro.") include_directories("${hypro_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES ${hypro_LIBRARIES}) else() - message(FATAL_ERROR "storm - HyPro was requested but not found") + message(FATAL_ERROR "Storm - HyPro was requested but not found") endif() endif() - - ############################################################# ## ## gmp ## ############################################################# -# GMP is optional (unless MathSAT is used, see below) -find_package(GMP QUIET) +if (NOT STORM_USE_CLN_EA OR NOT "${MSAT_ROOT}" STREQUAL "") + find_package(GMP QUIET REQUIRED) +else() + # GMP is optional in this case + find_package(GMP QUIET) +endif() + +if(GMP_FOUND) + set(STORM_HAVE_GMP ON) + message(STATUS "Storm - Linking with gmp.") + include_directories("${GMP_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${GMP_LIBRARY}) +elseif(MPIR_FOUND) + set(STORM_HAVE_GMP ON) + message(STATUS "Storm - Linking with mpir (gmp).") + include_directories("${GMP_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIR_LIBRARY}) + list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIRXX_LIBRARY}) +endif(GMP_FOUND) ############################################################# ## @@ -335,20 +350,10 @@ endif() # MathSAT Defines set(STORM_HAVE_MSAT ${ENABLE_MSAT}) if (ENABLE_MSAT) - message (STATUS "storm - Linking with MathSAT.") + message (STATUS "Storm - Linking with MathSAT.") link_directories("${MSAT_ROOT}/lib") include_directories("${MSAT_ROOT}/include") list(APPEND STORM_LINK_LIBRARIES "mathsat") - if(GMP_FOUND) - include_directories("${GMP_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${GMP_LIBRARY}) - elseif(MPIR_FOUND) - include_directories("${GMP_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIR_LIBRARY}) - list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIRXX_LIBRARY}) - else(GMP_FOUND) - message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") - endif(GMP_FOUND) endif(ENABLE_MSAT) ############################################################# @@ -386,8 +391,8 @@ ExternalProject_Get_Property(sylvan source_dir) ExternalProject_Get_Property(sylvan binary_dir) set(Sylvan_INCLUDE_DIR "${source_dir}/src") set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan${STATIC_EXT}") -message(STATUS "storm - Using shipped version of sylvan.") -message(STATUS "storm - Linking with sylvan.") +message(STATUS "Storm - Using shipped version of sylvan.") +message(STATUS "Storm - Linking with sylvan.") add_imported_library(sylvan STATIC ${Sylvan_LIBRARY} ${Sylvan_INCLUDE_DIR}) add_dependencies(sylvan_STATIC sylvan) if(STORM_SHIPPED_CARL) @@ -397,7 +402,7 @@ list(APPEND STORM_DEP_TARGETS sylvan_STATIC) find_package(Hwloc QUIET REQUIRED) if(HWLOC_FOUND) - message(STATUS "storm - Linking with hwloc ${HWLOC_VERSION}.") + message(STATUS "Storm - Linking with hwloc ${HWLOC_VERSION}.") add_imported_library(hwloc STATIC ${HWLOC_LIBRARIES} "") list(APPEND STORM_DEP_TARGETS hwloc_STATIC) else() @@ -453,14 +458,14 @@ if (STORM_USE_INTELTBB) find_package(TBB QUIET REQUIRED) if (TBB_FOUND) - message(STATUS "storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") - message(STATUS "storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") + message(STATUS "Storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") + message(STATUS "Storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") set(STORM_HAVE_INTELTBB ON) link_directories(${TBB_LIBRARY_DIRS}) include_directories(${TBB_INCLUDE_DIRS}) list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc) else(TBB_FOUND) - message(FATAL_ERROR "storm - TBB was requested, but not found.") + message(FATAL_ERROR "Storm - TBB was requested, but not found.") endif(TBB_FOUND) endif(STORM_USE_INTELTBB) @@ -472,7 +477,7 @@ endif(STORM_USE_INTELTBB) find_package(Threads QUIET REQUIRED) if (NOT Threads_FOUND) - message(FATAL_ERROR "storm - Threads was requested, but not found.") + message(FATAL_ERROR "Storm - Threads was requested, but not found.") endif() include_directories(${THREADS_INCLUDE_DIRS}) list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT}) @@ -512,11 +517,11 @@ if(ENABLE_CUDA) COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR ) if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT) - message(FATAL_ERROR "storm (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") + message(FATAL_ERROR "Storm (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0) - message(STATUS "storm (CudaPlugin) - Result of Type Alignment Check: OK.") + message(STATUS "Storm (CudaPlugin) - Result of Type Alignment Check: OK.") else() - message(FATAL_ERROR "storm (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})") + message(FATAL_ERROR "Storm (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})") endif() # Test for Float 64bit Alignment @@ -525,15 +530,15 @@ if(ENABLE_CUDA) COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR ) if(NOT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT) - message(FATAL_ERROR "storm (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") + message(FATAL_ERROR "Storm (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 2) - message(STATUS "storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.") + message(STATUS "Storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.") set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "define") elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 3) - message(STATUS "storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.") + message(STATUS "Storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.") set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "undef") else() - message(FATAL_ERROR "storm (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})") + message(FATAL_ERROR "Storm (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})") endif() # # Make a version file containing the current version from git. @@ -552,7 +557,7 @@ if(ENABLE_CUDA) else() set(STORM_CUDAPLUGIN_VERSION_DIRTY 0) endif() - message(STATUS "storm (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})") + message(STATUS "Storm (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})") # Configure a header file to pass some of the CMake settings to the source code @@ -586,9 +591,9 @@ if(ENABLE_CUDA) if(CUSP_FOUND) include_directories(${CUSP_INCLUDE_DIR}) cuda_include_directories(${CUSP_INCLUDE_DIR}) - message(STATUS "storm (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}.") + message(STATUS "Storm (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}.") else() - message(FATAL_ERROR "storm (CudaPlugin) - Could not find CUSP.") + message(FATAL_ERROR "Storm (CudaPlugin) - Could not find CUSP.") endif() ############################################################# @@ -599,9 +604,9 @@ if(ENABLE_CUDA) if(THRUST_FOUND) include_directories(${THRUST_INCLUDE_DIR}) cuda_include_directories(${THRUST_INCLUDE_DIR}) - message(STATUS "storm (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}.") + message(STATUS "Storm (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}.") else() - message(FATAL_ERROR "storm (CudaPlugin) - Could not find Thrust. Check your CUDA installation.") + message(FATAL_ERROR "Storm (CudaPlugin) - Could not find Thrust. Check your CUDA installation.") endif() include_directories(${CUDA_INCLUDE_DIRS}) @@ -611,7 +616,7 @@ if(ENABLE_CUDA) ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES} ) - message (STATUS "storm - Linking with CUDA.") + message (STATUS "Storm - Linking with CUDA.") list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME}) include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") endif() diff --git a/resources/3rdparty/sylvan/src/CMakeLists.txt b/resources/3rdparty/sylvan/src/CMakeLists.txt index d91263353..0c516c483 100755 --- a/resources/3rdparty/sylvan/src/CMakeLists.txt +++ b/resources/3rdparty/sylvan/src/CMakeLists.txt @@ -13,8 +13,9 @@ set(SOURCES sylvan_sl.c sylvan_stats.c sylvan_table.c - storm_function_wrapper.cpp + storm_wrapper.cpp sylvan_storm_rational_function.c + sylvan_storm_rational_number.c ) set(HEADERS @@ -35,8 +36,9 @@ set(HEADERS sylvan_stats.h sylvan_table.h sylvan_tls.h - storm_function_wrapper.h + storm_wrapper.h sylvan_storm_rational_function.h + sylvan_storm_rational_number.h ) option(BUILD_SHARED_LIBS "Enable/disable creation of shared libraries" ON) diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp deleted file mode 100644 index c4c6f3dcb..000000000 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp +++ /dev/null @@ -1,475 +0,0 @@ -#include "storm_function_wrapper.h" - -#include -#include -#include -#include -#include -#include - -#include "storm/adapters/CarlAdapter.h" -#include "storm/utility/constants.h" -#include "sylvan_storm_rational_function.h" - -#include "storm/exceptions/InvalidOperationException.h" - -#include -#include -#include -#include - -std::mutex carlMutex; - -void storm_rational_function_init(storm_rational_function_ptr* a) { - std::lock_guard lock(carlMutex); - { - storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); - - if (srf_ptr == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl; - return; - } - - *a = srf_ptr; - } -} - -void storm_rational_function_destroy(storm_rational_function_ptr a) { - std::lock_guard lock(carlMutex); - { - storm::RationalFunction* srf = (storm::RationalFunction*)a; - delete srf; - } -} - -int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - int result = 0; - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - - if (srf_a == srf_b) { - result = 1; - } - } - - return result; -} - -storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl; - return result; - } - - *result_srf += srf_b; - result = (storm_rational_function_ptr)result_srf; - } - - return result; -} - -storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl; - return result; - } - - *result_srf -= srf_b; - result = (storm_rational_function_ptr)result_srf; - } - return result; -} - -storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl; - return result; - } - - *result_srf *= srf_b; - result = (storm_rational_function_ptr)result_srf; - } - return result; -} - -storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; - return result; - } - - *result_srf /= srf_b; - result = (storm_rational_function_ptr)result_srf; - } - return result; -} - -storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - - uint64_t exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); - storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; - return result; - } - result = (storm_rational_function_ptr)result_srf; - } - return result; -} - -storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { - throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be rational function."; - } - throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rationals."; - - // storm::RationalFunction* result_srf = new storm::RationalFunction(carl::mod(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); -// if (result_srf == nullptr) { -// std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; -// return result; -// } -// result = (storm_rational_function_ptr)result_srf; - - } - return result; -} - -storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { - throw storm::exceptions::InvalidOperationException() << "Operands of min must not be rational function."; - } - - storm::RationalFunction* result_srf = new storm::RationalFunction(std::min(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; - return result; - } - result = (storm_rational_function_ptr)result_srf; - - } - return result; -} - -storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { - throw storm::exceptions::InvalidOperationException() << "Operands of max must not be rational function."; - } - - storm::RationalFunction* result_srf = new storm::RationalFunction(std::max(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; - return result; - } - result = (storm_rational_function_ptr)result_srf; - } - return result; -} - -int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { - throw storm::exceptions::InvalidOperationException() << "Operands of less must not be rational functions."; - } - - if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) { - return 1; - } else { - return 0; - } - return -1; -} - -int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b) { - std::lock_guard lock(carlMutex); - - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { - throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be rational functions."; - } - if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) { - return 1; - } else { - return 0; - } - - return -1; -} - -uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { - std::lock_guard lock(carlMutex); - - uint64_t result = seed; - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - // carl::hash_add(result, srf_a); - result = seed ^ (carl::hash_value(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); - } - return result; -} - -storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; - return result; - } - - *result_srf = -srf_a; - result = (storm_rational_function_ptr)result_srf; - } - return result; -} - -storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - if (!storm::utility::isInteger(srf_a)) { - throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be rational function."; - } - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; - return result; - } - - *result_srf = storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber())); - result = (storm_rational_function_ptr)result_srf; - - } - return result; -} - -storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - if (!storm::utility::isInteger(srf_a)) { - throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be rational function."; - } - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; - return result; - } - - *result_srf = storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber())); - result = (storm_rational_function_ptr)result_srf; - } - return result; -} - -int storm_rational_function_is_zero(storm_rational_function_ptr a) { - std::lock_guard lock(carlMutex); - - bool resultIsZero = false; - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - resultIsZero = srf_a.isZero(); - } - - if (resultIsZero) { - return 1; - } else { - return 0; - } -} - -double storm_rational_function_get_constant(storm_rational_function_ptr a) { - std::lock_guard lock(carlMutex); - - double result = -1.0; - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - - if (srf_a.isConstant()) { - result = carl::toDouble(storm::RationalNumber(srf_a.nominatorAsNumber() / srf_a.denominatorAsNumber())); - } else { - std::cout << "Defaulting to -1.0 since this is not a constant: " << srf_a << std::endl; - } - } - return result; -} - -storm_rational_function_ptr storm_rational_function_get_zero() { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction* result_srf = new storm::RationalFunction(0); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_get_zero()!" << std::endl; - return result; - } - result = (storm_rational_function_ptr)result_srf; - } - - return result; -} - -storm_rational_function_ptr storm_rational_function_get_one() { - std::lock_guard lock(carlMutex); - storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - - { - storm::RationalFunction* result_srf = new storm::RationalFunction(1); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_get_one()!" << std::endl; - return result; - } - result = (storm_rational_function_ptr)result_srf; - } - - return result; -} - -void print_storm_rational_function(storm_rational_function_ptr a) { - std::lock_guard lock(carlMutex); - { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - std::cout << srf_a << std::flush; - } -} - -void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { - std::lock_guard lock(carlMutex); - { - std::stringstream ss; - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - ss << srf_a; - std::string s = ss.str(); - fprintf(out, "%s", s.c_str()); - } -} - -MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map>> const& replacements) { - if (currentFunction.isConstant()) { - return mtbdd_storm_rational_function((storm_rational_function_ptr)¤tFunction); - } - - std::set variablesInFunction = currentFunction.gatherVariables(); - std::map>>::const_iterator it = replacements.cbegin(); - std::map>>::const_iterator end = replacements.cend(); - - // Walking the (ordered) map enforces an ordering on the MTBDD - for (; it != end; ++it) { - if (variablesInFunction.find(it->second.first) != variablesInFunction.cend()) { - std::map highReplacement = {{it->second.first, it->second.second.first}}; - std::map lowReplacement = {{it->second.first, it->second.second.second}}; - - std::lock_guard* lock = new std::lock_guard(carlMutex); - storm::RationalFunction const highSrf = currentFunction.substitute(highReplacement); - storm::RationalFunction const lowSrf = currentFunction.substitute(lowReplacement); - delete lock; - - MTBDD high = testiTest(highSrf, replacements); - MTBDD low = testiTest(lowSrf, replacements); - LACE_ME - return mtbdd_ite(mtbdd_ithvar(it->first), high, low); - } else { - //std::cout << "No match for variable " << it->second.first << std::endl; - } - } - - return mtbdd_storm_rational_function((storm_rational_function_ptr)¤tFunction); -} - - -MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - { - // Scope the lock. - std::lock_guard lock(carlMutex); - if (srf_a.isConstant()) { - return dd; - } - } - - std::map>>* replacements = (std::map>>*)context; - return testiTest(srf_a, *replacements); -} - -char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen) { - std::lock_guard lock(carlMutex); - std::stringstream ss; - storm::RationalFunction& srf_a = *(storm::RationalFunction*)val; - ss << srf_a; - std::string s = ss.str(); - char* result = (char*)malloc(s.size() + 1); - std::memcpy(result, s.c_str(), s.size() + 1); - return result; -} diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h deleted file mode 100644 index fe51d982f..000000000 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.h +++ /dev/null @@ -1,58 +0,0 @@ -#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H -#define SYLVAN_STORM_FUNCTION_WRAPPER_H - -#include -#include -#include - -#ifdef __cplusplus -extern "C" { -#endif - -typedef void* storm_rational_function_ptr; - -// basic functions (for sylvan) -void storm_rational_function_init(storm_rational_function_ptr* a); -void storm_rational_function_destroy(storm_rational_function_ptr a); -int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b); - -// binary -storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b); -storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b); -storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b); -storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b); -storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b); - -storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b); -storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b); -storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b); - -int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b); -int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b); - -// unary -storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a); - -storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a); -storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a); - -uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); -int storm_rational_function_is_zero(storm_rational_function_ptr a); - -storm_rational_function_ptr storm_rational_function_get_zero(); -storm_rational_function_ptr storm_rational_function_get_one(); - -void print_storm_rational_function(storm_rational_function_ptr a); -void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); - -MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context); - -double storm_rational_function_get_constant(storm_rational_function_ptr a); - -char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen); - -#ifdef __cplusplus -} -#endif - -#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp new file mode 100644 index 000000000..da2e94f71 --- /dev/null +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -0,0 +1,612 @@ +#include "storm_wrapper.h" + +#include +#include +#include +#include +#include +#include + +#include "storm/adapters/CarlAdapter.h" +#include "storm/utility/constants.h" +#include "storm/exceptions/InvalidOperationException.h" + +#include +#include +#include +#include + +// TODO: remove and replace by proper detection in cmake +#define RATIONAL_NUMBER_THREAD_SAFE + +// A mutex that is used to lock all operations accessing rational numbers as they are not necessarily thread-safe. +#ifndef RATIONAL_NUMBER_THREAD_SAFE +std::mutex rationalNumberMutex; +#endif + +// A mutex that is used to lock all operations accessing rational functions as carl is not necessarily thread-safe. +#ifndef RATIONAL_FUNCTION_THREAD_SAFE +std::mutex rationalFunctionMutex; +#endif + +/*************************************************** + Function-wrappers for storm::RationalNumber + ****************************************************/ + +void storm_rational_number_init(storm_rational_number_ptr* a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*((storm::RationalNumber*)(*a))); + *a = srn_ptr; +} + +void storm_rational_number_destroy(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalFunction* srn_ptr = (storm::RationalFunction*)a; + delete srn_ptr; +} + +int storm_rational_number_equals(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber*)b; + + return (srn_a == srn_b) ? 1 : 0; +} + +char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, size_t buflen) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + std::stringstream ss; + storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val; + ss << srn_a; + std::string s = ss.str(); + if (s.size() < buflen + 1) { + std::memcpy(buf, s.c_str(), s.size() + 1); + return buf; + } else { + char* result = (char*)malloc(s.size() + 1); + std::memcpy(result, s.c_str(), s.size() + 1); + return result; + } +} + +storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber* result_srn = new storm::RationalNumber(*((storm::RationalNumber const*)a)); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_get_zero() { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero()); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_get_one() { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one()); + return (storm_rational_number_ptr)result_srn; +} + +int storm_rational_number_is_zero(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0; +} + +uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + + // Taken from boost::hash_combine that we do not call here for the lack of boost headers. + return seed ^ (std::hash()(srn_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); +} + +double storm_rational_number_get_value_double(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + return storm::utility::convertNumber(srn_a); +} + +storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + uint64_t exponentAsInteger = carl::toInt(srn_b); + storm::RationalNumber* result_srn = new storm::RationalNumber(carl::pow(srn_a, exponentAsInteger)); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational numbers."; +} + +storm_rational_number_ptr storm_rational_number_min(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + return storm_rational_number_less_or_equal(a, b) ? storm_rational_number_clone(a) : storm_rational_number_clone(b); +} + +storm_rational_number_ptr storm_rational_number_max(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + return storm_rational_number_less(a, b) ? storm_rational_number_clone(b) : storm_rational_number_clone(a); +} + + + + +int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + return srn_a < srn_b ? 1 : 0; +} + +int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_rational_number_ptr b) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + + return srn_a <= srn_b ? 1 : 0; +} + +storm_rational_number_ptr storm_rational_number_negate(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a)); + return (storm_rational_number_ptr)result_srn; +} + +storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a)); + return (storm_rational_number_ptr)result_srn; +} + + +void print_storm_rational_number(storm_rational_number_ptr a) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + std::cout << srn_a << std::flush; +} + +void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + std::stringstream ss; + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + ss << srn_a; + std::string s = ss.str(); + fprintf(out, "%s", s.c_str()); +} + +/*************************************************** + Function-wrappers for storm::RationalFunction + ****************************************************/ + +void storm_rational_function_init(storm_rational_function_ptr* a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); + *a = srf_ptr; +} + +void storm_rational_function_destroy(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction* srf = (storm::RationalFunction*)a; + delete srf; +} + +int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction*)b; + + return (srf_a == srf_b) ? 1 : 0; +} + +char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + std::stringstream ss; + storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val; + ss << srf_a; + std::string s = ss.str(); + if (s.size() < buflen + 1) { + std::memcpy(buf, s.c_str(), s.size() + 1); + return buf; + } else { + char* result = (char*)malloc(s.size() + 1); + std::memcpy(result, s.c_str(), s.size() + 1); + return result; + } +} + +storm_rational_function_ptr storm_rational_function_clone(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction* result_srf = new storm::RationalFunction(*((storm::RationalFunction const*)a)); + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_get_zero() { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero()); + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_get_one() { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one()); + return (storm_rational_function_ptr)result_srf; +} + +int storm_rational_function_is_zero(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + return storm::utility::isZero(*(storm::RationalFunction const*)a) ? 1 : 0; +} + +uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + + // Taken from boost::hash_combine that we do not call here for the lack of boost headers. + return seed ^ (carl::hash_value(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); +} + +double storm_rational_function_get_value_double(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + if (srf_a.isConstant()) { + return storm::utility::convertNumber(srf_a); + } else { + throw storm::exceptions::InvalidOperationException() << "Cannot evaluate rational function as it's not constant."; + } +} + +storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf += srf_b; + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf -= srf_b; + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf *= srf_b; + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf *= srf_b; + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + + uint64_t exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); + storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions."; + } + throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational functions."; +} + +storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + if (storm_rational_function_less_or_equal(a, b)) { + return storm_rational_function_clone(a); + } else { + return storm_rational_function_clone(b); + } +} + +storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + if (storm_rational_function_less(a, b)) { + return storm_rational_function_clone(b); + } else { + return storm_rational_function_clone(a); + } +} + +int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions."; + } + + if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) { + return 1; + } else { + return 0; + } + return -1; +} + +int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions."; + } + + if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) { + return 1; + } else { + return 0; + } + return -1; +} + +storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a); + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + if (!storm::utility::isInteger(srf_a)) { + throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function."; + } + storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber())); + return (storm_rational_function_ptr)result_srf; +} + +storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + if (!storm::utility::isInteger(srf_a)) { + throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function."; + } + storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber())); + return (storm_rational_function_ptr)result_srf; +} + + +void print_storm_rational_function(storm_rational_function_ptr a) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + std::cout << srf_a << std::flush; +} + +void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + std::stringstream ss; + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + ss << srf_a; + std::string s = ss.str(); + fprintf(out, "%s", s.c_str()); +} diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.h b/resources/3rdparty/sylvan/src/storm_wrapper.h new file mode 100644 index 000000000..537c33a40 --- /dev/null +++ b/resources/3rdparty/sylvan/src/storm_wrapper.h @@ -0,0 +1,102 @@ +#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H +#define SYLVAN_STORM_FUNCTION_WRAPPER_H + +#include +#include +#include + +#ifdef __cplusplus +extern "C" { +#endif + + /*************************************************** + Function-wrappers for storm::RationalNumber + ****************************************************/ + + typedef void* storm_rational_number_ptr; + + // Functions that are registered to sylvan for the rational number type. + void storm_rational_number_init(storm_rational_number_ptr* a); + void storm_rational_number_destroy(storm_rational_number_ptr a); + int storm_rational_number_equals(storm_rational_number_ptr a, storm_rational_number_ptr b); + char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, size_t buflen); + + // Fundamental functions. + storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr a); + storm_rational_number_ptr storm_rational_number_get_zero(); + storm_rational_number_ptr storm_rational_number_get_one(); + int storm_rational_number_is_zero(storm_rational_number_ptr a); + uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed); + double storm_rational_number_get_value_double(storm_rational_number_ptr a); + + // Binary operations. + storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a, storm_rational_number_ptr b); + storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b); + storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr a, storm_rational_number_ptr b); + storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr a, storm_rational_number_ptr b); + storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm_rational_number_ptr b); + storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm_rational_number_ptr b); + storm_rational_number_ptr storm_rational_number_min(storm_rational_number_ptr a, storm_rational_number_ptr b); + storm_rational_number_ptr storm_rational_number_max(storm_rational_number_ptr a, storm_rational_number_ptr b); + + // Binary relations. + int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_number_ptr b); + int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_rational_number_ptr b); + + // Unary operations. + storm_rational_number_ptr storm_rational_number_negate(storm_rational_number_ptr a); + storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a); + storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a); + + // Printing functions. + void print_storm_rational_number(storm_rational_number_ptr a); + void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out); + + /*************************************************** + Function-wrappers for storm::RationalFunction + ****************************************************/ + + typedef void* storm_rational_function_ptr; + + // Functions that are registered to sylvan for the rational function type. + void storm_rational_function_init(storm_rational_function_ptr* a); + void storm_rational_function_destroy(storm_rational_function_ptr a); + int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b); + char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen); + + // Fundamental functions. + storm_rational_function_ptr storm_rational_function_clone(storm_rational_function_ptr a); + storm_rational_function_ptr storm_rational_function_get_zero(); + storm_rational_function_ptr storm_rational_function_get_one(); + int storm_rational_function_is_zero(storm_rational_function_ptr a); + uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); + double storm_rational_function_get_value_double(storm_rational_function_ptr a); + + // Binary operations. + storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b); + storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b); + storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b); + storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b); + storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b); + storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b); + storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b); + storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b); + + // Binary relations. + int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b); + int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b); + + // Unary operations. + storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a); + storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a); + storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a); + + // Printing functions. + void print_storm_rational_function(storm_rational_function_ptr a); + void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); + +#ifdef __cplusplus +} +#endif + +#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 7fe65c75d..af0dbc4aa 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -1,8 +1,9 @@ #include -#include "storm_function_wrapper.h" +#include "storm_wrapper.h" -// Import the srf_type created for rational function.s +// Import the types created for rational numbers and functions. +extern uint32_t srn_type; extern uint32_t srf_type; /** @@ -357,6 +358,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v) return mtbdd_getdouble(a) != 0.0 ? mtbdd_true : mtbdd_false; } else if (mtbddnode_gettype(na) == 2) { return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false; + } else if (mtbddnode_gettype(na) == srn_type) { + return storm_rational_number_is_zero((storm_rational_number_ptr)mtbdd_getvalue(a)) == 0 ? mtbdd_true : mtbdd_false; } #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) else if (mtbddnode_gettype(na) == srf_type) { @@ -491,6 +494,8 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars) return mtbdd_getdouble(dd) != 0 ? powl(2.0L, nvars) : 0.0; } else if (mtbddnode_gettype(na) == 2) { return mtbdd_getnumer(dd) != 0 ? powl(2.0L, nvars) : 0.0; + } else if (mtbddnode_gettype(na) == srn_type) { + return storm_rational_number_is_zero((storm_rational_number_ptr)mtbdd_getvalue(dd)) == 0 ? powl(2.0L, nvars) : 0.0; } #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) else if (mtbddnode_gettype(na) == srf_type) { @@ -528,6 +533,8 @@ int mtbdd_iszero(MTBDD dd) { return mtbdd_getdouble(dd) == 0; } else if (mtbdd_gettype(dd) == 2) { return mtbdd_getnumer(dd) == 0; + } else if (mtbdd_gettype(dd) == srn_type) { + return storm_rational_number_is_zero((storm_rational_number_ptr)mtbdd_getvalue(dd)) == 1 ? 1 : 0; } #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) else if (mtbdd_gettype(dd) == srf_type) { @@ -918,3 +925,36 @@ TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint return res; } } + +TASK_IMPL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, dd, mtbdd_uapply_op, op, size_t, param) +{ + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Check cache */ + MTBDD result; + + // Caching would be done here, but is omitted (as this is the purpose of this function). + + /* Check terminal case */ + result = WRAP(op, dd, param); + if (result != mtbdd_invalid) { + // Caching would be done here, but is omitted (as this is the purpose of this function). + return result; + } + + /* Get cofactors */ + mtbddnode_t ndd = MTBDD_GETNODE(dd); + MTBDD ddlow = node_getlow(dd, ndd); + MTBDD ddhigh = node_gethigh(dd, ndd); + + /* Recursive */ + mtbdd_refs_spawn(SPAWN(mtbdd_uapply_nocache, ddhigh, op, param)); + MTBDD low = mtbdd_refs_push(CALL(mtbdd_uapply_nocache, ddlow, op, param)); + MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_uapply_nocache)); + mtbdd_refs_pop(1); + result = mtbdd_makenode(mtbddnode_getvariable(ndd), low, high); + + // Caching would be done here, but is omitted (as this is the purpose of this function). + return result; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 6077b7e3b..77497c0b0 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -146,3 +146,5 @@ TASK_DECL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, MTBDD, uint32_t); TASK_DECL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, MTBDD, uint32_t); #define mtbdd_maxExistsRepresentative(a, vars) (CALL(mtbdd_maxExistsRepresentative, a, vars, 0)) +TASK_DECL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, mtbdd_uapply_op, size_t); +#define mtbdd_uapply_nocache(dd, op, param) CALL(mtbdd_uapply_nocache, dd, op, param) diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp index afcc027e6..bdb71bf81 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp @@ -1,7 +1,11 @@ - Mtbdd toDoubleMtbdd() const; - Mtbdd toInt64Mtbdd() const; +// Methods to convert a BDD to the canonical 0/1 MTBDD for different types. +Mtbdd toDoubleMtbdd() const; +Mtbdd toInt64Mtbdd() const; +Mtbdd toStormRationalNumberMtbdd() const; #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) - Mtbdd toStormRationalFunctionMtbdd() const; +Mtbdd toStormRationalFunctionMtbdd() const; #endif - Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; - Bdd ExistAbstractRepresentative(const BddSet& cube) const; + +// Other functions to add to sylvan's Bdd class. +Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; +Bdd ExistAbstractRepresentative(const BddSet& cube) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index bfe5ff1cb..eb2ec97de 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -1,119 +1,96 @@ +// Functions that are to be added to sylvan's Mtbdd class. +// Functions that operate on all or standard Mtbdds. +Bdd NotZero() const; +size_t CountLeaves() const; +double NonZeroCount(size_t variableCount) const; +bool isValid() const; +void PrintDot(FILE *out) const; +std::string GetShaHash() const; - /** - * @brief Computes f - g - */ - Mtbdd Minus(const Mtbdd &other) const; +Mtbdd Minus(const Mtbdd &other) const; +Mtbdd Divide(const Mtbdd &other) const; - /** - * @brief Computes f / g - */ - Mtbdd Divide(const Mtbdd &other) const; - -#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) - /** - * @brief Creates a Mtbdd leaf representing the rational function value - */ - static Mtbdd stormRationalFunctionTerminal(storm::RationalFunction const& value); - - Bdd EqualsRF(const Mtbdd& other) const; - Bdd LessRF(const Mtbdd& other) const; - Bdd LessOrEqualRF(const Mtbdd& other) const; - - Mtbdd MinRF(const Mtbdd& other) const; - Mtbdd MaxRF(const Mtbdd& other) const; - - /** - * @brief Computes f + g for Rational Functions - */ - Mtbdd PlusRF(const Mtbdd &other) const; - - /** - * @brief Computes f * g for Rational Functions - */ - Mtbdd TimesRF(const Mtbdd &other) const; +Bdd Equals(const Mtbdd& other) const; +Bdd Less(const Mtbdd& other) const; +Bdd LessOrEqual(const Mtbdd& other) const; - Mtbdd AndExistsRF(const Mtbdd &other, const BddSet &variables) const; +Bdd AbstractMinRepresentative(const BddSet &variables) const; +Bdd AbstractMaxRepresentative(const BddSet &variables) const; - /** - * @brief Computes f - g for Rational Functions - */ - Mtbdd MinusRF(const Mtbdd &other) const; +Mtbdd Pow(const Mtbdd& other) const; +Mtbdd Mod(const Mtbdd& other) const; +Mtbdd Logxy(const Mtbdd& other) const; - /** - * @brief Computes f / g for Rational Functions - */ - Mtbdd DivideRF(const Mtbdd &other) const; +Mtbdd Floor() const; +Mtbdd Ceil() const; +Mtbdd Minimum() const; +Mtbdd Maximum() const; - Mtbdd PowRF(const Mtbdd& other) const; +bool EqualNorm(const Mtbdd& other, double epsilon) const; +bool EqualNormRel(const Mtbdd& other, double epsilon) const; - Mtbdd AbstractPlusRF(const BddSet &variables) const; - - Mtbdd ReplaceLeavesRF(void* context) const; +// Functions that operate on Mtbdds over rational numbers. +static Mtbdd stormRationalNumberTerminal(storm::RationalNumber const& value); - Mtbdd FloorRF() const; - Mtbdd CeilRF() const; +Bdd EqualsRN(const Mtbdd& other) const; +Bdd LessRN(const Mtbdd& other) const; +Bdd LessOrEqualRN(const Mtbdd& other) const; - Mtbdd AbstractMinRF(const BddSet &variables) const; - Mtbdd AbstractMaxRF(const BddSet &variables) const; +Mtbdd MinRN(const Mtbdd& other) const; +Mtbdd MaxRN(const Mtbdd& other) const; - Bdd BddThresholdRF(storm::RationalFunction const& rf) const; - Bdd BddStrictThresholdRF(storm::RationalFunction const& rf) const; +Mtbdd PlusRN(const Mtbdd &other) const; +Mtbdd MinusRN(const Mtbdd &other) const; +Mtbdd TimesRN(const Mtbdd &other) const; +Mtbdd DivideRN(const Mtbdd &other) const; - Mtbdd MinimumRF() const; - Mtbdd MaximumRF() const; +Mtbdd FloorRN() const; +Mtbdd CeilRN() const; +Mtbdd PowRN(const Mtbdd& other) const; +Mtbdd MinimumRN() const; +Mtbdd MaximumRN() const; - Mtbdd ToDoubleRF() const; -#endif - - /** - * @brief Computes abstraction by minimum - */ - Bdd AbstractMinRepresentative(const BddSet &variables) const; - - /** - * @brief Computes abstraction by maximum - */ - Bdd AbstractMaxRepresentative(const BddSet &variables) const; - - Bdd NotZero() const; - - Bdd Equals(const Mtbdd& other) const; - - Bdd Less(const Mtbdd& other) const; - - Bdd LessOrEqual(const Mtbdd& other) const; +Mtbdd AndExistsRN(const Mtbdd &other, const BddSet &variables) const; +Mtbdd AbstractPlusRN(const BddSet &variables) const; +Mtbdd AbstractMinRN(const BddSet &variables) const; +Mtbdd AbstractMaxRN(const BddSet &variables) const; - Mtbdd Minimum() const; +Bdd BddThresholdRN(storm::RationalNumber const& rn) const; +Bdd BddStrictThresholdRN(storm::RationalNumber const& rn) const; - Mtbdd Maximum() const; +Mtbdd ToDoubleRN() const; - bool EqualNorm(const Mtbdd& other, double epsilon) const; +// Functions that operate on Mtbdds over rational functions. +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +static Mtbdd stormRationalFunctionTerminal(storm::RationalFunction const& value); - bool EqualNormRel(const Mtbdd& other, double epsilon) const; - - Mtbdd Floor() const; +Bdd EqualsRF(const Mtbdd& other) const; +Bdd LessRF(const Mtbdd& other) const; +Bdd LessOrEqualRF(const Mtbdd& other) const; - Mtbdd Ceil() const; - - Mtbdd Pow(const Mtbdd& other) const; +Mtbdd MinRF(const Mtbdd& other) const; +Mtbdd MaxRF(const Mtbdd& other) const; - Mtbdd Mod(const Mtbdd& other) const; +Mtbdd PlusRF(const Mtbdd &other) const; +Mtbdd MinusRF(const Mtbdd &other) const; +Mtbdd TimesRF(const Mtbdd &other) const; +Mtbdd DivideRF(const Mtbdd &other) const; - Mtbdd Logxy(const Mtbdd& other) const; - - size_t CountLeaves() const; +Mtbdd FloorRF() const; +Mtbdd CeilRF() const; +Mtbdd PowRF(const Mtbdd& other) const; +Mtbdd MinimumRF() const; +Mtbdd MaximumRF() const; - /** - * @brief Compute the number of non-zero variable assignments, using variables in cube. - */ - double NonZeroCount(size_t variableCount) const; +Mtbdd AndExistsRF(const Mtbdd &other, const BddSet &variables) const; +Mtbdd AbstractPlusRF(const BddSet &variables) const; +Mtbdd AbstractMinRF(const BddSet &variables) const; +Mtbdd AbstractMaxRF(const BddSet &variables) const; - bool isValid() const; +Bdd BddThresholdRF(storm::RationalFunction const& rf) const; +Bdd BddStrictThresholdRF(storm::RationalFunction const& rf) const; - /** - * @brief Writes .dot file of this Bdd. Not thread-safe! - */ - void PrintDot(FILE *out) const; +Mtbdd ToDoubleRF() const; +#endif - std::string GetShaHash() const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 0f970b8c6..00740768d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -1,6 +1,10 @@ -#include "storm_function_wrapper.h" +#include "storm_wrapper.h" +#include "sylvan_storm_rational_number.h" #include "sylvan_storm_rational_function.h" +/********************************************* + Functions added to sylvan's Sylvan class. + *********************************************/ void Sylvan::initCustomMtbdd() { @@ -8,11 +12,9 @@ Sylvan::initCustomMtbdd() sylvan_storm_rational_function_init(); } -Bdd -Bdd::ExistAbstractRepresentative(const BddSet& cube) const { - LACE_ME; - return sylvan_existsRepresentative(bdd, cube.set.bdd); -} +/********************************************* + Functions added to sylvan's Bdd class. + *********************************************/ Mtbdd Bdd::toDoubleMtbdd() const { @@ -26,296 +28,454 @@ Bdd::toInt64Mtbdd() const { return mtbdd_bool_to_int64(bdd); } -#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) Mtbdd -Mtbdd::stormRationalFunctionTerminal(storm::RationalFunction const& value) -{ - storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value); - return mtbdd_storm_rational_function(ptr); +Bdd::toStormRationalNumberMtbdd() const { + LACE_ME; + return mtbdd_bool_to_storm_rational_number(bdd); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) Mtbdd Bdd::toStormRationalFunctionMtbdd() const { LACE_ME; return mtbdd_bool_to_storm_rational_function(bdd); } +#endif -Bdd -Mtbdd::EqualsRF(const Mtbdd& other) const { +Mtbdd +Bdd::Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const { LACE_ME; - return mtbdd_equals_rational_function(mtbdd, other.mtbdd); + return mtbdd_ite(bdd, thenDd.GetMTBDD(), elseDd.GetMTBDD()); } Bdd -Mtbdd::LessRF(const Mtbdd& other) const { +Bdd::ExistAbstractRepresentative(const BddSet& cube) const { LACE_ME; - return sylvan_storm_rational_function_less(mtbdd, other.mtbdd); + return sylvan_existsRepresentative(bdd, cube.set.bdd); } +/********************************************* + Functions added to sylvan's Mtbdd class. + *********************************************/ + Bdd -Mtbdd::LessOrEqualRF(const Mtbdd& other) const { +Mtbdd::NotZero() const +{ LACE_ME; - return sylvan_storm_rational_function_less_or_equal(mtbdd, other.mtbdd); + return mtbdd_not_zero(mtbdd); } -Mtbdd -Mtbdd::MinRF(const Mtbdd& other) const { +size_t +Mtbdd::CountLeaves() const { LACE_ME; - return sylvan_storm_rational_function_min(mtbdd, other.mtbdd); + return mtbdd_leafcount(mtbdd); } -Mtbdd -Mtbdd::MaxRF(const Mtbdd& other) const { +double +Mtbdd::NonZeroCount(size_t variableCount) const { LACE_ME; - return sylvan_storm_rational_function_max(mtbdd, other.mtbdd); + return mtbdd_non_zero_count(mtbdd, variableCount); } -Mtbdd -Mtbdd::ToDoubleRF() const { +bool +Mtbdd::isValid() const { LACE_ME; - return sylvan_storm_rational_function_to_double(mtbdd); + return mtbdd_test_isvalid(mtbdd) == 1; +} + +void +Mtbdd::PrintDot(FILE *out) const { + mtbdd_fprintdot(out, mtbdd); +} + +std::string +Mtbdd::GetShaHash() const { + char buf[65]; + mtbdd_getsha(mtbdd, buf); + return std::string(buf); } Mtbdd -Mtbdd::PlusRF(const Mtbdd &other) const +Mtbdd::Minus(const Mtbdd &other) const { LACE_ME; - return sylvan_storm_rational_function_plus(mtbdd, other.mtbdd); + return mtbdd_minus(mtbdd, other.mtbdd); } - Mtbdd -Mtbdd::TimesRF(const Mtbdd &other) const +Mtbdd::Divide(const Mtbdd &other) const { LACE_ME; - return sylvan_storm_rational_function_times(mtbdd, other.mtbdd); + return mtbdd_divide(mtbdd, other.mtbdd); } -Mtbdd -Mtbdd::AndExistsRF(const Mtbdd &other, const BddSet &variables) const { +Bdd +Mtbdd::Equals(const Mtbdd& other) const { LACE_ME; - return sylvan_storm_rational_function_and_exists(mtbdd, other.mtbdd, variables.set.bdd); + return mtbdd_equals(mtbdd, other.mtbdd); } -Mtbdd -Mtbdd::MinusRF(const Mtbdd &other) const +Bdd +Mtbdd::Less(const Mtbdd& other) const { + LACE_ME; + return mtbdd_less_as_bdd(mtbdd, other.mtbdd); +} + +Bdd +Mtbdd::LessOrEqual(const Mtbdd& other) const { + LACE_ME; + return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd); +} + +Bdd +Mtbdd::AbstractMinRepresentative(const BddSet &variables) const { LACE_ME; - return sylvan_storm_rational_function_minus(mtbdd, other.mtbdd); + return mtbdd_minExistsRepresentative(mtbdd, variables.set.bdd); } -Mtbdd -Mtbdd::DivideRF(const Mtbdd &other) const +Bdd +Mtbdd::AbstractMaxRepresentative(const BddSet &variables) const { LACE_ME; - return sylvan_storm_rational_function_divide(mtbdd, other.mtbdd); + return mtbdd_maxExistsRepresentative(mtbdd, variables.set.bdd); } Mtbdd -Mtbdd::PowRF(const Mtbdd& other) const { +Mtbdd::Pow(const Mtbdd& other) const { LACE_ME; - return sylvan_storm_rational_function_pow(mtbdd, other.mtbdd); + return mtbdd_pow(mtbdd, other.mtbdd); } +Mtbdd +Mtbdd::Mod(const Mtbdd& other) const { + LACE_ME; + return mtbdd_mod(mtbdd, other.mtbdd); +} -Mtbdd Mtbdd::AbstractPlusRF(const BddSet &variables) const { - LACE_ME; - return sylvan_storm_rational_function_abstract_plus(mtbdd, variables.set.bdd); +Mtbdd +Mtbdd::Logxy(const Mtbdd& other) const { + LACE_ME; + return mtbdd_logxy(mtbdd, other.mtbdd); } -Mtbdd Mtbdd::ReplaceLeavesRF(void* context) const { - LACE_ME; - return sylvan_storm_rational_function_replace_leaves(mtbdd, (size_t)context); +Mtbdd +Mtbdd::Floor() const { + LACE_ME; + return mtbdd_floor(mtbdd); } +Mtbdd +Mtbdd::Ceil() const { + LACE_ME; + return mtbdd_ceil(mtbdd); +} Mtbdd -Mtbdd::FloorRF() const { +Mtbdd::Minimum() const { LACE_ME; - return sylvan_storm_rational_function_floor(mtbdd); + return mtbdd_minimum(mtbdd); } Mtbdd -Mtbdd::CeilRF() const { +Mtbdd::Maximum() const { LACE_ME; - return sylvan_storm_rational_function_ceil(mtbdd); + return mtbdd_maximum(mtbdd); } -Mtbdd Mtbdd::AbstractMinRF(const BddSet &variables) const { +bool +Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const { LACE_ME; - return sylvan_storm_rational_function_abstract_min(mtbdd, variables.set.bdd); + return mtbdd_equal_norm_d(mtbdd, other.mtbdd, epsilon); } -Mtbdd Mtbdd::AbstractMaxRF(const BddSet &variables) const { +bool +Mtbdd::EqualNormRel(const Mtbdd& other, double epsilon) const { LACE_ME; - return sylvan_storm_rational_function_abstract_max(mtbdd, variables.set.bdd); + return mtbdd_equal_norm_rel_d(mtbdd, other.mtbdd, epsilon); +} + +// Functions for Mtbdds over rational numbers. +Mtbdd +Mtbdd::stormRationalNumberTerminal(storm::RationalNumber const& value) +{ + storm_rational_number_ptr ptr = (storm_rational_number_ptr)(&value); + return mtbdd_storm_rational_number(ptr); } Bdd -Mtbdd::BddStrictThresholdRF(storm::RationalFunction const& rf) const { +Mtbdd::EqualsRN(const Mtbdd& other) const { LACE_ME; - return sylvan_storm_rational_function_strict_threshold(mtbdd, (void*)&rf); + return mtbdd_equals_rational_number(mtbdd, other.mtbdd); } Bdd -Mtbdd::BddThresholdRF(storm::RationalFunction const& rf) const { +Mtbdd::LessRN(const Mtbdd& other) const { LACE_ME; - return sylvan_storm_rational_function_threshold(mtbdd, (void*)&rf); + return sylvan_storm_rational_number_less(mtbdd, other.mtbdd); +} + +Bdd +Mtbdd::LessOrEqualRN(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_number_less_or_equal(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::MinimumRF() const { +Mtbdd::MinRN(const Mtbdd& other) const { LACE_ME; - return sylvan_storm_rational_function_minimum(mtbdd); + return sylvan_storm_rational_number_min(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::MaximumRF() const { +Mtbdd::MaxRN(const Mtbdd& other) const { LACE_ME; - return sylvan_storm_rational_function_maximum(mtbdd); + return sylvan_storm_rational_number_max(mtbdd, other.mtbdd); } -#endif +Mtbdd +Mtbdd::PlusRN(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_number_plus(mtbdd, other.mtbdd); +} Mtbdd -Bdd::Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const { +Mtbdd::MinusRN(const Mtbdd &other) const +{ LACE_ME; - return mtbdd_ite(bdd, thenDd.GetMTBDD(), elseDd.GetMTBDD()); + return sylvan_storm_rational_number_minus(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Minus(const Mtbdd &other) const +Mtbdd::TimesRN(const Mtbdd &other) const { LACE_ME; - return mtbdd_minus(mtbdd, other.mtbdd); + return sylvan_storm_rational_number_times(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Divide(const Mtbdd &other) const +Mtbdd::DivideRN(const Mtbdd &other) const { LACE_ME; - return mtbdd_divide(mtbdd, other.mtbdd); + return sylvan_storm_rational_number_divide(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::FloorRN() const { + LACE_ME; + return sylvan_storm_rational_number_floor(mtbdd); +} + +Mtbdd +Mtbdd::CeilRN() const { + LACE_ME; + return sylvan_storm_rational_number_ceil(mtbdd); +} + +Mtbdd +Mtbdd::PowRN(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_number_pow(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::MinimumRN() const { + LACE_ME; + return sylvan_storm_rational_number_minimum(mtbdd); +} + +Mtbdd +Mtbdd::MaximumRN() const { + LACE_ME; + return sylvan_storm_rational_number_maximum(mtbdd); +} + +Mtbdd +Mtbdd::AndExistsRN(const Mtbdd &other, const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_number_and_exists(mtbdd, other.mtbdd, variables.set.bdd); +} + +Mtbdd Mtbdd::AbstractPlusRN(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_number_abstract_plus(mtbdd, variables.set.bdd); +} + +Mtbdd Mtbdd::AbstractMinRN(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_number_abstract_min(mtbdd, variables.set.bdd); +} + +Mtbdd Mtbdd::AbstractMaxRN(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_number_abstract_max(mtbdd, variables.set.bdd); } Bdd -Mtbdd::NotZero() const -{ +Mtbdd::BddThresholdRN(storm::RationalNumber const& rn) const { LACE_ME; - return mtbdd_not_zero(mtbdd); + return sylvan_storm_rational_number_threshold(mtbdd, (void*)&rn); } Bdd -Mtbdd::Equals(const Mtbdd& other) const { +Mtbdd::BddStrictThresholdRN(storm::RationalNumber const& rn) const { LACE_ME; - return mtbdd_equals(mtbdd, other.mtbdd); + return sylvan_storm_rational_number_strict_threshold(mtbdd, (void*)&rn); +} + +Mtbdd +Mtbdd::ToDoubleRN() const { + LACE_ME; + return sylvan_storm_rational_number_to_double(mtbdd); +} + + + +// Functions for Mtbdds over rational functions. +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +Mtbdd +Mtbdd::stormRationalFunctionTerminal(storm::RationalFunction const& value) +{ + storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value); + return mtbdd_storm_rational_function(ptr); } Bdd -Mtbdd::Less(const Mtbdd& other) const { +Mtbdd::EqualsRF(const Mtbdd& other) const { LACE_ME; - return mtbdd_less_as_bdd(mtbdd, other.mtbdd); + return mtbdd_equals_rational_function(mtbdd, other.mtbdd); } Bdd -Mtbdd::LessOrEqual(const Mtbdd& other) const { +Mtbdd::LessRF(const Mtbdd& other) const { LACE_ME; - return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd); + return sylvan_storm_rational_function_less(mtbdd, other.mtbdd); } -bool -Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const { +Bdd +Mtbdd::LessOrEqualRF(const Mtbdd& other) const { LACE_ME; - return mtbdd_equal_norm_d(mtbdd, other.mtbdd, epsilon); + return sylvan_storm_rational_function_less_or_equal(mtbdd, other.mtbdd); } -bool -Mtbdd::EqualNormRel(const Mtbdd& other, double epsilon) const { +Mtbdd +Mtbdd::MinRF(const Mtbdd& other) const { LACE_ME; - return mtbdd_equal_norm_rel_d(mtbdd, other.mtbdd, epsilon); + return sylvan_storm_rational_function_min(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Floor() const { +Mtbdd::MaxRF(const Mtbdd& other) const { LACE_ME; - return mtbdd_floor(mtbdd); + return sylvan_storm_rational_function_max(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Ceil() const { +Mtbdd::PlusRF(const Mtbdd &other) const +{ LACE_ME; - return mtbdd_ceil(mtbdd); + return sylvan_storm_rational_function_plus(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Pow(const Mtbdd& other) const { +Mtbdd::MinusRF(const Mtbdd &other) const +{ LACE_ME; - return mtbdd_pow(mtbdd, other.mtbdd); + return sylvan_storm_rational_function_minus(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Mod(const Mtbdd& other) const { +Mtbdd::TimesRF(const Mtbdd &other) const +{ LACE_ME; - return mtbdd_mod(mtbdd, other.mtbdd); + return sylvan_storm_rational_function_times(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Logxy(const Mtbdd& other) const { +Mtbdd::DivideRF(const Mtbdd &other) const +{ LACE_ME; - return mtbdd_logxy(mtbdd, other.mtbdd); + return sylvan_storm_rational_function_divide(mtbdd, other.mtbdd); } -size_t -Mtbdd::CountLeaves() const { +Mtbdd +Mtbdd::FloorRF() const { LACE_ME; - return mtbdd_leafcount(mtbdd); + return sylvan_storm_rational_function_floor(mtbdd); } -double -Mtbdd::NonZeroCount(size_t variableCount) const { +Mtbdd +Mtbdd::CeilRF() const { LACE_ME; - return mtbdd_non_zero_count(mtbdd, variableCount); + return sylvan_storm_rational_function_ceil(mtbdd); } -bool -Mtbdd::isValid() const { +Mtbdd +Mtbdd::PowRF(const Mtbdd& other) const { LACE_ME; - return mtbdd_test_isvalid(mtbdd) == 1; + return sylvan_storm_rational_function_pow(mtbdd, other.mtbdd); } Mtbdd -Mtbdd::Minimum() const { +Mtbdd::MinimumRF() const { LACE_ME; - return mtbdd_minimum(mtbdd); + return sylvan_storm_rational_function_minimum(mtbdd); } Mtbdd -Mtbdd::Maximum() const { +Mtbdd::MaximumRF() const { LACE_ME; - return mtbdd_maximum(mtbdd); + return sylvan_storm_rational_function_maximum(mtbdd); } -void -Mtbdd::PrintDot(FILE *out) const { - mtbdd_fprintdot(out, mtbdd); +Mtbdd +Mtbdd::AndExistsRF(const Mtbdd &other, const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_and_exists(mtbdd, other.mtbdd, variables.set.bdd); } -std::string -Mtbdd::GetShaHash() const { - char buf[65]; - mtbdd_getsha(mtbdd, buf); - return std::string(buf); +Mtbdd Mtbdd::AbstractPlusRF(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_abstract_plus(mtbdd, variables.set.bdd); +} + +Mtbdd Mtbdd::AbstractMinRF(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_abstract_min(mtbdd, variables.set.bdd); +} + +Mtbdd Mtbdd::AbstractMaxRF(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_abstract_max(mtbdd, variables.set.bdd); } Bdd -Mtbdd::AbstractMinRepresentative(const BddSet &variables) const -{ +Mtbdd::BddThresholdRF(storm::RationalFunction const& rf) const { LACE_ME; - return mtbdd_minExistsRepresentative(mtbdd, variables.set.bdd); + return sylvan_storm_rational_function_threshold(mtbdd, (void*)&rf); } Bdd -Mtbdd::AbstractMaxRepresentative(const BddSet &variables) const -{ +Mtbdd::BddStrictThresholdRF(storm::RationalFunction const& rf) const { LACE_ME; - return mtbdd_maxExistsRepresentative(mtbdd, variables.set.bdd); + return sylvan_storm_rational_function_strict_threshold(mtbdd, (void*)&rf); } + +Mtbdd +Mtbdd::ToDoubleRF() const { + LACE_ME; + return sylvan_storm_rational_function_to_double(mtbdd); +} +#endif + + + + + + + + + + + diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index b05e0b972..93c2b0320 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -15,207 +15,88 @@ #include #include -#include - -#undef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG - -#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG -int depth = 0; - -#define LOG_I(funcName) do { for (int i = 0; i < depth; ++i) { printf(" "); } ++depth; printf("Entering function " funcName "\n"); } while (0 != 0); -#define LOG_O(funcName) do { --depth; for (int i = 0; i < depth; ++i) { printf(" "); } printf("Leaving function " funcName "\n"); } while (0 != 0); -#else -#define LOG_I(funcName) -#define LOG_O(funcName) -#endif - uint32_t srf_type; -/** - * helper function for hash - */ -#ifndef rotl64 -//static inline uint64_t -//rotl64(uint64_t x, int8_t r) -//{ -// return ((x<>(64-r))); -//} -#endif - -storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal) { - uint64_t value = mtbdd_getvalue(terminal); - return (storm_rational_function_ptr*)value; +static uint64_t sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed) { + storm_rational_function_ptr x = (storm_rational_function_ptr)v; + return storm_rational_function_hash(x, seed); } -static uint64_t -sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed) -{ - LOG_I("i-hash") - /* Hash the storm::RationalFunction in pointer v */ - - storm_rational_function_ptr x = (storm_rational_function_ptr)v; - - uint64_t hash = storm_rational_function_hash(x, seed); - -#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG - printf("Hashing ptr %p with contents ", x); - print_storm_rational_function(x); - printf(" with seed %zu, hash = %zu\n", seed, hash); -#endif - - LOG_O("i-hash") - return hash; +static int sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right) { + return storm_rational_function_equals((storm_rational_function_ptr)(size_t)left, (storm_rational_function_ptr)(size_t)right); } -static int -sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right) -{ - LOG_I("i-equals") - /* This function is called by the unique table when comparing a new - leaf with an existing leaf */ - storm_rational_function_ptr a = (storm_rational_function_ptr)(size_t)left; - storm_rational_function_ptr b = (storm_rational_function_ptr)(size_t)right; - - /* Just compare x and y */ - int result = storm_rational_function_equals(a, b); - - LOG_O("i-equals") - return result; +static void sylvan_storm_rational_function_create(uint64_t *val) { + // This function is called by the unique table when a leaf does not yet exist. We make a copy, which will be stored in the hash table. + storm_rational_function_ptr* x = (storm_rational_function_ptr*)(size_t)val; + storm_rational_function_init(x); } -static void -sylvan_storm_rational_function_create(uint64_t *val) -{ - LOG_I("i-create") - -#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG - void* tmp = (void*)*val; - printf("sylvan_storm_rational_function_create(ptr = %p, value = ", tmp); - print_storm_rational_function(*((storm_rational_function_ptr*)(size_t)val)); - printf(")\n"); -#endif - - /* This function is called by the unique table when a leaf does not yet exist. - We make a copy, which will be stored in the hash table. */ - storm_rational_function_ptr* x = (storm_rational_function_ptr*)(size_t)val; - storm_rational_function_init(x); - -#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG - tmp = (void*)*val; - printf("sylvan_storm_rational_function_create_2(ptr = %p)\n", tmp); -#endif - - LOG_O("i-create") +static void sylvan_storm_rational_function_destroy(uint64_t val) { + // This function is called by the unique table when a leaf is removed during garbage collection. + storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)val; + storm_rational_function_destroy(x); } -static void -sylvan_storm_rational_function_destroy(uint64_t val) -{ - LOG_I("i-destroy") - /* This function is called by the unique table - when a leaf is removed during garbage collection. */ - storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)val; - storm_rational_function_destroy(x); - LOG_O("i-destroy") -} - -static char* -sylvan_storm_rational_function_to_str(int comp, uint64_t val, char *buf, size_t buflen) -{ +static char* sylvan_storm_rational_function_to_str(int comp, uint64_t val, char *buf, size_t buflen) { return storm_rational_function_to_str((storm_rational_function_ptr)(size_t)val, *buf, buflen); (void)comp; } - -/** - * Initialize storm::RationalFunction custom leaves - */ -void -sylvan_storm_rational_function_init() -{ - /* Register custom leaf */ +void sylvan_storm_rational_function_init() { + // Register custom leaf type storing rational functions. srf_type = sylvan_mt_create_type(); sylvan_mt_set_hash(srf_type, sylvan_storm_rational_function_hash); sylvan_mt_set_equals(srf_type, sylvan_storm_rational_function_equals); sylvan_mt_set_create(srf_type, sylvan_storm_rational_function_create); sylvan_mt_set_destroy(srf_type, sylvan_storm_rational_function_destroy); sylvan_mt_set_to_str(srf_type, sylvan_storm_rational_function_to_str); - // sylvan_mt_set_write_binary(srf_type, gmp_write_binary); - // sylvan_mt_set_read_binary(srf_type, gmp_read_binary); + // sylvan_mt_set_write_binary(srf_type, sylvan_storm_rational_function_write_binary); + // sylvan_mt_set_read_binary(srf_type, sylvan_storm_rational_function_read_binary); } uint32_t sylvan_storm_rational_function_get_type() { return srf_type; } -/** - * Create storm::RationalFunction leaf - */ -MTBDD -mtbdd_storm_rational_function(storm_rational_function_ptr val) -{ - LOG_I("i-mtbdd_") - uint64_t terminalValue = (uint64_t)val; - -#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG - printf("mtbdd_storm_rational_function(ptr = %p, value = ", val); - print_storm_rational_function(val); - printf(")\n"); -#endif - - MTBDD result = mtbdd_makeleaf(srf_type, terminalValue); - - LOG_O("i-mtbdd_") - return result; +MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val) { + uint64_t terminalValue = (uint64_t)val; + return mtbdd_makeleaf(srf_type, terminalValue); } -/** - * Converts a BDD to a MTBDD with storm::RationalFunction leaves - */ -TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v) -{ - LOG_I("task_impl_2 to_srf") +storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal) { + uint64_t value = mtbdd_getvalue(terminal); + return (storm_rational_function_ptr*)value; +} + +TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v) { if (a == mtbdd_false) { - MTBDD result = mtbdd_storm_rational_function(storm_rational_function_get_zero()); - LOG_O("task_impl_2 to_srf - ZERO") - return result; + return mtbdd_storm_rational_function(storm_rational_function_get_zero()); } if (a == mtbdd_true) { - MTBDD result = mtbdd_storm_rational_function(storm_rational_function_get_one()); - LOG_O("task_impl_2 to_srf - ONE") - return result; + return mtbdd_storm_rational_function(storm_rational_function_get_one()); } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). (void)v; - LOG_O("task_impl_2 to_srf - INVALID") return mtbdd_invalid; } -TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd) -{ +TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd) { return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0); } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_equals") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions */ - if (a == mtbdd_false) return b; - if (b == mtbdd_false) return a; - - /* If both leaves, compute plus */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); - if (storm_rational_function_equals(ma, mb)) { - return mtbdd_true; - } else { - return mtbdd_false; - } + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); + return storm_rational_function_equals(ma, mb) ? mtbdd_true : mtbdd_false; } /* Commutative, so swap a,b for better cache performance */ @@ -227,13 +108,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, pa, MTBDD*, return mtbdd_invalid; } -/** - * Operation "plus" for two storm::RationalFunction MTBDDs - * Interpret partial function as "0" - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_plus") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions */ @@ -242,12 +117,11 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, p /* If both leaves, compute plus */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres = storm_rational_function_plus(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -262,27 +136,20 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, p return mtbdd_invalid; } -/** - * Operation "minus" for two storm::RationalFunction MTBDDs - * Interpret partial function as "0" - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_minus") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions */ if (a == mtbdd_false) return sylvan_storm_rational_function_neg(b); if (b == mtbdd_false) return a; - /* If both leaves, compute plus */ + /* If both leaves, compute minus */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres = storm_rational_function_minus(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -291,31 +158,19 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, return mtbdd_invalid; } -/** - * Operation "times" for two storm::RationalFunction MTBDDs. - * One of the parameters can be a BDD, then it is interpreted as a filter. - * For partial functions, domain is intersection - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_times") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; - /* Check for partial functions and for Boolean (filter) */ + /* Check for partial functions */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - /* If one of Boolean, interpret as filter */ - if (a == mtbdd_true) return b; - if (b == mtbdd_true) return a; - - /* Handle multiplication of leaves */ + /* If both leaves, compute multiplication */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres = storm_rational_function_times(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -330,26 +185,20 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, return mtbdd_invalid; } -/** - * Operation "divide" for two storm::RationalFunction MTBDDs. - * For partial functions, domain is intersection - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_divide") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - /* Handle division of leaves */ + /* If both leaves, compute division */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); storm_rational_function_ptr mres; if (storm_rational_function_is_zero(ma)) { mres = storm_rational_function_get_zero(); } else { - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); mres = storm_rational_function_divide(ma, mb); } MTBDD res = mtbdd_storm_rational_function(mres); @@ -361,80 +210,53 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_less") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions and for Boolean (filter) */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - /* If one of Boolean, interpret as filter */ - if (a == mtbdd_true) return b; - if (b == mtbdd_true) return a; - - /* Handle multiplication of leaves */ + /* If both leaves, compute less */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); - if (storm_rational_function_less(ma, mb)) { - return mtbdd_true; - } else { - return mtbdd_false; - } + return storm_rational_function_less(ma, mb) ? mtbdd_true : mtbdd_false; } return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_less_or_equal") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions and for Boolean (filter) */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - - /* If one of Boolean, interpret as filter */ - if (a == mtbdd_true) return b; - if (b == mtbdd_true) return a; - - /* Handle multiplication of leaves */ + + /* If both leaves, compute less or equal */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); - if (storm_rational_function_less_or_equal(ma, mb)) { - return mtbdd_true; - } else { - return mtbdd_false; - } + return storm_rational_function_less_or_equal(ma, mb) ? mtbdd_true : mtbdd_false; } return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_mod") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions and for Boolean (filter) */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - /* If one of Boolean, interpret as filter */ - if (a == mtbdd_true) return b; - if (b == mtbdd_true) return a; - - /* Handle multiplication of leaves */ + /* If both leaves, compute modulo */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres = storm_rational_function_mod(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -443,26 +265,19 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, pa, MTBDD*, pb return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_mod") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions and for Boolean (filter) */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - /* If one of Boolean, interpret as filter */ - if (a == mtbdd_true) return b; - if (b == mtbdd_true) return a; - - /* Handle multiplication of leaves */ + /* If both leaves, compute min */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres = storm_rational_function_min(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -477,9 +292,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, pa, MTBDD*, pb return mtbdd_invalid; } -TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, a, MTBDD, b, int, k) -{ - LOG_I("task_impl_3 abstract_op_min") +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, a, MTBDD, b, int, k) { if (k==0) { return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_min)); } else { @@ -493,26 +306,19 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, a, MTB } } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_max, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_mod") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_max, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions and for Boolean (filter) */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - /* If one of Boolean, interpret as filter */ - if (a == mtbdd_true) return b; - if (b == mtbdd_true) return a; - - /* Handle multiplication of leaves */ + /* If both leaves, compute max */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres = storm_rational_function_max(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -527,9 +333,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_max, MTBDD*, pa, MTBDD*, pb return mtbdd_invalid; } -TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, a, MTBDD, b, int, k) -{ - LOG_I("task_impl_3 abstract_op_max") +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, a, MTBDD, b, int, k) { if (k==0) { return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_max)); } else { @@ -543,26 +347,19 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, a, MTB } } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, pa, MTBDD*, pb) -{ - LOG_I("task_impl_2 op_pow") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; /* Check for partial functions and for Boolean (filter) */ if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - /* If one of Boolean, interpret as filter */ - if (a == mtbdd_true) return b; - if (b == mtbdd_true) return a; - /* Handle multiplication of leaves */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres = storm_rational_function_pow(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -571,15 +368,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, pa, MTBDD*, pb return mtbdd_invalid; } -/** - * The abstraction operators are called in either of two ways: - * - with k=0, then just calculate "a op b" - * - with k<>0, then just calculate "a := a op a", k times - */ - -TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MTBDD, b, int, k) -{ - LOG_I("task_impl_3 abstract_op_plus") +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MTBDD, b, int, k) { if (k==0) { return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus)); } else { @@ -593,9 +382,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MT } } -TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, MTBDD, b, int, k) -{ - LOG_I("task_impl_3 abstract_op_times") +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, MTBDD, b, int, k) { if (k==0) { return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times)); } else { @@ -609,22 +396,16 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, M } } -/** - * Operation "neg" for one storm::RationalFunction MTBDD - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p) -{ - LOG_I("task_impl_2 op_neg") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p) { /* Handle partial functions */ if (dd == mtbdd_false) return mtbdd_false; /* Compute result for leaf */ if (mtbdd_isleaf(dd)) { - storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd); + storm_rational_function_ptr mdd = mtbdd_getstorm_rational_function_ptr(dd); storm_rational_function_ptr mres = storm_rational_function_negate(mdd); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -634,19 +415,16 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p) (void)p; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_floor, MTBDD, dd, size_t, p) -{ - LOG_I("task_impl_2 op_neg") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_floor, MTBDD, dd, size_t, p) { /* Handle partial functions */ if (dd == mtbdd_false) return mtbdd_false; /* Compute result for leaf */ if (mtbdd_isleaf(dd)) { - storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd); + storm_rational_function_ptr mdd = mtbdd_getstorm_rational_function_ptr(dd); storm_rational_function_ptr mres = storm_rational_function_floor(mdd); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -656,19 +434,16 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_floor, MTBDD, dd, size_t, p (void)p; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_ceil, MTBDD, dd, size_t, p) -{ - LOG_I("task_impl_2 op_neg") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_ceil, MTBDD, dd, size_t, p) { /* Handle partial functions */ if (dd == mtbdd_false) return mtbdd_false; /* Compute result for leaf */ if (mtbdd_isleaf(dd)) { - storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd); + storm_rational_function_ptr mdd = mtbdd_getstorm_rational_function_ptr(dd); storm_rational_function_ptr mres = storm_rational_function_ceil(mdd); MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -678,45 +453,14 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_ceil, MTBDD, dd, size_t, p) (void)p; } -/** - * Operation "replace leaves" for one storm::RationalFunction MTBDD - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, dd, size_t, context) -{ - LOG_I("task_impl_2 op_replace") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, dd, size_t, p) { /* Handle partial functions */ if (dd == mtbdd_false) return mtbdd_false; /* Compute result for leaf */ if (mtbdd_isleaf(dd)) { - if (mtbdd_gettype(dd) != srf_type) { - assert(0); - } - - storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd); - return storm_rational_function_leaf_parameter_replacement(dd, mdd, (void*)context); - } - - return mtbdd_invalid; -} -/** - * Operation to double for one storm::RationalFunction MTBDD - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, dd, size_t, p) -{ - LOG_I("task_impl_2 op_toDouble") - /* Handle partial functions */ - if (dd == mtbdd_false) return mtbdd_false; - - /* Compute result for leaf */ - if (mtbdd_isleaf(dd)) { - if (mtbdd_gettype(dd) != srf_type) { - printf("Can not convert to double, this has type %u!\n", mtbdd_gettype(dd)); - assert(0); - } - - storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd); - MTBDD result = mtbdd_double(storm_rational_function_get_constant(mdd)); + storm_rational_function_ptr mdd = mtbdd_getstorm_rational_function_ptr(dd); + MTBDD result = mtbdd_double(storm_rational_function_get_value_double(mdd)); return result; } @@ -724,12 +468,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, dd, size_ (void)p; } -/** - * Multiply and , and abstract variables using summation. - * This is similar to the "and_exists" operation in BDDs. - */ -TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b, MTBDD, v) -{ +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b, MTBDD, v) { /* Check terminal cases */ /* If v == true, then is an empty set */ @@ -803,80 +542,24 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b return result; } -/** - * Apply a unary operation to
. - * Callback is consulted after the cache, thus the application to a terminal is cached. - */ -TASK_DECL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, mtbdd_uapply_op, size_t); -#define mtbdd_uapply_nocache(dd, op, param) CALL(mtbdd_uapply_nocache, dd, op, param) - -/** - * Functionality regarding the replacement of leaves in MTBDDs. - */ - -/** - * Operation "replace" for one storm::RationalFunction MTBDD - */ -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, size_t) - -/** - * Compute the MTBDD that arises from a after calling the mtbddLeaveReplacementFunction on each leaf. - */ -#define sylvan_storm_rational_function_replace_leaves(a, ctx) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_replace_leaves), ctx) - -/** - * Takes a storm::RationalFunction MTBDD and transforms it into a double MTBDD - */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, size_t) - -/** - * Compute the MTBDD that arises from a after calling the mtbddLeaveReplacementFunction on each leaf. - */ #define sylvan_storm_rational_function_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_to_double), 0) - - -TASK_DECL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD); -#define sylvan_storm_rational_function_minimum(dd) CALL(sylvan_storm_rational_function_minimum, dd) - -TASK_DECL_1(MTBDD, sylvan_storm_rational_function_maximum, MTBDD); -#define sylvan_storm_rational_function_maximum(dd) CALL(sylvan_storm_rational_function_maximum, dd) - TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, size_t) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, size_t) @@ -211,7 +82,6 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, si TASK_DECL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, storm_rational_function_ptr); #define sylvan_storm_rational_function_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value) - TASK_DECL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, storm_rational_function_ptr); #define sylvan_storm_rational_function_strict_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value) diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c new file mode 100644 index 000000000..46470188b --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c @@ -0,0 +1,641 @@ +#include + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include +#include +#include + +uint32_t srn_type; + +static uint64_t sylvan_storm_rational_number_hash(const uint64_t v, const uint64_t seed) { + storm_rational_number_ptr x = (storm_rational_number_ptr)v; + return storm_rational_number_hash(x, seed); +} + +static int sylvan_storm_rational_number_equals(const uint64_t left, const uint64_t right) { + return storm_rational_number_equals((storm_rational_number_ptr)(size_t)left, (storm_rational_number_ptr)(size_t)right); +} + +static void sylvan_storm_rational_number_create(uint64_t *val) { + // This function is called by the unique table when a leaf does not yet exist. We make a copy, which will be stored in the hash table. + storm_rational_number_ptr* x = (storm_rational_number_ptr*)(size_t)val; + storm_rational_number_init(x); +} + +static void sylvan_storm_rational_number_destroy(uint64_t val) { + // This function is called by the unique table when a leaf is removed during garbage collection. + storm_rational_number_ptr x = (storm_rational_number_ptr)(size_t)val; + storm_rational_number_destroy(x); +} + +static char* sylvan_storm_rational_number_to_str(int comp, uint64_t val, char *buf, size_t buflen) { + return storm_rational_number_to_str((storm_rational_number_ptr)(size_t)val, *buf, buflen); + (void)comp; +} + +void sylvan_storm_rational_number_init() { + // Register custom leaf type storing rational functions. + srn_type = sylvan_mt_create_type(); + sylvan_mt_set_hash(srn_type, sylvan_storm_rational_number_hash); + sylvan_mt_set_equals(srn_type, sylvan_storm_rational_number_equals); + sylvan_mt_set_create(srn_type, sylvan_storm_rational_number_create); + sylvan_mt_set_destroy(srn_type, sylvan_storm_rational_number_destroy); + sylvan_mt_set_to_str(srn_type, sylvan_storm_rational_number_to_str); + // sylvan_mt_set_write_binary(srn_type, sylvan_storm_rational_number_write_binary); + // sylvan_mt_set_read_binary(srn_type, sylvan_storm_rational_number_read_binary); +} + +uint32_t sylvan_storm_rational_number_get_type() { + return srn_type; +} + +MTBDD mtbdd_storm_rational_number(storm_rational_number_ptr val) { + uint64_t terminalValue = (uint64_t)val; + return mtbdd_makeleaf(srn_type, terminalValue); +} + +storm_rational_number_ptr mtbdd_getstorm_rational_number_ptr(MTBDD terminal) { + uint64_t value = mtbdd_getvalue(terminal); + return (storm_rational_number_ptr*)value; +} + +TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_number, MTBDD, a, size_t, v) { + if (a == mtbdd_false) { + return mtbdd_storm_rational_number(storm_rational_number_get_zero()); + } + if (a == mtbdd_true) { + return mtbdd_storm_rational_number(storm_rational_number_get_one()); + } + + // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). + (void)v; + + return mtbdd_invalid; +} + +TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_number, MTBDD, dd) { + return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_number), 0); +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_equals, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + return storm_rational_number_equals(ma, mb) ? mtbdd_true : mtbdd_false; + } + + /* Commutative, so swap a,b for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_plus, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false) return b; + if (b == mtbdd_false) return a; + + /* If both leaves, compute plus */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + + storm_rational_number_ptr mres = storm_rational_number_plus(ma, mb); + MTBDD res = mtbdd_storm_rational_number(mres); + storm_rational_number_destroy(mres); + + return res; + } + + /* Commutative, so swap a,b for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_minus, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false) return sylvan_storm_rational_number_neg(b); + if (b == mtbdd_false) return a; + + /* If both leaves, compute minus */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + + storm_rational_number_ptr mres = storm_rational_number_minus(ma, mb); + MTBDD res = mtbdd_storm_rational_number(mres); + storm_rational_number_destroy(mres); + + return res; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_times, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If both leaves, compute multiplication */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + + storm_rational_number_ptr mres = storm_rational_number_times(ma, mb); + MTBDD res = mtbdd_storm_rational_number(mres); + storm_rational_number_destroy(mres); + + return res; + } + + /* Commutative, so make "a" the lowest for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_divide, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If both leaves, compute division */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mres; + if (storm_rational_number_is_zero(ma)) { + mres = storm_rational_number_get_zero(); + } else { + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + mres = storm_rational_number_divide(ma, mb); + } + MTBDD res = mtbdd_storm_rational_number(mres); + storm_rational_number_destroy(mres); + + return res; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_less, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If both leaves, compute less */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + + return storm_rational_number_less(ma, mb) ? mtbdd_true : mtbdd_false; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If both leaves, compute less or equal */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + + return storm_rational_number_less_or_equal(ma, mb) ? mtbdd_true : mtbdd_false; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_mod, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If both leaves, compute modulo */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + + storm_rational_number_ptr mres = storm_rational_number_mod(ma, mb); + MTBDD res = mtbdd_storm_rational_number(mres); + storm_rational_number_destroy(mres); + + return res; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_min, MTBDD*, pa, MTBDD*, pb) { + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If both leaves, compute min */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); + + storm_rational_number_ptr mres = storm_rational_number_min(ma, mb); + MTBDD res = mtbdd_storm_rational_number(mres); + storm_rational_number_destroy(mres); + + return res; + } + + /* Commutative, so make "a" the lowest for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + +TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_abstract_op_min, MTBDD, a, MTBDD, b, int, k) { + if (k==0) { + return mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_min)); + } else { + MTBDD res = a; + for (int i=0; i is an empty set */ + if (v == mtbdd_true) return mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_times)); + + /* Try the times operator on a and b */ + MTBDD result = CALL(sylvan_storm_rational_number_op_times, &a, &b); + if (result != mtbdd_invalid) { + /* Times operator successful, store reference (for garbage collection) */ + mtbdd_refs_push(result); + /* ... and perform abstraction */ + result = mtbdd_abstract(result, v, TASK(sylvan_storm_rational_number_abstract_op_plus)); + mtbdd_refs_pop(1); + /* Note that the operation cache is used in mtbdd_abstract */ + return result; + } + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Check cache. Note that we do this now, since the times operator might swap a and b (commutative) */ + if (cache_get3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, &result)) return result; + + /* Now, v is not a constant, and either a or b is not a constant */ + + /* Get top variable */ + int la = mtbdd_isleaf(a); + int lb = mtbdd_isleaf(b); + mtbddnode_t na = la ? 0 : MTBDD_GETNODE(a); + mtbddnode_t nb = lb ? 0 : MTBDD_GETNODE(b); + uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); + uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); + uint32_t var = va < vb ? va : vb; + + mtbddnode_t nv = MTBDD_GETNODE(v); + uint32_t vv = mtbddnode_getvariable(nv); + + if (vv < var) { + /* Recursive, then abstract result */ + result = CALL(sylvan_storm_rational_number_and_exists, a, b, node_gethigh(v, nv)); + mtbdd_refs_push(result); + result = mtbdd_apply(result, result, TASK(sylvan_storm_rational_number_op_plus)); + mtbdd_refs_pop(1); + } else { + /* Get cofactors */ + MTBDD alow, ahigh, blow, bhigh; + alow = (!la && va == var) ? node_getlow(a, na) : a; + ahigh = (!la && va == var) ? node_gethigh(a, na) : a; + blow = (!lb && vb == var) ? node_getlow(b, nb) : b; + bhigh = (!lb && vb == var) ? node_gethigh(b, nb) : b; + + if (vv == var) { + /* Recursive, then abstract result */ + mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_number_and_exists, ahigh, bhigh, node_gethigh(v, nv))); + MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_number_and_exists, alow, blow, node_gethigh(v, nv))); + MTBDD high = mtbdd_refs_push(mtbdd_refs_sync(SYNC(sylvan_storm_rational_number_and_exists))); + result = CALL(mtbdd_apply, low, high, TASK(sylvan_storm_rational_number_op_plus)); + mtbdd_refs_pop(2); + } else /* vv > v */ { + /* Recursive, then create node */ + mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_number_and_exists, ahigh, bhigh, v)); + MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_number_and_exists, alow, blow, v)); + MTBDD high = mtbdd_refs_sync(SYNC(sylvan_storm_rational_number_and_exists)); + mtbdd_refs_pop(1); + result = mtbdd_makenode(var, low, high); + } + } + + /* Store in cache */ + cache_put3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, result); + return result; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t, svalue) { + storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; + + if (mtbdd_isleaf(a)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + return storm_rational_number_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, size_t, svalue) { + storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; + + if (mtbdd_isleaf(a)) { + storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + + return storm_rational_number_less(ma, value) ? mtbdd_false : mtbdd_true; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, dd, storm_rational_number_ptr, value) +{ + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_threshold), *(size_t*)value); +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_strict_threshold, MTBDD, dd, storm_rational_number_ptr, value) +{ + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_strict_threshold), *(size_t*)value); +} + +TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) { + /* Check terminal case */ + if (a == mtbdd_false) return mtbdd_false; + mtbddnode_t na = MTBDD_GETNODE(a); + if (mtbddnode_isleaf(na)) return a; + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, &result)) return result; + + /* Call recursive */ + SPAWN(mtbdd_minimum, node_getlow(a, na)); + MTBDD high = CALL(sylvan_storm_rational_number_minimum, node_gethigh(a, na)); + MTBDD low = SYNC(sylvan_storm_rational_number_minimum); + + storm_rational_number_ptr fl = mtbdd_getstorm_rational_number_ptr(low); + storm_rational_number_ptr fh = mtbdd_getstorm_rational_number_ptr(high); + + if (storm_rational_number_less_or_equal(fl, fh)) { + return low; + } else { + return high; + } + + /* Store in cache */ + cache_put3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, result); + return result; +} + +TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD, a) +{ + /* Check terminal case */ + if (a == mtbdd_false) return mtbdd_false; + mtbddnode_t na = MTBDD_GETNODE(a); + if (mtbddnode_isleaf(na)) return a; + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, &result)) return result; + + /* Call recursive */ + SPAWN(mtbdd_minimum, node_getlow(a, na)); + MTBDD high = CALL(sylvan_storm_rational_number_maximum, node_gethigh(a, na)); + MTBDD low = SYNC(sylvan_storm_rational_number_maximum); + + storm_rational_number_ptr fl = mtbdd_getstorm_rational_number_ptr(low); + storm_rational_number_ptr fh = mtbdd_getstorm_rational_number_ptr(high); + + if (storm_rational_number_less(fl, fh)) { + return high; + } else { + return low; + } + + /* Store in cache */ + cache_put3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, result); + return result; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h new file mode 100644 index 000000000..6a5cc155f --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h @@ -0,0 +1,89 @@ +#ifndef SYLVAN_STORM_RATIONAL_NUMBER_H +#define SYLVAN_STORM_RATIONAL_NUMBER_H + +#include +#include + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +void sylvan_storm_rational_number_init(); +uint32_t sylvan_storm_rational_number_get_type(); +MTBDD mtbdd_storm_rational_number(storm_rational_number_ptr val); +storm_rational_number_ptr mtbdd_getstorm_rational_number_ptr(MTBDD terminal); + +TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_number, MTBDD, size_t) +TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_number, MTBDD) +#define mtbdd_bool_to_storm_rational_number(dd) CALL(mtbdd_bool_to_storm_rational_number, dd) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_equals, MTBDD*, MTBDD*) +#define mtbdd_equals_rational_number(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_equals)) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_plus, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_minus, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_times, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_divide, MTBDD*, MTBDD*) + +TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_plus, MTBDD, MTBDD, int) +TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_times, MTBDD, MTBDD, int) +TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_min, MTBDD, MTBDD, int) +TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_max, MTBDD, MTBDD, int) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_less, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_less_or_equal, MTBDD*, MTBDD*) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_mod, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_pow, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_min, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_max, MTBDD*, MTBDD*) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_neg, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_floor, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_ceil, MTBDD, size_t) + +#define sylvan_storm_rational_number_plus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_plus)) +#define sylvan_storm_rational_number_minus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_minus)) +#define sylvan_storm_rational_number_times(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_times)) +#define sylvan_storm_rational_number_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_divide)) +#define sylvan_storm_rational_number_less(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_less)) +#define sylvan_storm_rational_number_less_or_equal(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_less_or_equal)) +#define sylvan_storm_rational_number_mod(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_less_or_equal)) +#define sylvan_storm_rational_number_min(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_min)) +#define sylvan_storm_rational_number_max(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_max)) +#define sylvan_storm_rational_number_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_number_op_neg), 0) +#define sylvan_storm_rational_number_floor(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_number_op_floor), 0) +#define sylvan_storm_rational_number_ceil(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_number_op_ceil), 0) +#define sylvan_storm_rational_number_pow(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_pow)) + +TASK_DECL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD); +#define sylvan_storm_rational_number_minimum(dd) CALL(sylvan_storm_rational_number_minimum, dd) + +TASK_DECL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD); +#define sylvan_storm_rational_number_maximum(dd) CALL(sylvan_storm_rational_number_maximum, dd) + +TASK_DECL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, MTBDD, MTBDD); +#define sylvan_storm_rational_number_and_exists(a, b, vars) CALL(sylvan_storm_rational_number_and_exists, a, b, vars) + +#define sylvan_storm_rational_number_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_number_abstract_op_plus)) +#define sylvan_storm_rational_number_abstract_min(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_number_abstract_op_min)) +#define sylvan_storm_rational_number_abstract_max(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_number_abstract_op_max)) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_to_double, MTBDD, size_t) +#define sylvan_storm_rational_number_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_number_op_to_double), 0) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, size_t) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, storm_rational_number_ptr); +#define sylvan_storm_rational_number_threshold(dd, value) CALL(sylvan_storm_rational_number_strict_threshold, dd, value) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_strict_threshold, MTBDD, storm_rational_number_ptr); +#define sylvan_storm_rational_number_strict_threshold(dd, value) CALL(sylvan_storm_rational_number_strict_threshold, dd, value) + +#ifdef __cplusplus +} +#endif /* __cplusplus */ + + +#endif // SYLVAN_STORM_RATIONAL_NUMBER_H diff --git a/src/storm/adapters/CarlAdapter.h b/src/storm/adapters/CarlAdapter.h index d6360041e..41a1c0cde 100644 --- a/src/storm/adapters/CarlAdapter.h +++ b/src/storm/adapters/CarlAdapter.h @@ -1,27 +1,7 @@ -#ifndef STORM_ADAPTERS_CARLADAPTER_H_ -#define STORM_ADAPTERS_CARLADAPTER_H_ +#pragma once -// Include config to know whether CARL is available or not. -#include "storm-config.h" +#include "storm/adapters/NumberAdapter.h" -#include - -#ifdef STORM_HAVE_CLN -#pragma clang diagnostic push -#pragma clang diagnostic ignored "-Wmismatched-tags" - -#pragma GCC diagnostic push - -#include - -#pragma GCC diagnostic pop -#pragma clang diagnostic pop - -#endif - -#ifdef STORM_HAVE_CARL - -#include #include #include #include @@ -58,27 +38,20 @@ namespace carl { } -inline size_t hash_value(mpq_class const& q) { - std::hash h; - return h(q); -} - - -#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_NUMBERS -namespace cln { - inline size_t hash_value(cl_RA const& n) { - std::hash h; - return h(n); - } -} -#endif - - -#include "NumberAdapter.h" - namespace storm { typedef carl::Variable RationalFunctionVariable; - typedef carl::MultivariatePolynomial RawPolynomial; + +#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_EA + typedef cln::cl_RA RationalFunctionCoefficient; +#elif defined STORM_HAVE_GMP && !defined STORM_USE_CLN_EA + typedef mpq_class RationalFunctionCoefficient; +#elif defined STORM_USE_CLN_EA +#error CLN is to be used, but is not available. +#else +#error GMP is to be used, but is not available. +#endif + + typedef carl::MultivariatePolynomial RawPolynomial; typedef carl::FactorizedPolynomial Polynomial; typedef carl::Cache> RawPolynomialCache; typedef carl::Relation CompareRelation; @@ -87,7 +60,3 @@ namespace storm { typedef carl::Interval Interval; template using ArithConstraint = carl::SimpleConstraint; } - -#endif - -#endif /* STORM_ADAPTERS_CARLADAPTER_H_ */ diff --git a/src/storm/adapters/NumberAdapter.h b/src/storm/adapters/NumberAdapter.h index 55427841b..3258dcb96 100644 --- a/src/storm/adapters/NumberAdapter.h +++ b/src/storm/adapters/NumberAdapter.h @@ -2,14 +2,44 @@ #include "storm-config.h" -#ifdef STORM_HAVE_CARL +#if defined STORM_HAVE_CLN +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wmismatched-tags" +#include +#pragma clang diagnostic pop +#endif + +#if defined STORM_HAVE_GMP +#include +#include +#endif #include + +#if defined STORM_HAVE_CLN && (defined STORM_USE_CLN_EA || defined STORM_USE_CLN_RF) +namespace cln { + inline size_t hash_value(cl_RA const& n) { + std::hash h; + return h(n); + } +} +#endif + +#if defined STORM_HAVE_GMP && (!defined STORM_USE_CLN_EA || !defined STORM_USE_CLN_RF) +inline size_t hash_value(mpq_class const& q) { + std::hash h; + return h(q); +} +#endif + namespace storm { -#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_NUMBERS +#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_EA typedef cln::cl_RA RationalNumber; -#else +#elif defined STORM_HAVE_GMP && !defined STORM_USE_CLN_EA typedef mpq_class RationalNumber; +#elif defined STORM_USE_CLN_EA +#error CLN is to be used, but is not available. +#else +#error GMP is to be used, but is not available. #endif } -#endif diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index d53974178..a7834b281 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -468,7 +468,7 @@ namespace storm { // If the new state was already found as a successor state, update the probability // and otherwise insert it. - auto probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()); + ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()); if (edge.hasRate()) { probability *= this->evaluator->asRational(edge.getRate()); } diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 103659212..fd5f687a6 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -817,42 +817,6 @@ namespace storm { return internalAdd; } -#ifdef STORM_HAVE_CARL - template - Add Add::replaceLeaves(std::map>> const&) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Not yet implemented: replaceLeaves"); - } - - template<> - Add Add::replaceLeaves(std::map>> const& replacementMap) const { - std::map>> internalReplacementMap; - std::set containedMetaVariables = this->getContainedMetaVariables(); - - uint32_t highestIndex = 0; - for (storm::expressions::Variable const& var: containedMetaVariables) { - uint32_t index = this->getDdManager().getMetaVariable(var).getDdVariables().at(0).getIndex(); - if (index > highestIndex) { - highestIndex = index; - } - } - - std::map>>::const_iterator it = replacementMap.cbegin(); - std::map>>::const_iterator end = replacementMap.cend(); - - for (; it != end; ++it) { - DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(it->second.first); - STORM_LOG_THROW(metaVariable.getNumberOfDdVariables() == 1, storm::exceptions::InvalidArgumentException, "Cannot use MetaVariable with more then one internal DD variable."); - - auto const& ddVariable = metaVariable.getDdVariables().at(0); - STORM_LOG_ASSERT(ddVariable.getIndex() > highestIndex, "Can not replace leaves with DD variable that would not be at the bottom!"); - - internalReplacementMap.insert(std::make_pair(ddVariable.getIndex(), std::make_pair(it->first, it->second.second))); - containedMetaVariables.insert(it->second.first); - } - - return Add(this->getDdManager(), internalAdd.replaceLeaves(internalReplacementMap), containedMetaVariables); - } - template template Add Add::toValueType() const { @@ -862,6 +826,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); } +#ifdef STORM_HAVE_CARL template<> template<> Add Add::toValueType() const { diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 627d47de6..62d6b999c 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -245,25 +245,15 @@ namespace storm { * @return The resulting function represented as an ADD. */ Add maximum(Add const& other) const; - -#ifdef STORM_HAVE_CARL - /*! - * Replaces the leaves in this MTBDD, using the supplied variable replacement map. - * - * @param replacementMap The variable replacement map. - * @return The resulting function represented as an ADD. - */ - Add replaceLeaves(std::map>> const& replacementMap) const; - - /*! + + /*! * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else. * * @return The resulting function represented as an ADD. */ template Add toValueType() const; -#endif - + /*! * Sum-abstracts from the given meta variables. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index eca2fdfce..65933570c 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -49,6 +49,21 @@ namespace storm { } } + template<> + storm::RationalNumber InternalAdd::getValue(MTBDD const& node) { + STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); + + bool negated = mtbdd_hascomp(node); + + STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_number_get_type(), "Expected a storm::RationalNumber value."); + uint64_t value = mtbdd_getvalue(node); + storm_rational_number_ptr ptr = (storm_rational_number_ptr)value; + + storm::RationalNumber* rationalNumber = (storm::RationalNumber*)(ptr); + + return negated ? -(*rationalNumber) : (*rationalNumber); + } + #ifdef STORM_HAVE_CARL template<> storm::RationalFunction InternalAdd::getValue(MTBDD const& node) { @@ -81,6 +96,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::operator+(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.PlusRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator+(InternalAdd const& other) const { @@ -94,6 +114,12 @@ namespace storm { return *this; } + template<> + InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.PlusRN(other.sylvanMtbdd); + return *this; + } + #ifdef STORM_HAVE_CARL template<> InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { @@ -107,6 +133,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Times(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::operator*(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.TimesRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator*(InternalAdd const& other) const { @@ -120,6 +151,12 @@ namespace storm { return *this; } + template<> + InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.TimesRN(other.sylvanMtbdd); + return *this; + } + #ifdef STORM_HAVE_CARL template<> InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { @@ -133,6 +170,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Minus(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::operator-(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.MinusRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator-(InternalAdd const& other) const { @@ -146,6 +188,12 @@ namespace storm { return *this; } + template<> + InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.MinusRN(other.sylvanMtbdd); + return *this; + } + #ifdef STORM_HAVE_CARL template<> InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { @@ -159,6 +207,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Divide(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::operator/(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.DivideRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator/(InternalAdd const& other) const { @@ -172,6 +225,12 @@ namespace storm { return *this; } + template<> + InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.DivideRN(other.sylvanMtbdd); + return *this; + } + #ifdef STORM_HAVE_CARL template<> InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { @@ -185,6 +244,11 @@ namespace storm { return InternalBdd(ddManager, this->sylvanMtbdd.Equals(other.sylvanMtbdd)); } + template<> + InternalBdd InternalAdd::equals(InternalAdd const& other) const { + return InternalBdd(ddManager, this->sylvanMtbdd.EqualsRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::equals(InternalAdd const& other) const { @@ -202,6 +266,11 @@ namespace storm { return InternalBdd(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd)); } + template<> + InternalBdd InternalAdd::less(InternalAdd const& other) const { + return InternalBdd(ddManager, this->sylvanMtbdd.LessRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::less(InternalAdd const& other) const { @@ -214,6 +283,11 @@ namespace storm { return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqual(other.sylvanMtbdd)); } + template<> + InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqualRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { @@ -236,6 +310,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::pow(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.PowRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::pow(InternalAdd const& other) const { @@ -248,6 +327,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Mod(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::mod(InternalAdd const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational numbers."); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::mod(InternalAdd const&) const { @@ -260,6 +344,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Logxy(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::logxy(InternalAdd const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (logxy) not supported by rational numbers."); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::logxy(InternalAdd const&) const { @@ -272,6 +361,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Floor()); } + template<> + InternalAdd InternalAdd::floor() const { + return InternalAdd(ddManager, this->sylvanMtbdd.FloorRN()); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::floor() const { @@ -284,6 +378,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Ceil()); } + template<> + InternalAdd InternalAdd::ceil() const { + return InternalAdd(ddManager, this->sylvanMtbdd.CeilRN()); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::ceil() const { @@ -296,6 +395,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Min(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.MinRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::minimum(InternalAdd const& other) const { @@ -308,6 +412,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Max(other.sylvanMtbdd)); } + template<> + InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.MaxRN(other.sylvanMtbdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::maximum(InternalAdd const& other) const { @@ -315,18 +424,6 @@ namespace storm { } #endif - template - InternalAdd InternalAdd::replaceLeaves(std::map>> const&) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Replacing leaves is not supported for types other than rational functions."); - } - -#ifdef STORM_HAVE_CARL - template<> - InternalAdd InternalAdd::replaceLeaves(std::map>> const& replacementMap) const { - return InternalAdd(ddManager, this->sylvanMtbdd.ReplaceLeavesRF((void*)&replacementMap)); - } -#endif - template template InternalAdd InternalAdd::toValueType() const { @@ -335,6 +432,13 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); } + + template<> + template<> + InternalAdd InternalAdd::toValueType() const { + return InternalAdd(ddManager, this->sylvanMtbdd.ToDoubleRN()); + } + #ifdef STORM_HAVE_CARL template<> @@ -349,6 +453,11 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlus(cube.sylvanBdd)); } + template<> + InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlusRN(cube.sylvanBdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { @@ -366,6 +475,11 @@ namespace storm { return InternalBdd(ddManager, this->sylvanMtbdd.AbstractMinRepresentative(cube.sylvanBdd)); } + template<> + InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMinRN(cube.sylvanBdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { @@ -383,6 +497,11 @@ namespace storm { return InternalBdd(ddManager, this->sylvanMtbdd.AbstractMaxRepresentative(cube.sylvanBdd)); } + template<> + InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMaxRN(cube.sylvanBdd)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { @@ -439,6 +558,16 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } + + template<> + InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + InternalBdd summationVariables = ddManager->getBddOne(); + for (auto const& ddVariable : summationDdVariables) { + summationVariables &= ddVariable; + } + + return InternalAdd(ddManager, this->sylvanMtbdd.AndExistsRN(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); + } #ifdef STORM_HAVE_CARL template<> @@ -457,20 +586,34 @@ namespace storm { return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThreshold(value)); } + template<> + InternalBdd InternalAdd::greater(storm::RationalNumber const& value) const { + return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThresholdRN(value)); + } + +#ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::greater(storm::RationalFunction const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThresholdRF(value)); } +#endif template InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddThreshold(value)); } + + template<> + InternalBdd InternalAdd::greaterOrEqual(storm::RationalNumber const& value) const { + return InternalBdd(ddManager, this->sylvanMtbdd.BddThresholdRN(value)); + } +#ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddThresholdRF(value)); } +#endif template InternalBdd InternalAdd::less(ValueType const& value) const { @@ -524,21 +667,35 @@ namespace storm { ValueType InternalAdd::getMin() const { return getValue(this->sylvanMtbdd.Minimum().GetMTBDD()); } + + template <> + storm::RationalNumber InternalAdd::getMin() const { + return getValue(this->sylvanMtbdd.MinimumRN().GetMTBDD()); + } +#ifdef STORM_HAVE_CARL template <> storm::RationalFunction InternalAdd::getMin() const { return getValue(this->sylvanMtbdd.MinimumRF().GetMTBDD()); } +#endif template ValueType InternalAdd::getMax() const { return getValue(this->sylvanMtbdd.Maximum().GetMTBDD()); } + template<> + storm::RationalNumber InternalAdd::getMax() const { + return getValue(this->sylvanMtbdd.MaximumRN().GetMTBDD()); + } + +#ifdef STORM_HAVE_CARL template<> storm::RationalFunction InternalAdd::getMax() const { return getValue(this->sylvanMtbdd.MaximumRF().GetMTBDD()); } +#endif template ValueType InternalAdd::getValue() const { @@ -904,10 +1061,15 @@ namespace storm { template MTBDD InternalAdd::getLeaf(storm::RationalFunction const& value) { storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value); - return mtbdd_storm_rational_function(ptr); } + template + MTBDD InternalAdd::getLeaf(storm::RationalNumber const& value) { + storm_rational_function_ptr ptr = (storm_rational_number_ptr)(&value); + return mtbdd_storm_rational_number(ptr); + } + template sylvan::Mtbdd InternalAdd::getSylvanMtbdd() const { return sylvanMtbdd; @@ -915,7 +1077,9 @@ namespace storm { template class InternalAdd; template class InternalAdd; - + + template class InternalAdd; + #ifdef STORM_HAVE_CARL template class InternalAdd; #endif diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 1dd0358ad..b53fb0f76 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -248,15 +248,6 @@ namespace storm { */ InternalAdd maximum(InternalAdd const& other) const; -#ifdef STORM_HAVE_CARL - /*! - * Replaces the leaves in this MTBDD, using the supplied variable replacement map. - * - * @param replacementMap The variable replacement map. - * @return The resulting function represented as an ADD. - */ - InternalAdd replaceLeaves(std::map>> const& replacementMap) const; - /*! * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else. * @@ -264,7 +255,6 @@ namespace storm { */ template InternalAdd toValueType() const; -#endif /*! * Sum-abstracts from the given cube. @@ -708,9 +698,16 @@ namespace storm { */ static MTBDD getLeaf(uint_fast64_t value); + /*! + * Retrieves the sylvan representation of the given storm::RatíonalNumber. + * + * @return The sylvan node for the given value. + */ + static MTBDD getLeaf(storm::RationalNumber const& value); + #ifdef STORM_HAVE_CARL /*! - * Retrieves the sylvan representation of the given storm::RatíonalFunction value. + * Retrieves the sylvan representation of the given storm::RatíonalFunction. * * @return The sylvan node for the given value. */ diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index 4ef3a4a79..c026fbb1f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -82,6 +82,11 @@ namespace storm { return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::one())); } + template<> + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalNumberTerminal(storm::utility::one())); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getAddOne() const { @@ -103,6 +108,11 @@ namespace storm { return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero())); } + template<> + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalNumberTerminal(storm::utility::zero())); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getAddZero() const { @@ -119,7 +129,12 @@ namespace storm { InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const { return InternalAdd(this, sylvan::Mtbdd::int64Terminal(value)); } - + + template<> + InternalAdd InternalDdManager::getConstant(storm::RationalNumber const& value) const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalNumberTerminal(value)); + } + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const { @@ -162,18 +177,27 @@ namespace storm { template InternalAdd InternalDdManager::getAddOne() const; template InternalAdd InternalDdManager::getAddOne() const; + + template InternalAdd InternalDdManager::getAddOne() const; + #ifdef STORM_HAVE_CARL template InternalAdd InternalDdManager::getAddOne() const; #endif template InternalAdd InternalDdManager::getAddZero() const; template InternalAdd InternalDdManager::getAddZero() const; + + template InternalAdd InternalDdManager::getAddZero() const; + #ifdef STORM_HAVE_CARL template InternalAdd InternalDdManager::getAddZero() const; #endif template InternalAdd InternalDdManager::getConstant(double const& value) const; template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; + + template InternalAdd InternalDdManager::getConstant(storm::RationalNumber const& value) const; + #ifdef STORM_HAVE_CARL template InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; #endif diff --git a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp index 169b8922c..394e0fe08 100644 --- a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp +++ b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp @@ -190,6 +190,9 @@ namespace storm { template class AddIterator; template class AddIterator; + + template class AddIterator; + #ifdef STORM_HAVE_CARL template class AddIterator; #endif diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index e095fe4ed..2a31ee964 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -25,7 +25,7 @@ namespace storm { uint_fast64_t maxCol = halfspaces.front().normalVector().size(); uint_fast64_t maxRow = halfspaces.size(); A = EigenMatrix(maxRow, maxCol); - b = EigenVector(maxRow); + b = EigenVector(static_cast(maxRow)); for ( uint_fast64_t row = 0; row < maxRow; ++row ){ assert(halfspaces[row].normalVector().size() == maxCol); b(row) = halfspaces[row].offset(); diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp index 1dbca4cdf..cf982d0a0 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp @@ -27,7 +27,7 @@ namespace storm { std::vector const& subset = subsetEnum.getCurrentSubset(); EigenMatrix subMatrix(dimension, dimension); - EigenVector subVector(dimension); + EigenVector subVector(static_cast(dimension)); for (uint_fast64_t i = 0; i < dimension; ++i){ subMatrix.row(i) = constraintMatrix.row(subset[i]); subVector(i) = constraintVector(subset[i]); @@ -35,7 +35,7 @@ namespace storm { EigenVector point = subMatrix.fullPivLu().solve(subVector); bool pointContained = true; - for(uint_fast64_t row=0; row < constraintMatrix.rows(); ++row){ + for(int_fast64_t row=0; row < constraintMatrix.rows(); ++row){ if((constraintMatrix.row(row) * point)(0) > constraintVector(row)){ pointContained = false; break; diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index f2dbbef36..a7ae7ac80 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -150,7 +150,7 @@ namespace storm { uint_fast64_t numOfAdditionalConstraints = additionalConstraints.size(); uint_fast64_t numOfRegularConstraints = resultMatrix.rows(); EigenMatrix newA(numOfRegularConstraints + numOfAdditionalConstraints, resultMatrix.cols()); - EigenVector newb(numOfRegularConstraints + numOfAdditionalConstraints); + EigenVector newb(static_cast(numOfRegularConstraints + numOfAdditionalConstraints)); uint_fast64_t row = 0; for (; row < numOfRegularConstraints; ++ row) { newA.row(row) = resultMatrix.row(row); @@ -166,7 +166,7 @@ namespace storm { // clear the additionally added points. Note that the order of the points might have changed storm::storage::BitVector keptPoints(points.size(), true); for(uint_fast64_t pointIndex = 0; pointIndex < points.size(); ++pointIndex) { - for(uint_fast64_t row = 0; row < resultMatrix.rows(); ++row) { + for(int_fast64_t row = 0; row < resultMatrix.rows(); ++row) { if((resultMatrix.row(row) * points[pointIndex])(0) > resultVector(row)) { keptPoints.set(pointIndex, false); break; @@ -178,7 +178,7 @@ namespace storm { if(generateRelevantVerticesAndVertexSets) { storm::storage::BitVector keptVertices(relevantVertices.size(), true); for(uint_fast64_t vertexIndex = 0; vertexIndex < relevantVertices.size(); ++vertexIndex) { - for(uint_fast64_t row = 0; row < resultMatrix.rows(); ++row) { + for(int_fast64_t row = 0; row < resultMatrix.rows(); ++row) { if((resultMatrix.row(row) * relevantVertices[vertexIndex])(0) > resultVector(row)) { keptVertices.set(vertexIndex, false); break; diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 821b25bdb..1e88b8dfc 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -415,6 +415,11 @@ namespace storm { return carl::toInt(func.nominatorAsNumber()); } + template<> + double convertNumber(RationalFunction const& func) { + return carl::toDouble(func.nominatorAsNumber()); + } + template<> RationalFunction convertNumber(RationalFunction const& number){ return number; diff --git a/src/storm/utility/sylvan.h b/src/storm/utility/sylvan.h index f6d4e5ec1..c068b6ab9 100644 --- a/src/storm/utility/sylvan.h +++ b/src/storm/utility/sylvan.h @@ -13,6 +13,7 @@ #pragma GCC system_header // Only way to suppress some warnings atm. #include "sylvan_obj.hpp" +#include "sylvan_storm_rational_number.h" #include "sylvan_storm_rational_function.h" #pragma GCC diagnostic pop diff --git a/src/test/storage/SylvanDdTest.cpp b/src/test/storage/SylvanDdTest.cpp index 9d8c091cc..f480c6894 100644 --- a/src/test/storage/SylvanDdTest.cpp +++ b/src/test/storage/SylvanDdTest.cpp @@ -412,216 +412,6 @@ TEST(SylvanDd, EncodingTest) { EXPECT_EQ(2ul, add.getLeafCount()); } -#ifdef STORM_HAVE_CARL -TEST(SylvanDd, RationalFunctionLeaveReplacementNonVariable) { - std::shared_ptr> manager(new storm::dd::DdManager()); - storm::dd::Add zero; - ASSERT_NO_THROW(zero = manager->template getAddZero()); - - std::map>> replacementMap; - storm::dd::Add zeroReplacementResult = zero.replaceLeaves(replacementMap); - - EXPECT_EQ(0ul, zeroReplacementResult.getNonZeroCount()); - EXPECT_EQ(1ul, zeroReplacementResult.getLeafCount()); - EXPECT_EQ(1ul, zeroReplacementResult.getNodeCount()); - EXPECT_TRUE(zeroReplacementResult == zero); -} - -TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) { - std::shared_ptr> manager(new storm::dd::DdManager()); - - storm::dd::Add function; - - std::shared_ptr cache = std::make_shared(); - - carl::StringParser parser; - parser.setVariables({"x"}); - - storm::RawPolynomial polyX = parser.parseMultivariatePolynomial("x"); - storm::RationalFunction variableX = storm::RationalFunction(storm::Polynomial(polyX, cache)); - - ASSERT_NO_THROW(function = manager->template getConstant(variableX)); - - std::pair xExpr; - ASSERT_NO_THROW(xExpr = manager->addMetaVariable("x", 0, 1)); - - std::map>> replacementMap; - storm::RationalNumber rnOneThird = storm::RationalNumber(1) / storm::RationalNumber(3); - storm::RationalNumber rnTwoThird = storm::RationalNumber(2) / storm::RationalNumber(3); - replacementMap.insert(std::make_pair(parser.variables().find("x")->second, std::make_pair(xExpr.first, std::make_pair(rnOneThird, rnTwoThird)))); - - storm::dd::Add replacedAddSimpleX = function.replaceLeaves(replacementMap); - - storm::dd::Bdd bddX0 = manager->getEncoding(xExpr.first, 0); - storm::dd::Bdd bddX1 = manager->getEncoding(xExpr.first, 1); - - storm::dd::Add complexAdd = - (bddX0.template toAdd() * manager->template getConstant(storm::RationalFunction(rnTwoThird))) - + (bddX1.template toAdd() * manager->template getConstant(storm::RationalFunction(rnOneThird))); - - EXPECT_EQ(2ul, replacedAddSimpleX.getNonZeroCount()); - EXPECT_EQ(2ul, replacedAddSimpleX.getLeafCount()); - EXPECT_EQ(3ul, replacedAddSimpleX.getNodeCount()); - EXPECT_TRUE(replacedAddSimpleX == complexAdd); - - storm::dd::Add abstractedAddMax = replacedAddSimpleX.toValueType().maxAbstract({xExpr.first}); - storm::dd::Add abstractedAddMin = replacedAddSimpleX.toValueType().minAbstract({xExpr.first}); - EXPECT_TRUE(abstractedAddMax == manager->template getConstant(0.66666666666666666666)); - EXPECT_TRUE(abstractedAddMin == manager->template getConstant(0.33333333333333333333)); -} - -TEST(SylvanDd, RationalFunctionLeaveReplacementTwoVariables) { - std::shared_ptr> manager(new storm::dd::DdManager()); - - storm::dd::Add function; - std::shared_ptr cache = std::make_shared(); - carl::StringParser parser; - parser.setVariables({"x", "y"}); - - storm::RationalFunction variableX(storm::Polynomial(parser.template parseMultivariatePolynomial("x"), cache)); - storm::RationalFunction variableY(storm::Polynomial(parser.template parseMultivariatePolynomial("y"), cache)); - ASSERT_NO_THROW(function = manager->template getConstant(variableX * variableY)); - - std::pair xExpr; - std::pair yExpr; - ASSERT_NO_THROW(xExpr = manager->addMetaVariable("x", 0, 1)); - ASSERT_NO_THROW(yExpr = manager->addMetaVariable("y", 0, 1)); - - std::map>> replacementMap; - storm::RationalNumber rnOneThird = storm::RationalNumber(1) / storm::RationalNumber(3); - storm::RationalNumber rnTwoThird = storm::RationalNumber(2) / storm::RationalNumber(3); - storm::RationalNumber rnOne = storm::RationalNumber(1); - storm::RationalNumber rnTen = storm::RationalNumber(10); - replacementMap.insert(std::make_pair(parser.variables().find("x")->second, std::make_pair(xExpr.first, std::make_pair(rnOneThird, rnTwoThird)))); - replacementMap.insert(std::make_pair(parser.variables().find("y")->second, std::make_pair(yExpr.first, std::make_pair(rnOne, rnTen)))); - - storm::dd::Add replacedAdd = function.replaceLeaves(replacementMap); - - storm::dd::Bdd bddX0 = manager->getEncoding(xExpr.first, 0); - storm::dd::Bdd bddX1 = manager->getEncoding(xExpr.first, 1); - storm::dd::Bdd bddY0 = manager->getEncoding(yExpr.first, 0); - storm::dd::Bdd bddY1 = manager->getEncoding(yExpr.first, 1); - - storm::dd::Add complexAdd = - ((bddX0 && bddY0).template toAdd() * manager->template getConstant(storm::RationalFunction(rnTwoThird * rnTen))) - + ((bddX0 && bddY1).template toAdd() * manager->template getConstant(storm::RationalFunction(rnTwoThird))) - + ((bddX1 && bddY0).template toAdd() * manager->template getConstant(storm::RationalFunction(rnOneThird * rnTen))) - + ((bddX1 && bddY1).template toAdd() * manager->template getConstant(storm::RationalFunction(rnOneThird))); - - EXPECT_EQ(4ul, replacedAdd.getNonZeroCount()); - EXPECT_EQ(4ul, replacedAdd.getLeafCount()); - EXPECT_EQ(7ul, replacedAdd.getNodeCount()); - EXPECT_TRUE(replacedAdd == complexAdd); -} - -TEST(SylvanDd, RationalFunctionCarlSubstituteTest) { - std::shared_ptr cache = std::make_shared(); - carl::StringParser parser; - parser.setVariables({"x", "y", "z"}); - storm::RationalFunction zHalfed = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2"), cache)); - storm::RationalFunction rationalFunction = storm::RationalFunction(storm::Polynomial(parser.parseMultivariatePolynomial("2*x+x*y"), cache), storm::Polynomial(parser.parseMultivariatePolynomial("1"), cache)) + zHalfed; - - std::map replacement = {{parser.variables().find("x")->second, storm::RationalNumber(2)}}; - storm::RationalFunction subX = rationalFunction.substitute(replacement); - - storm::RationalFunction cmp = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("4+2*y"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("1"), cache)) + zHalfed; - EXPECT_EQ(subX, cmp); - - storm::RawPolynomial poly(parser.template parseMultivariatePolynomial("2*x+x*y") + parser.template parseMultivariatePolynomial("z") / storm::RationalNumber(2)); - storm::RawPolynomial polySub = poly.substitute(replacement); - EXPECT_EQ(polySub, parser.template parseMultivariatePolynomial("4+2*y") + parser.template parseMultivariatePolynomial("z") / storm::RationalNumber(2)); -} - -TEST(DISABLED_SylvanDd, RationalFunctionLeaveReplacementComplexFunction) { - std::shared_ptr> manager(new storm::dd::DdManager()); - - storm::dd::Add function; - std::shared_ptr cache = std::make_shared(); - carl::StringParser parser; - parser.setVariables({"x", "y", "z"}); - storm::RationalFunction zDivTwoY = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2*y"), cache)); - - storm::RationalFunction rationalFunction = storm::RationalFunction(storm::Polynomial(parser.parseMultivariatePolynomial("2*x+x*y"), cache), storm::Polynomial(parser.parseMultivariatePolynomial("1"), cache)) + zDivTwoY; - ASSERT_NO_THROW(function = manager->template getConstant(rationalFunction)); - - std::pair xExpr; - std::pair yExpr; - std::pair zExpr; - ASSERT_NO_THROW(xExpr = manager->addMetaVariable("x", 0, 1)); - ASSERT_NO_THROW(yExpr = manager->addMetaVariable("y", 0, 1)); - ASSERT_NO_THROW(zExpr = manager->addMetaVariable("z", 0, 1)); - - std::map>> replacementMap; - storm::RationalNumber rnTwo(2); - storm::RationalNumber rnThree(3); - storm::RationalNumber rnFive(5); - storm::RationalNumber rnSeven(7); - storm::RationalNumber rnEleven(11); - storm::RationalNumber rnThirteen(13); - replacementMap.insert(std::make_pair(parser.variables().find("x")->second, std::make_pair(xExpr.first, std::make_pair(rnTwo, rnSeven)))); - replacementMap.insert(std::make_pair(parser.variables().find("y")->second, std::make_pair(yExpr.first, std::make_pair(rnThree, rnEleven)))); - replacementMap.insert(std::make_pair(parser.variables().find("z")->second, std::make_pair(zExpr.first, std::make_pair(rnFive, rnThirteen)))); - - storm::dd::Add replacedAdd = function.replaceLeaves(replacementMap); - - storm::dd::Bdd bddX0 = manager->getEncoding(xExpr.first, 0); - storm::dd::Bdd bddX1 = manager->getEncoding(xExpr.first, 1); - storm::dd::Bdd bddY0 = manager->getEncoding(yExpr.first, 0); - storm::dd::Bdd bddY1 = manager->getEncoding(yExpr.first, 1); - storm::dd::Bdd bddZ0 = manager->getEncoding(zExpr.first, 0); - storm::dd::Bdd bddZ1 = manager->getEncoding(zExpr.first, 1); - - auto f = [&](bool x, bool y, bool z) { - storm::RationalNumber result(2); - if (!x) { - result *= rnSeven; - } else { - result *= rnTwo; - } - - storm::RationalNumber partTwo(1); - if (!x) { - partTwo *= rnSeven; - } else { - partTwo *= rnTwo; - } - if (!y) { - partTwo *= rnEleven; - } else { - partTwo *= rnThree; - } - - storm::RationalNumber partThree(1); - if (!z) { - partThree *= rnThirteen; - } else { - partThree *= rnFive; - } - if (!y) { - partThree /= storm::RationalNumber(2) * rnEleven; - } else { - partThree /= storm::RationalNumber(2) * rnThree; - } - - return result + partTwo + partThree; - }; - - storm::dd::Add complexAdd = - ((bddX0 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(false, false, false)))) - + ((bddX0 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(false, false, true)))) - + ((bddX0 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(false, true, false)))) - + ((bddX0 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(false, true, true)))) - + ((bddX1 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(true, false, false)))) - + ((bddX1 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(true, false, true)))) - + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(true, true, false)))) - + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(true, true, true)))); - - EXPECT_EQ(8ul, replacedAdd.getNonZeroCount()); - EXPECT_EQ(8ul, replacedAdd.getLeafCount()); - EXPECT_EQ(15ul, replacedAdd.getNodeCount()); - EXPECT_TRUE(replacedAdd == complexAdd); -} - TEST(SylvanDd, RationalFunctionConstants) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Add zero; @@ -747,7 +537,6 @@ TEST(SylvanDd, RationalFunctionIdentityTest) { EXPECT_EQ(10ul, identity.getLeafCount()); EXPECT_EQ(21ul, identity.getNodeCount()); } -#endif TEST(SylvanDd, RangeTest) { std::shared_ptr> manager(new storm::dd::DdManager()); diff --git a/storm-config.h.in b/storm-config.h.in index ae56a6fd9..9e6e07ba6 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -53,14 +53,19 @@ // Whether CLN is available and to be used (define/undef) #cmakedefine STORM_HAVE_CLN +// Whether GMP is available and to be used (define/undef) +#cmakedefine STORM_HAVE_GMP + // Whether carl is available and to be used. #cmakedefine STORM_HAVE_CARL -#cmakedefine STORM_USE_CLN_NUMBERS +#cmakedefine STORM_USE_CLN_EA + +#cmakedefine STORM_USE_CLN_RF #cmakedefine STORM_HAVE_XERCES -// Whether smtrat is available and to be used. +// Whether smtrat is available and to be used. #cmakedefine STORM_HAVE_SMTRAT // Whether HyPro is available and to be used.
. - */ -TASK_IMPL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, dd, mtbdd_uapply_op, op, size_t, param) -{ - /* Maybe perform garbage collection */ - sylvan_gc_test(); - - /* Check cache */ - MTBDD result; - //if (cache_get3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, &result)) return result; - - /* Check terminal case */ - result = WRAP(op, dd, param); - if (result != mtbdd_invalid) { - /* Store in cache */ - //cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result); - return result; - } - - /* Get cofactors */ - mtbddnode_t ndd = MTBDD_GETNODE(dd); - MTBDD ddlow = node_getlow(dd, ndd); - MTBDD ddhigh = node_gethigh(dd, ndd); - - /* Recursive */ - mtbdd_refs_spawn(SPAWN(mtbdd_uapply_nocache, ddhigh, op, param)); - MTBDD low = mtbdd_refs_push(CALL(mtbdd_uapply_nocache, ddlow, op, param)); - MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_uapply_nocache)); - mtbdd_refs_pop(1); - result = mtbdd_makenode(mtbddnode_getvariable(ndd), low, high); - - /* Store in cache */ - //cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result); - return result; -} - -/** - * Monad that converts double/fraction to a Boolean MTBDD, translate terminals >= value to 1 and to 0 otherwise; - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t, svalue) -{ - LOG_I("task_impl_2 op_threshold") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t, svalue) { storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; if (mtbdd_isleaf(a)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); - - if (storm_rational_function_less_or_equal(ma, value)) { - return mtbdd_false; - } else { - return mtbdd_true; - } + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + return storm_rational_function_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true; } return mtbdd_invalid; } -/** - * Monad that converts double/fraction to a Boolean BDD, translate terminals > value to 1 and to 0 otherwise; - */ -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t, svalue) -{ - LOG_I("task_impl_2 op_strict_threshold") +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t, svalue) { storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; if (mtbdd_isleaf(a)) { - storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); - if (storm_rational_function_less(ma, value)) { - return mtbdd_false; - } else { - return mtbdd_true; - } + return storm_rational_function_less(ma, value) ? mtbdd_false : mtbdd_true; } return mtbdd_invalid; @@ -892,8 +575,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, dd, s return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_strict_threshold), *(size_t*)value); } -TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD, a) -{ +TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD, a) { /* Check terminal case */ if (a == mtbdd_false) return mtbdd_false; mtbddnode_t na = MTBDD_GETNODE(a); diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index 8543ade19..259e10a1d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -1,209 +1,80 @@ -/** - * This is an implementation of storm::RationalFunction custom leaves of MTBDDs - */ - #ifndef SYLVAN_STORM_RATIONAL_FUNCTION_H #define SYLVAN_STORM_RATIONAL_FUNCTION_H #include -#include +#include #define SYLVAN_HAVE_CARL 1 #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) -#define SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID (3) - #ifdef __cplusplus extern "C" { #endif /* __cplusplus */ -/** - * Initialize storm::RationalFunction custom leaves - */ void sylvan_storm_rational_function_init(); - -/** - * Returns the identifier necessary to use these custom leaves. - */ uint32_t sylvan_storm_rational_function_get_type(); - -/** - * Create storm::RationalFunction leaf - */ MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val); - storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal); -/** - * Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise; - */ TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD) #define mtbdd_bool_to_storm_rational_function(dd) CALL(mtbdd_bool_to_storm_rational_function, dd) -// Operation "equals" TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, MTBDD*) #define mtbdd_equals_rational_function(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_equals)) -/** - * Operation "plus" for two storm::RationalFunction MTBDDs - */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, MTBDD*) -TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, MTBDD, int) - -/** - * Operation "minus" for two storm::RationalFunction MTBDDs - */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, MTBDD*) - -/** - * Operation "times" for two storm::RationalFunction MTBDDs - */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, MTBDD*) -TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBDD, int) - -/** - * Operation "divide" for two storm::RationalFunction MTBDDs - */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, MTBDD, int) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBDD, int) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, MTBDD, int) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, MTBDD, int) + TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_less, MTBDD*, MTBDD*) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_less_or_equal, MTBDD*, MTBDD*) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, MTBDD*) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, MTBDD*) -TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, MTBDD, int) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_max, MTBDD*, MTBDD*) -TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, MTBDD, int) -/** - * Operation "negate" for one storm::RationalFunction MTBDD - */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t) - TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_floor, MTBDD, size_t) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_ceil, MTBDD, size_t) -/** - * Compute a + b - */ #define sylvan_storm_rational_function_plus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus)) - -/** - * Compute a - b - */ #define sylvan_storm_rational_function_minus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_minus)) - -/** - * Compute a * b - */ #define sylvan_storm_rational_function_times(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times)) - -/** - * Compute a / b - */ #define sylvan_storm_rational_function_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_divide)) - -/** - * Compute a < b - */ #define sylvan_storm_rational_function_less(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less)) - -/** - * Compute a <= b - */ #define sylvan_storm_rational_function_less_or_equal(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less_or_equal)) - -/** - * Compute a mod b - */ #define sylvan_storm_rational_function_mod(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less_or_equal)) - -/** - * Compute min(a, b) - */ #define sylvan_storm_rational_function_min(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_min)) - -/** - * Compute max(a, b) - */ #define sylvan_storm_rational_function_max(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_max)) - -/** - * Compute -a - */ #define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0) - -/** - * Compute floor(a) - */ #define sylvan_storm_rational_function_floor(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_floor), 0) - -/** - * Compute ceil(a) - */ #define sylvan_storm_rational_function_ceil(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_ceil), 0) - -/** - * Compute a^b - */ -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, MTBDD*) #define sylvan_storm_rational_function_pow(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_pow)) - -/** - * Multiply and , and abstract variables using summation. - * This is similar to the "and_exists" operation in BDDs. - */ +TASK_DECL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD); +#define sylvan_storm_rational_function_minimum(dd) CALL(sylvan_storm_rational_function_minimum, dd) + +TASK_DECL_1(MTBDD, sylvan_storm_rational_function_maximum, MTBDD); +#define sylvan_storm_rational_function_maximum(dd) CALL(sylvan_storm_rational_function_maximum, dd) + TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBDD); #define sylvan_storm_rational_function_and_exists(a, b, vars) CALL(sylvan_storm_rational_function_and_exists, a, b, vars) -/** - * Abstract the variables in from by taking the sum of all values - */ #define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus)) #define sylvan_storm_rational_function_abstract_min(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_min)) #define sylvan_storm_rational_function_abstract_max(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_max)) -/** - * Apply a unary operation to