diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 1d02cadb3..2eddadd3a 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -21,19 +21,19 @@ namespace storm { InternalAdd::InternalAdd() : ddManager(nullptr), sylvanMtbdd() { // Intentionally left empty. } - + template InternalAdd::InternalAdd(InternalDdManager const* ddManager, sylvan::Mtbdd const& sylvanMtbdd) : ddManager(ddManager), sylvanMtbdd(sylvanMtbdd) { // Intentionally left empty. } - + template ValueType InternalAdd::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::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::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::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 bool InternalAdd::operator==(InternalAdd const& other) const { return this->sylvanMtbdd == other.sylvanMtbdd; } - + template bool InternalAdd::operator!=(InternalAdd const& other) const { return this->sylvanMtbdd != other.sylvanMtbdd; } - + template InternalAdd InternalAdd::operator+(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd)); @@ -100,7 +100,7 @@ namespace storm { InternalAdd InternalAdd::operator+(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.PlusRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator+(InternalAdd const& other) const { @@ -119,7 +119,7 @@ namespace storm { this->sylvanMtbdd = this->sylvanMtbdd.PlusRN(other.sylvanMtbdd); return *this; } - + #ifdef STORM_HAVE_CARL template<> InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { @@ -137,7 +137,7 @@ namespace storm { InternalAdd InternalAdd::operator*(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.TimesRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator*(InternalAdd const& other) const { @@ -174,7 +174,7 @@ namespace storm { InternalAdd InternalAdd::operator-(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.MinusRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator-(InternalAdd const& other) const { @@ -193,7 +193,7 @@ namespace storm { this->sylvanMtbdd = this->sylvanMtbdd.MinusRN(other.sylvanMtbdd); return *this; } - + #ifdef STORM_HAVE_CARL template<> InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { @@ -211,7 +211,7 @@ namespace storm { InternalAdd InternalAdd::operator/(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.DivideRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator/(InternalAdd const& other) const { @@ -230,7 +230,7 @@ namespace storm { this->sylvanMtbdd = this->sylvanMtbdd.DivideRN(other.sylvanMtbdd); return *this; } - + #ifdef STORM_HAVE_CARL template<> InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { @@ -248,7 +248,7 @@ namespace storm { InternalBdd InternalAdd::equals(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.EqualsRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::equals(InternalAdd const& other) const { @@ -270,7 +270,7 @@ namespace storm { InternalBdd InternalAdd::less(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.LessRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::less(InternalAdd const& other) const { @@ -314,7 +314,7 @@ namespace storm { InternalAdd InternalAdd::pow(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.PowRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::pow(InternalAdd const& other) const { @@ -331,7 +331,7 @@ namespace storm { InternalAdd InternalAdd::mod(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational numbers."); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::mod(InternalAdd const&) const { @@ -365,7 +365,7 @@ namespace storm { InternalAdd InternalAdd::floor() const { return InternalAdd(ddManager, this->sylvanMtbdd.FloorRN()); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::floor() const { @@ -382,14 +382,14 @@ namespace storm { InternalAdd InternalAdd::ceil() const { return InternalAdd(ddManager, this->sylvanMtbdd.CeilRN()); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::ceil() const { return InternalAdd(ddManager, this->sylvanMtbdd.CeilRF()); } #endif - + template InternalAdd InternalAdd::sharpenKwekMehlhorn(size_t precision) const { return InternalAdd(ddManager, this->sylvanMtbdd.SharpenKwekMehlhorn(precision)); @@ -411,7 +411,7 @@ namespace storm { InternalAdd InternalAdd::minimum(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.MinRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::minimum(InternalAdd const& other) const { @@ -428,7 +428,7 @@ namespace storm { InternalAdd InternalAdd::maximum(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.MaxRN(other.sylvanMtbdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::maximum(InternalAdd const& other) const { @@ -474,7 +474,7 @@ namespace storm { InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlusRN(cube.sylvanBdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { @@ -486,7 +486,7 @@ namespace storm { InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd)); } - + template InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { return InternalBdd(ddManager, this->sylvanMtbdd.AbstractMinRepresentative(cube.sylvanBdd)); @@ -501,7 +501,7 @@ namespace storm { InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMinRN(cube.sylvanBdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { @@ -513,7 +513,7 @@ namespace storm { InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd)); } - + template InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const& cube) const { return InternalBdd(ddManager, this->sylvanMtbdd.AbstractMaxRepresentative(cube.sylvanBdd)); @@ -528,7 +528,7 @@ namespace storm { InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMaxRN(cube.sylvanBdd)); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { @@ -554,7 +554,7 @@ namespace storm { return this->sylvanMtbdd.EqualNormRN(other.sylvanMtbdd, precision); } } - + template<> bool InternalAdd::equalModuloPrecision(InternalAdd const& other, storm::RationalFunction const& precision, bool relative) const { if (relative) { @@ -577,7 +577,7 @@ namespace storm { } return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices)); } - + template InternalAdd InternalAdd::permuteVariables(std::vector> const& from, std::vector> const& to) const { std::vector fromIndices; @@ -588,17 +588,17 @@ namespace storm { } return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices)); } - + template InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { InternalBdd summationVariables = ddManager->getBddOne(); for (auto const& ddVariable : summationDdVariables) { summationVariables &= ddVariable; } - + return InternalAdd(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } - + #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { @@ -606,7 +606,7 @@ namespace storm { for (auto const& ddVariable : summationDdVariables) { summationVariables &= ddVariable; } - + return InternalAdd(ddManager, this->sylvanMtbdd.AndExistsRF(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } #endif @@ -617,7 +617,7 @@ namespace storm { for (auto const& ddVariable : summationDdVariables) { summationVariables &= ddVariable; } - + return InternalAdd(ddManager, this->sylvanMtbdd.AndExistsRN(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } @@ -627,7 +627,7 @@ namespace storm { for (auto const& ddVariable : summationDdVariables) { summationVariables &= ddVariable; } - + return InternalAdd(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(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(ddManager, this->sylvanMtbdd.AndExistsRN(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd())); } @@ -669,7 +669,7 @@ namespace storm { return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThresholdRF(value)); } #endif - + template InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddThreshold(value)); @@ -679,7 +679,7 @@ namespace storm { InternalBdd InternalAdd::greaterOrEqual(storm::RationalNumber const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddThresholdRN(value)); } - + #ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const& value) const { @@ -691,32 +691,32 @@ namespace storm { InternalBdd InternalAdd::less(ValueType const& value) const { return !this->greaterOrEqual(value); } - + template InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { return !this->greater(value); } - + template InternalBdd InternalAdd::notZero() const { return InternalBdd(ddManager, this->sylvanMtbdd.NotZero()); } - + template InternalAdd InternalAdd::constrain(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (constrain) not yet implemented."); } - + template InternalAdd InternalAdd::restrict(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (restrict) not yet implemented."); } - + template InternalBdd InternalAdd::getSupport() const { return InternalBdd(ddManager, sylvan::Bdd(static_cast(this->sylvanMtbdd.Support().GetMTBDD()))); } - + template uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { if (numberOfDdVariables == 0) { @@ -724,17 +724,17 @@ namespace storm { } return static_cast(this->sylvanMtbdd.NonZeroCount(numberOfDdVariables)); } - + template uint_fast64_t InternalAdd::getLeafCount() const { return static_cast(this->sylvanMtbdd.CountLeaves()); } - + template uint_fast64_t InternalAdd::getNodeCount() const { return static_cast(this->sylvanMtbdd.NodeCount()); } - + template ValueType InternalAdd::getMin() const { return getValue(this->sylvanMtbdd.Minimum().GetMTBDD()); @@ -744,14 +744,14 @@ namespace storm { storm::RationalNumber InternalAdd::getMin() const { return getValue(this->sylvanMtbdd.MinimumRN().GetMTBDD()); } - + #ifdef STORM_HAVE_CARL template <> storm::RationalFunction InternalAdd::getMin() const { return getValue(this->sylvanMtbdd.MinimumRF().GetMTBDD()); } #endif - + template ValueType InternalAdd::getMax() const { return getValue(this->sylvanMtbdd.Maximum().GetMTBDD()); @@ -761,44 +761,44 @@ namespace storm { storm::RationalNumber InternalAdd::getMax() const { return getValue(this->sylvanMtbdd.MaximumRN().GetMTBDD()); } - + #ifdef STORM_HAVE_CARL template<> storm::RationalFunction InternalAdd::getMax() const { return getValue(this->sylvanMtbdd.MaximumRF().GetMTBDD()); } #endif - + template ValueType InternalAdd::getValue() const { return getValue(this->sylvanMtbdd.GetMTBDD()); } - + template bool InternalAdd::isOne() const { return *this == ddManager->getAddOne(); } - + template bool InternalAdd::isZero() const { return *this == ddManager->getAddZero(); } - + template bool InternalAdd::isConstant() const { return this->sylvanMtbdd.isTerminal(); } - + template uint_fast64_t InternalAdd::getIndex() const { return static_cast(this->sylvanMtbdd.TopVar()); } - + template uint_fast64_t InternalAdd::getLevel() const { return this->getIndex(); } - + template void InternalAdd::exportToDot(std::string const& filename, std::vector 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 AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const& variableCube, uint_fast64_t numberOfDdVariables, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { return AddIterator::createBeginIterator(fullDdManager, this->getSylvanMtbdd(), variableCube.getSylvanBdd(), numberOfDdVariables, &metaVariables, enumerateDontCareMetaVariables); } - + template AddIterator InternalAdd::end(DdManager const& fullDdManager) const { return AddIterator::createEndIterator(fullDdManager); } - + template Odd InternalAdd::createOdd(std::vector const& ddVariableIndices) const { // Prepare a unique table for each level that keeps the constructed ODD nodes unique. std::vector>> uniqueTableForLevels(ddVariableIndices.size() + 1); - + // Now construct the ODD structure from the ADD. std::shared_ptr 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 std::shared_ptr InternalAdd::createOddRec(BDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>& 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 elseNode = createOddRec(mtbdd_regular(mtbdd_getlow(dd)), currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr 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(elseNode, totalElseOffset, thenNode, totalThenOffset); uniqueTableForLevels[currentLevel].emplace(dd, oddNode); return oddNode; } } } - + template InternalDdManager const& InternalAdd::getInternalDdManager() const { return *ddManager; } - + template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function 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 void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function 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 void InternalAdd::forEach(Odd const& odd, std::vector const& ddVariableIndices, std::function const& function) const { forEachRec(this->getSylvanMtbdd().GetMTBDD(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, function); } - + template void InternalAdd::forEachRec(MTBDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::function 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 std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const { std::vector result; decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0); return result; } - + template void InternalAdd::decodeGroupLabelsRec(MTBDD dd, std::vector& labels, std::vector 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 std::vector> InternalAdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { std::vector> result; splitIntoGroupsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); return result; } - + template std::vector, InternalAdd>> InternalAdd::splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const { std::vector, InternalAdd>> 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 std::vector>> InternalAdd::splitIntoGroups(std::vector> const& vectors, std::vector const& ddGroupVariableIndices) const { std::vector>> 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 void InternalAdd::splitIntoGroupsRec(MTBDD dd, bool negated, std::vector>& groups, std::vector 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(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(ddManager, negated1 ? sylvan::Mtbdd(dd1).Negate() : sylvan::Mtbdd(dd1)), InternalAdd(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 void InternalAdd::splitIntoGroupsRec(std::vector const& dds, storm::storage::BitVector const& negatedDds, std::vector>>& groups, std::vector 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> 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 void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector 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 void InternalAdd::toMatrixComponentsRec(MTBDD dd, bool negated, std::vector const& rowGroupOffsets, std::vector& rowIndications, std::vector>& 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 const& ddRowVariableIndices, std::vector 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 InternalAdd InternalAdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices) { uint_fast64_t offset = 0; return InternalAdd(ddManager, sylvan::Mtbdd(fromVectorRec(offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices))); } - + template MTBDD InternalAdd::fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices) { if (currentLevel == maxLevel) { @@ -1203,7 +1203,7 @@ namespace storm { if (odd.getThenOffset() + odd.getElseOffset() == 0) { return getLeaf(storm::utility::zero()); } - + // Determine the new else-successor. MTBDD elseSuccessor; if (odd.getElseOffset() > 0) { @@ -1212,7 +1212,7 @@ namespace storm { elseSuccessor = getLeaf(storm::utility::zero()); } 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()); } 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 MTBDD InternalAdd::getLeaf(double value) { return mtbdd_double(value); } - + template MTBDD InternalAdd::getLeaf(uint_fast64_t value) { return mtbdd_int64(value); @@ -1261,14 +1261,14 @@ namespace storm { sylvan::Mtbdd InternalAdd::getSylvanMtbdd() const { return sylvanMtbdd; } - + template std::string InternalAdd::getStringId() const { std::stringstream ss; ss << this->getSylvanMtbdd().GetMTBDD(); return ss.str(); } - + template class InternalAdd; template class InternalAdd;