From 2441d9b8d717d27a881b06f0a4a8f48b8777914a Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 7 Aug 2017 20:32:02 +0200 Subject: [PATCH] removed conversion operator for Bdd --- src/storm/storage/dd/Add.cpp | 30 ++++++++++++------------- src/storm/storage/dd/Bdd.cpp | 43 ++++++++++++++++-------------------- src/storm/storage/dd/Bdd.h | 5 ----- 3 files changed, 34 insertions(+), 44 deletions(-) diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 7a4956ce8..b76219624 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -154,31 +154,31 @@ namespace storm { template Add Add::sumAbstract(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); - return Add(this->getDdManager(), internalAdd.sumAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + return Add(this->getDdManager(), internalAdd.sumAbstract(cube.getInternalBdd()), Dd::subtractMetaVariables(*this, cube)); } template Add Add::minAbstract(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); - return Add(this->getDdManager(), internalAdd.minAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + return Add(this->getDdManager(), internalAdd.minAbstract(cube.getInternalBdd()), Dd::subtractMetaVariables(*this, cube)); } template Bdd Add::minAbstractRepresentative(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); - return Bdd(this->getDdManager(), internalAdd.minAbstractRepresentative(cube), this->getContainedMetaVariables()); + return Bdd(this->getDdManager(), internalAdd.minAbstractRepresentative(cube.getInternalBdd()), this->getContainedMetaVariables()); } template Add Add::maxAbstract(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); - return Add(this->getDdManager(), internalAdd.maxAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + return Add(this->getDdManager(), internalAdd.maxAbstract(cube.getInternalBdd()), Dd::subtractMetaVariables(*this, cube)); } template Bdd Add::maxAbstractRepresentative(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); - return Bdd(this->getDdManager(), internalAdd.maxAbstractRepresentative(cube), this->getContainedMetaVariables()); + return Bdd(this->getDdManager(), internalAdd.maxAbstractRepresentative(cube.getInternalBdd()), this->getContainedMetaVariables()); } template @@ -195,14 +195,14 @@ namespace storm { STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present."); DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { - fromBdds.push_back(ddVariable); + fromBdds.push_back(ddVariable.getInternalBdd()); } } for (auto const& metaVariable : to) { STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { - toBdds.push_back(ddVariable); + toBdds.push_back(ddVariable.getInternalBdd()); } } @@ -240,10 +240,10 @@ namespace storm { } } for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable); + from.push_back(ddVariable.getInternalBdd()); } for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable); + to.push_back(ddVariable.getInternalBdd()); } } @@ -272,10 +272,10 @@ namespace storm { } for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable); + from.push_back(ddVariable.getInternalBdd()); } for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable); + to.push_back(ddVariable.getInternalBdd()); } } @@ -293,7 +293,7 @@ namespace storm { std::vector> summationDdVariables; for (auto const& metaVariable : summationMetaVariables) { for (auto const& ddVariable : this->getDdManager().getMetaVariable(metaVariable).getDdVariables()) { - summationDdVariables.push_back(ddVariable); + summationDdVariables.push_back(ddVariable.getInternalBdd()); } } @@ -310,7 +310,7 @@ namespace storm { std::vector> summationDdVariables; for (auto const& metaVariable : summationMetaVariables) { for (auto const& ddVariable : this->getDdManager().getMetaVariable(metaVariable).getDdVariables()) { - summationDdVariables.push_back(ddVariable); + summationDdVariables.push_back(ddVariable.getInternalBdd()); } } @@ -318,7 +318,7 @@ namespace storm { std::set containedMetaVariables; std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - return Add(this->getDdManager(), internalAdd.multiplyMatrix(otherMatrix, summationDdVariables), containedMetaVariables); + return Add(this->getDdManager(), internalAdd.multiplyMatrix(otherMatrix.getInternalBdd(), summationDdVariables), containedMetaVariables); } template @@ -843,7 +843,7 @@ namespace storm { numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables(); } - return internalAdd.begin(this->getDdManager(), Bdd::getCube(this->getDdManager(), this->getContainedMetaVariables()), numberOfDdVariables, this->getContainedMetaVariables(), enumerateDontCareMetaVariables); + return internalAdd.begin(this->getDdManager(), Bdd::getCube(this->getDdManager(), this->getContainedMetaVariables()).getInternalBdd(), numberOfDdVariables, this->getContainedMetaVariables(), enumerateDontCareMetaVariables); } template diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 9e0b818fd..2f21a5ef4 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -141,19 +141,19 @@ namespace storm { template Bdd Bdd::existsAbstract(std::set const& metaVariables) const { Bdd cube = getCube(this->getDdManager(), metaVariables); - return Bdd(this->getDdManager(), internalBdd.existsAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + return Bdd(this->getDdManager(), internalBdd.existsAbstract(cube.getInternalBdd()), Dd::subtractMetaVariables(*this, cube)); } template Bdd Bdd::existsAbstractRepresentative(std::set const& metaVariables) const { Bdd cube = getCube(this->getDdManager(), metaVariables); - return Bdd(this->getDdManager(), internalBdd.existsAbstractRepresentative(cube), this->getContainedMetaVariables()); + return Bdd(this->getDdManager(), internalBdd.existsAbstractRepresentative(cube.getInternalBdd()), this->getContainedMetaVariables()); } template Bdd Bdd::universalAbstract(std::set const& metaVariables) const { Bdd cube = getCube(this->getDdManager(), metaVariables); - return Bdd(this->getDdManager(), internalBdd.universalAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + return Bdd(this->getDdManager(), internalBdd.universalAbstract(cube.getInternalBdd()), Dd::subtractMetaVariables(*this, cube)); } template @@ -165,17 +165,17 @@ namespace storm { std::set containedMetaVariables; std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - return Bdd(this->getDdManager(), internalBdd.andExists(other, cube), containedMetaVariables); + return Bdd(this->getDdManager(), internalBdd.andExists(other.getInternalBdd(), cube.getInternalBdd()), containedMetaVariables); } template Bdd Bdd::constrain(Bdd const& constraint) const { - return Bdd(this->getDdManager(), internalBdd.constrain(constraint), Dd::joinMetaVariables(*this, constraint)); + return Bdd(this->getDdManager(), internalBdd.constrain(constraint.getInternalBdd()), Dd::joinMetaVariables(*this, constraint)); } template Bdd Bdd::restrict(Bdd const& constraint) const { - return Bdd(this->getDdManager(), internalBdd.restrict(constraint), Dd::joinMetaVariables(*this, constraint)); + return Bdd(this->getDdManager(), internalBdd.restrict(constraint.getInternalBdd()), Dd::joinMetaVariables(*this, constraint)); } template @@ -187,7 +187,7 @@ namespace storm { for (auto const& metaVariable : rowMetaVariables) { DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { - rowVariables.push_back(ddVariable); + rowVariables.push_back(ddVariable.getInternalBdd()); } } @@ -195,11 +195,11 @@ namespace storm { for (auto const& metaVariable : columnMetaVariables) { DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { - columnVariables.push_back(ddVariable); + columnVariables.push_back(ddVariable.getInternalBdd()); } } - return Bdd(this->getDdManager(), internalBdd.relationalProduct(relation, rowVariables, columnVariables), newMetaVariables); + return Bdd(this->getDdManager(), internalBdd.relationalProduct(relation.getInternalBdd(), rowVariables, columnVariables), newMetaVariables); } template @@ -211,7 +211,7 @@ namespace storm { for (auto const& metaVariable : rowMetaVariables) { DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { - rowVariables.push_back(ddVariable); + rowVariables.push_back(ddVariable.getInternalBdd()); } } @@ -219,11 +219,11 @@ namespace storm { for (auto const& metaVariable : columnMetaVariables) { DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { - columnVariables.push_back(ddVariable); + columnVariables.push_back(ddVariable.getInternalBdd()); } } - return Bdd(this->getDdManager(), internalBdd.inverseRelationalProduct(relation, rowVariables, columnVariables), newMetaVariables); + return Bdd(this->getDdManager(), internalBdd.inverseRelationalProduct(relation.getInternalBdd(), rowVariables, columnVariables), newMetaVariables); } template @@ -235,7 +235,7 @@ namespace storm { for (auto const& metaVariable : rowMetaVariables) { DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { - rowVariables.push_back(ddVariable); + rowVariables.push_back(ddVariable.getInternalBdd()); } } @@ -243,11 +243,11 @@ namespace storm { for (auto const& metaVariable : columnMetaVariables) { DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { - columnVariables.push_back(ddVariable); + columnVariables.push_back(ddVariable.getInternalBdd()); } } - return Bdd(this->getDdManager(), internalBdd.inverseRelationalProductWithExtendedRelation(relation, rowVariables, columnVariables), newMetaVariables); + return Bdd(this->getDdManager(), internalBdd.inverseRelationalProductWithExtendedRelation(relation.getInternalBdd(), rowVariables, columnVariables), newMetaVariables); } template @@ -278,10 +278,10 @@ namespace storm { } for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable); + from.emplace_back(ddVariable.getInternalBdd()); } for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable); + to.emplace_back(ddVariable.getInternalBdd()); } } @@ -301,14 +301,14 @@ namespace storm { STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present."); DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { - fromBdds.push_back(ddVariable); + fromBdds.push_back(ddVariable.getInternalBdd()); } } for (auto const& metaVariable : to) { STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { - toBdds.push_back(ddVariable); + toBdds.push_back(ddVariable.getInternalBdd()); } } @@ -418,11 +418,6 @@ namespace storm { return result; } - template - Bdd::operator InternalBdd() const { - return internalBdd; - } - template class Bdd; template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index 4a6ae2309..b8ec614f6 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -384,11 +384,6 @@ namespace storm { friend struct FromVectorHelper; private: - /*! - * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions. - */ - operator InternalBdd() const; - // The internal BDD that depends on the chosen library. InternalBdd internalBdd; };