sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

more work on refactoring DD abstraction layer 

Former-commit-id: 83bf755a91
tempestpy_adaptions
dehnert 9 years ago
parent
d683e38d4a
commit
52062b523d
9 changed files with 155 additions and 150 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 89
      src/storage/dd/Bdd.cpp
  2. 21
      src/storage/dd/Bdd.h
  3. 22
      src/storage/dd/Dd.cpp
  4. 18
      src/storage/dd/Dd.h
  5. 20
      src/storage/dd/DdManager.cpp
  6. 10
      src/storage/dd/DdManager.h
  7. 5
      src/storage/dd/DdMetaVariable.h
  8. 59
      src/storage/dd/cudd/InternalCuddBdd.cpp
  9. 61
      src/storage/dd/cudd/InternalCuddBdd.h

89
src/storage/dd/Bdd.cpp
View File

@ -2,6 +2,8 @@
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Odd.h"
#include "src/logic/ComparisonType.h"
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/dd/DdManager.h"
@ -19,22 +21,23 @@ namespace storm {
}
template<DdType LibraryType>
Bdd<LibraryType>::Bdd(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) {
Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) {
switch (comparisonType) {
case storm::logic::ComparisonType::Less:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
break;
return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
case storm::logic::ComparisonType::LessEqual:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
break;
return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
case storm::logic::ComparisonType::Greater:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
break;
return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
case storm::logic::ComparisonType::GreaterEqual:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
break;
return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
}
}
template<DdType LibraryType>
template<typename ValueType>
Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(ddManager, values, odd, metaVariables, filter), metaVariables);
}
template<DdType LibraryType>
@ -106,64 +109,36 @@ namespace storm {
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
Bdd<LibraryType> cubeBdd = this->getDdManager()->getBddOne();
std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
for (auto const& metaVariable : metaVariables) {
// First check whether the BDD contains the meta variable and erase it, if this is the case.
STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
newMetaVariables.erase(metaVariable);
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeBdd &= ddMetaVariable.getCube();
}
return Bdd<LibraryType>(internalBdd.existsAbstract(cubeBdd));
Bdd<LibraryType> cube = this->getCube(metaVariables);
return Bdd<LibraryType>(this->getDdManager(), internalBdd.existsAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
InternalBdd<LibraryType> cubeBdd = this->getDdManager()->getBddOne();
std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
for (auto const& metaVariable : metaVariables) {
// First check whether the BDD contains the meta variable and erase it, if this is the case.
STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
newMetaVariables.erase(metaVariable);
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeBdd &= ddMetaVariable.getCube();
}
return Bdd<LibraryType>(internalBdd.universalAbstract(cubeBdd));
Bdd<LibraryType> cube = this->getCube(metaVariables);
return Bdd<LibraryType>(this->getDdManager(), internalBdd.universalAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::andExists(Bdd<LibraryType> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
InternalBdd<DdType::CUDD> cubeBdd(this->getDdManager()->getBddOne());
for (auto const& metaVariable : existentialVariables) {
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeBdd &= ddMetaVariable.getCube();
}
Bdd<DdType::CUDD> cube = this->getCube(existentialVariables);
std::set<storm::expressions::Variable> unionOfMetaVariables;
std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
std::set<storm::expressions::Variable> containedMetaVariables;
std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
return Bdd<LibraryType>(internalBdd.andExists(other.internalBdd, cubeBdd));
return Bdd<LibraryType>(this->getDdManager(), internalBdd.andExists(other, cube), containedMetaVariables);
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::constrain(Bdd<LibraryType> const& constraint) const {
this->addMetaVariables(constraint.getContainedMetaVariables());
return internalBdd.constraint(constraint.internalBdd);
return Bdd<LibraryType>(this->getDdManager(), internalBdd.constrain(constraint), Dd<LibraryType>::joinMetaVariables(*this, constraint));
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::restrict(Bdd<LibraryType> const& constraint) const {
this->addMetaVariables(constraint.getContainedMetaVariables());
return internalBdd.constraint(constraint.internalBdd);
return Bdd<LibraryType>(this->getDdManager(), internalBdd.restrict(constraint), Dd<LibraryType>::joinMetaVariables(*this, constraint));
}
template<DdType LibraryType>
@ -191,7 +166,7 @@ namespace storm {
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::getSupport() const {
return Bdd<LibraryType>(internalBdd.getSupport());
return Bdd<LibraryType>(this->getDdManager(), internalBdd.getSupport(), this->getContainedMetaVariables());
}
template<DdType LibraryType>
@ -233,6 +208,26 @@ namespace storm {
internalBdd.exportToDot(filename, this->getDdManager()->getDdVariableNames());
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::getCube(std::set<storm::expressions::Variable> const& metaVariables) const {
Bdd<LibraryType> cube = this->getDdManager()->getBddOne();
for (auto const& metaVariable : metaVariables) {
STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
cube &= this->getDdManager()->getMetaVariable(metaVariable).getCube();
}
return cube;
}
template<DdType LibraryType>
Bdd<LibraryType>::operator InternalBdd<LibraryType>() {
return internalBdd;
}
template<DdType LibraryType>
Bdd<LibraryType>::operator InternalBdd<LibraryType> const() const {
return internalBdd;
}
template class Bdd<storm::dd::DdType::CUDD>;
}
}

21
src/storage/dd/Bdd.h
View File

@ -215,7 +215,21 @@ namespace storm {
virtual void exportToDot(std::string const& filename) const override;
/*!
* Retrieves the cube of all given meta variables.
*
* @param metaVariables The variables for which to create the cube.
* @return The resulting cube.
*/
Bdd<LibraryType> getCube(std::set<storm::expressions::Variable> const& metaVariables) const;
private:
/*!
* We provide a conversion operator from the BDD to its internal type to ease calling the internal functions.
*/
operator InternalBdd<LibraryType>();
operator InternalBdd<LibraryType> const() const;
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*
@ -235,8 +249,8 @@ namespace storm {
* @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
* @param value The value to compare with.
*/
Bdd(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
static Bdd<LibraryType> fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
/*!
* Builds a BDD representing the values that make the given filter function evaluate to true.
*
@ -248,8 +262,7 @@ namespace storm {
* @return The resulting (CUDD) BDD.
*/
template<typename ValueType>
static BDD fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
static Bdd<LibraryType> fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
// The internal BDD that depends on the chosen library.
InternalBdd<LibraryType> internalBdd;

22
src/storage/dd/Dd.cpp
View File

@ -62,28 +62,20 @@ namespace storm {
template<DdType LibraryType>
std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices() const {
return getSortedVariableIndices(*this->getDdManager(), this->getContainedMetaVariables());
return this->getDdManager()->getSortedVariableIndices(this->getContainedMetaVariables());
}
template<DdType LibraryType>
std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables) {
std::vector<uint_fast64_t> ddVariableIndices;
for (auto const& metaVariableName : metaVariables) {
auto const& metaVariable = manager.getMetaVariable(metaVariableName);
for (auto const& ddVariable : metaVariable.getDdVariables()) {
ddVariableIndices.push_back(ddVariable.getIndex());
}
}
// Next, we need to sort them, since they may be arbitrarily ordered otherwise.
std::sort(ddVariableIndices.begin(), ddVariableIndices.end());
return ddVariableIndices;
std::set<storm::expressions::Variable> Dd<LibraryType>::joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
std::set<storm::expressions::Variable> metaVariables;
std::set_union(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
return metaVariables;
}
template<DdType LibraryType>
std::set<storm::expressions::Variable> Dd<LibraryType>::joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
std::set<storm::expressions::Variable> Dd<LibraryType>::subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
std::set<storm::expressions::Variable> metaVariables;
std::set_union(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
return metaVariables;
}

18
src/storage/dd/Dd.h
View File

@ -114,15 +114,6 @@ namespace storm {
*/
std::vector<uint_fast64_t> getSortedVariableIndices() const;
/*!
* Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.
*
* @param manager The manager responsible for the DD.
* @param metaVariable The set of meta variables for which to retrieve the index list.
* @return The sorted list of variable indices.
*/
static std::vector<uint_fast64_t> getSortedVariableIndices(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables);
/*!
* Adds the given set of meta variables to the DD.
*
@ -168,6 +159,15 @@ namespace storm {
*/
static std::set<storm::expressions::Variable> joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second);
/*!
* Retrieves the set of meta variables that are contained in the first but not the second DD.
*
* @param first The first DD.
* @param second The second DD.
* @return The resulting set of meta variables.
*/
static std::set<storm::expressions::Variable> subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second);
private:
// A pointer to the manager responsible for this DD.
std::shared_ptr<DdManager<LibraryType> const> ddManager;

20
src/storage/dd/DdManager.cpp
View File

@ -0,0 +1,20 @@
namespace storm {
namespace dd {
template<DdType LibraryType>
std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables) {
std::vector<uint_fast64_t> ddVariableIndices;
for (auto const& metaVariableName : metaVariables) {
auto const& metaVariable = manager.getMetaVariable(metaVariableName);
for (auto const& ddVariable : metaVariable.getDdVariables()) {
ddVariableIndices.push_back(ddVariable.getIndex());
}
}
// Next, we need to sort them, since they may be arbitrarily ordered otherwise.
std::sort(ddVariableIndices.begin(), ddVariableIndices.end());
return ddVariableIndices;
}
}
}

10
src/storage/dd/DdManager.h
View File

@ -14,6 +14,16 @@ namespace storm {
Bdd<LibraryType> getBddOne() const;
Bdd<LibraryType> getBddZero() const;
DdMetaVariable<LibraryType> const& getMetaVariable(storm::expressions::Variable const& variable) const;
std::vector<std::string> getDdVariableNames() const;
/*!
* Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.
*
* @param manager The manager responsible for the DD.
* @param metaVariable The set of meta variables for which to retrieve the index list.
* @return The sorted list of variable indices.
*/
static std::vector<uint_fast64_t> getSortedVariableIndices(std::set<storm::expressions::Variable> const& metaVariables);
};
}
}

5
src/storage/dd/DdMetaVariable.h
View File

@ -1,6 +1,8 @@
#ifndef STORM_STORAGE_DD_DDMETAVARIBLE_H_
#define STORM_STORAGE_DD_DDMETAVARIBLE_H_
#include <vector>
#include "src/storage/dd/DdType.h"
namespace storm {
@ -9,7 +11,8 @@ namespace storm {
template<DdType LibraryType>
class DdMetaVariable {
public:
InternalBdd<LibraryType> getCube() const;
Bdd<LibraryType> getCube() const;
uint_fast64_t getNumberOfDdVariables() const;
};
}
}

59
src/storage/dd/cudd/InternalCuddBdd.cpp
View File

@ -2,6 +2,17 @@
namespace storm {
namespace dd {
InternalBdd<DdType::CUDD>::InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) {
// Intentionally left empty.
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
std::vector<uint_fast64_t> ddVariableIndices = ddManager->getSortedVariableIndices(metaVariables);
uint_fast64_t offset = 0;
return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter));
}
bool InternalBdd<DdType::CUDD>::operator==(InternalBdd<DdType::CUDD> const& other) const {
return this->getCuddBdd() == other.getCuddBdd();
}
@ -11,7 +22,7 @@ namespace storm {
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::ite(InternalBdd<DdType::CUDD> const& thenDd, InternalBdd<DdType::CUDD> const& elseDd) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
return InternalBdd<DdType::CUDD>(this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()));
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator||(InternalBdd<DdType::CUDD> const& other) const {
@ -37,15 +48,15 @@ namespace storm {
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::iff(InternalBdd<DdType::CUDD> const& other) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
return InternalBdd<DdType::CUDD>(this->getCuddBdd().Xnor(other.getCuddBdd()));
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::exclusiveOr(InternalBdd<DdType::CUDD> const& other) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
return InternalBdd<DdType::CUDD>(this->getCuddBdd().Xor(other.getCuddBdd()));
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::implies(InternalBdd<DdType::CUDD> const& other) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables);
return InternalBdd<DdType::CUDD>(this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator!() const {
@ -164,15 +175,9 @@ namespace storm {
return this->getCuddBdd().getNode();
}
Add<DdType::CUDD> InternalBdd<DdType::CUDD>::toAdd() const {
return Add<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables());
template<typename ValueType>
Add<DdType::CUDD, ValueType> InternalBdd<DdType::CUDD>::toAdd() const {
return Add<DdType::CUDD, ValueType>(this->getCuddBdd().Add());
}
@ -191,12 +196,6 @@ namespace storm {
template<typename ValueType>
BDD InternalBdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
std::vector<uint_fast64_t> ddVariableIndices = getSortedVariableIndices(*ddManager, metaVariables);
uint_fast64_t offset = 0;
return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter));
}
template<typename ValueType>
DdNode* InternalBdd<DdType::CUDD>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter) {
@ -290,27 +289,5 @@ namespace storm {
}
}
InternalBdd<DdType::CUDD>::InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables), cuddBdd(cuddBdd) {
// Intentionally left empty.
}
InternalBdd<DdType::CUDD>::InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd<DdType::CUDD>(ddManager, metaVariables) {
switch (comparisonType) {
case storm::logic::ComparisonType::Less:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
break;
case storm::logic::ComparisonType::LessEqual:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
break;
case storm::logic::ComparisonType::Greater:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
break;
case storm::logic::ComparisonType::GreaterEqual:
this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
break;
}
}
}
}

61
src/storage/dd/cudd/InternalCuddBdd.h
View File

@ -1,10 +1,15 @@
#ifndef STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_
#define STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_
#include <set>
#include "src/storage/dd/DdType.h"
#include "src/storage/dd/InternalBdd.h"
#include "src/storage/dd/InternalAdd.h"
#include "src/storage/dd/DdManager.h"
#include "src/storage/dd/DdMetaVariable.h"
// Include the C++-interface of CUDD.
#include "cuddObj.hh"
@ -29,16 +34,13 @@ namespace storm {
class InternalBdd<storm::dd::DdType::CUDD> {
public:
/*!
* Constructs a BDD representation of all encodings that are in the requested relation with the given value.
* Creates a DD that encapsulates the given CUDD ADD.
*
* @param ddManager The DD manager responsible for the resulting BDD.
* @param explicitValues The explicit values to compare to the given value.
* @param odd The ODD used for the translation from the explicit representation to a symbolic one.
* @param metaVariables The meta variables to use for the symbolic encoding.
* @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
* @param value The value to compare with.
* @param ddManager The manager responsible for this DD.
* @param cuddBdd The CUDD BDD to store.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd);
// Instantiate all copy/move constructors/assignments with the default implementation.
InternalBdd() = default;
@ -47,6 +49,19 @@ namespace storm {
InternalBdd(InternalBdd<DdType::CUDD>&& other) = default;
InternalBdd& operator=(InternalBdd<DdType::CUDD>&& other) = default;
/*!
* Builds a BDD representing the values that make the given filter function evaluate to true.
*
* @param ddManager The manager responsible for the BDD.
* @param values The values that are to be checked against the filter function.
* @param odd The ODD used for the translation.
* @param metaVariables The meta variables used for the translation.
* @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
* @return The resulting BDD.
*/
template<typename ValueType>
static InternalBdd<storm::dd::DdType::CUDD> fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
/*!
* Retrieves whether the two BDDs represent the same function.
*
@ -165,7 +180,7 @@ namespace storm {
* @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another.
* @return The resulting BDD.
*/
InternalBdd<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
InternalBdd<DdType::CUDD> swapVariables(std::vector<std::pair<std::reference_wrapper<DdMetaVariable<DdType::CUDD> const>, std::reference_wrapper<DdMetaVariable<DdType::CUDD> const>>> const& fromTo) const;
/*!
* Computes the logical and of the current and the given BDD and existentially abstracts from the given set
@ -175,7 +190,7 @@ namespace storm {
* @param existentialVariables The variables from which to existentially abstract.
* @return A BDD representing the result.
*/
InternalBdd<DdType::CUDD> andExists(InternalBdd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
InternalBdd<DdType::CUDD> andExists(InternalBdd<DdType::CUDD> const& other, InternalBdd<storm::dd::DdType::CUDD> const& cube) const;
/*!
* Computes the constraint of the current BDD with the given constraint. That is, the function value of the
@ -209,7 +224,7 @@ namespace storm {
*
* @return The number of encodings that are mapped to a non-zero value.
*/
uint_fast64_t getNonZeroCount() const;
uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
/*!
* Retrieves the number of leaves of the DD.
@ -271,28 +286,6 @@ namespace storm {
storm::storage::BitVector toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const;
private:
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*
* @param ddManager The manager responsible for this DD.
* @param cuddBdd The CUDD BDD to store.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
/*!
* Builds a BDD representing the values that make the given filter function evaluate to true.
*
* @param ddManager The manager responsible for the BDD.
* @param values The values that are to be checked against the filter function.
* @param odd The ODD used for the translation.
* @param metaVariables The meta variables used for the translation.
* @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
* @return The resulting (CUDD) BDD.
*/
template<typename ValueType>
static BDD fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
/*!
* Builds a BDD representing the values that make the given filter function evaluate to true.
*
@ -337,6 +330,8 @@ namespace storm {
*/
DdNode* getCuddDdNode() const;
std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
BDD cuddBdd;
};
}

Write Preview
Loading…
Cancel
Save