diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 4eb5eff5a..57cda7018 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -4,6 +4,7 @@ #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/utility/vector.h" #include "src/exceptions/InvalidArgumentException.h" @@ -433,70 +434,85 @@ namespace storm { return static_cast(this->getCuddAdd().NodeReadIndex()); } - std::vector Dd::toVector() const { - return this->toVector(Odd(*this)); + template + std::vector Dd::toVector() const { + return this->toVector(Odd(*this)); } - std::vector Dd::toVector(Odd const& odd) const { - std::vector result(odd.getTotalOffset()); + template + std::vector Dd::toVector(Odd const& rowOdd) const { + std::vector result(rowOdd.getTotalOffset()); std::vector ddVariableIndices = this->getSortedVariableIndices(); - toVectorRec(this->getCuddAdd().getNode(), result, odd, 0, ddVariableIndices.size(), 0, ddVariableIndices); + addToVectorRec(this->getCuddAdd().getNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result); return result; } - void Dd::toVectorRec(DdNode const* dd, std::vector& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector const& ddVariableIndices) const { - // For the empty DD, we do not need to add any entries. - if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentLevel == maxLevel) { - result[currentOffset] = Cudd_V(dd); - } 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. - toVectorRec(dd, result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices); - toVectorRec(dd, result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices); - } else { - // Otherwise, we simply recursively call the function for both (different) cases. - toVectorRec(Cudd_E(dd), result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices); - toVectorRec(Cudd_T(dd), result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices); - } - } - storm::storage::SparseMatrix Dd::toMatrix() const { std::set rowVariables; std::set columnVariables; - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - + for (auto const& variableName : this->getContainedMetaVariableNames()) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); if (variableName.size() > 0 && variableName.back() == '\'') { columnVariables.insert(variableName); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } } else { rowVariables.insert(variableName); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } + } + } + + return toMatrix(rowVariables, columnVariables, Odd(this->existsAbstract(rowVariables)), Odd(this->existsAbstract(columnVariables))); + } + + storm::storage::SparseMatrix Dd::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variableName : this->getContainedMetaVariableNames()) { + if (variableName.size() > 0 && variableName.back() == '\'') { + columnMetaVariables.insert(variableName); + } else { + rowMetaVariables.insert(variableName); } } - Odd columnOdd(this->existsAbstract(rowVariables)); - Odd rowOdd(this->existsAbstract(columnVariables)); + return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); + } + + storm::storage::SparseMatrix Dd::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& variableName : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + } + for (auto const& variableName : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + } // Prepare the vectors that represent the matrix. std::vector rowIndications(rowOdd.getTotalOffset() + 1); std::vector> columnsAndValues(this->getNonZeroCount()); + // 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->getCuddAdd().getNode(), rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - + toMatrixRec(this->getCuddAdd().getNode(), 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; @@ -508,7 +524,7 @@ namespace storm { rowIndications[0] = 0; // Now actually fill the entry vector. - toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + toMatrixRec(this->getCuddAdd().getNode(), 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) { @@ -516,21 +532,113 @@ namespace storm { } rowIndications[0] = 0; - // Create a trivial row grouping. - std::vector trivialRowGroupIndices(rowIndications.size()); - uint_fast64_t i = 0; - for (auto& entry : trivialRowGroupIndices) { - entry = i; - ++i; - } - // Construct matrix and return result. return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); } - void Dd::toMatrixRec(DdNode const* dd, 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 { - // FIXME: this method currently assumes a strict interleaved order, which does not seem necessary. + storm::storage::SparseMatrix Dd::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& variableName : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variableName); + } + for (auto const& variableName : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variableName); + } + for (auto const& variableName : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // TODO: assert that the group variables are at the very top of the variable ordering? + + // Start by computing the offsets (in terms of rows) for each row group. + Dd stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).sumAbstract(groupMetaVariables); + 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->getCuddAdd().getNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); + + // 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()); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i]; + + toMatrixRec(dd.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + + statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables); + addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { + rowGroupIndices[i] = rowGroupIndices[i - 1]; + } + rowGroupIndices[0] = 0; + + // 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.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { + rowGroupIndices[i] = rowGroupIndices[i - 1]; + } + rowGroupIndices[0] = 0; + + // 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)); + } + + void Dd::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 == this->getDdManager()->getZero().getCuddAdd().getNode()) { return; @@ -539,9 +647,9 @@ namespace storm { // 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[currentRowOffset]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); + columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); } - ++rowIndications[currentRowOffset]; + ++rowIndications[rowGroupOffsets[currentRowOffset]]; } else { DdNode const* elseElse; DdNode const* elseThen; @@ -572,13 +680,52 @@ namespace storm { } // Visit else-else. - toMatrixRec(elseElse, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + 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, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + 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, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + 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, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + } + } + + void Dd::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { + // For the empty DD, we do not need to create a group. + if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(Dd(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd), remainingMetaVariables)); + } else if (ddGroupVariableIndices[currentLevel] < dd->index) { + splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + } else { + splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + } + } + + template + void Dd::addToVectorRec(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) const { + // For the empty DD, we do not need to add any entries. + if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentLevel == maxLevel) { + targetVector[currentOffset] += static_cast(Cudd_V(dd)); + } 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. + addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); + addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); + } else { + // Otherwise, we simply recursively call the function for both (different) cases. + addToVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); + addToVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); } } @@ -733,6 +880,13 @@ namespace storm { dd.exportToDot(); return out; } - + + // Explicitly instantiate some templated functions. + template std::vector Dd::toVector() const; + template std::vector Dd::toVector(Odd const& rowOdd) const; + template void Dd::addToVectorRec(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) const; + template std::vector Dd::toVector() const; + template std::vector Dd::toVector(Odd const& rowOdd) const; + template void Dd::addToVectorRec(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) const; } } \ No newline at end of file diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 045f547a0..316e30c89 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -458,25 +458,67 @@ namespace storm { uint_fast64_t getIndex() const; /*! - * Converts the DD to a double vector. + * Converts the DD to a vector. * * @return The double vector that is represented by this DD. */ - std::vector toVector() const; + template + std::vector toVector() const; + + /*! + * Converts the DD 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 double vector that is represented by this DD. + */ + template + std::vector toVector(storm::dd::Odd const& rowOdd) const; /*! * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the * row, whereas all primed variables are assumed to encode the column. + * + * @return The matrix that is represented by this DD. */ storm::storage::SparseMatrix toMatrix() const; + + /*! + * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the + * row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used + * to determine the correct row and column, respectively, for each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this DD. + */ + storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the DD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the + * correct row and column, respectively, for each entry. + * + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this DD. + */ + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! - * Converts the DD to a double vector using the given ODD (that needs to be constructed for the DD). + * Converts the DD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to + * determine the correct row and column, respectively, for each entry. Note: this function assumes that + * the meta variables used to distinguish different row groups are at the very top of the DD. * - * @param odd The ODD for the DD. - * @return The double vector that is represented by this DD. + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this DD. */ - std::vector toVector(Odd const& odd) const; + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! * Retrieves whether the given meta variable is contained in the DD. @@ -618,20 +660,6 @@ namespace storm { */ Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames = std::set()); - /*! - * Helper function to convert the DD into a double vector. - * - * @param dd The DD to convert. - * @param result The resulting vector whose entries are to be set appropriately. This vector needs to be - * preallocated. - * @param odd The ODD used for the translation. - * @param currentLevel The currently considered level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param currentOffset The current offset. - * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. - */ - void toVectorRec(DdNode const* dd, std::vector& result, Odd const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector const& ddVariableIndices) const; - /*! * Helper function to convert the DD into a (sparse) matrix. * @@ -643,6 +671,7 @@ namespace storm { * need to be restored afterwards. * @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful * completion. + * @param rowGroupOffsets The row offsets at which a given row group starts. * @param rowOdd The ODD used for the row translation. * @param columnOdd The ODD used for the column translation. * @param currentRowLevel The currently considered row level in the DD. @@ -656,7 +685,33 @@ namespace storm { * only works if the offsets given in rowIndications are already correct. If they need to be computed first, * this flag needs to be false. */ - void toMatrixRec(DdNode const* dd, 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 = true) const; + void 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 = true) const; + + /*! + * Splits the given matrix DD into the groups using the given group variables. + * + * @param dd The DD to split. + * @param groups A vector that is to be filled with the DDs for the individual groups. + * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. + */ + void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; + + /*! + * Performs a recursive step to add the given DD-based vector to the given explicit vector. + * + * @param dd The DD to add to the explicit vector. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentOffset The current offset. + * @param odd The ODD used for the translation. + * @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. + */ + template + void addToVectorRec(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) const; /*! * Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support, diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 98a528b3d..e95348625 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -380,6 +380,7 @@ TEST(CuddDd, ToExpressionTest) { TEST(CuddDd, OddTest) { std::shared_ptr> manager(new storm::dd::DdManager()); + manager->addMetaVariable("a"); manager->addMetaVariable("x", 1, 9); storm::dd::Dd dd = manager->getIdentity("x"); @@ -389,17 +390,34 @@ TEST(CuddDd, OddTest) { EXPECT_EQ(12, odd.getNodeCount()); std::vector ddAsVector; - ASSERT_NO_THROW(ddAsVector = dd.toVector()); + ASSERT_NO_THROW(ddAsVector = dd.toVector()); EXPECT_EQ(9, ddAsVector.size()); for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { EXPECT_TRUE(i+1 == ddAsVector[i]); } + // Create a non-trivial matrix. dd = manager->getIdentity("x").equals(manager->getIdentity("x'")) * manager->getRange("x"); dd += manager->getEncoding("x", 1) * manager->getRange("x'") + manager->getEncoding("x'", 1) * manager->getRange("x"); + + // Create the ODDs. + storm::dd::Odd rowOdd; + ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange("x"))); + storm::dd::Odd columnOdd; + ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange("x'"))); + + // Try to translate the matrix. storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix = dd.toMatrix()); + ASSERT_NO_THROW(matrix = dd.toMatrix({"x"}, {"x'"}, rowOdd, columnOdd)); + EXPECT_EQ(9, matrix.getRowCount()); EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(25, matrix.getNonzeroEntryCount()); + + dd = manager->getRange("x") * manager->getRange("x'") * manager->getEncoding("a", 0).ite(dd, dd + manager->getConstant(1)); + ASSERT_NO_THROW(matrix = dd.toMatrix({"x"}, {"x'"}, {"a"}, rowOdd, columnOdd)); + EXPECT_EQ(18, matrix.getRowCount()); + EXPECT_EQ(9, matrix.getRowGroupCount()); + EXPECT_EQ(9, matrix.getColumnCount()); + EXPECT_EQ(106, matrix.getNonzeroEntryCount()); } \ No newline at end of file