From 9e90f416080ea41b72bc36504cf724e260929b59 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 27 Jul 2016 16:18:34 +0200 Subject: [PATCH] Implemented functions for BDD -> ADD conversion and some helpers. Former-commit-id: 78c9003366339d6a48f4740250d0b98365aabbd7 --- .../sylvan/src/storm_function_wrapper.cpp | 16 ++++++++++++ .../sylvan/src/storm_function_wrapper.h | 3 +++ resources/3rdparty/sylvan/src/sylvan_obj.cpp | 11 ++++++++ resources/3rdparty/sylvan/src/sylvan_obj.hpp | 9 +++++++ .../sylvan/src/sylvan_obj_bdd_storm.hpp | 3 +++ .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 8 ++++++ .../src/sylvan_storm_rational_function.c | 26 ++++++++++++++++++- .../src/sylvan_storm_rational_function.h | 7 +++++ src/storage/dd/sylvan/InternalSylvanAdd.cpp | 3 +-- src/storage/dd/sylvan/InternalSylvanBdd.cpp | 2 +- 10 files changed, 84 insertions(+), 4 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp index 3b9c19679..15d2cdc66 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -114,3 +114,19 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a) { return 0; } } + +storm_rational_function_ptr storm_rational_function_get_zero() { + static storm::RationalFunction zeroFunction(0); + static storm_rational_function_ptr_struct functionStruct; + functionStruct.storm_rational_function = (void*)&zeroFunction; + + return &functionStruct; +} + +storm_rational_function_ptr storm_rational_function_get_one() { + static storm::RationalFunction oneFunction(1); + static storm_rational_function_ptr_struct functionStruct; + functionStruct.storm_rational_function = (void*)&oneFunction; + + return &functionStruct; +} diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h index 3feeafec5..08b9f9471 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.h @@ -26,6 +26,9 @@ storm_rational_function_ptr storm_rational_function_negate(storm_rational_functi 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(); + #ifdef __cplusplus } #endif diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index a573c7a49..068c9a57f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -15,6 +15,7 @@ */ #include +#include using namespace sylvan; @@ -604,6 +605,16 @@ Mtbdd::doubleTerminal(double value) return mtbdd_double(value); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +Mtbdd +Mtbdd::stormRationalFunctionTerminal(storm::RationalFunction const& value) +{ + storm_rational_function_t functionStruct; + functionStruct.storm_rational_function = (void*)(&value); + return mtbdd_storm_rational_function(functionStruct); +} +#endif + Mtbdd Mtbdd::fractionTerminal(int64_t nominator, uint64_t denominator) { diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index e7f77f6ca..6cd81a2fb 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -23,6 +23,8 @@ #include #include +#include "src/adapters/CarlAdapter.h" + namespace sylvan { class BddSet; @@ -542,6 +544,13 @@ public: */ static Mtbdd doubleTerminal(double value); +#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); +#endif + /** * @brief Creates a Mtbdd leaf representing the fraction value / * Internally, Sylvan uses 32-bit values and reports overflows to stderr. diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp index 393ce988c..172bcf5c6 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp @@ -1,3 +1,6 @@ Mtbdd toDoubleMtbdd() const; Mtbdd toInt64Mtbdd() const; +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + Mtbdd toStormRationalFunctionMtbdd() const; +#endif Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 27706dcdd..f64ffeaa2 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -10,6 +10,14 @@ Bdd::toInt64Mtbdd() const { return mtbdd_bool_to_int64(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 + Mtbdd Bdd::Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const { LACE_ME; diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index c2fb73016..2991f322c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -90,7 +90,31 @@ uint32_t sylvan_storm_rational_function_get_type() { MTBDD mtbdd_storm_rational_function(storm_rational_function_t val) { - return mtbdd_makeleaf(sylvan_storm_rational_function_type, (size_t)val); + uint64_t terminalValue = (uint64_t)&val; + return mtbdd_makeleaf(sylvan_storm_rational_function_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) +{ + if (a == mtbdd_false) { + return mtbdd_storm_rational_function(*storm_rational_function_get_zero()); + } + if (a == mtbdd_true) { + 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; + + return mtbdd_invalid; +} + +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); } /** diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index 6cdb142a5..fd4ad7f3a 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -31,6 +31,13 @@ uint32_t sylvan_storm_rational_function_get_type(); */ MTBDD mtbdd_storm_rational_function(storm_rational_function_t val); +/** + * 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 "plus" for two storm::RationalFunction MTBDDs */ diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 92c6ca642..71975e7c3 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -617,9 +617,8 @@ namespace storm { MTBDD InternalAdd::getLeaf(storm::RationalFunction const& value) { storm_rational_function_ptr_struct helperStruct; helperStruct.storm_rational_function = (void*)(&value); - uint64_t terminalValue = (uint64_t)&helperStruct; - return sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), terminalValue).GetMTBDD(); + return mtbdd_storm_rational_function(helperStruct); } template diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 0ad6cfa47..09889d6bb 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -248,7 +248,7 @@ namespace storm { } #ifdef STORM_HAVE_CARL else if (std::is_same::value) { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Conversion to ADD is currently unsupported for storm::RationalFunction."); + return InternalAdd(ddManager, this->sylvanBdd.toStormRationalFunctionMtbdd()); } #endif else {