sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Remove trailing whitespace

tempestpy_adaptions
Daniel Basgöze 5 years ago
parent
002d9e1925
commit
b7c53c080b
1 changed files with 124 additions and 124 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 248
      src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

248
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -21,19 +21,19 @@ namespace storm {
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);
@ -50,47 +50,47 @@ namespace storm {
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));
@ -100,7 +100,7 @@ namespace storm {
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 {
@ -119,7 +119,7 @@ namespace storm {
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) {
@ -137,7 +137,7 @@ namespace storm {
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 {
@ -174,7 +174,7 @@ namespace storm {
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 {
@ -193,7 +193,7 @@ namespace storm {
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) {
@ -211,7 +211,7 @@ namespace storm {
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 {
@ -230,7 +230,7 @@ namespace storm {
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) {
@ -248,7 +248,7 @@ namespace storm {
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 {
@ -270,7 +270,7 @@ namespace storm {
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 {
@ -314,7 +314,7 @@ namespace storm {
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 {
@ -331,7 +331,7 @@ namespace storm {
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 {
@ -365,7 +365,7 @@ namespace storm {
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 {
@ -382,14 +382,14 @@ namespace storm {
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));
@ -411,7 +411,7 @@ namespace storm {
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 {
@ -428,7 +428,7 @@ namespace storm {
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 {
@ -474,7 +474,7 @@ namespace storm {
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 {
@ -486,7 +486,7 @@ namespace storm {
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));
@ -501,7 +501,7 @@ namespace storm {
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 {
@ -513,7 +513,7 @@ namespace storm {
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));
@ -528,7 +528,7 @@ namespace storm {
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 {
@ -554,7 +554,7 @@ namespace storm {
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) {
@ -577,7 +577,7 @@ namespace storm {
}
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;
@ -588,17 +588,17 @@ namespace storm {
}
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 {
@ -606,7 +606,7 @@ namespace storm {
for (auto const& ddVariable : summationDdVariables) {
summationVariables &= ddVariable;
}
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AndExistsRF(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
}
#endif
@ -617,7 +617,7 @@ namespace storm {
for (auto const& ddVariable : summationDdVariables) {
summationVariables &= ddVariable;
}
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.AndExistsRN(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
}
@ -627,7 +627,7 @@ namespace storm {
for (auto const& ddVariable : summationDdVariables) {
summationVariables &= ddVariable;
}
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AndExists(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd()));
}
@ -638,7 +638,7 @@ namespace storm {
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
@ -649,7 +649,7 @@ namespace storm {
for (auto const& ddVariable : summationDdVariables) {
summationVariables &= ddVariable;
}
return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.AndExistsRN(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd()));
}
@ -669,7 +669,7 @@ namespace storm {
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));
@ -679,7 +679,7 @@ namespace storm {
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 {
@ -691,32 +691,32 @@ namespace storm {
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) {
@ -724,17 +724,17 @@ namespace storm {
}
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());
@ -744,14 +744,14 @@ namespace storm {
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());
@ -761,44 +761,44 @@ namespace storm {
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.
@ -814,29 +814,29 @@ namespace storm {
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.
@ -845,15 +845,15 @@ namespace storm {
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;
@ -874,27 +874,27 @@ namespace storm {
// 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) {
@ -902,19 +902,19 @@ namespace storm {
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));
@ -927,19 +927,19 @@ namespace storm {
// 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.
@ -952,12 +952,12 @@ namespace storm {
} 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);
@ -965,27 +965,27 @@ namespace storm {
// 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>
std::vector<std::vector<InternalAdd<DdType::Sylvan, ValueType>>> InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroups(std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& vectors, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
std::vector<std::vector<InternalAdd<DdType::Sylvan, ValueType>>> result;
@ -997,18 +997,18 @@ namespace storm {
}
dds.push_back(this->getSylvanMtbdd().GetMTBDD());
negatedDds.set(vectors.size(), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()));
splitIntoGroupsRec(dds, negatedDds, 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)) {
@ -1018,11 +1018,11 @@ namespace storm {
// 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);
@ -1036,7 +1036,7 @@ namespace storm {
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)) {
@ -1046,18 +1046,18 @@ namespace storm {
} 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;
@ -1069,18 +1069,18 @@ namespace storm {
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>::splitIntoGroupsRec(std::vector<MTBDD> const& dds, storm::storage::BitVector const& negatedDds, std::vector<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.
@ -1096,7 +1096,7 @@ namespace storm {
return;
}
}
if (currentLevel == maxLevel) {
std::vector<InternalAdd<DdType::Sylvan, ValueType>> newGroup;
for (uint64_t ddIndex = 0; ddIndex < dds.size(); ++ddIndex) {
@ -1122,19 +1122,19 @@ namespace storm {
splitIntoGroupsRec(elseSubDds, elseNegatedSubDds, 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) {
@ -1146,7 +1146,7 @@ namespace storm {
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)) {
@ -1160,7 +1160,7 @@ namespace storm {
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;
@ -1169,7 +1169,7 @@ namespace storm {
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.
@ -1180,13 +1180,13 @@ namespace storm {
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) {
@ -1203,7 +1203,7 @@ namespace storm {
if (odd.getThenOffset() + odd.getElseOffset() == 0) {
return getLeaf(storm::utility::zero<ValueType>());
}
// Determine the new else-successor.
MTBDD elseSuccessor;
if (odd.getElseOffset() > 0) {
@ -1212,7 +1212,7 @@ namespace storm {
elseSuccessor = getLeaf(storm::utility::zero<ValueType>());
}
mtbdd_refs_push(elseSuccessor);
// Determine the new then-successor.
MTBDD thenSuccessor;
if (odd.getThenOffset() > 0) {
@ -1221,25 +1221,25 @@ namespace storm {
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);
@ -1261,14 +1261,14 @@ namespace storm {
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>;

Write Preview
Loading…
Cancel
Save