From f7c26fd4b1a3eb8b66a01465f9e974418da8faa3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 17 Nov 2015 17:09:11 +0100 Subject: [PATCH] more modifications needed for refactoring of DD stuff Former-commit-id: b7b7f522319f81986f80965b9effc3a0e5595612 --- src/storage/dd/Add.cpp | 9 ++++- src/storage/dd/Add.h | 4 +- src/storage/dd/AddIterator.h | 2 +- src/storage/dd/Bdd.cpp | 11 ++---- src/storage/dd/Bdd.h | 3 +- src/storage/dd/Dd.h | 11 +++++- src/storage/dd/DdManager.cpp | 8 ++-- src/storage/dd/DdManager.h | 6 +++ src/storage/dd/DdMetaVariable.h | 8 +++- src/storage/dd/cudd/CuddAddIterator.cpp | 14 +++---- src/storage/dd/cudd/CuddAddIterator.h | 4 +- src/storage/dd/cudd/CuddOdd.cpp | 8 ++-- src/storage/dd/cudd/InternalCuddAdd.cpp | 44 +++++++++++---------- src/storage/dd/cudd/InternalCuddAdd.h | 9 +++-- src/storage/dd/cudd/InternalCuddBdd.cpp | 8 ++-- src/storage/dd/cudd/InternalCuddBdd.h | 2 +- src/storage/dd/cudd/InternalCuddDdManager.h | 4 ++ 17 files changed, 93 insertions(+), 62 deletions(-) diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index a8fc25f56..67297f627 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -595,12 +595,12 @@ namespace storm { template AddIterator Add::begin(bool enumerateDontCareMetaVariables) const { - return internalAdd.begin(this->getContainedMetaVariables(), enumerateDontCareMetaVariables); + return internalAdd.begin(this->getDdManager(), this->getContainedMetaVariables(), enumerateDontCareMetaVariables); } template AddIterator Add::end(bool enumerateDontCareMetaVariables) const { - return internalAdd.end(enumerateDontCareMetaVariables); + return internalAdd.end(this->getDdManager(), enumerateDontCareMetaVariables); } template @@ -630,6 +630,11 @@ namespace storm { return Bdd(this->getDdManager(), internalAdd.toBdd(), this->getContainedMetaVariables()); } + template + Add::operator InternalAdd() const { + return internalAdd; + } + template class Add; } } \ No newline at end of file diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index c42a0fb4c..1a67f5dce 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -25,6 +25,7 @@ namespace storm { public: friend class DdManager; friend class Bdd; + friend class Odd; // Instantiate all copy/move constructors/assignments with the default implementation. Add() = default; @@ -629,8 +630,7 @@ namespace storm { /*! * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions. */ - operator InternalAdd(); - operator InternalAdd const() const; + operator InternalAdd() const; /*! * Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also diff --git a/src/storage/dd/AddIterator.h b/src/storage/dd/AddIterator.h index 17186a874..ebcb40910 100644 --- a/src/storage/dd/AddIterator.h +++ b/src/storage/dd/AddIterator.h @@ -7,7 +7,7 @@ namespace storm { namespace dd { // Declare DdIterator class so we can then specialize it for the different DD types. template - class DdForwardIterator; + class AddIterator; } } diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 7f9f5830c..08c47a82f 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -37,7 +37,7 @@ namespace storm { template template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { - return Bdd(ddManager, InternalBdd::fromVector(ddManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables); + return Bdd(ddManager, InternalBdd::fromVector(&ddManager->internalDdManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables); } template @@ -176,7 +176,7 @@ namespace storm { template storm::storage::BitVector Bdd::toVector(storm::dd::Odd const& rowOdd) const { - return internalBdd.toVector(rowOdd); + return internalBdd.toVector(rowOdd, this->getDdManager()->getSortedVariableIndices()); } template @@ -233,12 +233,7 @@ namespace storm { } template - Bdd::operator InternalBdd() { - return internalBdd; - } - - template - Bdd::operator InternalBdd const() const { + Bdd::operator InternalBdd() const { return internalBdd; } diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index 17671f2ed..5f672453d 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -241,8 +241,7 @@ namespace storm { /*! * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions. */ - operator InternalBdd(); - operator InternalBdd const() const; + operator InternalBdd() const; /*! * Creates a DD that encapsulates the given CUDD ADD. diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h index be3181f3c..e347f1021 100644 --- a/src/storage/dd/Dd.h +++ b/src/storage/dd/Dd.h @@ -11,14 +11,21 @@ namespace storm { namespace dd { // Forward-declare some classes. - template class DdManager; - template class Bdd; + template + class DdManager; + + template + class Bdd; + + template + class Odd; template class Dd { public: // Declare the DdManager so it can access the internals of a DD. friend class DdManager; + friend class Odd; // Instantiate all copy/move constructors/assignments with the default implementation. Dd() = default; diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 28b57a866..95226f8aa 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -118,8 +118,8 @@ namespace storm { variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {unprimed})); } - metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables, this->shared_from_this())); - metaVariableMap.emplace(primed, DdMetaVariable(name + "'", low, high, variablesPrime, this->shared_from_this())); + metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables)); + metaVariableMap.emplace(primed, DdMetaVariable(name + "'", low, high, variablesPrime)); return std::make_pair(unprimed, primed); } @@ -141,8 +141,8 @@ namespace storm { variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); - metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables, this->shared_from_this())); - metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime, this->shared_from_this())); + metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables)); + metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime)); return std::make_pair(unprimed, primed); } diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index 6d7dcc5be..d4f23fdfd 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -8,6 +8,7 @@ #include "src/storage/dd/DdMetaVariable.h" #include "src/storage/dd/Bdd.h" #include "src/storage/dd/Add.h" +#include "src/storage/dd/AddIterator.h" #include "src/storage/expressions/Variable.h" @@ -15,12 +16,17 @@ namespace storm { namespace dd { + template + class Odd; + // Declare DdManager class so we can then specialize it for the different DD types. template class DdManager : public std::enable_shared_from_this> { public: friend class Bdd; friend class Add; + friend class AddIterator; + friend class Odd; /*! * Creates an empty manager without any meta variables. diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 2e92c34c7..c9f426f38 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -5,6 +5,7 @@ #include "src/storage/dd/DdType.h" #include "src/storage/dd/Bdd.h" +#include "src/storage/dd/AddIterator.h" namespace storm { namespace dd { @@ -23,7 +24,12 @@ namespace storm { public: friend class DdManager; friend class Bdd; - friend class Add; + + template + friend class Add; + + template + friend class AddIterator; /*! * Retrieves the name of the meta variable. diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp index e19d9396e..070a3982d 100644 --- a/src/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storage/dd/cudd/CuddAddIterator.cpp @@ -1,5 +1,5 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" -#include "src/storage/dd/cudd/CuddDdManager.h" +#include "src/storage/dd/DdManager.h" #include "src/storage/dd/DdMetaVariable.h" #include "src/utility/macros.h" #include "src/storage/expressions/ExpressionManager.h" @@ -7,12 +7,12 @@ namespace storm { namespace dd { template - AddIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + AddIterator::AddIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { // Intentionally left empty. } template - AddIterator::DdForwardIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { + AddIterator::AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { // If the given generator is not yet at its end, we need to create the current valuation from the cube from // scratch. if (!this->isAtEnd) { @@ -22,7 +22,7 @@ namespace storm { } template - AddIterator::DdForwardIterator(AddIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { + AddIterator::AddIterator(AddIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { // Null-out the pointers of which we took possession. other.cube = nullptr; other.generator = nullptr; @@ -49,7 +49,7 @@ namespace storm { } template - AddIterator::~DdForwardIterator() { + AddIterator::~AddIterator() { // We free the pointers sind Cudd allocates them using malloc rather than new/delete. if (this->cube != nullptr) { free(this->cube); @@ -89,7 +89,7 @@ namespace storm { for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) { auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<0>(this->relevantDontCareDdVariables[index])); - if (ddMetaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + if (ddMetaVariable.getType() == MetaVariableType::Bool) { if ((this->cubeCounter & (1ull << index)) != 0) { currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), true); } else { @@ -117,7 +117,7 @@ namespace storm { bool metaVariableAppearsInCube = false; std::vector> localRelenvantDontCareDdVariables; auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable); - if (ddMetaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + if (ddMetaVariable.getType() == MetaVariableType::Bool) { if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 0) { metaVariableAppearsInCube = true; currentValuation.setBooleanValue(metaVariable, false); diff --git a/src/storage/dd/cudd/CuddAddIterator.h b/src/storage/dd/cudd/CuddAddIterator.h index 262667195..577c1695f 100644 --- a/src/storage/dd/cudd/CuddAddIterator.h +++ b/src/storage/dd/cudd/CuddAddIterator.h @@ -20,12 +20,12 @@ namespace storm { class DdManager; template - class Add; + class InternalAdd; template class AddIterator { public: - friend class Add; + friend class InternalAdd; // Default-instantiate the constructor. AddIterator(); diff --git a/src/storage/dd/cudd/CuddOdd.cpp b/src/storage/dd/cudd/CuddOdd.cpp index fe38a2c48..0e238e1ff 100644 --- a/src/storage/dd/cudd/CuddOdd.cpp +++ b/src/storage/dd/cudd/CuddOdd.cpp @@ -8,8 +8,8 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/utility/macros.h" -#include "src/storage/dd/cudd/CuddDdManager.h" -#include "src/storage/dd/cudd/CuddDdMetaVariable.h" +#include "src/storage/dd/DdManager.h" +#include "src/storage/dd/DdMetaVariable.h" namespace storm { namespace dd { @@ -23,7 +23,7 @@ namespace storm { std::vector>>> uniqueTableForLevels(ddVariableIndices.size() + 1); // Now construct the ODD structure from the ADD. - std::shared_ptr> rootOdd = buildOddFromAddRec(add.getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> rootOdd = buildOddFromAddRec(add.internalAdd.getCuddDdNode(), manager->internalDdManager.getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Finally, move the children of the root ODD into this ODD. this->elseNode = std::move(rootOdd->elseNode); @@ -42,7 +42,7 @@ namespace storm { std::vector, std::shared_ptr>, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1); // Now construct the ODD structure from the BDD. - std::shared_ptr> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->internalDdManager.getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Finally, move the children of the root ODD into this ODD. this->elseNode = std::move(rootOdd->elseNode); diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 9b19ce73f..0b9d0f6dd 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -39,6 +39,7 @@ namespace storm { template InternalAdd& InternalAdd::operator|=(InternalAdd const& other) { this->cuddAdd = this->getCuddAdd() | other.getCuddAdd(); + return *this; } template @@ -49,6 +50,7 @@ namespace storm { template InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { this->cuddAdd = this->getCuddAdd() + other.getCuddAdd(); + return *this; } template @@ -59,6 +61,7 @@ namespace storm { template InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { this->cuddAdd = this->getCuddAdd() * other.getCuddAdd(); + return *this; } template @@ -69,16 +72,18 @@ namespace storm { template InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { this->cuddAdd = this->getCuddAdd() - other.getCuddAdd(); + return *this; } template InternalAdd InternalAdd::operator/(InternalAdd const& other) const { - return InternalAdd(ddManager, this->getCuddAdd() / other.getCuddAdd()); + return InternalAdd(ddManager, this->getCuddAdd().Divide(other.getCuddAdd())); } template InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { - this->cuddAdd = this->getCuddAdd() / other.getCuddAdd(); + this->cuddAdd = this->getCuddAdd().Divide(other.getCuddAdd()); + return *this; } template @@ -148,17 +153,17 @@ namespace storm { template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { - return InternalAdd(ddManager, this->getCuddAdd().ExistAbstract(cube.getCuddBdd())); + return InternalAdd(ddManager, this->getCuddAdd().ExistAbstract(cube.toAdd().getCuddAdd())); } template InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { - return InternalAdd(ddManager, this->getCuddAdd().MinAbstract(cube.getCuddBdd())); + return InternalAdd(ddManager, this->getCuddAdd().MinAbstract(cube.toAdd().getCuddAdd())); } template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { - return InternalAdd(ddManager, this->getCuddAdd().MaxAbstract(cube.getCuddBdd())); + return InternalAdd(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd().getCuddAdd())); } template @@ -178,7 +183,7 @@ namespace storm { fromAdd.push_back(it1->getCuddAdd()); toAdd.push_back(it2->getCuddAdd()); } - return InternalBdd(ddManager, this->getCuddBdd().SwapVariables(fromAdd, toAdd)); + return InternalAdd(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); } template @@ -186,7 +191,7 @@ namespace storm { // Create the CUDD summation variables. std::vector summationAdds; for (auto const& ddVariable : summationDdVariables) { - summationAdds.push_back(ddVariable.toAdd().getCuddAdd()); + summationAdds.push_back(ddVariable.getCuddAdd()); } return InternalAdd(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds)); @@ -302,7 +307,7 @@ namespace storm { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); std::vector cuddAddVector = { this->getCuddAdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); + ddManager->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); // Finally, delete the names. @@ -315,16 +320,16 @@ namespace storm { } template - AddIterator InternalAdd::begin(std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + AddIterator InternalAdd::begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { int* cube; double value; DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); - return AddIterator(ddManager, generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &metaVariables, enumerateDontCareMetaVariables); + return AddIterator(fullDdManager, generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &metaVariables, enumerateDontCareMetaVariables); } template - AddIterator InternalAdd::end(bool enumerateDontCareMetaVariables) const { - return AddIterator(ddManager, nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); + AddIterator InternalAdd::end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables) const { + return AddIterator(fullDdManager, nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); } template @@ -404,10 +409,10 @@ namespace storm { } template - storm::storage::SparseMatrix InternalAdd::toMatrix(storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) const { + 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()); + std::vector> columnsAndValues(this->getNonZeroCount(numberOfDdVariables)); // Create a trivial row grouping. std::vector trivialRowGroupIndices(rowIndications.size()); @@ -450,7 +455,7 @@ 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(this->getDdManager()->getCuddManager().getManager())) { + if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { return; } @@ -503,10 +508,9 @@ namespace storm { 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).toAdd().sumAbstract(groupVariableCube); - std::vector rowGroupIndicesAsValueType = stateToNumberOfChoices.toVector(rowOdd); - std::vector rowGroupIndices(rowGroupIndicesAsValueType.size() + 1); - std::transform(rowGroupIndicesAsValueType.begin(), rowGroupIndicesAsValueType.end(), rowGroupIndices.begin(), [] (ValueType const& value) { return static_cast(value); }); + 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) { @@ -540,7 +544,7 @@ namespace storm { } // 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); }; + 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. diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 8b0fd3dbe..bfb9f1897 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -23,6 +23,9 @@ namespace storm { } namespace dd { + template + class DdManager; + template class InternalDdManager; @@ -486,7 +489,7 @@ namespace storm { * if a meta variable does not at all influence the the function value. * @return An iterator that points to the first meta variable assignment with a non-zero function value. */ - AddIterator begin(std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; + AddIterator begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; /*! * Retrieves an iterator that points past the end of the container. @@ -495,7 +498,7 @@ namespace storm { * if a meta variable does not at all influence the the function value. * @return An iterator that points past the end of the container. */ - AddIterator end(bool enumerateDontCareMetaVariables = true) const; + 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 @@ -510,7 +513,7 @@ namespace storm { void composeVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; - storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) 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; diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 9320ef406..8e53d9573 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -1,6 +1,9 @@ #include "src/storage/dd/cudd/InternalCuddBdd.h" #include "src/storage/dd/cudd/InternalCuddDdManager.h" +#include "src/storage/dd/cudd/CuddOdd.h" + +#include "src/storage/BitVector.h" namespace storm { namespace dd { @@ -228,10 +231,9 @@ namespace storm { } } - storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd) const { - std::vector ddVariableIndices = this->getSortedVariableIndices(); + storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const { storm::storage::BitVector result(rowOdd.getTotalOffset()); - this->toVectorRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices); + this->toVectorRec(this->getCuddDdNode(), ddManager->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices); return result; } diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index b627e7912..1fa776c3f 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -288,7 +288,7 @@ namespace storm { * @param rowOdd The ODD used for determining the correct row. * @return The bit vector that is represented by this BDD. */ - storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd) const; + storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const; private: /*! diff --git a/src/storage/dd/cudd/InternalCuddDdManager.h b/src/storage/dd/cudd/InternalCuddDdManager.h index a83b03bc2..a967ca0dd 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.h +++ b/src/storage/dd/cudd/InternalCuddDdManager.h @@ -16,12 +16,16 @@ namespace storm { template class InternalBdd; + + template + class Odd; template<> class InternalDdManager { public: friend class InternalAdd; friend class InternalBdd; + friend class Odd; /*! * Creates a new internal manager for CUDD DDs.