diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 9b30445f3..faf6e2663 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -47,7 +47,7 @@ ExternalProject_Add( DOWNLOAD_COMMAND "" PREFIX "sylvan" SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/sylvan - CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release + CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=On -DCMAKE_BUILD_TYPE=Release BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan" INSTALL_COMMAND "" INSTALL_DIR "${PROJECT_BINARY_DIR}/sylvan" diff --git a/resources/3rdparty/sylvan/CMakeLists.txt b/resources/3rdparty/sylvan/CMakeLists.txt index d9999a0f3..1007c5917 100644 --- a/resources/3rdparty/sylvan/CMakeLists.txt +++ b/resources/3rdparty/sylvan/CMakeLists.txt @@ -5,6 +5,7 @@ enable_testing() set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11 -fPIC") set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11 -fPIC") +option(USE_CARL "Sets whether carl should be included." ON) option(WITH_COVERAGE "Add generation of test coverage" OFF) if(WITH_COVERAGE) set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -O0 -g -coverage") @@ -28,9 +29,26 @@ if(WITH_COVERAGE) ) endif() +if(USE_CARL) + find_package(carl QUIET REQUIRED) + if(carl_FOUND) + add_definitions(-DSYLVAN_HAVE_CARL) + include_directories("${carl_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES}) + message(STATUS "Sylvan - using CARL.") + else() + message(FATAL_ERROR "Sylvan - CARL was requested but not found") + endif() +else() + message(STATUS "Sylvan - not using CARL.") +endif() + + set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) find_package(GMP REQUIRED) include_directories(${GMP_INCLUDE_DIR}) +include_directories("${PROJECT_SOURCE_DIR}/../../../") +include_directories("${PROJECT_BINARY_DIR}/../include") include_directories(src) include_directories(src) diff --git a/resources/3rdparty/sylvan/examples/CMakeLists.txt b/resources/3rdparty/sylvan/examples/CMakeLists.txt index bb335935d..ce2d0d740 100644 --- a/resources/3rdparty/sylvan/examples/CMakeLists.txt +++ b/resources/3rdparty/sylvan/examples/CMakeLists.txt @@ -12,6 +12,12 @@ target_link_libraries(lddmc sylvan) add_executable(simple simple.cpp) target_link_libraries(simple sylvan stdc++) +if(USE_CARL) + message(STATUS "Sylvan - Example for Storm enabled.") + add_executable(storm-rf storm.cpp) + target_link_libraries(storm-rf sylvan stdc++ ${carl_LIBRARIES}) +endif(USE_CARL) + include(CheckIncludeFiles) check_include_files("gperftools/profiler.h" HAVE_PROFILER) diff --git a/resources/3rdparty/sylvan/examples/storm.cpp b/resources/3rdparty/sylvan/examples/storm.cpp new file mode 100644 index 000000000..c9bcfb032 --- /dev/null +++ b/resources/3rdparty/sylvan/examples/storm.cpp @@ -0,0 +1,127 @@ +#ifdef NDEBUG +#undef NDEBUG +#endif + +#include +#include +#include + +#include +#include +#include +#include + +using namespace sylvan; + +VOID_TASK_0(storm_rf) +{ + Bdd one = Bdd::bddOne(); // the True terminal + Bdd zero = Bdd::bddZero(); // the False terminal + + // check if they really are the True/False terminal + assert(one.GetBDD() == sylvan_true); + assert(zero.GetBDD() == sylvan_false); + + Bdd a = Bdd::bddVar(0); // create a BDD variable x_0 + Bdd b = Bdd::bddVar(1); // create a BDD variable x_1 + + // check if a really is the Boolean formula "x_0" + assert(!a.isConstant()); + assert(a.TopVar() == 0); + assert(a.Then() == one); + assert(a.Else() == zero); + + // check if b really is the Boolean formula "x_1" + assert(!b.isConstant()); + assert(b.TopVar() == 1); + assert(b.Then() == one); + assert(b.Else() == zero); + + // compute !a + Bdd not_a = !a; + + // check if !!a is really a + assert((!not_a) == a); + + // compute a * b and !(!a + !b) and check if they are equivalent + Bdd a_and_b = a * b; + Bdd not_not_a_or_not_b = !(!a + !b); + assert(a_and_b == not_not_a_or_not_b); + + // perform some simple quantification and check the results + Bdd ex = a_and_b.ExistAbstract(a); // \exists a . a * b + assert(ex == b); + Bdd andabs = a.AndAbstract(b, a); // \exists a . a * b using AndAbstract + assert(ex == andabs); + Bdd univ = a_and_b.UnivAbstract(a); // \forall a . a * b + assert(univ == zero); + + // alternative method to get the cube "ab" using bddCube + BddSet variables = a * b; + std::vector vec = {1, 1}; + assert(a_and_b == Bdd::bddCube(variables, vec)); + + // test the bddCube method for all combinations + assert((!a * !b) == Bdd::bddCube(variables, std::vector({0, 0}))); + assert((!a * b) == Bdd::bddCube(variables, std::vector({0, 1}))); + assert((!a) == Bdd::bddCube(variables, std::vector({0, 2}))); + assert((a * !b) == Bdd::bddCube(variables, std::vector({1, 0}))); + assert((a * b) == Bdd::bddCube(variables, std::vector({1, 1}))); + assert((a) == Bdd::bddCube(variables, std::vector({1, 2}))); + assert((!b) == Bdd::bddCube(variables, std::vector({2, 0}))); + assert((b) == Bdd::bddCube(variables, std::vector({2, 1}))); + assert(one == Bdd::bddCube(variables, std::vector({2, 2}))); +} + +VOID_TASK_1(_main, void*, arg) +{ + // Initialize Sylvan + // With starting size of the nodes table 1 << 21, and maximum size 1 << 27. + // With starting size of the cache table 1 << 20, and maximum size 1 << 20. + // Memory usage: 24 bytes per node, and 36 bytes per cache bucket + // - 1<<24 nodes: 384 MB + // - 1<<25 nodes: 768 MB + // - 1<<26 nodes: 1536 MB + // - 1<<27 nodes: 3072 MB + // - 1<<24 cache: 576 MB + // - 1<<25 cache: 1152 MB + // - 1<<26 cache: 2304 MB + // - 1<<27 cache: 4608 MB + sylvan_init_package(1LL<<22, 1LL<<26, 1LL<<22, 1LL<<26); + + // Initialize the BDD module with granularity 1 (cache every operation) + // A higher granularity (e.g. 6) often results in better performance in practice + sylvan_init_bdd(1); + + // Now we can do some simple stuff using the C++ objects. + CALL(storm_rf); + + // Report statistics (if SYLVAN_STATS is 1 in the configuration) + sylvan_stats_report(stdout, 1); + + // And quit, freeing memory + sylvan_quit(); + + // We didn't use arg + (void)arg; +} + +int +main (int argc, char *argv[]) +{ + int n_workers = 0; // automatically detect number of workers + size_t deque_size = 0; // default value for the size of task deques for the workers + size_t program_stack_size = 0; // default value for the program stack of each pthread + + // Initialize the Lace framework for workers. + lace_init(n_workers, deque_size); + + // Spawn and start all worker pthreads; suspends current thread until done. + lace_startup(program_stack_size, TASK(_main), NULL); + + // The lace_startup command also exits Lace after _main is completed. + + return 0; + (void)argc; // unused variable + (void)argv; // unused variable +} diff --git a/resources/3rdparty/sylvan/src/CMakeLists.txt b/resources/3rdparty/sylvan/src/CMakeLists.txt index 50a645f22..eb27a6fc4 100644 --- a/resources/3rdparty/sylvan/src/CMakeLists.txt +++ b/resources/3rdparty/sylvan/src/CMakeLists.txt @@ -13,6 +13,8 @@ add_library(sylvan sha2.c stats.h stats.c + storm_function_wrapper.h + storm_function_wrapper.cpp sylvan.h sylvan_bdd.h sylvan_bdd.c @@ -30,6 +32,8 @@ add_library(sylvan sylvan_mtbdd_int.h sylvan_obj.hpp sylvan_obj.cpp + sylvan_storm_rational_function.h + sylvan_storm_rational_function.c tls.h ) @@ -42,6 +46,11 @@ set_target_properties(sylvan PROPERTIES target_link_libraries(sylvan m pthread) +if(USE_CARL) + message(STATUS "Sylvan - linking CARL.") + target_link_libraries(sylvan ${carl_LIBRARIES}) +endif(USE_CARL) + if(UNIX AND NOT APPLE) target_link_libraries(sylvan rt) endif() diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp new file mode 100644 index 000000000..3b9c19679 --- /dev/null +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -0,0 +1,116 @@ +#include "storm_function_wrapper.h" + +#include +#include "src/adapters/CarlAdapter.h" + +void storm_rational_function_init(storm_rational_function_ptr* a) { + storm_rational_function_ptr srf_ptr = static_cast(malloc(sizeof(storm_rational_function_ptr_struct))); + + if (srf_ptr == nullptr) { + return; + } + + srf_ptr->storm_rational_function = new storm::RationalFunction(*(storm::RationalFunction*)((*a)->storm_rational_function)); + + *a = srf_ptr; +} + +void storm_rational_function_destroy(storm_rational_function_ptr a) { + delete (storm::RationalFunction*)a->storm_rational_function; + a->storm_rational_function = nullptr; + free((void*)a); +} + +int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { + storm::RationalFunction* srf_a = (storm::RationalFunction*)a->storm_rational_function; + storm::RationalFunction* srf_b = (storm::RationalFunction*)b->storm_rational_function; + + if (*srf_a == *srf_b) { + return 0; + } + + return -1; +} + +storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf += srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); + result->storm_rational_function = (void*)result_srf; + + return result; +} + +storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf -= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); + result->storm_rational_function = (void*)result_srf; + + return result; +} + +storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf *= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); + result->storm_rational_function = (void*)result_srf; + + return result; +} + +storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf /= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); + result->storm_rational_function = (void*)result_srf; + + return result; +} + +uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; + + size_t hash = carl::hash_value(srf_a); + uint64_t result = hash ^ seed; + + return result; +} + +storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + *result_srf = -srf_a; + + storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); + result->storm_rational_function = (void*)result_srf; + + return result; +} + +int storm_rational_function_is_zero(storm_rational_function_ptr a) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; + + if (srf_a.isZero()) { + return 1; + } else { + return 0; + } +} diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h new file mode 100644 index 000000000..3feeafec5 --- /dev/null +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.h @@ -0,0 +1,33 @@ +#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H +#define SYLVAN_STORM_FUNCTION_WRAPPER_H + +#include + +#ifdef __cplusplus +extern "C" { +#endif + +typedef struct { + void* storm_rational_function; +} storm_rational_function_ptr_struct; +typedef storm_rational_function_ptr_struct storm_rational_function_t[1]; +typedef storm_rational_function_ptr_struct* storm_rational_function_ptr; + + +// equals, plus, minus, divide, times, create, destroy +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); +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_negate(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); + +#ifdef __cplusplus +} +#endif + +#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H \ No newline at end of file diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c new file mode 100644 index 000000000..fcbd1f911 --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -0,0 +1,240 @@ +#include + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +/*#include */ +#include + +#include + +/** + * helper function for hash + */ +#ifndef rotl64 +static inline uint64_t +rotl64(uint64_t x, int8_t r) +{ + return ((x<>(64-r))); +} +#endif + +static uint64_t +sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed) +{ + /* Hash the storm::RationalFunction in pointer v */ + + storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)v; + + return storm_rational_function_hash(x, seed); +} + +static int +sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right) +{ + /* 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 */ + return (storm_rational_function_equals(a, b) == 0) ? 1 : 0; +} + +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_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 uint32_t sylvan_storm_rational_function_type; +static uint64_t CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS; + +/** + * Initialize storm::RationalFunction custom leaves + */ +void +sylvan_storm_rational_function_init() +{ + /* Register custom leaf 3 */ + sylvan_storm_rational_function_type = mtbdd_register_custom_leaf(sylvan_storm_rational_function_hash, sylvan_storm_rational_function_equals, sylvan_storm_rational_function_create, sylvan_storm_rational_function_destroy); + CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS = cache_next_opid(); +} + +/** + * Create storm::RationalFunction leaf + */ +MTBDD +mtbdd_storm_rational_function(storm_rational_function_t val) +{ + return mtbdd_makeleaf(sylvan_storm_rational_function_type, (size_t)val); +} + +/** + * 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) +{ + 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_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 mres = storm_rational_function_plus(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + /* Commutative, so swap a,b for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + 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) +{ + 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 (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 mres = storm_rational_function_minus(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + 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) +{ + 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 mres = storm_rational_function_times(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + /* Commutative, so make "a" the lowest for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + 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) +{ + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* Handle division 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 mres = storm_rational_function_divide(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + return mtbdd_invalid; +} + +/** + * Operation "neg" for one storm::RationalFunction MTBDD + */ +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 mres = storm_rational_function_negate(mdd); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + return res; + } + + return mtbdd_invalid; + (void)p; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h new file mode 100644 index 000000000..2080ca11c --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -0,0 +1,87 @@ +/** + * 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 + +#define SYLVAN_HAVE_CARL 1 + +#ifdef SYLVAN_HAVE_CARL + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +/** + * Initialize storm::RationalFunction custom leaves + */ +void sylvan_storm_rational_function_init(); + +/** + * Create storm::RationalFunction leaf + */ +MTBDD mtbdd_storm_rational_function(storm_rational_function_t val); + +/** + * 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*); + +/** + * Operation "negate" for one storm::RationalFunction MTBDD + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, 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 + */ +#define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0); + +#ifdef __cplusplus +} +#endif /* __cplusplus */ + +#endif // SYLVAN_HAVE_CARL + +#endif // SYLVAN_STORM_RATIONAL_FUNCTION_H