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

started refactoring DD-interface a bit in an attempt to ease the integration of sylvan 

Former-commit-id: 3a90e171b8
main
dehnert 9 years ago
parent
4e86ef2e47
commit
d683e38d4a
19 changed files with 1184 additions and 722 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. 8
      src/storage/dd/Add.cpp
  2. 6
      src/storage/dd/Add.h
  3. 238
      src/storage/dd/Bdd.cpp
  4. 250
      src/storage/dd/Bdd.h
  5. 92
      src/storage/dd/Dd.cpp
  6. 172
      src/storage/dd/Dd.h
  7. 0
      src/storage/dd/DdManager.cpp
  8. 10
      src/storage/dd/DdManager.h
  9. 6
      src/storage/dd/DdMetaVariable.h
  10. 3
      src/storage/dd/DdType.h
  11. 14
      src/storage/dd/InternalAdd.h
  12. 14
      src/storage/dd/InternalBdd.h
  13. 0
      src/storage/dd/Odd.cpp
  14. 6
      src/storage/dd/Odd.h
  15. 384
      src/storage/dd/cudd/CuddBdd.cpp
  16. 70
      src/storage/dd/cudd/CuddDd.cpp
  17. 182
      src/storage/dd/cudd/CuddDd.h
  18. 316
      src/storage/dd/cudd/InternalCuddBdd.cpp
  19. 135
      src/storage/dd/cudd/InternalCuddBdd.h

8
src/storage/dd/Add.cpp
View File

@ -0,0 +1,8 @@
#include "src/storage/dd/Add.h"
namespace storm {
namespace dd {
template class Add<storm::dd::DdType::CUDD, double>;
}
}

6
src/storage/dd/Add.h
View File

@ -6,8 +6,10 @@
namespace storm {
namespace dd {
// Declare Add class so we can then specialize it for the different ADD types.
template<DdType Type> class Add;
template<DdType Type, typename ValueType>
class Add {
};
}
}

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

