diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 690299c5c..3d8225a25 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -386,238 +386,424 @@ namespace storm { std::vector Add::toVector(Odd const& rowOdd) const { std::vector result(rowOdd.getTotalOffset()); std::vector ddVariableIndices = this->getDdManager()->getSortedVariableIndices(); - addToVector(rowOdd, ddVariableIndices, result); + addToExplicitVector(rowOdd, ddVariableIndices, result); return result; } + + template + void Add::addToExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { + internalAdd.composeWithExplicitVector(odd, ddVariableIndices, targetVector, std::plus()); + } + + 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()); + } + } + + // Use the group variables to split the ADD into separate ADDs for each group. + std::vector> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices); + + // 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) { + internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, groupOffsets, result, std::plus()); + + // FIXME: something more needed? modification of groupOffsets? + } + + return result; + } + + 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()); + + // 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 toMatrix 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. + internalAdd.toMatrixComponents(trivialRowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 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. + internalAdd.toMatrixComponents(trivialRowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 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 + 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()); + + Bdd columnVariableCube = Bdd::getCube(*this->getDdManager(), columnMetaVariables); + + // Start by computing the offsets (in terms of rows) for each row group. + Add stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).template toAdd().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. Note that this only works if the group variables are + // at the very top. + std::vector> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices); + + // 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()->template getAddZero(); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i]; + + dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false); + + statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).template toAdd(); + stateToRowGroupCount += statesWithGroupEnabled[i]; + statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); + + // 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]; + + dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true); + + statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); + + // 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> 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()); + + Bdd columnVariableCube = Bdd::getCube(*this->getDdManager(), columnMetaVariables); + + // 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. Note that this only works if the group variables are at the very top. + std::vector, InternalAdd>> groups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices); + + // 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()->template getAddZero(); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + std::pair, InternalAdd> const& ddPair = groups[i]; + + ddPair.first.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false); + ddPair.second.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus()); + + statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).template toAdd(); + stateToRowGroupCount += statesWithGroupEnabled[i]; + statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); + + // 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; + + dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true); + + statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); + + // 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 -// 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.composeVectors(odd, ddVariableIndices, targetVector, fct); + 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 diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 1a67f5dce..da5cf9b5d 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -27,6 +27,9 @@ namespace storm { friend class Bdd; friend class Odd; + template + friend class Add; + // Instantiate all copy/move constructors/assignments with the default implementation. Add() = default; Add(Add const& other) = default; @@ -673,7 +676,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 addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + void addToExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; /*! * Builds an ADD representing the given vector. diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 8a7010177..611e23714 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -343,12 +343,17 @@ namespace storm { } template - 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); + void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + composeWithExplicitVectorRec(this->getCuddDdNode(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + } + + template + void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const { + composeWithExplicitVectorRec(this->getCuddDdNode(), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); } template - 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 { + void InternalAdd::composeWithExplicitVectorRec(DdNode const* dd, std::vector const* offsets, 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(ddManager->getCuddManager().getManager())) { return; @@ -356,59 +361,137 @@ namespace storm { // 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] = function(targetVector[currentOffset], Cudd_V(dd)); + ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset]; + targetValue = function(targetValue, 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. - composeVectorsRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - composeVectorsRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } else { // Otherwise, we simply recursively call the function for both (different) cases. - 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); + composeWithExplicitVectorRec(Cudd_E(dd), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeWithExplicitVectorRec(Cudd_T(dd), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } } + + template + std::vector> InternalAdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { + std::vector> result; + splitIntoGroupsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + return result; + } + + template + void InternalAdd::splitIntoGroupsRec(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(ddManager->getCuddManager().getManager())) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd))); + } else if (ddGroupVariableIndices[currentLevel] < dd->index) { + splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } else { + splitIntoGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } + + template + std::vector, InternalAdd>> InternalAdd::splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const { + std::vector, InternalAdd>> result; + splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + return result; + } + + template + void InternalAdd::splitIntoGroupsRec(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 + void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const { + return toMatrixComponentsRec(this->getCuddDdNode(), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues); + } + template + void InternalAdd::toMatrixComponentsRec(DdNode const* dd, std::vector const& rowGroupOffsets, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { + // For the empty DD, we do not need to add any entries. + if (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. + toMatrixComponentsRec(elseElse, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit else-then. + toMatrixComponentsRec(elseThen, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit then-else. + toMatrixComponentsRec(thenElse, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit then-then. + toMatrixComponentsRec(thenThen, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + } + } -// 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. @@ -454,59 +537,6 @@ namespace storm { // } // // 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); @@ -654,24 +684,6 @@ namespace storm { // } // // 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())) { diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 7057f4506..d16e4e093 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -500,25 +500,15 @@ namespace storm { */ AddIterator end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables = true) 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; + void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + + void composeWithExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function const& function) const; + + std::vector> splitIntoGroups(std::vector const& ddGroupVariableIndices) const; + + void toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const; + + std::vector, InternalAdd>> splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const; static InternalAdd fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices); @@ -549,21 +539,21 @@ 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 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; + void composeWithExplicitVectorRec(DdNode const* dd, std::vector const* offsets, 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. + * Splits the given matrix DD into the groups using the given group variables. * - * @param dd The DD to convert. - * @param result The vector that will hold the values 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 currentRowLevel The currently considered row level in the DD. + * @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 currentRowOffset The current row offset. - * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. + * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. */ - void 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; + void splitIntoGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + + void splitIntoGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; /*! * Helper function to convert the DD into a (sparse) matrix. @@ -590,33 +580,7 @@ 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, 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) const; - - /*! - * Splits the given matrix and vector DDs into the groups using the given group variables. - * - * @param dd1 The matrix DD to split. - * @param dd2 The vector DD to split. - * @param groups A vector that is to be filled with the pairs of matrix/vector 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 remainingMetaVariables1 The meta variables that remain in the matrix DD after the groups have been split. - * @param remainingMetaVariables2 The meta variables that remain in the vector DD after the groups have been split. - */ - void splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + void toMatrixComponentsRec(DdNode const* dd, std::vector const& rowGroupOffsets, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const; /*! * Builds an ADD representing the given vector.