diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 7f511770d..e646e473d 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -25,12 +25,12 @@ namespace storm { InternalBdd::InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) { // Intentionally left empty. } - + InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter) { uint_fast64_t offset = 0; return InternalBdd(ddManager, sylvan::Bdd(fromVectorRec(offset, 0, sortedDdVariableIndices.size(), odd, sortedDdVariableIndices, filter))); } - + BDD InternalBdd::fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, Odd const& odd, std::vector const& ddVariableIndices, std::function const& filter) { 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 @@ -50,7 +50,7 @@ namespace storm { if (odd.getThenOffset() + odd.getElseOffset() == 0) { return sylvan_false; } - + // Determine the new else-successor. BDD elseSuccessor; if (odd.getElseOffset() > 0) { @@ -59,7 +59,7 @@ namespace storm { elseSuccessor = sylvan_false; } bdd_refs_push(elseSuccessor); - + // Determine the new then-successor. BDD thenSuccessor; if (odd.getThenOffset() > 0) { @@ -68,29 +68,29 @@ namespace storm { thenSuccessor = sylvan_false; } bdd_refs_push(thenSuccessor); - + // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor); BDD currentVar = sylvan_ithvar(static_cast(ddVariableIndices[currentLevel])); bdd_refs_push(currentVar); LACE_ME; BDD result = sylvan_ite(currentVar, thenSuccessor, elseSuccessor); - + // Dispose of the intermediate results. bdd_refs_pop(3); - + return result; } } - + bool InternalBdd::operator==(InternalBdd const& other) const { return sylvanBdd == other.sylvanBdd; } - + bool InternalBdd::operator!=(InternalBdd const& other) const { return sylvanBdd != other.sylvanBdd; } - + InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const&, std::vector> const&) const { return InternalBdd(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, sylvan::Bdd(sylvan_false))); } @@ -98,10 +98,10 @@ namespace storm { InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const&, std::vector> const&) const { return InternalBdd(ddManager, this->sylvanBdd.RelPrev(relation.sylvanBdd, sylvan::Bdd(sylvan_false))); } - + InternalBdd InternalBdd::inverseRelationalProductWithExtendedRelation(InternalBdd const& relation, std::vector> const& rowVariables, std::vector> const& columnVariables) const { // Currently, there is no specialized version to perform this operation, so we fall back to the regular operations. - + InternalBdd columnCube = ddManager->getBddOne(); for (auto const& variable : columnVariables) { columnCube &= variable; @@ -109,79 +109,79 @@ namespace storm { return this->swapVariables(rowVariables, columnVariables).andExists(relation, columnCube); } - + InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { return InternalBdd(ddManager, this->sylvanBdd.Ite(thenDd.sylvanBdd, elseDd.sylvanBdd)); } - + template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const { return InternalAdd(ddManager, this->sylvanBdd.Ite(thenAdd.getSylvanMtbdd(), elseAdd.getSylvanMtbdd())); } - + InternalBdd InternalBdd::operator||(InternalBdd const& other) const { return InternalBdd(ddManager, this->sylvanBdd | other.sylvanBdd); } - + InternalBdd& InternalBdd::operator|=(InternalBdd const& other) { this->sylvanBdd |= other.sylvanBdd; return *this; } - + InternalBdd InternalBdd::operator&&(InternalBdd const& other) const { return InternalBdd(ddManager, this->sylvanBdd & other.sylvanBdd); } - + InternalBdd& InternalBdd::operator&=(InternalBdd const& other) { this->sylvanBdd &= other.sylvanBdd; return *this; } - + InternalBdd InternalBdd::iff(InternalBdd const& other) const { return InternalBdd(ddManager, !(this->sylvanBdd ^ other.sylvanBdd)); } - + InternalBdd InternalBdd::exclusiveOr(InternalBdd const& other) const { return InternalBdd(ddManager, this->sylvanBdd ^ other.sylvanBdd); } - + InternalBdd InternalBdd::implies(InternalBdd const& other) const { return InternalBdd(ddManager, (!this->sylvanBdd) | other.sylvanBdd); } - + InternalBdd InternalBdd::operator!() const { return InternalBdd(ddManager, !this->sylvanBdd); } - + InternalBdd& InternalBdd::complement() { this->sylvanBdd = !this->sylvanBdd; return *this; } - + InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { return InternalBdd(ddManager, this->sylvanBdd.ExistAbstract(cube.sylvanBdd)); } - + InternalBdd InternalBdd::existsAbstractRepresentative(InternalBdd const& cube) const { return InternalBdd(ddManager, this->sylvanBdd.ExistAbstractRepresentative(cube.sylvanBdd)); } - + InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { return InternalBdd(ddManager, this->sylvanBdd.UnivAbstract(cube.sylvanBdd)); } - + InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { return InternalBdd(ddManager, this->sylvanBdd.AndAbstract(other.sylvanBdd, cube.sylvanBdd)); } - + InternalBdd InternalBdd::constrain(InternalBdd const& constraint) const { return InternalBdd(ddManager, this->sylvanBdd.Constrain(constraint.sylvanBdd)); } - + InternalBdd InternalBdd::restrict(InternalBdd const& constraint) const { return InternalBdd(ddManager, this->sylvanBdd.Restrict(constraint.sylvanBdd)); } - + InternalBdd InternalBdd::swapVariables(std::vector> const& from, std::vector> const& to) const { std::vector fromIndices; std::vector toIndices; @@ -193,45 +193,45 @@ namespace storm { } return InternalBdd(ddManager, this->sylvanBdd.Permute(fromIndices, toIndices)); } - + InternalBdd InternalBdd::getSupport() const { return InternalBdd(ddManager, this->sylvanBdd.Support()); } - + uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { if (numberOfDdVariables == 0) { return 0; } return static_cast(this->sylvanBdd.SatCount(numberOfDdVariables)); } - + uint_fast64_t InternalBdd::getLeafCount() const { // For BDDs, the leaf count is always one, because the only leaf is the false leaf (and true is represented // by a negation edge to false). return 1; } - + uint_fast64_t InternalBdd::getNodeCount() const { // We have to add one to also count the false-leaf, which is the only leaf appearing in BDDs. return static_cast(this->sylvanBdd.NodeCount()); } - + bool InternalBdd::isOne() const { return this->sylvanBdd.isOne(); } - + bool InternalBdd::isZero() const { return this->sylvanBdd.isZero(); } - + uint_fast64_t InternalBdd::getIndex() const { return static_cast(this->sylvanBdd.TopVar()); } - + uint_fast64_t InternalBdd::getLevel() const { return this->getIndex(); } - + void InternalBdd::exportToDot(std::string const& filename, std::vector const&, bool) const { FILE* filePointer = fopen(filename.c_str() , "a+"); this->sylvanBdd.PrintDot(filePointer); @@ -243,41 +243,41 @@ namespace storm { this->sylvanBdd.PrintText(filePointer); fclose(filePointer); } - + sylvan::Bdd& InternalBdd::getSylvanBdd() { return sylvanBdd; } - + sylvan::Bdd const& InternalBdd::getSylvanBdd() const { return sylvanBdd; } - + template InternalAdd InternalBdd::toAdd() const { if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toDoubleMtbdd()); } else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toInt64Mtbdd()); - } + } #ifdef STORM_HAVE_CARL else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toStormRationalNumberMtbdd()); - } + } else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toStormRationalFunctionMtbdd()); - } + } #endif else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal ADD type."); } } - + storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const { storm::storage::BitVector result(rowOdd.getTotalOffset()); this->toVectorRec(bdd_regular(this->getSylvanBdd().GetBDD()), result, rowOdd, bdd_isnegated(this->getSylvanBdd().GetBDD()), 0, ddVariableIndices.size(), 0, ddVariableIndices); return result; } - + void InternalBdd::toVectorRec(BDD dd, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { // If there are no more values to select, we can directly return. if (dd == sylvan_false && !complement) { @@ -285,7 +285,7 @@ namespace storm { } else if (dd == sylvan_true && complement) { return; } - + // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentRowLevel == maxLevel) { result.set(currentRowOffset, true); @@ -296,34 +296,34 @@ namespace storm { // Otherwise, we compute the ODDs for both the then- and else successors. BDD elseDdNode = sylvan_low(dd); BDD thenDdNode = sylvan_high(dd); - + // Determine whether we have to evaluate the successors as if they were complemented. bool elseComplemented = bdd_isnegated(elseDdNode) ^ complement; bool thenComplemented = bdd_isnegated(thenDdNode) ^ complement; - + toVectorRec(bdd_regular(elseDdNode), result, rowOdd.getElseSuccessor(), elseComplemented, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); toVectorRec(bdd_regular(thenDdNode), result, rowOdd.getThenSuccessor(), thenComplemented, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); } } - + Odd InternalBdd::createOdd(std::vector const& ddVariableIndices) const { // Prepare a unique table for each level that keeps the constructed ODD nodes unique. std::vector, std::shared_ptr, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1); - + // Now construct the ODD structure from the BDD. std::shared_ptr rootOdd = createOddRec(bdd_regular(this->getSylvanBdd().GetBDD()), bdd_isnegated(this->getSylvanBdd().GetBDD()), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); - + // Return a copy of the root node to remove the shared_ptr encapsulation. return Odd(*rootOdd); } - + std::size_t InternalBdd::HashFunctor::operator()(std::pair const& key) const { std::size_t result = 0; boost::hash_combine(result, key.first); boost::hash_combine(result, key.second); return result; } - + std::shared_ptr InternalBdd::createOddRec(BDD dd, bool complement, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& 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(std::make_pair(dd, complement)); @@ -331,23 +331,23 @@ namespace storm { return iterator->second; } else { // Otherwise, we need to recursively compute the ODD. - + // If we are already at 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; - + // If the DD is not the zero leaf, then the then-offset is 1. if (dd != mtbdd_false) { thenOffset = 1; } - + // If we need to complement the 'terminal' node, we need to negate its offset. if (complement) { thenOffset = 1 - thenOffset; } - + auto oddNode = std::make_shared(nullptr, elseOffset, nullptr, thenOffset); uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); return oddNode; @@ -368,23 +368,23 @@ namespace storm { // Determine whether we have to evaluate the successors as if they were complemented. bool elseComplemented = bdd_isnegated(elseDdNode) ^ complement; bool thenComplemented = bdd_isnegated(thenDdNode) ^ complement; - + std::shared_ptr elseNode = createOddRec(bdd_regular(elseDdNode), elseComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = createOddRec(bdd_regular(thenDdNode), thenComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); - + auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); return oddNode; } } } - + template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const { uint_fast64_t currentIndex = 0; filterExplicitVectorRec(bdd_regular(this->getSylvanBdd().GetBDD()), 0, bdd_isnegated(this->getSylvanBdd().GetBDD()), ddVariableIndices.size(), ddVariableIndices, 0, odd, targetValues, currentIndex, sourceValues); } - + template void InternalBdd::filterExplicitVectorRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values) { // If there are no more values to select, we can directly return. @@ -393,7 +393,7 @@ namespace storm { } else if (dd == sylvan_true && complement) { return; } - + if (currentLevel == maxLevel) { result[currentIndex++] = values[currentOffset]; } else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) { @@ -405,21 +405,21 @@ namespace storm { // Otherwise, we compute the ODDs for both the then- and else successors. BDD thenDdNode = sylvan_high(dd); BDD elseDdNode = sylvan_low(dd); - + // Determine whether we have to evaluate the successors as if they were complemented. bool elseComplemented = bdd_isnegated(elseDdNode) ^ complement; bool thenComplemented = bdd_isnegated(thenDdNode) ^ complement; - + filterExplicitVectorRec(bdd_regular(elseDdNode), currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values); filterExplicitVectorRec(bdd_regular(thenDdNode), currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values); } } - + void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const { uint_fast64_t currentIndex = 0; filterExplicitVectorRec(bdd_regular(this->getSylvanBdd().GetBDD()), 0, bdd_isnegated(this->getSylvanBdd().GetBDD()), ddVariableIndices.size(), ddVariableIndices, 0, odd, targetValues, currentIndex, sourceValues); } - + void InternalBdd::filterExplicitVectorRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, storm::storage::BitVector& result, uint_fast64_t& currentIndex, storm::storage::BitVector const& values) { // If there are no more values to select, we can directly return. if (dd == sylvan_false && !complement) { @@ -427,7 +427,7 @@ namespace storm { } else if (dd == sylvan_true && complement) { return; } - + if (currentLevel == maxLevel) { result.set(currentIndex++, values.get(currentOffset)); } else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) { @@ -439,28 +439,28 @@ namespace storm { // Otherwise, we compute the ODDs for both the then- and else successors. BDD thenDdNode = sylvan_high(dd); BDD elseDdNode = sylvan_low(dd); - + // Determine whether we have to evaluate the successors as if they were complemented. bool elseComplemented = bdd_isnegated(elseDdNode) ^ complement; bool thenComplemented = bdd_isnegated(thenDdNode) ^ complement; - + filterExplicitVectorRec(bdd_regular(elseDdNode), currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values); filterExplicitVectorRec(bdd_regular(thenDdNode), currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values); } } - + std::vector> InternalBdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { std::vector> result; splitIntoGroupsRec(this->getSylvanBdd().GetBDD(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); return result; } - + void InternalBdd::splitIntoGroupsRec(BDD dd, 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 (dd == sylvan_false) { return; } - + if (currentLevel == maxLevel) { groups.push_back(InternalBdd(ddManager, sylvan::Bdd(dd))); } else if (bdd_isterminal(dd) || ddGroupVariableIndices[currentLevel] < sylvan_var(dd)) { @@ -470,39 +470,39 @@ namespace storm { // Otherwise, we compute the ODDs for both the then- and else successors. BDD thenDdNode = sylvan_high(dd); BDD elseDdNode = sylvan_low(dd); - + splitIntoGroupsRec(elseDdNode, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(thenDdNode, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } } - + std::pair, std::unordered_map> InternalBdd::toExpression(storm::expressions::ExpressionManager& manager) const { std::pair, std::unordered_map> result; - + // Create (and maintain) a mapping from the DD nodes to a counter that says the how-many-th node (within the // nodes of equal index) the node was. std::unordered_map nodeToCounterMap; std::vector nextCounterForIndex(ddManager->getNumberOfDdVariables(), 0); std::unordered_map, storm::expressions::Variable> countIndexToVariablePair; - + bool negated = bdd_isnegated(this->getSylvanBdd().GetBDD()); - + // Translate from the top node downwards. storm::expressions::Variable topVariable = this->toExpressionRec(bdd_regular(this->getSylvanBdd().GetBDD()), manager, result.first, result.second, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); - + // Create the final expression. if (negated) { result.first.push_back(!topVariable); } else { result.first.push_back(topVariable); } - + return result; } - + storm::expressions::Variable InternalBdd::toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map& indexToVariableMap, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex) { STORM_LOG_ASSERT(!bdd_isnegated(dd), "Expected non-negated BDD node."); - + // First, try to look up the current node if it's not a terminal node. auto nodeCounterIt = nodeToCounterMap.find(dd); if (nodeCounterIt != nodeToCounterMap.end()) { @@ -511,10 +511,10 @@ namespace storm { STORM_LOG_ASSERT(variableIt != countIndexToVariablePair.end(), "Unable to find node."); return variableIt->second; } - + // If the node was not yet encountered, we create a variable and associate it with the appropriate expression. storm::expressions::Variable newNodeVariable = manager.declareFreshBooleanVariable(); - + // Since we want to reuse the variable whenever possible, we insert the appropriate entries in the hash table. if (!bdd_isterminal(dd)) { // If we are dealing with a non-terminal node, we count it as a new node with this index. @@ -526,7 +526,7 @@ namespace storm { nodeToCounterMap[dd] = 0; countIndexToVariablePair[std::make_pair(0, sylvan_var(dd))] = newNodeVariable; } - + // In the terminal case, we can only have a one since we are considering non-negated nodes only. if (bdd_isterminal(dd)) { if (dd == sylvan_true) { @@ -542,7 +542,7 @@ namespace storm { BDD E = bdd_regular(e); storm::expressions::Variable thenVariable = toExpressionRec(T, manager, expressions, indexToVariableMap, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); storm::expressions::Variable elseVariable = toExpressionRec(E, manager, expressions, indexToVariableMap, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); - + // Create the appropriate expression. // Create the appropriate expression. auto indexVariable = indexToVariableMap.find(sylvan_var(dd)); @@ -555,21 +555,21 @@ namespace storm { } expressions.push_back(storm::expressions::iff(newNodeVariable, storm::expressions::ite(levelVariable, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable))); } - + // Return the variable for this node. return newNodeVariable; } - + template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; - + template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; - + template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const;