@ -0,0 +1,238 @@
#include "src/storage/dd/Bdd.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Odd.h"
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/dd/DdManager.h"
#include "src/storage/BitVector.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace dd {
template<DdType LibraryType>
Bdd<LibraryType>::Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, InternalBdd<LibraryType> const& internalBdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<LibraryType>(ddManager, containedMetaVariables), internalBdd(internalBdd) {
// Intentionally left empty.
}
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) {
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;
}
}
template<DdType LibraryType>
bool Bdd<LibraryType>::operator==(Bdd<LibraryType> const& other) const {
return internalBdd == other.internalBdd;
}
template<DdType LibraryType>
bool Bdd<LibraryType>::operator!=(Bdd<LibraryType> const& other) const {
return internalBdd != other.internalBdd;
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::ite(Bdd<LibraryType> const& thenBdd, Bdd<LibraryType> const& elseBdd) const {
std::set<storm::expressions::Variable> metaVariables = Dd<LibraryType>::joinMetaVariables(*this, thenBdd);
metaVariables.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end());
return Bdd<LibraryType>(this->getDdManager(), internalBdd.ite(thenBdd.internalBdd, elseBdd.internalBdd), metaVariables);
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::operator||(Bdd<LibraryType> const& other) const {
return Bdd<LibraryType>(this->getDdManager(), internalBdd || other.internalBdd, Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType>
Bdd<LibraryType>& Bdd<LibraryType>::operator|=(Bdd<LibraryType> const& other) {
this->addMetaVariables(other.getContainedMetaVariables());
internalBdd |= other.internalBdd;
return *this;
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::operator&&(Bdd<LibraryType> const& other) const {
return Bdd<LibraryType>(this->getDdManager(), internalBdd && other.internalBdd, Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType>
Bdd<LibraryType>& Bdd<LibraryType>::operator&=(Bdd<LibraryType> const& other) {
this->addMetaVariables(other.getContainedMetaVariables());
internalBdd &= other.internalBdd;
return *this;
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::iff(Bdd<LibraryType> const& other) const {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.iff(other.internalBdd), Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::exclusiveOr(Bdd<LibraryType> const& other) const {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.exclusiveOr(other.internalBdd), Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::implies(Bdd<LibraryType> const& other) const {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.implies(other.internalBdd), Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::operator!() const {
return Bdd<LibraryType>(this->getDdManager(), !internalBdd, this->getContainedMetaVariables());
}
template<DdType LibraryType>
Bdd<LibraryType>& Bdd<LibraryType>::complement() {
internalBdd.complement();
return *this;
}
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));
}
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));
}
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();
}
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));
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::constrain(Bdd<LibraryType> const& constraint) const {
this->addMetaVariables(constraint.getContainedMetaVariables());
return internalBdd.constraint(constraint.internalBdd);
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::restrict(Bdd<LibraryType> const& constraint) const {
this->addMetaVariables(constraint.getContainedMetaVariables());
return internalBdd.constraint(constraint.internalBdd);
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
std::set<storm::expressions::Variable> newContainedMetaVariables;
std::vector<std::pair<std::reference_wrapper<DdMetaVariable<LibraryType> const>, std::reference_wrapper<DdMetaVariable<LibraryType> const>>> fromTo;
for (auto const& metaVariablePair : metaVariablePairs) {
std::reference_wrapper<DdMetaVariable<LibraryType> const> variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
std::reference_wrapper<DdMetaVariable<LibraryType> const> variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
fromTo.push_back(std::make_pair(variable1, variable2));
}
return Bdd<LibraryType>(internalBdd.swapVariables(fromTo));
}
template<DdType LibraryType>
template<typename ValueType>
Add<LibraryType, ValueType> Bdd<LibraryType>::toAdd() const {
return Add<LibraryType, ValueType>(internalBdd.template toAdd<ValueType>());
}
template<DdType LibraryType>
storm::storage::BitVector Bdd<LibraryType>::toVector(storm::dd::Odd<LibraryType> const& rowOdd) const {
return internalBdd.toVector(rowOdd);
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::getSupport() const {
return Bdd<LibraryType>(internalBdd.getSupport());
}
template<DdType LibraryType>
uint_fast64_t Bdd<LibraryType>::getNonZeroCount() const {
std::size_t numberOfDdVariables = 0;
for (auto const& metaVariable : this->getContainedMetaVariables()) {
numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables();
}
return internalBdd.getNonZeroCount(numberOfDdVariables);
}
template<DdType LibraryType>
uint_fast64_t Bdd<LibraryType>::getLeafCount() const {
return internalBdd.getLeafCount();
}
template<DdType LibraryType>
uint_fast64_t Bdd<LibraryType>::getNodeCount() const {
return internalBdd.getNodeCount();
}
template<DdType LibraryType>
uint_fast64_t Bdd<LibraryType>::getIndex() const {
return internalBdd.getIndex();
}
template<DdType LibraryType>
bool Bdd<LibraryType>::isOne() const {
return internalBdd.isOne();
}
template<DdType LibraryType>
bool Bdd<LibraryType>::isZero() const {
return internalBdd.isZero();
}
template<DdType LibraryType>
void Bdd<LibraryType>::exportToDot(std::string const& filename) const {
internalBdd.exportToDot(filename, this->getDdManager()->getDdVariableNames());
}
template class Bdd<storm::dd::DdType::CUDD>;
}
}

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

@ -4,10 +4,256 @@
#include "src/storage/dd/Dd.h"
#include "src/storage/dd/DdType.h"
#include "src/storage/dd/cudd/InternalCuddBdd.h"
namespace storm {
namespace dd {
// Declare Bdd class so we can then specialize it for the different BDD types.
template<DdType Type> class Bdd;
template<DdType LibraryType, typename ValueType>
class Add;
template<DdType LibraryType>
class Bdd : public Dd<LibraryType> {
public:
// Instantiate all copy/move constructors/assignments with the default implementation.
Bdd() = default;
Bdd(Bdd<LibraryType> const& other) = default;
Bdd& operator=(Bdd<LibraryType> const& other) = default;
Bdd(Bdd<LibraryType>&& other) = default;
Bdd& operator=(Bdd<LibraryType>&& other) = default;
/*!
* Retrieves whether the two BDDs represent the same function.
*
* @param other The BDD that is to be compared with the current one.
* @return True if the BDDs represent the same function.
*/
bool operator==(Bdd<LibraryType> const& other) const;
/*!
* Retrieves whether the two BDDs represent different functions.
*
* @param other The BDD that is to be compared with the current one.
* @return True if the BDDs represent the different functions.
*/
bool operator!=(Bdd<LibraryType> const& other) const;
/*!
* Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero
* function value to the function values specified by the first DD and all others to the function values
* specified by the second DD.
*
* @param thenBdd The BDD defining the 'then' part.
* @param elseBdd The BDD defining the 'else' part.
* @return The resulting BDD.
*/
Bdd<LibraryType> ite(Bdd<LibraryType> const& thenBdd, Bdd<LibraryType> const& elseBdd) const;
/*!
* Performs a logical or of the current and the given BDD.
*
* @param other The second BDD used for the operation.
* @return The logical or of the operands.
*/
Bdd<LibraryType> operator||(Bdd<LibraryType> const& other) const;
/*!
* Performs a logical or of the current and the given BDD and assigns it to the current BDD.
*
* @param other The second BDD used for the operation.
* @return A reference to the current BDD after the operation
*/
Bdd<LibraryType>& operator|=(Bdd<LibraryType> const& other);
/*!
* Performs a logical and of the current and the given BDD.
*
* @param other The second BDD used for the operation.
* @return The logical and of the operands.
*/
Bdd<LibraryType> operator&&(Bdd<LibraryType> const& other) const;
/*!
* Performs a logical and of the current and the given BDD and assigns it to the current BDD.
*
* @param other The second BDD used for the operation.
* @return A reference to the current BDD after the operation
*/
Bdd<LibraryType>& operator&=(Bdd<LibraryType> const& other);
/*!
* Performs a logical iff of the current and the given BDD.
*
* @param other The second BDD used for the operation.
* @return The logical iff of the operands.
*/
Bdd<LibraryType> iff(Bdd<LibraryType> const& other) const;
/*!
* Performs a logical exclusive-or of the current and the given BDD.
*
* @param other The second BDD used for the operation.
* @return The logical exclusive-or of the operands.
*/
Bdd<LibraryType> exclusiveOr(Bdd<LibraryType> const& other) const;
/*!
* Performs a logical implication of the current and the given BDD.
*
* @param other The second BDD used for the operation.
* @return The logical implication of the operands.
*/
Bdd<LibraryType> implies(Bdd<LibraryType> const& other) const;
/*!
* Logically inverts the current BDD.
*
* @return The resulting BDD.
*/
Bdd<LibraryType> operator!() const;
/*!
* Logically complements the current BDD.
*
* @return A reference to the current BDD after the operation.
*/
Bdd<LibraryType>& complement();
/*!
* Existentially abstracts from the given meta variables.
*
* @param metaVariables The meta variables from which to abstract.
*/
Bdd<LibraryType> existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Universally abstracts from the given meta variables.
*
* @param metaVariables The meta variables from which to abstract.
*/
Bdd<LibraryType> universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Computes the logical and of the current and the given BDD and existentially abstracts from the given set
* of variables.
*
* @param other The second BDD for the logical and.
* @param existentialVariables The variables from which to existentially abstract.
* @return A BDD representing the result.
*/
Bdd<LibraryType> andExists(Bdd<LibraryType> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
/*!
* Computes the constraint of the current BDD with the given constraint. That is, the function value of the
* resulting BDD will be the same as the current ones for all assignments mapping to one in the constraint
* and may be different otherwise.
*
* @param constraint The constraint to use for the operation.
* @return The resulting BDD.
*/
Bdd<LibraryType> constrain(Bdd<LibraryType> const& constraint) const;
/*!
* Computes the restriction of the current BDD with the given constraint. That is, the function value of the
* resulting DD will be the same as the current ones for all assignments mapping to one in the constraint
* and may be different otherwise.
*
* @param constraint The constraint to use for the operation.
* @return The resulting BDD.
*/
Bdd<LibraryType> restrict(Bdd<LibraryType> const& constraint) const;
/*!
* Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have
* the same number of underlying BDD variables.
*
* @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another.
* @return The resulting BDD.
*/
Bdd<LibraryType> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
/*!
* Retrieves whether this DD represents the constant one function.
*
* @return True if this DD represents the constant one function.
*/
bool isOne() const;
/*!
* Retrieves whether this DD represents the constant zero function.
*
* @return True if this DD represents the constant zero function.
*/
bool isZero() const;
/*!
* Converts a BDD to an equivalent ADD.
*
* @return The corresponding ADD.
*/
template<typename ValueType>
Add<LibraryType, ValueType> toAdd() const;
/*!
* Converts the BDD to a bit 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 bit vector that is represented by this BDD.
*/
storm::storage::BitVector toVector(storm::dd::Odd<LibraryType> const& rowOdd) const;
virtual Bdd<LibraryType> getSupport() const override;
virtual uint_fast64_t getNonZeroCount() const override;
virtual uint_fast64_t getLeafCount() const override;
virtual uint_fast64_t getNodeCount() const override;
virtual uint_fast64_t getIndex() const override;
virtual void exportToDot(std::string const& filename) const override;
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.
*/
Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, InternalBdd<LibraryType> const& internalBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
/*!
* Constructs a BDD representation of all encodings that are in the requested relation with the given value.
*
* @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.
*/
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);
/*!
* 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);
// The internal BDD that depends on the chosen library.
InternalBdd<LibraryType> internalBdd;
};
}
}

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

@ -0,0 +1,92 @@
#include "src/storage/dd/Dd.h"
#include <algorithm>
#include "src/storage/dd/DdManager.h"
namespace storm {
namespace dd {
template<DdType LibraryType>
Dd<LibraryType>::Dd(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) {
// Intentionally left empty.
}
template<DdType LibraryType>
bool Dd<LibraryType>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const {
return containedMetaVariables.find(metaVariable) != containedMetaVariables.end();
}
template<DdType LibraryType>
bool Dd<LibraryType>::containsMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) const {
return std::includes(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end());
}
template<DdType LibraryType>
std::set<storm::expressions::Variable> const& Dd<LibraryType>::getContainedMetaVariables() const {
return this->containedMetaVariables;
}
template<DdType LibraryType>
std::set<storm::expressions::Variable>& Dd<LibraryType>::getContainedMetaVariables() {
return this->containedMetaVariables;
}
template<DdType LibraryType>
std::shared_ptr<DdManager<LibraryType> const> Dd<LibraryType>::getDdManager() const {
return this->ddManager;
}
template<DdType LibraryType>
void Dd<LibraryType>::addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
std::set<storm::expressions::Variable> result;
std::set_union(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin()));
containedMetaVariables = std::move(result);
}
template<DdType LibraryType>
void Dd<LibraryType>::addMetaVariable(storm::expressions::Variable const& metaVariable) {
this->getContainedMetaVariables().insert(metaVariable);
}
template<DdType LibraryType>
void Dd<LibraryType>::removeMetaVariable(storm::expressions::Variable const& metaVariable) {
this->getContainedMetaVariables().erase(metaVariable);
}
template<DdType LibraryType>
void Dd<LibraryType>::removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
std::set<storm::expressions::Variable> result;
std::set_difference(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin()));
containedMetaVariables = std::move(result);
}
template<DdType LibraryType>
std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices() const {
return getSortedVariableIndices(*this->getDdManager(), 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;
}
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> metaVariables;
std::set_union(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
return metaVariables;
}
template class Dd<storm::dd::DdType::CUDD>;
}
}

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

@ -1,12 +1,180 @@
#ifndef STORM_STORAGE_DD_DD_H_
#define STORM_STORAGE_DD_DD_H_
#include <vector>
#include <string>
#include <set>
#include "src/storage/dd/DdType.h"
#include "src/storage/expressions/Variable.h"
namespace storm {
namespace dd {
// Declare Dd class so we can then specialize it for the different DD types.
template<DdType Type> class Dd;
// Forward-declare some classes.
template<DdType LibraryType> class DdManager;
template<DdType LibraryType> class Bdd;
template<DdType LibraryType>
class Dd {
public:
// Declare the DdManager so it can access the internals of a DD.
friend class DdManager<LibraryType>;
// Instantiate all copy/move constructors/assignments with the default implementation.
Dd() = default;
Dd(Dd<LibraryType> const& other) = default;
Dd& operator=(Dd<LibraryType> const& other) = default;
Dd(Dd<LibraryType>&& other) = default;
Dd& operator=(Dd<LibraryType>&& other) = default;
/*!
* Retrieves the support of the current DD.
*
* @return The support represented as a BDD.
*/
virtual Bdd<LibraryType> getSupport() const = 0;
/*!
* Retrieves the number of encodings that are mapped to a non-zero value.
*
* @return The number of encodings that are mapped to a non-zero value.
*/
virtual uint_fast64_t getNonZeroCount() const = 0;
/*!
* Retrieves the number of leaves of the DD.
*
* @return The number of leaves of the DD.
*/
virtual uint_fast64_t getLeafCount() const = 0;
/*!
* Retrieves the number of nodes necessary to represent the DD.
*
* @return The number of nodes in this DD.
*/
virtual uint_fast64_t getNodeCount() const = 0;
/*!
* Retrieves the index of the topmost variable in the DD.
*
* @return The index of the topmost variable in DD.
*/
virtual uint_fast64_t getIndex() const = 0;
/*!
* Retrieves whether the given meta variable is contained in the DD.
*
* @param metaVariable The meta variable for which to query membership.
* @return True iff the meta variable is contained in the DD.
*/
bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const;
/*!
* Retrieves whether the given meta variables are all contained in the DD.
*
* @param metaVariables The meta variables for which to query membership.
* @return True iff all meta variables are contained in the DD.
*/
bool containsMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Retrieves the set of all meta variables contained in the DD.
*
* @return The set of all meta variables contained in the DD.
*/
std::set<storm::expressions::Variable> const& getContainedMetaVariables() const;
/*!
* Exports the DD to the given file in the dot format.
*
* @param filename The name of the file to which the DD is to be exported.
*/
virtual void exportToDot(std::string const& filename) const = 0;
/*!
* Retrieves the manager that is responsible for this DD.
*
* A pointer to the manager that is responsible for this DD.
*/
std::shared_ptr<DdManager<LibraryType> const> getDdManager() const;
/*!
* Retrieves the set of all meta variables contained in the DD.
*
* @return The set of all meta variables contained in the DD.
*/
std::set<storm::expressions::Variable>& getContainedMetaVariables();
protected:
/*!
* Retrieves the (sorted) list of the variable indices of DD variables contained in this DD.
*
* @return The sorted list of variable indices.
*/
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.
*
* @param metaVariables The set of meta variables to add.
*/
void addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables);
/*!
* Adds the given meta variable to the set of meta variables that are contained in this DD.
*
* @param metaVariable The name of the meta variable to add.
*/
void addMetaVariable(storm::expressions::Variable const& metaVariable);
/*!
* Removes the given meta variable to the set of meta variables that are contained in this DD.
*
* @param metaVariable The name of the meta variable to remove.
*/
void removeMetaVariable(storm::expressions::Variable const& metaVariable);
/*!
* Removes the given set of meta variables from the DD.
*
* @param metaVariables The set of meta variables to remove.
*/
void removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables);
/*!
* Creates a DD with the given manager and meta variables.
*
* @param ddManager The manager responsible for this DD.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
Dd(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
/*!
* Retrieves the set of meta variables contained in both DDs.
*
* @param first The first DD.
* @param second The second DD.
* @return The set of all contained meta variables.
*/
static std::set<storm::expressions::Variable> joinMetaVariables(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;
// The meta variables that appear in this DD.
std::set<storm::expressions::Variable> containedMetaVariables;
};
}
}

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

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

