From 231c3ec060828b06bd2faa07905ff3e3773d04e3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 18 Nov 2015 16:10:34 +0100 Subject: [PATCH] started lifting toVector, etc. from the internal classes to the general superclasses Former-commit-id: 0501487b221651c23a00dcf3d8ba596fba8fbc0c --- src/storage/dd/Add.cpp | 448 ++++++++-------- src/storage/dd/cudd/InternalCuddAdd.cpp | 671 ++++++++++++------------ src/storage/dd/cudd/InternalCuddAdd.h | 39 +- 3 files changed, 580 insertions(+), 578 deletions(-) diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 67297f627..690299c5c 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -390,234 +390,234 @@ namespace storm { return result; } - template - std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector const& groupOffsets) const { - std::set rowMetaVariables; - - // Prepare the proper sets of meta variables. - for (auto const& variable : this->getContainedMetaVariables()) { - if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { - continue; - } - - rowMetaVariables.insert(variable); - } - std::vector ddGroupVariableIndices; - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::vector ddRowVariableIndices; - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - } - - return internalAdd.toVector(ddGroupVariableIndices, rowOdd, ddRowVariableIndices, groupOffsets); - } - - template - storm::storage::SparseMatrix Add::toMatrix() const { - std::set rowVariables; - std::set columnVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnVariables.insert(variable); - } else { - rowVariables.insert(variable); - } - } - - return toMatrix(rowVariables, columnVariables, Odd(this->sumAbstract(rowVariables)), Odd(this->sumAbstract(columnVariables))); - } - - template - storm::storage::SparseMatrix Add::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::set rowMetaVariables; - std::set columnMetaVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnMetaVariables.insert(variable); - } else { - rowMetaVariables.insert(variable); - } - } - - return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); - } - - template - storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); - - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); - - return internalAdd.toMatrix(rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); - } - - template - storm::storage::SparseMatrix Add::toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::set rowMetaVariables; - std::set columnMetaVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. - if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { - continue; - } - - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnMetaVariables.insert(variable); - } else { - rowMetaVariables.insert(variable); - } - } - - // Create the canonical row group sizes and build the matrix. - return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); - } - - template - storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - std::vector ddGroupVariableIndices; - std::set rowAndColumnMetaVariables; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - - return internalAdd.toMatrix(ddGroupVariableIndices, Bdd::getCube(*this->getDdManager(), groupMetaVariables), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices, Bdd::getCube(*this->getDdManager(), columnMetaVariables)); - } - - template - std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::set rowMetaVariables; - std::set columnMetaVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. - if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { - continue; - } - - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnMetaVariables.insert(variable); - } else { - rowMetaVariables.insert(variable); - } - } - - // Create the canonical row group sizes and build the matrix. - return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); - } - - template - std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - std::vector ddGroupVariableIndices; - std::set rowAndColumnMetaVariables; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - - return internalAdd.toMatrixVector(vector.internalAdd, ddGroupVariableIndices, std::move(rowGroupIndices), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices, Bdd::getCube(*this->getDdManager(), columnMetaVariables)); - } - - template - void Add::exportToDot(std::string const& filename) const { - internalAdd.exportToDot(filename, this->getDdManager()->getDdVariableNames()); - } - - template - AddIterator Add::begin(bool enumerateDontCareMetaVariables) const { - return internalAdd.begin(this->getDdManager(), this->getContainedMetaVariables(), enumerateDontCareMetaVariables); - } - - template - AddIterator Add::end(bool enumerateDontCareMetaVariables) const { - return internalAdd.end(this->getDdManager(), enumerateDontCareMetaVariables); - } - - template - std::ostream& operator<<(std::ostream& out, Add const& add) { - out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl; - std::vector variableNames; - for (auto const& variable : add.getContainedMetaVariables()) { - variableNames.push_back(variable.getName()); - } - out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl; - return out; - } +// template +// std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector const& groupOffsets) const { +// std::set rowMetaVariables; +// +// // Prepare the proper sets of meta variables. +// for (auto const& variable : this->getContainedMetaVariables()) { +// if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { +// continue; +// } +// +// rowMetaVariables.insert(variable); +// } +// std::vector ddGroupVariableIndices; +// for (auto const& variable : groupMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddGroupVariableIndices.push_back(ddVariable.getIndex()); +// } +// } +// std::vector ddRowVariableIndices; +// for (auto const& variable : rowMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddRowVariableIndices.push_back(ddVariable.getIndex()); +// } +// } +// +// return internalAdd.toVector(ddGroupVariableIndices, rowOdd, ddRowVariableIndices, groupOffsets); +// } +// +// template +// storm::storage::SparseMatrix Add::toMatrix() const { +// std::set rowVariables; +// std::set columnVariables; +// +// for (auto const& variable : this->getContainedMetaVariables()) { +// if (variable.getName().size() > 0 && variable.getName().back() == '\'') { +// columnVariables.insert(variable); +// } else { +// rowVariables.insert(variable); +// } +// } +// +// return toMatrix(rowVariables, columnVariables, Odd(this->sumAbstract(rowVariables)), Odd(this->sumAbstract(columnVariables))); +// } +// +// template +// storm::storage::SparseMatrix Add::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { +// std::set rowMetaVariables; +// std::set columnMetaVariables; +// +// for (auto const& variable : this->getContainedMetaVariables()) { +// if (variable.getName().size() > 0 && variable.getName().back() == '\'') { +// columnMetaVariables.insert(variable); +// } else { +// rowMetaVariables.insert(variable); +// } +// } +// +// return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); +// } +// +// template +// storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { +// std::vector ddRowVariableIndices; +// std::vector ddColumnVariableIndices; +// +// for (auto const& variable : rowMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddRowVariableIndices.push_back(ddVariable.getIndex()); +// } +// } +// std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); +// +// for (auto const& variable : columnMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddColumnVariableIndices.push_back(ddVariable.getIndex()); +// } +// } +// std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); +// +// return internalAdd.toMatrix(rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); +// } +// +// template +// storm::storage::SparseMatrix Add::toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { +// std::set rowMetaVariables; +// std::set columnMetaVariables; +// +// for (auto const& variable : this->getContainedMetaVariables()) { +// // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. +// if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { +// continue; +// } +// +// if (variable.getName().size() > 0 && variable.getName().back() == '\'') { +// columnMetaVariables.insert(variable); +// } else { +// rowMetaVariables.insert(variable); +// } +// } +// +// // Create the canonical row group sizes and build the matrix. +// return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); +// } +// +// template +// storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { +// std::vector ddRowVariableIndices; +// std::vector ddColumnVariableIndices; +// std::vector ddGroupVariableIndices; +// std::set rowAndColumnMetaVariables; +// +// for (auto const& variable : rowMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddRowVariableIndices.push_back(ddVariable.getIndex()); +// } +// rowAndColumnMetaVariables.insert(variable); +// } +// std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); +// for (auto const& variable : columnMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddColumnVariableIndices.push_back(ddVariable.getIndex()); +// } +// rowAndColumnMetaVariables.insert(variable); +// } +// std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); +// for (auto const& variable : groupMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddGroupVariableIndices.push_back(ddVariable.getIndex()); +// } +// } +// std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); +// +// return internalAdd.toMatrix(ddGroupVariableIndices, Bdd::getCube(*this->getDdManager(), groupMetaVariables), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices, Bdd::getCube(*this->getDdManager(), columnMetaVariables)); +// } +// +// template +// std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { +// std::set rowMetaVariables; +// std::set columnMetaVariables; +// +// for (auto const& variable : this->getContainedMetaVariables()) { +// // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. +// if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { +// continue; +// } +// +// if (variable.getName().size() > 0 && variable.getName().back() == '\'') { +// columnMetaVariables.insert(variable); +// } else { +// rowMetaVariables.insert(variable); +// } +// } +// +// // Create the canonical row group sizes and build the matrix. +// return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); +// } +// +// template +// std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { +// std::vector ddRowVariableIndices; +// std::vector ddColumnVariableIndices; +// std::vector ddGroupVariableIndices; +// std::set rowAndColumnMetaVariables; +// +// for (auto const& variable : rowMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddRowVariableIndices.push_back(ddVariable.getIndex()); +// } +// rowAndColumnMetaVariables.insert(variable); +// } +// std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); +// for (auto const& variable : columnMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddColumnVariableIndices.push_back(ddVariable.getIndex()); +// } +// rowAndColumnMetaVariables.insert(variable); +// } +// std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); +// for (auto const& variable : groupMetaVariables) { +// DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); +// for (auto const& ddVariable : metaVariable.getDdVariables()) { +// ddGroupVariableIndices.push_back(ddVariable.getIndex()); +// } +// } +// std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); +// +// return internalAdd.toMatrixVector(vector.internalAdd, ddGroupVariableIndices, std::move(rowGroupIndices), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices, Bdd::getCube(*this->getDdManager(), columnMetaVariables)); +// } +// +// template +// void Add::exportToDot(std::string const& filename) const { +// internalAdd.exportToDot(filename, this->getDdManager()->getDdVariableNames()); +// } +// +// template +// AddIterator Add::begin(bool enumerateDontCareMetaVariables) const { +// return internalAdd.begin(this->getDdManager(), this->getContainedMetaVariables(), enumerateDontCareMetaVariables); +// } +// +// template +// AddIterator Add::end(bool enumerateDontCareMetaVariables) const { +// return internalAdd.end(this->getDdManager(), enumerateDontCareMetaVariables); +// } +// +// template +// std::ostream& operator<<(std::ostream& out, Add const& add) { +// out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl; +// std::vector variableNames; +// for (auto const& variable : add.getContainedMetaVariables()) { +// variableNames.push_back(variable.getName()); +// } +// out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl; +// return out; +// } template void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { std::function fct = [] (ValueType const& a, ValueType const& b) -> ValueType { return a + b; }; - return internalAdd.composeVector(odd, ddVariableIndices, targetVector, fct); + return internalAdd.composeVectors(odd, ddVariableIndices, targetVector, fct); } template diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 0b9d0f6dd..8a7010177 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -343,34 +343,14 @@ namespace storm { } template - std::vector InternalAdd::toVector(std::vector const& ddGroupVariableIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, std::vector const& groupOffsets) const { - // Start by splitting the symbolic vector into groups. - std::vector> groups; - splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); - - // Now iterate over the groups and add them to the resulting vector. - std::vector result(groupOffsets.back(), storm::utility::zero()); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - toVectorRec(groups[i].getCuddDdNode(), result, groupOffsets, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); - } - - return result; + void InternalAdd::composeVectors(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + composeVectorsRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); } template - void InternalAdd::addToExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { - composeVector(odd, ddVariableIndices, targetVector, std::plus()); - } - - template - void InternalAdd::composeVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { - composeVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); - } - - template - void InternalAdd::composeVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + void InternalAdd::composeVectorsRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { // For the empty DD, we do not need to add any entries. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { return; } @@ -380,322 +360,343 @@ namespace storm { } else if (ddVariableIndices[currentLevel] < dd->index) { // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set // and for the one in which it is not set. - composeVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + composeVectorsRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeVectorsRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } else { // Otherwise, we simply recursively call the function for both (different) cases. - composeVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); - } - } - - template - void InternalAdd::toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { - // For the empty DD, we do not need to add any entries. - if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { - 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[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); - } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { - toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); - toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); - } else { - toVectorRec(Cudd_E(dd), result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); - toVectorRec(Cudd_T(dd), result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); - } - } - - template - storm::storage::SparseMatrix InternalAdd::toMatrix(uint_fast64_t numberOfDdVariables, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) const { - // Prepare the vectors that represent the matrix. - std::vector rowIndications(rowOdd.getTotalOffset() + 1); - std::vector> columnsAndValues(this->getNonZeroCount(numberOfDdVariables)); - - // Create a trivial row grouping. - std::vector trivialRowGroupIndices(rowIndications.size()); - uint_fast64_t i = 0; - for (auto& entry : trivialRowGroupIndices) { - entry = i; - ++i; - } - - // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent - // it from actually generating the entries in the entry vector. - toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - - // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert - // the resulting (DD) vector to an explicit vector. - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - // Construct matrix and return result. - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); - } - - template - void InternalAdd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, 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 (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentRowLevel + currentColumnLevel == maxLevel) { - if (generateValues) { - columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); - } - ++rowIndications[rowGroupOffsets[currentRowOffset]]; - } else { - DdNode const* elseElse; - DdNode const* elseThen; - DdNode const* thenElse; - DdNode const* thenThen; - - if (ddColumnVariableIndices[currentColumnLevel] < dd->index) { - elseElse = elseThen = thenElse = thenThen = dd; - } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) { - elseElse = thenElse = Cudd_E(dd); - elseThen = thenThen = Cudd_T(dd); - } else { - DdNode const* elseNode = Cudd_E(dd); - if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) { - elseElse = elseThen = elseNode; - } else { - elseElse = Cudd_E(elseNode); - elseThen = Cudd_T(elseNode); - } - - DdNode const* thenNode = Cudd_T(dd); - if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) { - thenElse = thenThen = thenNode; - } else { - thenElse = Cudd_E(thenNode); - thenThen = Cudd_T(thenNode); - } - } - - // Visit else-else. - toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit else-then. - toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit then-else. - toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit then-then. - toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); - } - } - - template - storm::storage::SparseMatrix InternalAdd::toMatrix(std::vector const& ddGroupVariableIndices, InternalBdd const& groupVariableCube, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const { - // Start by computing the offsets (in terms of rows) for each row group. - InternalAdd stateToNumberOfChoices = this->notZero().existsAbstract(columnVariableCube).template toAdd().sumAbstract(groupVariableCube); - std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); - rowGroupIndices.resize(rowGroupIndices.size() + 1); - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { - tmp2 = rowGroupIndices[i]; - rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowGroupIndices[0] = 0; - - // Next, we split the matrix into one for each group. This only works if the group variables are at the very - // top. - std::vector> groups; - splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); - - // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); - - // Now compute the indices at which the individual rows start. - std::vector rowIndications(rowGroupIndices.back() + 1); - - std::vector> statesWithGroupEnabled(groups.size()); - InternalAdd stateToRowGroupCount = this->getDdManager()->getAddZero(); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - - statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).toAdd(); - stateToRowGroupCount += statesWithGroupEnabled[i]; - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; - composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - tmp = 0; - tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); - } - - template - std::pair, std::vector> InternalAdd::toMatrixVector(InternalAdd const& vector, std::vector const& ddGroupVariableIndices, std::vector&& rowGroupIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const { - // Transform the row group sizes to the actual row group indices. - rowGroupIndices.resize(rowGroupIndices.size() + 1); - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { - tmp2 = rowGroupIndices[i]; - rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowGroupIndices[0] = 0; - - // Create the explicit vector we need to fill later. - std::vector explicitVector(rowGroupIndices.back()); - - // Next, we split the matrix into one for each group. This only works if the group variables are at the very top. - std::vector, InternalAdd>> groups; - splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); - - // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); - - // Now compute the indices at which the individual rows start. - std::vector rowIndications(rowGroupIndices.back() + 1); - - std::vector> statesWithGroupEnabled(groups.size()); - storm::dd::InternalAdd stateToRowGroupCount = this->getDdManager()->getAddZero(); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - std::pair, storm::dd::InternalAdd> ddPair = groups[i]; - - toMatrixRec(ddPair.first.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - toVectorRec(ddPair.second.getCuddDdNode(), explicitVector, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); - - statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).toAdd(); - stateToRowGroupCount += statesWithGroupEnabled[i]; - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; - composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - tmp = 0; - tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i].first; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); - } - - template - void InternalAdd::splitGroupsRec(DdNode* 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 == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - if (currentLevel == maxLevel) { - groups.push_back(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd))); - } else if (ddGroupVariableIndices[currentLevel] < dd->index) { - splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - } else { - splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + composeVectorsRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeVectorsRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } } + - template - void InternalAdd::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& 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 (dd1 == Cudd_ReadZero(ddManager->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { - return; - } - - if (currentLevel == maxLevel) { - groups.push_back(std::make_pair(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd1)), - InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd2)))); - } else if (ddGroupVariableIndices[currentLevel] < dd1->index) { - if (ddGroupVariableIndices[currentLevel] < dd2->index) { - splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - } else { - splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - } - } else if (ddGroupVariableIndices[currentLevel] < dd2->index) { - splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - } else { - splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); - } - } +// template +// std::vector InternalAdd::toVector(std::vector const& ddGroupVariableIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, std::vector const& groupOffsets) const { +// // Start by splitting the symbolic vector into groups. +// std::vector> groups; +// splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); +// +// // Now iterate over the groups and add them to the resulting vector. +// std::vector result(groupOffsets.back(), storm::utility::zero()); +// for (uint_fast64_t i = 0; i < groups.size(); ++i) { +// toVectorRec(groups[i].getCuddDdNode(), result, groupOffsets, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); +// } +// +// return result; +// } +// +// template +// void InternalAdd::addToExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { +// composeVector(odd, ddVariableIndices, targetVector, std::plus()); +// } +// +// template +// void InternalAdd::toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { +// // For the empty DD, we do not need to add any entries. +// if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { +// 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[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); +// } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { +// toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); +// toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); +// } else { +// toVectorRec(Cudd_E(dd), result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); +// toVectorRec(Cudd_T(dd), result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); +// } +// } +// +// template +// storm::storage::SparseMatrix InternalAdd::toMatrix(uint_fast64_t numberOfDdVariables, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) const { +// // Prepare the vectors that represent the matrix. +// std::vector rowIndications(rowOdd.getTotalOffset() + 1); +// std::vector> columnsAndValues(this->getNonZeroCount(numberOfDdVariables)); +// +// // Create a trivial row grouping. +// std::vector trivialRowGroupIndices(rowIndications.size()); +// uint_fast64_t i = 0; +// for (auto& entry : trivialRowGroupIndices) { +// entry = i; +// ++i; +// } +// +// // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent +// // it from actually generating the entries in the entry vector. +// toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); +// +// // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert +// // the resulting (DD) vector to an explicit vector. +// +// // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. +// uint_fast64_t tmp = 0; +// uint_fast64_t tmp2 = 0; +// for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { +// tmp2 = rowIndications[i]; +// rowIndications[i] = rowIndications[i - 1] + tmp; +// std::swap(tmp, tmp2); +// } +// rowIndications[0] = 0; +// +// // Now actually fill the entry vector. +// toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); +// +// // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. +// for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { +// rowIndications[i] = rowIndications[i - 1]; +// } +// rowIndications[0] = 0; +// +// // Construct matrix and return result. +// return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); +// } +// +// template +// void InternalAdd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, 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 (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { +// return; +// } +// +// // If we are at the maximal level, the value to be set is stored as a constant in the DD. +// if (currentRowLevel + currentColumnLevel == maxLevel) { +// if (generateValues) { +// columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); +// } +// ++rowIndications[rowGroupOffsets[currentRowOffset]]; +// } else { +// DdNode const* elseElse; +// DdNode const* elseThen; +// DdNode const* thenElse; +// DdNode const* thenThen; +// +// if (ddColumnVariableIndices[currentColumnLevel] < dd->index) { +// elseElse = elseThen = thenElse = thenThen = dd; +// } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) { +// elseElse = thenElse = Cudd_E(dd); +// elseThen = thenThen = Cudd_T(dd); +// } else { +// DdNode const* elseNode = Cudd_E(dd); +// if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) { +// elseElse = elseThen = elseNode; +// } else { +// elseElse = Cudd_E(elseNode); +// elseThen = Cudd_T(elseNode); +// } +// +// DdNode const* thenNode = Cudd_T(dd); +// if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) { +// thenElse = thenThen = thenNode; +// } else { +// thenElse = Cudd_E(thenNode); +// thenThen = Cudd_T(thenNode); +// } +// } +// +// // Visit else-else. +// toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); +// // Visit else-then. +// toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); +// // Visit then-else. +// toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); +// // Visit then-then. +// toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); +// } +// } +// +// template +// storm::storage::SparseMatrix InternalAdd::toMatrix(std::vector const& ddGroupVariableIndices, InternalBdd const& groupVariableCube, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const { +// // Start by computing the offsets (in terms of rows) for each row group. +// InternalAdd stateToNumberOfChoices = this->notZero().existsAbstract(columnVariableCube).template toAdd().sumAbstract(groupVariableCube); +// std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); +// rowGroupIndices.resize(rowGroupIndices.size() + 1); +// uint_fast64_t tmp = 0; +// uint_fast64_t tmp2 = 0; +// for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { +// tmp2 = rowGroupIndices[i]; +// rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; +// std::swap(tmp, tmp2); +// } +// rowGroupIndices[0] = 0; +// +// // Next, we split the matrix into one for each group. This only works if the group variables are at the very +// // top. +// std::vector> groups; +// splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); +// +// // Create the actual storage for the non-zero entries. +// std::vector> columnsAndValues(this->getNonZeroCount()); +// +// // Now compute the indices at which the individual rows start. +// std::vector rowIndications(rowGroupIndices.back() + 1); +// +// std::vector> statesWithGroupEnabled(groups.size()); +// InternalAdd stateToRowGroupCount = this->getDdManager()->getAddZero(); +// for (uint_fast64_t i = 0; i < groups.size(); ++i) { +// auto const& dd = groups[i]; +// +// toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); +// +// statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).toAdd(); +// stateToRowGroupCount += statesWithGroupEnabled[i]; +// statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); +// } +// +// // Since we modified the rowGroupIndices, we need to restore the correct values. +// std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; +// composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); +// +// // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. +// tmp = 0; +// tmp2 = 0; +// for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { +// tmp2 = rowIndications[i]; +// rowIndications[i] = rowIndications[i - 1] + tmp; +// std::swap(tmp, tmp2); +// } +// rowIndications[0] = 0; +// +// // Now actually fill the entry vector. +// for (uint_fast64_t i = 0; i < groups.size(); ++i) { +// auto const& dd = groups[i]; +// +// toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); +// +// statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); +// } +// +// // Since we modified the rowGroupIndices, we need to restore the correct values. +// composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); +// +// // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. +// for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { +// rowIndications[i] = rowIndications[i - 1]; +// } +// rowIndications[0] = 0; +// +// return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); +// } +// +// template +// std::pair, std::vector> InternalAdd::toMatrixVector(InternalAdd const& vector, std::vector const& ddGroupVariableIndices, std::vector&& rowGroupIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const { +// // Transform the row group sizes to the actual row group indices. +// rowGroupIndices.resize(rowGroupIndices.size() + 1); +// uint_fast64_t tmp = 0; +// uint_fast64_t tmp2 = 0; +// for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { +// tmp2 = rowGroupIndices[i]; +// rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; +// std::swap(tmp, tmp2); +// } +// rowGroupIndices[0] = 0; +// +// // Create the explicit vector we need to fill later. +// std::vector explicitVector(rowGroupIndices.back()); +// +// // Next, we split the matrix into one for each group. This only works if the group variables are at the very top. +// std::vector, InternalAdd>> groups; +// splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); +// +// // Create the actual storage for the non-zero entries. +// std::vector> columnsAndValues(this->getNonZeroCount()); +// +// // Now compute the indices at which the individual rows start. +// std::vector rowIndications(rowGroupIndices.back() + 1); +// +// std::vector> statesWithGroupEnabled(groups.size()); +// storm::dd::InternalAdd stateToRowGroupCount = this->getDdManager()->getAddZero(); +// for (uint_fast64_t i = 0; i < groups.size(); ++i) { +// std::pair, storm::dd::InternalAdd> ddPair = groups[i]; +// +// toMatrixRec(ddPair.first.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); +// toVectorRec(ddPair.second.getCuddDdNode(), explicitVector, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); +// +// statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).toAdd(); +// stateToRowGroupCount += statesWithGroupEnabled[i]; +// statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); +// } +// +// // Since we modified the rowGroupIndices, we need to restore the correct values. +// std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; +// composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); +// +// // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. +// tmp = 0; +// tmp2 = 0; +// for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { +// tmp2 = rowIndications[i]; +// rowIndications[i] = rowIndications[i - 1] + tmp; +// std::swap(tmp, tmp2); +// } +// rowIndications[0] = 0; +// +// // Now actually fill the entry vector. +// for (uint_fast64_t i = 0; i < groups.size(); ++i) { +// auto const& dd = groups[i].first; +// +// toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); +// +// statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); +// } +// +// // Since we modified the rowGroupIndices, we need to restore the correct values. +// composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); +// +// // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. +// for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { +// rowIndications[i] = rowIndications[i - 1]; +// } +// rowIndications[0] = 0; +// +// return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); +// } +// +// template +// void InternalAdd::splitGroupsRec(DdNode* 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 == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { +// return; +// } +// +// if (currentLevel == maxLevel) { +// groups.push_back(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd))); +// } else if (ddGroupVariableIndices[currentLevel] < dd->index) { +// splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// } else { +// splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// } +// } +// +// template +// void InternalAdd::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& 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 (dd1 == Cudd_ReadZero(ddManager->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { +// return; +// } +// +// if (currentLevel == maxLevel) { +// groups.push_back(std::make_pair(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd1)), +// InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd2)))); +// } else if (ddGroupVariableIndices[currentLevel] < dd1->index) { +// if (ddGroupVariableIndices[currentLevel] < dd2->index) { +// splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// } else { +// splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// } +// } else if (ddGroupVariableIndices[currentLevel] < dd2->index) { +// splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// } else { +// splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); +// } +// } template InternalAdd InternalAdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices) { diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index bfb9f1897..7057f4506 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -500,24 +500,25 @@ namespace storm { */ AddIterator end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables = true) const; - /*! - * Converts the ADD to a vector. The given offset-labeled DD is used to determine the correct row of - * each entry. - * - * @param rowOdd The ODD used for determining the correct row. - * @return The vector that is represented by this ADD. - */ - std::vector toVector(std::vector const& ddGroupVariableIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, std::vector const& groupOffsets) const; - - void addToExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - - void composeVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; - - storm::storage::SparseMatrix toMatrix(uint_fast64_t numberOfDdVariables, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) const; - - storm::storage::SparseMatrix toMatrix(std::vector const& ddGroupVariableIndices, InternalBdd const& groupVariableCube, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const; - - std::pair, std::vector> toMatrixVector(InternalAdd const& vector, std::vector const& ddGroupVariableIndices, std::vector&& rowGroupIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const; + void composeVectors(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + +// /*! +// * Converts the ADD to a vector. The given offset-labeled DD is used to determine the correct row of +// * each entry. +// * +// * @param rowOdd The ODD used for determining the correct row. +// * @return The vector that is represented by this ADD. +// */ +// std::vector toVector(std::vector const& ddGroupVariableIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, std::vector const& groupOffsets) const; +// +// void addToExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; +// +// +// storm::storage::SparseMatrix toMatrix(uint_fast64_t numberOfDdVariables, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) const; +// +// storm::storage::SparseMatrix toMatrix(std::vector const& ddGroupVariableIndices, InternalBdd const& groupVariableCube, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const; +// +// std::pair, std::vector> toMatrixVector(InternalAdd const& vector, std::vector const& ddGroupVariableIndices, std::vector&& rowGroupIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const; static InternalAdd fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices); @@ -548,7 +549,7 @@ namespace storm { * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. * @param targetVector The vector to which the translated DD-based vector is to be added. */ - void composeVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + void composeVectorsRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; /*! * Helper function to convert the DD into an (explicit) vector.