You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
1223 lines
71 KiB
1223 lines
71 KiB
#include "storm/storage/dd/sylvan/InternalSylvanAdd.h"
|
|
|
|
#include "storm/storage/dd/sylvan/SylvanAddIterator.h"
|
|
#include "storm/storage/dd/sylvan/InternalSylvanDdManager.h"
|
|
#include "storm/storage/dd/DdManager.h"
|
|
|
|
#include "storm/storage/SparseMatrix.h"
|
|
#include "storm/storage/BitVector.h"
|
|
|
|
#include "storm/utility/macros.h"
|
|
#include "storm/utility/constants.h"
|
|
#include "storm/exceptions/NotImplementedException.h"
|
|
#include "storm/exceptions/InvalidOperationException.h"
|
|
#include "storm/exceptions/NotSupportedException.h"
|
|
|
|
#include "storm-config.h"
|
|
|
|
namespace storm {
|
|
namespace dd {
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType>::InternalAdd() : ddManager(nullptr), sylvanMtbdd() {
|
|
// Intentionally left empty.
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType>::InternalAdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Mtbdd const& sylvanMtbdd) : ddManager(ddManager), sylvanMtbdd(sylvanMtbdd) {
|
|
// Intentionally left empty.
|
|
}
|
|
|
|
template<typename ValueType>
|
|
ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue(MTBDD const& node) {
|
|
STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
|
|
|
|
bool negated = mtbdd_hascomp(node);
|
|
MTBDD n = mtbdd_regular(node);
|
|
|
|
if (std::is_same<ValueType, double>::value) {
|
|
STORM_LOG_ASSERT(mtbdd_gettype(n) == 1, "Expected a double value.");
|
|
return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n);
|
|
} else if (std::is_same<ValueType, uint_fast64_t>::value) {
|
|
STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value.");
|
|
return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node);
|
|
}
|
|
#ifdef STORM_HAVE_CARL
|
|
else if (std::is_same<ValueType, storm::RationalFunction>::value) {
|
|
STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value.");
|
|
}
|
|
#endif
|
|
else {
|
|
STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD.");
|
|
}
|
|
}
|
|
|
|
template<>
|
|
storm::RationalNumber InternalAdd<DdType::Sylvan, storm::RationalNumber>::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.");
|
|
storm_rational_number_ptr ptr = (storm_rational_number_ptr)mtbdd_getstorm_rational_number_ptr(node);
|
|
storm::RationalNumber* rationalNumber = (storm::RationalNumber*)(ptr);
|
|
|
|
return negated ? -(*rationalNumber) : (*rationalNumber);
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
storm::RationalFunction InternalAdd<DdType::Sylvan, storm::RationalFunction>::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_function_get_type(), "Expected a storm::RationalFunction value.");
|
|
uint64_t value = mtbdd_getvalue(node);
|
|
storm_rational_function_ptr ptr = (storm_rational_function_ptr)value;
|
|
|
|
storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr);
|
|
|
|
return negated ? -(*rationalFunction) : (*rationalFunction);
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
bool InternalAdd<DdType::Sylvan, ValueType>::operator==(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return this->sylvanMtbdd == other.sylvanMtbdd;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
bool InternalAdd<DdType::Sylvan, ValueType>::operator!=(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return this->sylvanMtbdd != other.sylvanMtbdd;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator+(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator+(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.PlusRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator+(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.PlusRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator+=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.Plus(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber>& InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator+=(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.PlusRN(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator+=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.PlusRF(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator*(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Times(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator*(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.TimesRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator*(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.TimesRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator*=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.Times(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber>& InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator*=(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.TimesRN(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator*=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.TimesRF(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator-(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Minus(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator-(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.MinusRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator-(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.MinusRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator-=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.Minus(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber>& InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator-=(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.MinusRN(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator-=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.MinusRF(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator/(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Divide(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator/(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.DivideRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator/(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.DivideRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator/=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.Divide(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber>& InternalAdd<DdType::Sylvan, storm::RationalNumber>::operator/=(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.DivideRN(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator/=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
|
|
this->sylvanMtbdd = this->sylvanMtbdd.DivideRF(other.sylvanMtbdd);
|
|
return *this;
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::equals(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.Equals(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalNumber>::equals(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.EqualsRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::equals(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.EqualsRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::notEquals(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return !this->equals(other);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::less(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalNumber>::less(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::less(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::lessOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessOrEqual(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalNumber>::lessOrEqual(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessOrEqualRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::lessOrEqual(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessOrEqualRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greater(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return !this->lessOrEqual(other);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greaterOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return !this->less(other);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::pow(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::pow(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.PowRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::pow(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.PowRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::mod(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Mod(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::mod(InternalAdd<DdType::Sylvan, storm::RationalNumber> const&) const {
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational numbers.");
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::mod(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational functions.");
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::logxy(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Logxy(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::logxy(InternalAdd<DdType::Sylvan, storm::RationalNumber> const&) const {
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (logxy) not supported by rational numbers.");
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::logxy(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (logxy) not supported by rational functions.");
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::floor() const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Floor());
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::floor() const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.FloorRN());
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::floor() const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.FloorRF());
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::ceil() const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Ceil());
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::ceil() const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.CeilRN());
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::ceil() const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.CeilRF());
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, ValueType>::sharpenKwekMehlhorn(size_t precision) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.SharpenKwekMehlhorn(precision));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalFunction>::sharpenKwekMehlhorn(size_t precision) const {
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::minimum(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Min(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::minimum(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.MinRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minimum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.MinRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::maximum(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Max(other.sylvanMtbdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::maximum(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.MaxRN(other.sylvanMtbdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maximum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.MaxRF(other.sylvanMtbdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
template<typename TargetValueType>
|
|
InternalAdd<DdType::Sylvan, TargetValueType> InternalAdd<DdType::Sylvan, ValueType>::toValueType() const {
|
|
if (std::is_same<TargetValueType, ValueType>::value) {
|
|
return *this;
|
|
}
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type.");
|
|
}
|
|
|
|
template<>
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, double> InternalAdd<DdType::Sylvan, storm::RationalNumber>::toValueType() const {
|
|
return InternalAdd<DdType::Sylvan, double>(ddManager, this->sylvanMtbdd.ToDoubleRN());
|
|
}
|
|
|
|
template<>
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, double>::toValueType() const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.ToRationalNumber());
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, double> InternalAdd<DdType::Sylvan, storm::RationalFunction>::toValueType() const {
|
|
return InternalAdd<DdType::Sylvan, double>(ddManager, this->sylvanMtbdd.ToDoubleRF());
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::sumAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractPlus(cube.sylvanBdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::sumAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.AbstractPlusRN(cube.sylvanBdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::sumAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AbstractPlusRF(cube.sylvanBdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::minAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.AbstractMinRepresentative(cube.sylvanBdd));
|
|
}
|
|
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalNumber>::minAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.AbstractMinRepresentativeRN(cube.sylvanBdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.AbstractMinRN(cube.sylvanBdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AbstractMinRF(cube.sylvanBdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::maxAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.AbstractMaxRepresentative(cube.sylvanBdd));
|
|
}
|
|
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalNumber>::maxAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.AbstractMaxRepresentativeRN(cube.sylvanBdd));
|
|
}
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.AbstractMaxRN(cube.sylvanBdd));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AbstractMaxRF(cube.sylvanBdd));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
bool InternalAdd<DdType::Sylvan, ValueType>::equalModuloPrecision(InternalAdd<DdType::Sylvan, ValueType> const& other, ValueType const& precision, bool relative) const {
|
|
if (relative) {
|
|
return this->sylvanMtbdd.EqualNormRel(other.sylvanMtbdd, precision);
|
|
} else {
|
|
return this->sylvanMtbdd.EqualNorm(other.sylvanMtbdd, precision);
|
|
}
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
bool InternalAdd<DdType::Sylvan, storm::RationalNumber>::equalModuloPrecision(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other, storm::RationalNumber const& precision, bool relative) const {
|
|
if (relative) {
|
|
return this->sylvanMtbdd.EqualNormRelRN(other.sylvanMtbdd, precision);
|
|
} else {
|
|
return this->sylvanMtbdd.EqualNormRN(other.sylvanMtbdd, precision);
|
|
}
|
|
}
|
|
|
|
template<>
|
|
bool InternalAdd<DdType::Sylvan, storm::RationalFunction>::equalModuloPrecision(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other, storm::RationalFunction const& precision, bool relative) const {
|
|
if (relative) {
|
|
return this->sylvanMtbdd.EqualNormRelRF(other.sylvanMtbdd, precision);
|
|
} else {
|
|
return this->sylvanMtbdd.EqualNormRF(other.sylvanMtbdd, precision);
|
|
}
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const {
|
|
std::vector<uint32_t> fromIndices;
|
|
std::vector<uint32_t> toIndices;
|
|
for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
|
|
fromIndices.push_back(it1->getIndex());
|
|
fromIndices.push_back(it2->getIndex());
|
|
toIndices.push_back(it2->getIndex());
|
|
toIndices.push_back(it1->getIndex());
|
|
}
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::permuteVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const {
|
|
std::vector<uint32_t> fromIndices;
|
|
std::vector<uint32_t> toIndices;
|
|
for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
|
|
fromIndices.push_back(it1->getIndex());
|
|
toIndices.push_back(it2->getIndex());
|
|
}
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::multiplyMatrix(InternalAdd<DdType::Sylvan, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
|
|
InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
|
|
for (auto const& ddVariable : summationDdVariables) {
|
|
summationVariables &= ddVariable;
|
|
}
|
|
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::multiplyMatrix(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
|
|
InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
|
|
for (auto const& ddVariable : summationDdVariables) {
|
|
summationVariables &= ddVariable;
|
|
}
|
|
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AndExistsRF(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
|
|
}
|
|
#endif
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::multiplyMatrix(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
|
|
InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
|
|
for (auto const& ddVariable : summationDdVariables) {
|
|
summationVariables &= ddVariable;
|
|
}
|
|
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.AndExistsRN(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::multiplyMatrix(InternalBdd<DdType::Sylvan> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
|
|
InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
|
|
for (auto const& ddVariable : summationDdVariables) {
|
|
summationVariables &= ddVariable;
|
|
}
|
|
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AndExists(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd()));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::multiplyMatrix(InternalBdd<DdType::Sylvan> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
|
|
InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
|
|
for (auto const& ddVariable : summationDdVariables) {
|
|
summationVariables &= ddVariable;
|
|
}
|
|
|
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AndExistsRF(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd()));
|
|
}
|
|
#endif
|
|
|
|
template<>
|
|
InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::multiplyMatrix(InternalBdd<DdType::Sylvan> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
|
|
InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
|
|
for (auto const& ddVariable : summationDdVariables) {
|
|
summationVariables &= ddVariable;
|
|
}
|
|
|
|
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.AndExistsRN(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd()));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greater(ValueType const& value) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddStrictThreshold(value));
|
|
}
|
|
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalNumber>::greater(storm::RationalNumber const& value) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddStrictThresholdRN(value));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greater(storm::RationalFunction const& value) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddStrictThresholdRF(value));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greaterOrEqual(ValueType const& value) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddThreshold(value));
|
|
}
|
|
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalNumber>::greaterOrEqual(storm::RationalNumber const& value) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddThresholdRN(value));
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greaterOrEqual(storm::RationalFunction const& value) const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddThresholdRF(value));
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::less(ValueType const& value) const {
|
|
return !this->greaterOrEqual(value);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::lessOrEqual(ValueType const& value) const {
|
|
return !this->greater(value);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::notZero() const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.NotZero());
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::constrain(InternalAdd<DdType::Sylvan, ValueType> const&) const {
|
|
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (constrain) not yet implemented.");
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::restrict(InternalAdd<DdType::Sylvan, ValueType> const&) const {
|
|
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (restrict) not yet implemented.");
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::getSupport() const {
|
|
return InternalBdd<DdType::Sylvan>(ddManager, sylvan::Bdd(static_cast<BDD>(this->sylvanMtbdd.Support().GetMTBDD())));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
|
|
if (numberOfDdVariables == 0) {
|
|
return 0;
|
|
}
|
|
return static_cast<uint_fast64_t>(this->sylvanMtbdd.NonZeroCount(numberOfDdVariables));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getLeafCount() const {
|
|
return static_cast<uint_fast64_t>(this->sylvanMtbdd.CountLeaves());
|
|
}
|
|
|
|
template<typename ValueType>
|
|
uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getNodeCount() const {
|
|
return static_cast<uint_fast64_t>(this->sylvanMtbdd.NodeCount());
|
|
}
|
|
|
|
template<typename ValueType>
|
|
ValueType InternalAdd<DdType::Sylvan, ValueType>::getMin() const {
|
|
return getValue(this->sylvanMtbdd.Minimum().GetMTBDD());
|
|
}
|
|
|
|
template <>
|
|
storm::RationalNumber InternalAdd<DdType::Sylvan, storm::RationalNumber>::getMin() const {
|
|
return getValue(this->sylvanMtbdd.MinimumRN().GetMTBDD());
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template <>
|
|
storm::RationalFunction InternalAdd<DdType::Sylvan, storm::RationalFunction>::getMin() const {
|
|
return getValue(this->sylvanMtbdd.MinimumRF().GetMTBDD());
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
ValueType InternalAdd<DdType::Sylvan, ValueType>::getMax() const {
|
|
return getValue(this->sylvanMtbdd.Maximum().GetMTBDD());
|
|
}
|
|
|
|
template<>
|
|
storm::RationalNumber InternalAdd<DdType::Sylvan, storm::RationalNumber>::getMax() const {
|
|
return getValue(this->sylvanMtbdd.MaximumRN().GetMTBDD());
|
|
}
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template<>
|
|
storm::RationalFunction InternalAdd<DdType::Sylvan, storm::RationalFunction>::getMax() const {
|
|
return getValue(this->sylvanMtbdd.MaximumRF().GetMTBDD());
|
|
}
|
|
#endif
|
|
|
|
template<typename ValueType>
|
|
ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue() const {
|
|
return getValue(this->sylvanMtbdd.GetMTBDD());
|
|
}
|
|
|
|
template<typename ValueType>
|
|
bool InternalAdd<DdType::Sylvan, ValueType>::isOne() const {
|
|
return *this == ddManager->getAddOne<ValueType>();
|
|
}
|
|
|
|
template<typename ValueType>
|
|
bool InternalAdd<DdType::Sylvan, ValueType>::isZero() const {
|
|
return *this == ddManager->getAddZero<ValueType>();
|
|
}
|
|
|
|
template<typename ValueType>
|
|
bool InternalAdd<DdType::Sylvan, ValueType>::isConstant() const {
|
|
return this->sylvanMtbdd.isTerminal();
|
|
}
|
|
|
|
template<typename ValueType>
|
|
uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getIndex() const {
|
|
return static_cast<uint_fast64_t>(this->sylvanMtbdd.TopVar());
|
|
}
|
|
|
|
template<typename ValueType>
|
|
uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getLevel() const {
|
|
return this->getIndex();
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::exportToDot(std::string const& filename, std::vector<std::string> const&, bool) const {
|
|
// Open the file, dump the DD and close it again.
|
|
FILE* filePointer = fopen(filename.c_str() , "a+");
|
|
this->sylvanMtbdd.PrintDot(filePointer);
|
|
fclose(filePointer);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::exportToText(std::string const& filename) const {
|
|
// Open the file, dump the DD and close it again.
|
|
FILE* filePointer = fopen(filename.c_str() , "a+");
|
|
this->sylvanMtbdd.PrintText(filePointer);
|
|
fclose(filePointer);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
AddIterator<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::begin(DdManager<DdType::Sylvan> const& fullDdManager, InternalBdd<DdType::Sylvan> const& variableCube, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const {
|
|
return AddIterator<DdType::Sylvan, ValueType>::createBeginIterator(fullDdManager, this->getSylvanMtbdd(), variableCube.getSylvanBdd(), numberOfDdVariables, &metaVariables, enumerateDontCareMetaVariables);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
AddIterator<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::end(DdManager<DdType::Sylvan> const& fullDdManager) const {
|
|
return AddIterator<DdType::Sylvan, ValueType>::createEndIterator(fullDdManager);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
Odd InternalAdd<DdType::Sylvan, ValueType>::createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const {
|
|
// Prepare a unique table for each level that keeps the constructed ODD nodes unique.
|
|
std::vector<std::unordered_map<BDD, std::shared_ptr<Odd>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
|
|
|
|
// Now construct the ODD structure from the ADD.
|
|
std::shared_ptr<Odd> rootOdd = createOddRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
|
|
|
|
// Return a copy of the root node to remove the shared_ptr encapsulation.
|
|
return Odd(*rootOdd);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
std::shared_ptr<Odd> InternalAdd<DdType::Sylvan, ValueType>::createOddRec(BDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<BDD, std::shared_ptr<Odd>>>& uniqueTableForLevels) {
|
|
// Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
|
|
auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
|
|
if (iterator != uniqueTableForLevels[currentLevel].end()) {
|
|
return iterator->second;
|
|
} else {
|
|
// Otherwise, we need to recursively compute the ODD.
|
|
|
|
// If we are already past the maximal level that is to be considered, we can simply create an Odd without
|
|
// successors
|
|
if (currentLevel == maxLevel) {
|
|
uint_fast64_t elseOffset = 0;
|
|
uint_fast64_t thenOffset = 0;
|
|
|
|
STORM_LOG_ASSERT(mtbdd_isleaf(dd), "Expected leaf at last level.");
|
|
|
|
// If the DD is not the zero leaf, then the then-offset is 1.
|
|
if (!mtbdd_iszero(dd)) {
|
|
thenOffset = 1;
|
|
}
|
|
|
|
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
|
|
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
|
|
return oddNode;
|
|
} else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
|
|
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
|
|
// node for the then-successor as well.
|
|
std::shared_ptr<Odd> elseNode = createOddRec(dd, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
|
|
std::shared_ptr<Odd> thenNode = elseNode;
|
|
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
|
|
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
|
|
return oddNode;
|
|
} else {
|
|
// Otherwise, we compute the ODDs for both the then- and else successors.
|
|
std::shared_ptr<Odd> elseNode = createOddRec(mtbdd_regular(mtbdd_getlow(dd)), currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
|
|
std::shared_ptr<Odd> thenNode = createOddRec(mtbdd_regular(mtbdd_gethigh(dd)), currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
|
|
|
|
uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
|
|
uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
|
|
|
|
auto oddNode = std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
|
|
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
|
|
return oddNode;
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalDdManager<DdType::Sylvan> const& InternalAdd<DdType::Sylvan, ValueType>::getInternalDdManager() const {
|
|
return *ddManager;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
|
|
forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector] (uint64_t const& offset, ValueType const& value) { targetVector[offset] = function(targetVector[offset], value); });
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
|
|
forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, [&function, &targetVector, &offsets] (uint64_t const& offset, ValueType const& value) {
|
|
ValueType& targetValue = targetVector[offsets[offset]];
|
|
targetValue = function(targetValue, value);
|
|
});
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const {
|
|
forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, function);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::forEachRec(MTBDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void (uint64_t const&, ValueType const&)> const& function) const {
|
|
// For the empty DD, we do not need to add any entries.
|
|
if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
|
|
return;
|
|
}
|
|
|
|
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
|
|
if (currentLevel == maxLevel) {
|
|
function(currentOffset, getValue(dd));
|
|
} else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
|
|
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
|
|
// and for the one in which it is not set.
|
|
forEachRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
|
|
forEachRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
|
|
} else {
|
|
// Otherwise, we simply recursively call the function for both (different) cases.
|
|
MTBDD thenNode = mtbdd_gethigh(dd);
|
|
MTBDD elseNode = mtbdd_getlow(dd);
|
|
|
|
forEachRec(elseNode, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
|
|
forEachRec(thenNode, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
std::vector<uint64_t> InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const {
|
|
std::vector<uint64_t> result;
|
|
decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0);
|
|
return result;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const {
|
|
// For the empty DD, we do not need to create a group.
|
|
if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
|
|
return;
|
|
}
|
|
|
|
if (currentLevel == maxLevel) {
|
|
labels.push_back(label);
|
|
} else {
|
|
uint64_t elseLabel = label;
|
|
uint64_t thenLabel = label;
|
|
|
|
if (ddLabelVariableIndices.get(currentLevel)) {
|
|
elseLabel <<= 1;
|
|
thenLabel = (thenLabel << 1) | 1;
|
|
}
|
|
|
|
if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
|
|
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
|
|
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
|
|
} else {
|
|
// Otherwise, we compute the ODDs for both the then- and else successors.
|
|
MTBDD thenDdNode = mtbdd_gethigh(dd);
|
|
MTBDD elseDdNode = mtbdd_getlow(dd);
|
|
|
|
decodeGroupLabelsRec(mtbdd_regular(elseDdNode), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
|
|
decodeGroupLabelsRec(mtbdd_regular(thenDdNode), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
std::vector<InternalAdd<DdType::Sylvan, ValueType>> InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
|
|
std::vector<InternalAdd<DdType::Sylvan, ValueType>> result;
|
|
splitIntoGroupsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
|
|
return result;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
std::vector<std::pair<InternalAdd<DdType::Sylvan, ValueType>, InternalAdd<DdType::Sylvan, ValueType>>> InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroups(InternalAdd<DdType::Sylvan, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
|
|
std::vector<std::pair<InternalAdd<DdType::Sylvan, ValueType>, InternalAdd<DdType::Sylvan, ValueType>>> result;
|
|
splitIntoGroupsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), mtbdd_regular(vector.getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(vector.getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
|
|
return result;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroupsRec(MTBDD dd, bool negated, std::vector<InternalAdd<DdType::Sylvan, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const {
|
|
// For the empty DD, we do not need to create a group.
|
|
if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
|
|
return;
|
|
}
|
|
|
|
if (currentLevel == maxLevel) {
|
|
groups.push_back(InternalAdd<DdType::Sylvan, ValueType>(ddManager, negated ? sylvan::Mtbdd(dd).Negate() : sylvan::Mtbdd(dd)));
|
|
} else if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
|
|
splitIntoGroupsRec(dd, negated, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
splitIntoGroupsRec(dd, negated, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
} else {
|
|
// Otherwise, we compute the ODDs for both the then- and else successors.
|
|
MTBDD thenDdNode = mtbdd_gethigh(dd);
|
|
MTBDD elseDdNode = mtbdd_getlow(dd);
|
|
|
|
// Determine whether we have to evaluate the successors as if they were complemented.
|
|
bool elseComplemented = mtbdd_hascomp(elseDdNode) ^ negated;
|
|
bool thenComplemented = mtbdd_hascomp(thenDdNode) ^ negated;
|
|
|
|
// FIXME: We first traverse the else successor (unlike other variants of this method).
|
|
// Otherwise, the GameBasedMdpModelCheckerTest would not terminate. See github issue #64
|
|
splitIntoGroupsRec(mtbdd_regular(elseDdNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
splitIntoGroupsRec(mtbdd_regular(thenDdNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroupsRec(MTBDD dd1, bool negated1, MTBDD dd2, bool negated2, std::vector<std::pair<InternalAdd<DdType::Sylvan, ValueType>, InternalAdd<DdType::Sylvan, ValueType>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const {
|
|
// For the empty DD, we do not need to create a group.
|
|
if (mtbdd_isleaf(dd1) && mtbdd_isleaf(dd2) && mtbdd_iszero(dd1) && mtbdd_iszero(dd2)) {
|
|
return;
|
|
}
|
|
|
|
if (currentLevel == maxLevel) {
|
|
groups.push_back(std::make_pair(InternalAdd<DdType::Sylvan, ValueType>(ddManager, negated1 ? sylvan::Mtbdd(dd1).Negate() : sylvan::Mtbdd(dd1)), InternalAdd<DdType::Sylvan, ValueType>(ddManager, negated2 ? sylvan::Mtbdd(dd2).Negate() : sylvan::Mtbdd(dd2))));
|
|
} else if (mtbdd_isleaf(dd1) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd1)) {
|
|
if (mtbdd_isleaf(dd2) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd2)) {
|
|
splitIntoGroupsRec(dd1, negated1, dd2, negated2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
splitIntoGroupsRec(dd1, negated1, dd2, negated2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
} else {
|
|
MTBDD dd2ThenNode = mtbdd_gethigh(dd2);
|
|
MTBDD dd2ElseNode = mtbdd_getlow(dd2);
|
|
|
|
// Determine whether we have to evaluate the successors as if they were complemented.
|
|
bool elseComplemented = mtbdd_hascomp(dd2ElseNode) ^ negated2;
|
|
bool thenComplemented = mtbdd_hascomp(dd2ThenNode) ^ negated2;
|
|
|
|
splitIntoGroupsRec(dd1, negated1, mtbdd_regular(dd2ThenNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
splitIntoGroupsRec(dd1, negated1, mtbdd_regular(dd2ElseNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
}
|
|
} else if (mtbdd_isleaf(dd2) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd2)) {
|
|
MTBDD dd1ThenNode = mtbdd_gethigh(dd1);
|
|
MTBDD dd1ElseNode = mtbdd_getlow(dd1);
|
|
|
|
// Determine whether we have to evaluate the successors as if they were complemented.
|
|
bool elseComplemented = mtbdd_hascomp(dd1ElseNode) ^ negated1;
|
|
bool thenComplemented = mtbdd_hascomp(dd1ThenNode) ^ negated1;
|
|
|
|
splitIntoGroupsRec(mtbdd_regular(dd1ThenNode), thenComplemented, dd2, negated2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
splitIntoGroupsRec(mtbdd_regular(dd1ElseNode), elseComplemented, dd2, negated2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
} else {
|
|
MTBDD dd1ThenNode = mtbdd_gethigh(dd1);
|
|
MTBDD dd1ElseNode = mtbdd_getlow(dd1);
|
|
MTBDD dd2ThenNode = mtbdd_gethigh(dd2);
|
|
MTBDD dd2ElseNode = mtbdd_getlow(dd2);
|
|
|
|
// Determine whether we have to evaluate the successors as if they were complemented.
|
|
bool dd1ElseComplemented = mtbdd_hascomp(dd1ElseNode) ^ negated1;
|
|
bool dd1ThenComplemented = mtbdd_hascomp(dd1ThenNode) ^ negated1;
|
|
bool dd2ElseComplemented = mtbdd_hascomp(dd2ElseNode) ^ negated2;
|
|
bool dd2ThenComplemented = mtbdd_hascomp(dd2ThenNode) ^ negated2;
|
|
|
|
splitIntoGroupsRec(mtbdd_regular(dd1ThenNode), dd1ThenComplemented, mtbdd_regular(dd2ThenNode), dd2ThenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
splitIntoGroupsRec(mtbdd_regular(dd1ElseNode), dd1ElseComplemented, mtbdd_regular(dd2ElseNode), dd2ElseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const {
|
|
return toMatrixComponentsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
void InternalAdd<DdType::Sylvan, ValueType>::toMatrixComponentsRec(MTBDD dd, bool negated, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const {
|
|
// For the empty DD, we do not need to add any entries.
|
|
if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
|
|
return;
|
|
}
|
|
|
|
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
|
|
if (currentRowLevel + currentColumnLevel == maxLevel) {
|
|
if (generateValues) {
|
|
columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<uint_fast64_t, ValueType>(currentColumnOffset, negated ? -getValue(dd) : getValue(dd));
|
|
}
|
|
++rowIndications[rowGroupOffsets[currentRowOffset]];
|
|
} else {
|
|
MTBDD elseElse;
|
|
MTBDD elseThen;
|
|
MTBDD thenElse;
|
|
MTBDD thenThen;
|
|
|
|
if (mtbdd_isleaf(dd) || ddColumnVariableIndices[currentColumnLevel] < mtbdd_getvar(dd)) {
|
|
elseElse = elseThen = thenElse = thenThen = dd;
|
|
} else if (ddRowVariableIndices[currentColumnLevel] < mtbdd_getvar(dd)) {
|
|
elseElse = thenElse = mtbdd_getlow(dd);
|
|
elseThen = thenThen = mtbdd_gethigh(dd);
|
|
} else {
|
|
MTBDD elseNode = mtbdd_getlow(dd);
|
|
if (mtbdd_isleaf(elseNode) || ddColumnVariableIndices[currentColumnLevel] < mtbdd_getvar(elseNode)) {
|
|
elseElse = elseThen = elseNode;
|
|
} else {
|
|
elseElse = mtbdd_getlow(elseNode);
|
|
elseThen = mtbdd_gethigh(elseNode);
|
|
}
|
|
|
|
MTBDD thenNode = mtbdd_gethigh(dd);
|
|
if (mtbdd_isleaf(thenNode) || ddColumnVariableIndices[currentColumnLevel] < mtbdd_getvar(thenNode)) {
|
|
thenElse = thenThen = thenNode;
|
|
} else {
|
|
thenElse = mtbdd_getlow(thenNode);
|
|
thenThen = mtbdd_gethigh(thenNode);
|
|
}
|
|
}
|
|
|
|
// Visit else-else.
|
|
toMatrixComponentsRec(mtbdd_regular(elseElse), mtbdd_hascomp(elseElse) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
|
|
// Visit else-then.
|
|
toMatrixComponentsRec(mtbdd_regular(elseThen), mtbdd_hascomp(elseThen) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
|
|
// Visit then-else.
|
|
toMatrixComponentsRec(mtbdd_regular(thenElse), mtbdd_hascomp(thenElse) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
|
|
// Visit then-then.
|
|
toMatrixComponentsRec(mtbdd_regular(thenThen), mtbdd_hascomp(thenThen) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::fromVector(InternalDdManager<DdType::Sylvan> const* ddManager, std::vector<ValueType> const& values, storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices) {
|
|
uint_fast64_t offset = 0;
|
|
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, sylvan::Mtbdd(fromVectorRec(offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices)));
|
|
}
|
|
|
|
template<typename ValueType>
|
|
MTBDD InternalAdd<DdType::Sylvan, ValueType>::fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices) {
|
|
if (currentLevel == maxLevel) {
|
|
// If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one
|
|
// (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we
|
|
// need to copy the next value of the vector iff the then-offset is greater than zero.
|
|
if (odd.getThenOffset() > 0) {
|
|
return getLeaf(values[currentOffset++]);
|
|
} else {
|
|
return getLeaf(storm::utility::zero<ValueType>());
|
|
}
|
|
} else {
|
|
// If the total offset is zero, we can just return the constant zero DD.
|
|
if (odd.getThenOffset() + odd.getElseOffset() == 0) {
|
|
return getLeaf(storm::utility::zero<ValueType>());
|
|
}
|
|
|
|
// Determine the new else-successor.
|
|
MTBDD elseSuccessor;
|
|
if (odd.getElseOffset() > 0) {
|
|
elseSuccessor = fromVectorRec(currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices);
|
|
} else {
|
|
elseSuccessor = getLeaf(storm::utility::zero<ValueType>());
|
|
}
|
|
mtbdd_refs_push(elseSuccessor);
|
|
|
|
// Determine the new then-successor.
|
|
MTBDD thenSuccessor;
|
|
if (odd.getThenOffset() > 0) {
|
|
thenSuccessor = fromVectorRec(currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices);
|
|
} else {
|
|
thenSuccessor = getLeaf(storm::utility::zero<ValueType>());
|
|
}
|
|
mtbdd_refs_push(thenSuccessor);
|
|
|
|
// Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
|
|
MTBDD currentVar = mtbdd_makenode(ddVariableIndices[currentLevel], mtbdd_false, mtbdd_true);
|
|
mtbdd_refs_push(thenSuccessor);
|
|
LACE_ME;
|
|
MTBDD result = mtbdd_ite(currentVar, thenSuccessor, elseSuccessor);
|
|
|
|
// Dispose of the intermediate results
|
|
mtbdd_refs_pop(3);
|
|
|
|
return result;
|
|
}
|
|
}
|
|
|
|
template<typename ValueType>
|
|
MTBDD InternalAdd<DdType::Sylvan, ValueType>::getLeaf(double value) {
|
|
return mtbdd_double(value);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
MTBDD InternalAdd<DdType::Sylvan, ValueType>::getLeaf(uint_fast64_t value) {
|
|
return mtbdd_int64(value);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
MTBDD InternalAdd<DdType::Sylvan, ValueType>::getLeaf(storm::RationalFunction const& value) {
|
|
storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value);
|
|
return mtbdd_storm_rational_function(ptr);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
MTBDD InternalAdd<DdType::Sylvan, ValueType>::getLeaf(storm::RationalNumber const& value) {
|
|
storm_rational_function_ptr ptr = (storm_rational_number_ptr)(&value);
|
|
return mtbdd_storm_rational_number(ptr);
|
|
}
|
|
|
|
template<typename ValueType>
|
|
sylvan::Mtbdd InternalAdd<DdType::Sylvan, ValueType>::getSylvanMtbdd() const {
|
|
return sylvanMtbdd;
|
|
}
|
|
|
|
template<typename ValueType>
|
|
std::string InternalAdd<DdType::Sylvan, ValueType>::getStringId() const {
|
|
std::stringstream ss;
|
|
ss << this->getSylvanMtbdd().GetMTBDD();
|
|
return ss.str();
|
|
}
|
|
|
|
template class InternalAdd<DdType::Sylvan, double>;
|
|
template class InternalAdd<DdType::Sylvan, uint_fast64_t>;
|
|
|
|
template class InternalAdd<DdType::Sylvan, storm::RationalNumber>;
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template class InternalAdd<DdType::Sylvan, storm::RationalFunction>;
|
|
#endif
|
|
}
|
|
}
|