@ -2,11 +2,19 @@
#define STORM_STORAGE_DD_DDMANAGER_H_
#include "src/storage/dd/DdType.h"
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/expressions/Variable.h"
namespace storm {
namespace dd {
// Declare DdManager class so we can then specialize it for the different DD types.
template<DdType Type> class DdManager;
template<DdType LibraryType>
class DdManager {
public:
Bdd<LibraryType> getBddOne() const;
Bdd<LibraryType> getBddZero() const;
DdMetaVariable<LibraryType> const& getMetaVariable(storm::expressions::Variable const& variable) const;
};
}
}

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

@ -6,7 +6,11 @@
namespace storm {
namespace dd {
// Declare DdMetaVariable class so we can then specialize it for the different DD types.
template<DdType Type> class DdMetaVariable;
template<DdType LibraryType>
class DdMetaVariable {
public:
InternalBdd<LibraryType> getCube() const;
};
}
}

3
src/storage/dd/DdType.h
View File

@ -4,7 +4,8 @@
namespace storm {
namespace dd {
enum class DdType {
CUDD
CUDD,
Sylvan
};
}
}

14
src/storage/dd/InternalAdd.h
View File

@ -0,0 +1,14 @@
#ifndef STORM_STORAGE_DD_INTERNALADD_H_
#define STORM_STORAGE_DD_INTERNALADD_H_
#include "src/storage/dd/DdType.h"
namespace storm {
namespace dd {
template <storm::dd::DdType LibraryType, typename ValueType>
class InternalAdd;
}
}
#endif /* STORM_STORAGE_DD_INTERNALADD_H_ */

14
src/storage/dd/InternalBdd.h
View File

@ -0,0 +1,14 @@
#ifndef STORM_STORAGE_DD_INTERNALBDD_H_
#define STORM_STORAGE_DD_INTERNALBDD_H_
#include "src/storage/dd/DdType.h"
namespace storm {
namespace dd {
template <storm::dd::DdType LibraryType>
class InternalBdd;
}
}
#endif /* STORM_STORAGE_DD_CUDD_INTERNALBDD_H_ */

0
src/storage/dd/Odd.cpp
View File

6
src/storage/dd/Odd.h
View File

@ -5,8 +5,10 @@
namespace storm {
namespace dd {
// Declare Odd class so we can then specialize it for the different DD types.
template<DdType Type> class Odd;
template<DdType Type>
class Odd {
};
}
}

384
src/storage/dd/cudd/CuddBdd.cpp
View File

@ -1,384 +0,0 @@
#include <cstring>
#include <algorithm>
#include <functional>
#include "src/storage/dd/cudd/CuddAdd.h"
#include "src/storage/dd/cudd/CuddBdd.h"
#include "src/storage/dd/cudd/CuddOdd.h"
#include "src/storage/dd/cudd/CuddDdManager.h"
#include "src/storage/BitVector.h"
#include "src/logic/ComparisonType.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace dd {
Bdd<DdType::CUDD>::Bdd(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.
}
Bdd<DdType::CUDD>::Bdd(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;
}
}
Add<DdType::CUDD> Bdd<DdType::CUDD>::toAdd() const {
return Add<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables());
}
BDD Bdd<DdType::CUDD>::getCuddBdd() const {
return this->cuddBdd;
}
DdNode* Bdd<DdType::CUDD>::getCuddDdNode() const {
return this->getCuddBdd().getNode();
}
bool Bdd<DdType::CUDD>::operator==(Bdd<DdType::CUDD> const& other) const {
return this->getCuddBdd() == other.getCuddBdd();
}
bool Bdd<DdType::CUDD>::operator!=(Bdd<DdType::CUDD> const& other) const {
return !(*this == other);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::ite(Bdd<DdType::CUDD> const& thenDd, Bdd<DdType::CUDD> const& elseDd) const {
std::set<storm::expressions::Variable> metaVariableNames;
std::set_union(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end(), elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end(), std::inserter(metaVariableNames, metaVariableNames.begin()));
metaVariableNames.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end());
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::operator!() const {
Bdd<DdType::CUDD> result(*this);
result.complement();
return result;
}
Bdd<DdType::CUDD>& Bdd<DdType::CUDD>::complement() {
this->cuddBdd = ~this->getCuddBdd();
return *this;
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::operator&&(Bdd<DdType::CUDD> const& other) const {
Bdd<DdType::CUDD> result(*this);
result &= other;
return result;
}
Bdd<DdType::CUDD>& Bdd<DdType::CUDD>::operator&=(Bdd<DdType::CUDD> const& other) {
this->addMetaVariables(other.getContainedMetaVariables());
this->cuddBdd = this->getCuddBdd() & other.getCuddBdd();
return *this;
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::operator||(Bdd<DdType::CUDD> const& other) const {
Bdd<DdType::CUDD> result(*this);
result |= other;
return result;
}
Bdd<DdType::CUDD>& Bdd<DdType::CUDD>::operator|=(Bdd<DdType::CUDD> const& other) {
this->addMetaVariables(other.getContainedMetaVariables());
this->cuddBdd = this->getCuddBdd() | other.getCuddBdd();
return *this;
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::iff(Bdd<DdType::CUDD> const& other) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::exclusiveOr(Bdd<DdType::CUDD> const& other) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::implies(Bdd<DdType::CUDD> const& other) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
Bdd<DdType::CUDD> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeBdd.getCuddBdd()), newMetaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
Bdd<DdType::CUDD> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeBdd.getCuddBdd()), newMetaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
std::set<storm::expressions::Variable> newContainedMetaVariables;
std::vector<BDD> from;
std::vector<BDD> to;
for (auto const& metaVariablePair : metaVariablePairs) {
DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
// Check if it's legal so swap the meta variables.
STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size.");
// Keep track of the contained meta variables in the DD.
if (this->containsMetaVariable(metaVariablePair.first)) {
newContainedMetaVariables.insert(metaVariablePair.second);
}
if (this->containsMetaVariable(metaVariablePair.second)) {
newContainedMetaVariables.insert(metaVariablePair.first);
}
// Add the variables to swap to the corresponding vectors.
for (auto const& ddVariable : variable1.getDdVariables()) {
from.push_back(ddVariable.getCuddBdd());
}
for (auto const& ddVariable : variable2.getDdVariables()) {
to.push_back(ddVariable.getCuddBdd());
}
}
// Finally, call CUDD to swap the variables.
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::andExists(Bdd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
Bdd<DdType::CUDD> cubeBdd(this->getDdManager()->getBddOne());
for (auto const& metaVariable : existentialVariables) {
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeBdd &= ddMetaVariable.getCube();
}
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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeBdd.getCuddBdd()), containedMetaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::constrain(Bdd<DdType::CUDD> const& constraint) const {
std::set<storm::expressions::Variable> metaVariables;
std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::restrict(Bdd<DdType::CUDD> const& constraint) const {
std::set<storm::expressions::Variable> metaVariables;
std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
}
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::getSupport() const {
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
}
uint_fast64_t Bdd<DdType::CUDD>::getNonZeroCount() const {
std::size_t numberOfDdVariables = 0;
for (auto const& metaVariable : this->getContainedMetaVariables()) {
numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables();
}
return static_cast<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
}
uint_fast64_t Bdd<DdType::CUDD>::getLeafCount() const {
return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves());
}
uint_fast64_t Bdd<DdType::CUDD>::getNodeCount() const {
return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount());
}
bool Bdd<DdType::CUDD>::isOne() const {
return this->getCuddBdd().IsOne();
}
bool Bdd<DdType::CUDD>::isZero() const {
return this->getCuddBdd().IsZero();
}
uint_fast64_t Bdd<DdType::CUDD>::getIndex() const {
return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
}
void Bdd<DdType::CUDD>::exportToDot(std::string const& filename) const {
if (filename.empty()) {
std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
this->getDdManager()->getCuddManager().DumpDot(cuddBddVector);
} else {
// Build the name input of the DD.
std::vector<char*> ddNames;
std::string ddName("f");
ddNames.push_back(new char[ddName.size() + 1]);
std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back());
// Now build the variables names.
std::vector<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames();
std::vector<char*> ddVariableNames;
for (auto const& element : ddVariableNamesAsStrings) {
ddVariableNames.push_back(new char[element.size() + 1]);
std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back());
}
// Open the file, dump the DD and close it again.
FILE* filePointer = fopen(filename.c_str() , "w");
std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
fclose(filePointer);
// Finally, delete the names.
for (char* element : ddNames) {
delete element;
}
for (char* element : ddVariableNames) {
delete element;
}
}
}
template<typename ValueType>
BDD Bdd<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* Bdd<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) {
if (currentLevel == maxLevel) {
// If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one
// (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we
// need to copy the next value of the vector iff the then-offset is greater than zero.
if (odd.getThenOffset() > 0) {
if (filter(values[currentOffset++])) {
return Cudd_ReadOne(manager);
} else {
return Cudd_ReadLogicZero(manager);
}
} else {
return Cudd_ReadZero(manager);
}
} else {
// If the total offset is zero, we can just return the constant zero DD.
if (odd.getThenOffset() + odd.getElseOffset() == 0) {
return Cudd_ReadZero(manager);
}
// Determine the new else-successor.
DdNode* elseSuccessor = nullptr;
if (odd.getElseOffset() > 0) {
elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices, filter);
} else {
elseSuccessor = Cudd_ReadLogicZero(manager);
}
Cudd_Ref(elseSuccessor);
// Determine the new then-successor.
DdNode* thenSuccessor = nullptr;
if (odd.getThenOffset() > 0) {
thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices, filter);
} else {
thenSuccessor = Cudd_ReadLogicZero(manager);
}
Cudd_Ref(thenSuccessor);
// Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
DdNode* result = Cudd_bddIthVar(manager, static_cast<int>(ddVariableIndices[currentLevel]));
Cudd_Ref(result);
DdNode* newResult = Cudd_bddIte(manager, result, thenSuccessor, elseSuccessor);
Cudd_Ref(newResult);
// Dispose of the intermediate results
Cudd_RecursiveDeref(manager, result);
Cudd_RecursiveDeref(manager, thenSuccessor);
Cudd_RecursiveDeref(manager, elseSuccessor);
// Before returning, we remove the protection imposed by the previous call to Cudd_Ref.
Cudd_Deref(newResult);
return newResult;
}
}
storm::storage::BitVector Bdd<DdType::CUDD>::toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const {
std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
storm::storage::BitVector result(rowOdd.getTotalOffset());
this->toVectorRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices);
return result;
}
void Bdd<DdType::CUDD>::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {
// If there are no more values to select, we can directly return.
if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
return;
} else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
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.set(currentRowOffset, true);
} else if (ddRowVariableIndices[currentRowLevel] < dd->index) {
toVectorRec(dd, manager, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
toVectorRec(dd, manager, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
DdNode* elseDdNode = Cudd_E(dd);
DdNode* thenDdNode = Cudd_T(dd);
// Determine whether we have to evaluate the successors as if they were complemented.
bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
toVectorRec(Cudd_Regular(elseDdNode), manager, result, rowOdd.getElseSuccessor(), elseComplemented, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
toVectorRec(Cudd_Regular(thenDdNode), manager, result, rowOdd.getThenSuccessor(), thenComplemented, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
}
}
std::ostream& operator<<(std::ostream& out, const Bdd<DdType::CUDD>& bdd) {
bdd.exportToDot();
return out;
}
}
}

70
src/storage/dd/cudd/CuddDd.cpp
View File

@ -1,70 +0,0 @@
#include <algorithm>
#include "src/storage/dd/cudd/CuddDd.h"
#include "src/storage/dd/cudd/CuddDdManager.h"
namespace storm {
namespace dd {
Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) {
// Intentionally left empty.
}
bool Dd<DdType::CUDD>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const {
return containedMetaVariables.find(metaVariable) != containedMetaVariables.end();
}
bool Dd<DdType::CUDD>::containsMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) const {
return std::includes(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end());
}
std::set<storm::expressions::Variable> const& Dd<DdType::CUDD>::getContainedMetaVariables() const {
return this->containedMetaVariables;
}
std::set<storm::expressions::Variable>& Dd<DdType::CUDD>::getContainedMetaVariables() {
return this->containedMetaVariables;
}
std::shared_ptr<DdManager<DdType::CUDD> const> Dd<DdType::CUDD>::getDdManager() const {
return this->ddManager;
}
void Dd<DdType::CUDD>::addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
std::set<storm::expressions::Variable> result;
std::set_union(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin()));
containedMetaVariables = std::move(result);
}
void Dd<DdType::CUDD>::addMetaVariable(storm::expressions::Variable const& metaVariable) {
this->getContainedMetaVariables().insert(metaVariable);
}
void Dd<DdType::CUDD>::removeMetaVariable(storm::expressions::Variable const& metaVariable) {
this->getContainedMetaVariables().erase(metaVariable);
}
void Dd<DdType::CUDD>::removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
std::set<storm::expressions::Variable> result;
std::set_difference(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin()));
containedMetaVariables = std::move(result);
}
std::vector<uint_fast64_t> Dd<DdType::CUDD>::getSortedVariableIndices() const {
return getSortedVariableIndices(*this->getDdManager(), this->getContainedMetaVariables());
}
std::vector<uint_fast64_t> Dd<DdType::CUDD>::getSortedVariableIndices(DdManager<DdType::CUDD> 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;
}
}
}

182
src/storage/dd/cudd/CuddDd.h
View File

@ -1,182 +0,0 @@
#ifndef STORM_STORAGE_DD_CUDDDD_H_
#define STORM_STORAGE_DD_CUDDDD_H_
#include <set>
#include <memory>
#include "src/storage/dd/Dd.h"
#include "src/storage/expressions/Variable.h"
#include "src/utility/OsDetection.h"
// Include the C++-interface of CUDD.
#include "cuddObj.hh"
namespace storm {
namespace dd {
// Forward-declare some classes.
template<DdType Type> class DdManager;
template<DdType Type> class Odd;
template<DdType Type> class Bdd;
template<>
class Dd<DdType::CUDD> {
public:
// Declare the DdManager so it can access the internals of a DD.
friend class DdManager<DdType::CUDD>;
// Instantiate all copy/move constructors/assignments with the default implementation.
Dd() = default;
Dd(Dd<DdType::CUDD> const& other) = default;
Dd& operator=(Dd<DdType::CUDD> const& other) = default;
#ifndef WINDOWS
Dd(Dd<DdType::CUDD>&& other) = default;
Dd& operator=(Dd<DdType::CUDD>&& other) = default;
#endif
/*!
* Retrieves the support of the current DD.
*
* @return The support represented as a BDD.
*/
virtual Bdd<DdType::CUDD> getSupport() const = 0;
/*!
* Retrieves the number of encodings that are mapped to a non-zero value.
*
* @return The number of encodings that are mapped to a non-zero value.
*/
virtual uint_fast64_t getNonZeroCount() const = 0;
/*!
* Retrieves the number of leaves of the DD.
*
* @return The number of leaves of the DD.
*/
virtual uint_fast64_t getLeafCount() const = 0;
/*!
* Retrieves the number of nodes necessary to represent the DD.
*
* @return The number of nodes in this DD.
*/
virtual uint_fast64_t getNodeCount() const = 0;
/*!
* Retrieves the index of the topmost variable in the DD.
*
* @return The index of the topmost variable in DD.
*/
virtual uint_fast64_t getIndex() const = 0;
/*!
* Retrieves whether the given meta variable is contained in the DD.
*
* @param metaVariable The meta variable for which to query membership.
* @return True iff the meta variable is contained in the DD.
*/
bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const;
/*!
* Retrieves whether the given meta variables are all contained in the DD.
*
* @param metaVariables The meta variables for which to query membership.
* @return True iff all meta variables are contained in the DD.
*/
bool containsMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Retrieves the set of all meta variables contained in the DD.
*
* @return The set of all meta variables contained in the DD.
*/
std::set<storm::expressions::Variable> const& getContainedMetaVariables() const;
/*!
* Exports the DD to the given file in the dot format.
*
* @param filename The name of the file to which the DD is to be exported.
*/
virtual void exportToDot(std::string const& filename = "") const = 0;
/*!
* Retrieves the manager that is responsible for this DD.
*
* A pointer to the manager that is responsible for this DD.
*/
std::shared_ptr<DdManager<DdType::CUDD> const> getDdManager() const;
/*!
* Retrieves the set of all meta variables contained in the DD.
*
* @return The set of all meta variables contained in the DD.
*/
std::set<storm::expressions::Variable>& getContainedMetaVariables();
protected:
/*!
* Retrieves the (sorted) list of the variable indices of DD variables contained in this DD.
*
* @return The sorted list of variable indices.
*/
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<DdType::CUDD> const& manager, std::set<storm::expressions::Variable> const& metaVariables);
/*!
* Adds the given set of meta variables to the DD.
*
* @param metaVariables The set of meta variables to add.
*/
void addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables);
/*!
* Adds the given meta variable to the set of meta variables that are contained in this DD.
*
* @param metaVariable The name of the meta variable to add.
*/
void addMetaVariable(storm::expressions::Variable const& metaVariable);
/*!
* Removes the given meta variable to the set of meta variables that are contained in this DD.
*
* @param metaVariable The name of the meta variable to remove.
*/
void removeMetaVariable(storm::expressions::Variable const& metaVariable);
/*!
* Removes the given set of meta variables from the DD.
*
* @param metaVariables The set of meta variables to remove.
*/
void removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables);
protected:
/*!
* Creates a DD with the given manager and meta variables.
*
* @param ddManager The manager responsible for this DD.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
private:
// A pointer to the manager responsible for this DD.
std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
// The meta variables that appear in this DD.
std::set<storm::expressions::Variable> containedMetaVariables;
};
}
}
#endif /* STORM_STORAGE_DD_CUDDDD_H_ */

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

@ -0,0 +1,316 @@
#include "src/storage/dd/cudd/InternalCuddBdd.h"
namespace storm {
namespace dd {
bool InternalBdd<DdType::CUDD>::operator==(InternalBdd<DdType::CUDD> const& other) const {
return this->getCuddBdd() == other.getCuddBdd();
}
bool InternalBdd<DdType::CUDD>::operator!=(InternalBdd<DdType::CUDD> const& other) const {
return !(*this == other);
}
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);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator||(InternalBdd<DdType::CUDD> const& other) const {
InternalBdd<DdType::CUDD> result(*this);
result |= other;
return result;
}
InternalBdd<DdType::CUDD>& InternalBdd<DdType::CUDD>::operator|=(InternalBdd<DdType::CUDD> const& other) {
this->cuddBdd = this->getCuddBdd() | other.getCuddBdd();
return *this;
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator&&(InternalBdd<DdType::CUDD> const& other) const {
InternalBdd<DdType::CUDD> result(*this);
result &= other;
return result;
}
InternalBdd<DdType::CUDD>& InternalBdd<DdType::CUDD>::operator&=(InternalBdd<DdType::CUDD> const& other) {
this->cuddBdd = this->getCuddBdd() & other.getCuddBdd();
return *this;
}
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);
}
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);
}
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);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator!() const {
InternalBdd<DdType::CUDD> result(*this);
result.complement();
return result;
}
InternalBdd<DdType::CUDD>& InternalBdd<DdType::CUDD>::complement() {
this->cuddBdd = ~this->getCuddBdd();
return *this;
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::existsAbstract(InternalBdd<DdType> const& cube) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cube.getCuddBdd()), newMetaVariables);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::universalAbstract(InternalBdd<DdType> const& cube) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cube.getCuddBdd()), newMetaVariables);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::andExists(InternalBdd<DdType::CUDD> const& other, InternalBdd<DdType> const& cube) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cube.getCuddBdd()), containedMetaVariables);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::constrain(InternalBdd<DdType::CUDD> const& constraint) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::restrict(InternalBdd<DdType::CUDD> const& constraint) const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::swapVariables(std::vector<std::pair<std::reference_wrapper<DdMetaVariable<LibraryType> const>, std::reference_wrapper<DdMetaVariable<LibraryType> const>>> const& fromTo) const {
std::vector<BDD> fromBdd;
std::vector<BDD> toBdd;
for (auto const& metaVariablePair : fromTo) {
DdMetaVariable<DdType::CUDD> const& variable1 = metaVariablePair.first.get();
DdMetaVariable<DdType::CUDD> const& variable2 = metaVariablePair.second.get();
// Add the variables to swap to the corresponding vectors.
for (auto const& ddVariable : variable1.getDdVariables()) {
fromBdd.push_back(ddVariable.getCuddBdd());
}
for (auto const& ddVariable : variable2.getDdVariables()) {
toBdd.push_back(ddVariable.getCuddBdd());
}
}
// Finally, call CUDD to swap the variables.
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().SwapVariables(fromBdd, toBdd), newContainedMetaVariables);
}
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::getSupport() const {
return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
}
uint_fast64_t InternalBdd<DdType::CUDD>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
return static_cast<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
}
uint_fast64_t InternalBdd<DdType::CUDD>::getLeafCount() const {
return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves());
}
uint_fast64_t InternalBdd<DdType::CUDD>::getNodeCount() const {
return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount());
}
bool InternalBdd<DdType::CUDD>::isOne() const {
return this->getCuddBdd().IsOne();
}
bool InternalBdd<DdType::CUDD>::isZero() const {
return this->getCuddBdd().IsZero();
}
uint_fast64_t InternalBdd<DdType::CUDD>::getIndex() const {
return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
}
void InternalBdd<DdType::CUDD>::exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings) const {
// Build the name input of the DD.
std::vector<char*> ddNames;
std::string ddName("f");
ddNames.push_back(new char[ddName.size() + 1]);
std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back());
// Now build the variables names.
std::vector<char*> ddVariableNames;
for (auto const& element : ddVariableNamesAsStrings) {
ddVariableNames.push_back(new char[element.size() + 1]);
std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back());
}
// Open the file, dump the DD and close it again.
FILE* filePointer = fopen(filename.c_str() , "w");
std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
fclose(filePointer);
// Finally, delete the names.
for (char* element : ddNames) {
delete element;
}
for (char* element : ddVariableNames) {
delete element;
}
}
BDD InternalBdd<DdType::CUDD>::getCuddBdd() const {
return this->cuddBdd;
}
DdNode* InternalBdd<DdType::CUDD>::getCuddDdNode() const {
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>
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) {
if (currentLevel == maxLevel) {
// If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one
// (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we
// need to copy the next value of the vector iff the then-offset is greater than zero.
if (odd.getThenOffset() > 0) {
if (filter(values[currentOffset++])) {
return Cudd_ReadOne(manager);
} else {
return Cudd_ReadLogicZero(manager);
}
} else {
return Cudd_ReadZero(manager);
}
} else {
// If the total offset is zero, we can just return the constant zero DD.
if (odd.getThenOffset() + odd.getElseOffset() == 0) {
return Cudd_ReadZero(manager);
}
// Determine the new else-successor.
DdNode* elseSuccessor = nullptr;
if (odd.getElseOffset() > 0) {
elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices, filter);
} else {
elseSuccessor = Cudd_ReadLogicZero(manager);
}
Cudd_Ref(elseSuccessor);
// Determine the new then-successor.
DdNode* thenSuccessor = nullptr;
if (odd.getThenOffset() > 0) {
thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices, filter);
} else {
thenSuccessor = Cudd_ReadLogicZero(manager);
}
Cudd_Ref(thenSuccessor);
// Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
DdNode* result = Cudd_bddIthVar(manager, static_cast<int>(ddVariableIndices[currentLevel]));
Cudd_Ref(result);
DdNode* newResult = Cudd_bddIte(manager, result, thenSuccessor, elseSuccessor);
Cudd_Ref(newResult);
// Dispose of the intermediate results
Cudd_RecursiveDeref(manager, result);
Cudd_RecursiveDeref(manager, thenSuccessor);
Cudd_RecursiveDeref(manager, elseSuccessor);
// Before returning, we remove the protection imposed by the previous call to Cudd_Ref.
Cudd_Deref(newResult);
return newResult;
}
}
storm::storage::BitVector InternalBdd<DdType::CUDD>::toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const {
std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
storm::storage::BitVector result(rowOdd.getTotalOffset());
this->toVectorRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices);
return result;
}
void InternalBdd<DdType::CUDD>::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {
// If there are no more values to select, we can directly return.
if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
return;
} else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
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.set(currentRowOffset, true);
} else if (ddRowVariableIndices[currentRowLevel] < dd->index) {
toVectorRec(dd, manager, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
toVectorRec(dd, manager, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
DdNode* elseDdNode = Cudd_E(dd);
DdNode* thenDdNode = Cudd_T(dd);
// Determine whether we have to evaluate the successors as if they were complemented.
bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
toVectorRec(Cudd_Regular(elseDdNode), manager, result, rowOdd.getElseSuccessor(), elseComplemented, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
toVectorRec(Cudd_Regular(thenDdNode), manager, result, rowOdd.getThenSuccessor(), thenComplemented, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
}
}
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;
}
}
}
}

135
src/storage/dd/cudd/CuddBdd.h → src/storage/dd/cudd/InternalCuddBdd.h
View File

@ -1,9 +1,9 @@
#ifndef STORM_STORAGE_DD_CUDDBDD_H_
#define STORM_STORAGE_DD_CUDDBDD_H_
#ifndef STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_
#define STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_
#include "src/storage/dd/Bdd.h"
#include "src/storage/dd/cudd/CuddDd.h"
#include "src/utility/OsDetection.h"
#include "src/storage/dd/DdType.h"
#include "src/storage/dd/InternalBdd.h"
#include "src/storage/dd/InternalAdd.h"
// Include the C++-interface of CUDD.
#include "cuddObj.hh"
@ -20,18 +20,13 @@ namespace storm {
namespace storage {
class BitVector;
}
namespace dd {
// Forward-declare some classes.
template<DdType Type> class DdManager;
template<DdType Type> class Odd;
template<DdType Type> class Add;
template<DdType Type> class DdForwardIterator;
template<storm::dd::DdType LibraryType>
class Odd;
template<>
class Bdd<DdType::CUDD> : public Dd<DdType::CUDD> {
class InternalBdd<storm::dd::DdType::CUDD> {
public:
/*!
* Constructs a BDD representation of all encodings that are in the requested relation with the given value.
@ -43,30 +38,22 @@ 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<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);
// Declare the DdManager and DdIterator class as friend so it can access the internals of a DD.
friend class DdManager<DdType::CUDD>;
friend class DdForwardIterator<DdType::CUDD>;
friend class Add<DdType::CUDD>;
friend class Odd<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);
// Instantiate all copy/move constructors/assignments with the default implementation.
Bdd() = default;
Bdd(Bdd<DdType::CUDD> const& other) = default;
Bdd& operator=(Bdd<DdType::CUDD> const& other) = default;
#ifndef WINDOWS
Bdd(Bdd<DdType::CUDD>&& other) = default;
Bdd& operator=(Bdd<DdType::CUDD>&& other) = default;
#endif
InternalBdd() = default;
InternalBdd(InternalBdd<DdType::CUDD> const& other) = default;
InternalBdd& operator=(InternalBdd<DdType::CUDD> const& other) = default;
InternalBdd(InternalBdd<DdType::CUDD>&& other) = default;
InternalBdd& operator=(InternalBdd<DdType::CUDD>&& other) = default;
/*!
* Retrieves whether the two BDDs represent the same function.
*
* @param other The BDD that is to be compared with the current one.
* @return True if the BDDs represent the same function.
*/
bool operator==(Bdd<DdType::CUDD> const& other) const;
bool operator==(InternalBdd<DdType::CUDD> const& other) const;
/*!
* Retrieves whether the two BDDs represent different functions.
@ -74,7 +61,7 @@ namespace storm {
* @param other The BDD that is to be compared with the current one.
* @return True if the BDDs represent the different functions.
*/
bool operator!=(Bdd<DdType::CUDD> const& other) const;
bool operator!=(InternalBdd<DdType::CUDD> const& other) const;
/*!
* Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero
@ -85,7 +72,7 @@ namespace storm {
* @param elseBdd The BDD defining the 'else' part.
* @return The resulting BDD.
*/
Bdd<DdType::CUDD> ite(Bdd<DdType::CUDD> const& thenBdd, Bdd<DdType::CUDD> const& elseBdd) const;
InternalBdd<DdType::CUDD> ite(InternalBdd<DdType::CUDD> const& thenBdd, InternalBdd<DdType::CUDD> const& elseBdd) const;
/*!
* Performs a logical or of the current and the given BDD.
@ -93,7 +80,7 @@ namespace storm {
* @param other The second BDD used for the operation.
* @return The logical or of the operands.
*/
Bdd<DdType::CUDD> operator||(Bdd<DdType::CUDD> const& other) const;
InternalBdd<DdType::CUDD> operator||(InternalBdd<DdType::CUDD> const& other) const;
/*!
* Performs a logical or of the current and the given BDD and assigns it to the current BDD.
@ -101,7 +88,7 @@ namespace storm {
* @param other The second BDD used for the operation.
* @return A reference to the current BDD after the operation
*/
Bdd<DdType::CUDD>& operator|=(Bdd<DdType::CUDD> const& other);
InternalBdd<DdType::CUDD>& operator|=(InternalBdd<DdType::CUDD> const& other);
/*!
* Performs a logical and of the current and the given BDD.
@ -109,7 +96,7 @@ namespace storm {
* @param other The second BDD used for the operation.
* @return The logical and of the operands.
*/
Bdd<DdType::CUDD> operator&&(Bdd<DdType::CUDD> const& other) const;
InternalBdd<DdType::CUDD> operator&&(InternalBdd<DdType::CUDD> const& other) const;
/*!
* Performs a logical and of the current and the given BDD and assigns it to the current BDD.
@ -117,7 +104,7 @@ namespace storm {
* @param other The second BDD used for the operation.
* @return A reference to the current BDD after the operation
*/
Bdd<DdType::CUDD>& operator&=(Bdd<DdType::CUDD> const& other);
InternalBdd<DdType::CUDD>& operator&=(InternalBdd<DdType::CUDD> const& other);
/*!
* Performs a logical iff of the current and the given BDD.
@ -125,7 +112,7 @@ namespace storm {
* @param other The second BDD used for the operation.
* @return The logical iff of the operands.
*/
Bdd<DdType::CUDD> iff(Bdd<DdType::CUDD> const& other) const;
InternalBdd<DdType::CUDD> iff(InternalBdd<DdType::CUDD> const& other) const;
/*!
* Performs a logical exclusive-or of the current and the given BDD.
@ -133,7 +120,7 @@ namespace storm {
* @param other The second BDD used for the operation.
* @return The logical exclusive-or of the operands.
*/
Bdd<DdType::CUDD> exclusiveOr(Bdd<DdType::CUDD> const& other) const;
InternalBdd<DdType::CUDD> exclusiveOr(InternalBdd<DdType::CUDD> const& other) const;
/*!
* Performs a logical implication of the current and the given BDD.
@ -141,35 +128,35 @@ namespace storm {
* @param other The second BDD used for the operation.
* @return The logical implication of the operands.
*/
Bdd<DdType::CUDD> implies(Bdd<DdType::CUDD> const& other) const;
InternalBdd<DdType::CUDD> implies(InternalBdd<DdType::CUDD> const& other) const;
/*!
* Logically inverts the current BDD.
*
* @return The resulting BDD.
*/
Bdd<DdType::CUDD> operator!() const;
InternalBdd<DdType::CUDD> operator!() const;
/*!
* Logically complements the current BDD.
*
* @return A reference to the current BDD after the operation.
*/
Bdd<DdType::CUDD>& complement();
InternalBdd<DdType::CUDD>& complement();
/*!
* Existentially abstracts from the given meta variables.
*
* @param metaVariables The meta variables from which to abstract.
*/
Bdd<DdType::CUDD> existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
InternalBdd<DdType::CUDD> existsAbstract(InternalBdd<DdType::CUDD> const& cube) const;
/*!
* Universally abstracts from the given meta variables.
*
* @param metaVariables The meta variables from which to abstract.
*/
Bdd<DdType::CUDD> universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
InternalBdd<DdType::CUDD> universalAbstract(InternalBdd<DdType::CUDD> const& cube) const;
/*!
* Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have
@ -178,8 +165,8 @@ namespace storm {
* @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another.
* @return The resulting BDD.
*/
Bdd<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
InternalBdd<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
/*!
* Computes the logical and of the current and the given BDD and existentially abstracts from the given set
* of variables.
@ -188,7 +175,7 @@ namespace storm {
* @param existentialVariables The variables from which to existentially abstract.
* @return A BDD representing the result.
*/
Bdd<DdType::CUDD> andExists(Bdd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
InternalBdd<DdType::CUDD> andExists(InternalBdd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
/*!
* Computes the constraint of the current BDD with the given constraint. That is, the function value of the
@ -198,7 +185,7 @@ namespace storm {
* @param constraint The constraint to use for the operation.
* @return The resulting BDD.
*/
Bdd<DdType::CUDD> constrain(Bdd<DdType::CUDD> const& constraint) const;
InternalBdd<DdType::CUDD> constrain(InternalBdd<DdType::CUDD> const& constraint) const;
/*!
* Computes the restriction of the current BDD with the given constraint. That is, the function value of the
@ -208,35 +195,35 @@ namespace storm {
* @param constraint The constraint to use for the operation.
* @return The resulting BDD.
*/
Bdd<DdType::CUDD> restrict(Bdd<DdType::CUDD> const& constraint) const;
InternalBdd<DdType::CUDD> restrict(InternalBdd<DdType::CUDD> const& constraint) const;
/*!
* Retrieves the support of the current BDD.
*
* @return The support represented as a BDD.
*/
virtual Bdd<DdType::CUDD> getSupport() const override;
InternalBdd<DdType::CUDD> getSupport() const;
/*!
* Retrieves the number of encodings that are mapped to a non-zero value.
*
* @return The number of encodings that are mapped to a non-zero value.
*/
virtual uint_fast64_t getNonZeroCount() const override;
uint_fast64_t getNonZeroCount() const;
/*!
* Retrieves the number of leaves of the DD.
*
* @return The number of leaves of the DD.
*/
virtual uint_fast64_t getLeafCount() const override;
uint_fast64_t getLeafCount() const;
/*!
* Retrieves the number of nodes necessary to represent the DD.
*
* @return The number of nodes in this DD.
*/
virtual uint_fast64_t getNodeCount() const override;
uint_fast64_t getNodeCount() const;
/*!
* Retrieves whether this DD represents the constant one function.
@ -257,23 +244,22 @@ namespace storm {
*
* @return The index of the topmost variable in BDD.
*/
virtual uint_fast64_t getIndex() const override;
uint_fast64_t getIndex() const;
/*!
* Exports the BDD to the given file in the dot format.
*
* @param filename The name of the file to which the BDD is to be exported.
*/
virtual void exportToDot(std::string const& filename = "") const override;
friend std::ostream & operator<<(std::ostream& out, const Bdd<DdType::CUDD>& bdd);
void exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings) const;
/*!
* Converts a BDD to an equivalent ADD.
*
* @return The corresponding ADD.
*/
Add<DdType::CUDD> toAdd() const;
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> toAdd() const;
/*!
* Converts the BDD to a bit vector. The given offset-labeled DD is used to determine the correct row of
@ -285,20 +271,6 @@ namespace storm {
storm::storage::BitVector toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const;
private:
/*!
* Retrieves the CUDD BDD object associated with this DD.
*
* @return The CUDD BDD object associated with this DD.
*/
BDD getCuddBdd() const;
/*!
* Retrieves the raw DD node of CUDD associated with this BDD.
*
* @return The DD node of CUDD associated with this BDD.
*/
DdNode* getCuddDdNode() const;
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*
@ -306,7 +278,7 @@ namespace storm {
* @param cuddBdd The CUDD BDD to store.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
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.
@ -351,10 +323,23 @@ namespace storm {
*/
void toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
// The BDD created by CUDD.
/*!
* Retrieves the CUDD BDD object associated with this DD.
*
* @return The CUDD BDD object associated with this DD.
*/
BDD getCuddBdd() const;
/*!
* Retrieves the raw DD node of CUDD associated with this BDD.
*
* @return The DD node of CUDD associated with this BDD.
*/
DdNode* getCuddDdNode() const;
BDD cuddBdd;
};
}
}
#endif /* STORM_STORAGE_DD_CUDDBDD_H_ */
#endif /* STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_ */
Write Preview
Loading…
Cancel
Save