dehnert
10 years ago
8 changed files with 2687 additions and 1845 deletions
-
14src/storage/dd/Add.h
-
14src/storage/dd/Bdd.h
-
1174src/storage/dd/CuddAdd.cpp
-
845src/storage/dd/CuddAdd.h
-
321src/storage/dd/CuddBdd.cpp
-
275src/storage/dd/CuddBdd.h
-
1158src/storage/dd/CuddDd.cpp
-
731src/storage/dd/CuddDd.h
@ -0,0 +1,14 @@ |
|||
#ifndef STORM_STORAGE_DD_ADD_H_ |
|||
#define STORM_STORAGE_DD_ADD_H_ |
|||
|
|||
#include "src/storage/dd/Dd.h" |
|||
#include "src/storage/dd/DdType.h" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
// Declare Add class so we can then specialize it for the different ADD types. |
|||
template<DdType Type> class Add; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_ADD_H_ */ |
|||
@ -0,0 +1,14 @@ |
|||
#ifndef STORM_STORAGE_DD_BDD_H_ |
|||
#define STORM_STORAGE_DD_BDD_H_ |
|||
|
|||
#include "src/storage/dd/Dd.h" |
|||
#include "src/storage/dd/DdType.h" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
// Declare Bdd class so we can then specialize it for the different BDD types. |
|||
template<DdType Type> class Bdd; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_BDD_H_ */ |
|||
1174
src/storage/dd/CuddAdd.cpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,845 @@ |
|||
#ifndef STORM_STORAGE_DD_CUDDDD_H_ |
|||
#define STORM_STORAGE_DD_CUDDDD_H_ |
|||
|
|||
#include <map> |
|||
#include <set> |
|||
#include <memory> |
|||
#include <iostream> |
|||
#include <boost/variant.hpp> |
|||
|
|||
#include "src/storage/dd/Dd.h" |
|||
#include "src/storage/dd/CuddDdForwardIterator.h" |
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/storage/expressions/Expression.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<> |
|||
class Dd<DdType::CUDD> { |
|||
public: |
|||
// 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 Odd<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 whether the two DDs represent the same function. |
|||
* |
|||
* @param other The DD that is to be compared with the current one. |
|||
* @return True if the DDs represent the same function. |
|||
*/ |
|||
bool operator==(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves whether the two DDs represent different functions. |
|||
* |
|||
* @param other The DD that is to be compared with the current one. |
|||
* @return True if the DDs represent the different functions. |
|||
*/ |
|||
bool operator!=(Dd<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 |
|||
* function value to the function values specified by the first DD and all others to the function values |
|||
* specified by the second DD. |
|||
*/ |
|||
Dd<DdType::CUDD> ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> const& elseDd) const; |
|||
|
|||
/*! |
|||
* Performs a logical or of the current and the given DD. |
|||
* |
|||
* @param other The second DD used for the operation. |
|||
* @return The logical or of the operands. |
|||
*/ |
|||
Dd<DdType::CUDD> operator||(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Performs a logical or of the current and the given DD and assigns it to the current DD. |
|||
* |
|||
* @param other The second DD used for the operation. |
|||
* @return A reference to the current DD after the operation |
|||
*/ |
|||
Dd<DdType::CUDD>& operator|=(Dd<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Performs a logical and of the current and the given DD. |
|||
* |
|||
* @param other The second DD used for the operation. |
|||
* @return The logical and of the operands. |
|||
*/ |
|||
Dd<DdType::CUDD> operator&&(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Performs a logical and of the current and the given DD and assigns it to the current DD. |
|||
* |
|||
* @param other The second DD used for the operation. |
|||
* @return A reference to the current DD after the operation |
|||
*/ |
|||
Dd<DdType::CUDD>& operator&=(Dd<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Performs a logical iff of the current and the given DD. |
|||
* |
|||
* @param other The second DD used for the operation. |
|||
* @return The logical iff of the operands. |
|||
*/ |
|||
Dd<DdType::CUDD> iff(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Performs a logical exclusive-or of the current and the given DD. |
|||
* |
|||
* @param other The second DD used for the operation. |
|||
* @return The logical exclusive-or of the operands. |
|||
*/ |
|||
Dd<DdType::CUDD> exclusiveOr(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Performs a logical implication of the current and the given DD. |
|||
* |
|||
* @param other The second DD used for the operation. |
|||
* @return The logical implication of the operands. |
|||
*/ |
|||
Dd<DdType::CUDD> implies(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Adds the two DDs. |
|||
* |
|||
* @param other The DD to add to the current one. |
|||
* @return The result of the addition. |
|||
*/ |
|||
Dd<DdType::CUDD> operator+(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Adds the given DD to the current one. |
|||
* |
|||
* @param other The DD to add to the current one. |
|||
* @return A reference to the current DD after the operation. |
|||
*/ |
|||
Dd<DdType::CUDD>& operator+=(Dd<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Multiplies the two DDs. |
|||
* |
|||
* @param other The DD to multiply with the current one. |
|||
* @return The result of the multiplication. |
|||
*/ |
|||
Dd<DdType::CUDD> operator*(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Multiplies the given DD with the current one and assigns the result to the current DD. |
|||
* |
|||
* @param other The DD to multiply with the current one. |
|||
* @return A reference to the current DD after the operation. |
|||
*/ |
|||
Dd<DdType::CUDD>& operator*=(Dd<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Subtracts the given DD from the current one. |
|||
* |
|||
* @param other The DD to subtract from the current one. |
|||
* @return The result of the subtraction. |
|||
*/ |
|||
Dd<DdType::CUDD> operator-(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Subtracts the DD from the constant zero function. |
|||
* |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> operator-() const; |
|||
|
|||
/*! |
|||
* Subtracts the given DD from the current one and assigns the result to the current DD. |
|||
* |
|||
* @param other The DD to subtract from the current one. |
|||
* @return A reference to the current DD after the operation. |
|||
*/ |
|||
Dd<DdType::CUDD>& operator-=(Dd<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Divides the current DD by the given one. |
|||
* |
|||
* @param other The DD by which to divide the current one. |
|||
* @return The result of the division. |
|||
*/ |
|||
Dd<DdType::CUDD> operator/(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Divides the current DD by the given one and assigns the result to the current DD. |
|||
* |
|||
* @param other The DD by which to divide the current one. |
|||
* @return A reference to the current DD after the operation. |
|||
*/ |
|||
Dd<DdType::CUDD>& operator/=(Dd<DdType::CUDD> const& other); |
|||
|
|||
/*! |
|||
* Retrieves the logical complement of the current DD. The result will map all encodings with a value |
|||
* unequal to zero to false and all others to true. |
|||
* |
|||
* @return The logical complement of the current DD. |
|||
*/ |
|||
Dd<DdType::CUDD> operator!() const; |
|||
|
|||
/*! |
|||
* Logically complements the current DD. The result will map all encodings with a value |
|||
* unequal to zero to false and all others to true. |
|||
* |
|||
* @return A reference to the current DD after the operation. |
|||
*/ |
|||
Dd<DdType::CUDD>& complement(); |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one that have an identical function values. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> equals(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one that have distinct function values. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> notEquals(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are less |
|||
* than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> less(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are less or |
|||
* equal than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> lessOrEqual(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are greater |
|||
* than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> greater(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to one whose function value in the first DD are greater |
|||
* or equal than the one in the given DD. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> greaterOrEqual(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to the minimum of the function values of the two DDs. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> minimum(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Retrieves the function that maps all evaluations to the maximum of the function values of the two DDs. |
|||
* |
|||
* @param other The DD with which to perform the operation. |
|||
* @return The resulting function represented as a DD. |
|||
*/ |
|||
Dd<DdType::CUDD> maximum(Dd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Existentially abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariables The meta variables from which to abstract. |
|||
*/ |
|||
Dd<DdType::CUDD> 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. |
|||
*/ |
|||
Dd<DdType::CUDD> universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const; |
|||
|
|||
/*! |
|||
* Sum-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariables The meta variables from which to abstract. |
|||
*/ |
|||
Dd<DdType::CUDD> sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const; |
|||
|
|||
/*! |
|||
* Min-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariables The meta variables from which to abstract. |
|||
*/ |
|||
Dd<DdType::CUDD> minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const; |
|||
|
|||
/*! |
|||
* Max-abstracts from the given meta variables. |
|||
* |
|||
* @param metaVariables The meta variables from which to abstract. |
|||
*/ |
|||
Dd<DdType::CUDD> maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const; |
|||
|
|||
/*! |
|||
* Checks whether the current and the given DD represent the same function modulo some given precision. |
|||
* |
|||
* @param other The DD with which to compare. |
|||
* @param precision An upper bound on the maximal difference between any two function values that is to be |
|||
* tolerated. |
|||
* @param relative If set to true, not the absolute values have to be within the precision, but the relative |
|||
* values. |
|||
*/ |
|||
bool equalModuloPrecision(Dd<DdType::CUDD> const& other, double precision, bool relative = true) const; |
|||
|
|||
/*! |
|||
* Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have |
|||
* the same number of underlying DD variables. |
|||
* |
|||
* @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. |
|||
* @return The resulting DD. |
|||
*/ |
|||
Dd<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs); |
|||
|
|||
/*! |
|||
* Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta |
|||
* variables. |
|||
* |
|||
* @param otherMatrix The matrix with which to multiply. |
|||
* @param summationMetaVariables The names of the meta variables over which to sum during the matrix- |
|||
* matrix multiplication. |
|||
* @return A DD representing the result of the matrix-matrix multiplication. |
|||
*/ |
|||
Dd<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const; |
|||
|
|||
/*! |
|||
* Computes the logical and of the current and the given DD and existentially abstracts from the given set |
|||
* of variables. |
|||
* |
|||
* @param other The second DD for the logical and. |
|||
* @param existentialVariables The variables from which to existentially abstract. |
|||
* @return A DD representing the result. |
|||
*/ |
|||
Dd<DdType::CUDD> andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const; |
|||
|
|||
/*! |
|||
* Computes a DD that represents the function in which all assignments with a function value strictly larger |
|||
* than the given value are mapped to one and all others to zero. |
|||
* |
|||
* @param value The value used for the comparison. |
|||
* @return The resulting DD. |
|||
*/ |
|||
Dd<DdType::CUDD> greater(double value) const; |
|||
|
|||
/*! |
|||
* Computes a DD that represents the function in which all assignments with a function value larger or equal |
|||
* to the given value are mapped to one and all others to zero. |
|||
* |
|||
* @param value The value used for the comparison. |
|||
* @return The resulting DD. |
|||
*/ |
|||
Dd<DdType::CUDD> greaterOrEqual(double value) const; |
|||
|
|||
/*! |
|||
* Computes a DD that represents the function in which all assignments with a function value unequal to zero |
|||
* are mapped to one and all others to zero. |
|||
* |
|||
* @return The resulting DD. |
|||
*/ |
|||
Dd<DdType::CUDD> notZero() const; |
|||
|
|||
/*! |
|||
* Computes the constraint of the current DD 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 DD. |
|||
*/ |
|||
Dd<DdType::CUDD> constrain(Dd<DdType::CUDD> const& constraint) const; |
|||
|
|||
/*! |
|||
* Computes the restriction of the current DD 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 DD. |
|||
*/ |
|||
Dd<DdType::CUDD> restrict(Dd<DdType::CUDD> const& constraint) const; |
|||
|
|||
/*! |
|||
* Retrieves the support of the current DD. |
|||
* |
|||
* @return The support represented as a DD. |
|||
*/ |
|||
Dd<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. |
|||
*/ |
|||
uint_fast64_t getNonZeroCount() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of leaves of the DD. |
|||
* |
|||
* @return The number of leaves of the DD. |
|||
*/ |
|||
uint_fast64_t getLeafCount() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of nodes necessary to represent the DD. |
|||
* |
|||
* @return The number of nodes in this DD. |
|||
*/ |
|||
uint_fast64_t getNodeCount() const; |
|||
|
|||
/*! |
|||
* Retrieves the lowest function value of any encoding. |
|||
* |
|||
* @return The lowest function value of any encoding. |
|||
*/ |
|||
double getMin() const; |
|||
|
|||
/*! |
|||
* Retrieves the highest function value of any encoding. |
|||
* |
|||
* @return The highest function value of any encoding. |
|||
*/ |
|||
double getMax() const; |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given value of the meta variable to the given |
|||
* target value. |
|||
* |
|||
* @param metaVariable The meta variable that has to be equal to the given value. |
|||
* @param variableValue The value that the meta variable is supposed to have. This must be within the range |
|||
* of the meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue); |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given values of the two meta variables to the |
|||
* given target value. |
|||
* |
|||
* @param metaVariable1 The first meta variable that has to be equal to the first given |
|||
* value. |
|||
* @param variableValue1 The value that the first meta variable is supposed to have. This must be within the |
|||
* range of the meta variable. |
|||
* @param metaVariable2 The second meta variable that has to be equal to the second given |
|||
* value. |
|||
* @param variableValue2 The value that the second meta variable is supposed to have. This must be within |
|||
* the range of the meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue); |
|||
|
|||
/*! |
|||
* Sets the function values of all encodings that have the given values of the given meta variables to the |
|||
* given target value. |
|||
* |
|||
* @param metaVariableToValueMap A mapping of meta variables to the values they are supposed to have. All |
|||
* values must be within the range of the respective meta variable. |
|||
* @param targetValue The new function value of the modified encodings. |
|||
*/ |
|||
void setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>(), double targetValue = 0); |
|||
|
|||
/*! |
|||
* Retrieves the value of the function when all meta variables are assigned the values of the given mapping. |
|||
* Note that the mapping must specify values for all meta variables contained in the DD. |
|||
* |
|||
* @param metaVariableToValueMap A mapping of meta variables to their values. |
|||
* @return The value of the function evaluated with the given input. |
|||
*/ |
|||
double getValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>()) 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; |
|||
|
|||
/*! |
|||
* Retrieves whether this DD represents a constant function. |
|||
* |
|||
* @return True if this DD represents a constants function. |
|||
*/ |
|||
bool isConstant() const; |
|||
|
|||
/*! |
|||
* Retrieves the index of the topmost variable in the DD. |
|||
* |
|||
* @return The index of the topmost variable in DD. |
|||
*/ |
|||
uint_fast64_t getIndex() const; |
|||
|
|||
/*! |
|||
* Converts the DD to a vector. |
|||
* |
|||
* @return The double vector that is represented by this DD. |
|||
*/ |
|||
template<typename ValueType> |
|||
std::vector<ValueType> toVector() const; |
|||
|
|||
/*! |
|||
* Converts the DD to a vector. The given offset-labeled DD is used to determine the correct row of |
|||
* each entry. |
|||
* |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @return The double vector that is represented by this DD. |
|||
*/ |
|||
template<typename ValueType> |
|||
std::vector<ValueType> toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const; |
|||
|
|||
/*! |
|||
* Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the |
|||
* row, whereas all primed variables are assumed to encode the column. |
|||
* |
|||
* @return The matrix that is represented by this DD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix() const; |
|||
|
|||
/*! |
|||
* Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the |
|||
* row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used |
|||
* to determine the correct row and column, respectively, for each entry. |
|||
* |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this DD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* Converts the DD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the |
|||
* correct row and column, respectively, for each entry. |
|||
* |
|||
* @param rowMetaVariables The meta variables that encode the rows of the matrix. |
|||
* @param columnMetaVariables The meta variables that encode the columns of the matrix. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this DD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* Converts the DD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to |
|||
* determine the correct row and column, respectively, for each entry. Note: this function assumes that |
|||
* the meta variables used to distinguish different row groups are at the very top of the DD. |
|||
* |
|||
* @param rowMetaVariables The meta variables that encode the rows of the matrix. |
|||
* @param columnMetaVariables The meta variables that encode the columns of the matrix. |
|||
* @param groupMetaVariables The meta variables that are used to distinguish different row groups. |
|||
* @param rowOdd The ODD used for determining the correct row. |
|||
* @param columnOdd The ODD used for determining the correct column. |
|||
* @return The matrix that is represented by this DD. |
|||
*/ |
|||
storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; |
|||
|
|||
/*! |
|||
* 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; |
|||
|
|||
/*! |
|||
* 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(); |
|||
|
|||
/*! |
|||
* 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. |
|||
*/ |
|||
void exportToDot(std::string const& filename = "") const; |
|||
|
|||
/*! |
|||
* 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 an iterator that points to the first meta variable assignment with a non-zero function value. |
|||
* |
|||
* @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even |
|||
* if a meta variable does not at all influence the the function value. |
|||
* @return An iterator that points to the first meta variable assignment with a non-zero function value. |
|||
*/ |
|||
DdForwardIterator<DdType::CUDD> begin(bool enumerateDontCareMetaVariables = true) const; |
|||
|
|||
/*! |
|||
* Retrieves an iterator that points past the end of the container. |
|||
* |
|||
* @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even |
|||
* if a meta variable does not at all influence the the function value. |
|||
* @return An iterator that points past the end of the container. |
|||
*/ |
|||
DdForwardIterator<DdType::CUDD> end(bool enumerateDontCareMetaVariables = true) const; |
|||
|
|||
/*! |
|||
* Converts the DD into a (heavily nested) if-then-else expression that represents the very same function. |
|||
* The variable names used in the expression are derived from the meta variable name and are extended with a |
|||
* suffix ".i" if the meta variable is integer-valued, expressing that the variable is the i-th bit of the |
|||
* meta variable. |
|||
* |
|||
* @return The resulting expression. |
|||
*/ |
|||
storm::expressions::Expression toExpression() const; |
|||
|
|||
/*! |
|||
* Converts the DD into a (heavily nested) if-then-else (with negations) expression that evaluates to true |
|||
* if and only if the assignment is minterm of the DD. The variable names used in the expression are derived |
|||
* from the meta variable name and are extended with a suffix ".i" if the meta variable is integer-valued, |
|||
* expressing that the variable is the i-th bit of the meta variable. |
|||
* |
|||
* @return The resulting expression. |
|||
*/ |
|||
storm::expressions::Expression getMintermExpression() const; |
|||
|
|||
friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd); |
|||
|
|||
/*! |
|||
* Converts an MTBDD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as |
|||
* a call to notZero(). |
|||
* |
|||
* @return The corresponding BDD. |
|||
*/ |
|||
Dd<DdType::CUDD> toBdd() const; |
|||
|
|||
/*! |
|||
* Converts a BDD to an equivalent MTBDD. |
|||
* |
|||
* @return The corresponding MTBDD. |
|||
*/ |
|||
Dd<DdType::CUDD> toMtbdd() const; |
|||
|
|||
/*! |
|||
* Retrieves whether this DD is a BDD. |
|||
* |
|||
* @return True iff this DD is a BDD. |
|||
*/ |
|||
bool isBdd() const; |
|||
|
|||
/*! |
|||
* Retrieves whether this DD is an MTBDD. Even though MTBDDs technicall subsume BDDs, this will return false |
|||
* if the DD is actually a BDD. |
|||
* |
|||
* @return True iff this DD is an MTBDD. |
|||
*/ |
|||
bool isMtbdd() 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 CUDD MTBDD object associated with this DD. |
|||
* |
|||
* @return The CUDD MTBDD object associated with this DD. |
|||
*/ |
|||
ADD getCuddMtbdd() const; |
|||
|
|||
/*! |
|||
* Retrieves the CUDD object associated with this DD. |
|||
* |
|||
* @return The CUDD object associated with this DD. |
|||
*/ |
|||
ABDD const& getCuddDd() const; |
|||
|
|||
/*! |
|||
* Retrieves the raw DD node of CUDD associated with this DD. |
|||
* |
|||
* @return The DD node of CUDD associated with this DD. |
|||
*/ |
|||
DdNode* getCuddDdNode() const; |
|||
|
|||
/*! |
|||
* 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 addContainedMetaVariable(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 removeContainedMetaVariable(storm::expressions::Variable const& metaVariable); |
|||
|
|||
/*! |
|||
* Performs the recursive step of toExpression on the given DD. |
|||
* |
|||
* @param dd The dd to translate into an expression. |
|||
* @param variables The variables to use in the expression. |
|||
* @return The resulting expression. |
|||
*/ |
|||
static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector<storm::expressions::Variable> const& variables); |
|||
|
|||
/*! |
|||
* Performs the recursive step of getMintermExpression on the given DD. |
|||
* |
|||
* @param manager The manager of the DD. |
|||
* @param dd The dd whose minterms to translate into an expression. |
|||
* @param variables The variables to use in the expression. |
|||
* @return The resulting expression. |
|||
*/ |
|||
static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector<storm::expressions::Variable> const& variables); |
|||
|
|||
/*! |
|||
* Creates a DD that encapsulates the given CUDD ADD. |
|||
* |
|||
* @param ddManager The manager responsible for this DD. |
|||
* @param cuddDd The CUDD ADD to store. |
|||
* @param containedMetaVariables The meta variables that appear in the DD. |
|||
*/ |
|||
Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>()); |
|||
|
|||
/*! |
|||
* Creates a DD that encapsulates the given CUDD ADD. |
|||
* |
|||
* @param ddManager The manager responsible for this DD. |
|||
* @param cuddDd The CUDD ADD to store. |
|||
* @param containedMetaVariables The meta variables that appear in the DD. |
|||
*/ |
|||
Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>()); |
|||
|
|||
/*! |
|||
* Helper function to convert the DD into a (sparse) matrix. |
|||
* |
|||
* @param dd The DD to convert. |
|||
* @param rowIndications A vector indicating at which position in the columnsAndValues vector the entries |
|||
* of row i start. Note: this vector is modified in the computation. More concretely, each entry i in the |
|||
* vector will be increased by the number of entries in the row. This can be used to count the number |
|||
* of entries in each row. If the values are not to be modified, a copy needs to be provided or the entries |
|||
* need to be restored afterwards. |
|||
* @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful |
|||
* completion. |
|||
* @param rowGroupOffsets The row offsets at which a given row group starts. |
|||
* @param rowOdd The ODD used for the row translation. |
|||
* @param columnOdd The ODD used for the column translation. |
|||
* @param currentRowLevel The currently considered row level in the DD. |
|||
* @param currentColumnLevel The currently considered row level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param currentRowOffset The current row offset. |
|||
* @param currentColumnOffset The current row offset. |
|||
* @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. |
|||
* @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered. |
|||
* @param generateValues If set to true, the vector columnsAndValues is filled with the actual entries, which |
|||
* only works if the offsets given in rowIndications are already correct. If they need to be computed first, |
|||
* this flag needs to be false. |
|||
*/ |
|||
void toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues = true) const; |
|||
|
|||
/*! |
|||
* Splits the given matrix DD into the groups using the given group variables. |
|||
* |
|||
* @param dd The DD to split. |
|||
* @param groups A vector that is to be filled with the DDs for the individual groups. |
|||
* @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. |
|||
* @param currentLevel The currently considered level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. |
|||
*/ |
|||
void splitGroupsRec(DdNode* dd, std::vector<Dd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables) const; |
|||
|
|||
/*! |
|||
* Performs a recursive step to add the given DD-based vector to the given explicit vector. |
|||
* |
|||
* @param dd The DD to add to the explicit vector. |
|||
* @param currentLevel The currently considered level in the DD. |
|||
* @param maxLevel The number of levels that need to be considered. |
|||
* @param currentOffset The current offset. |
|||
* @param odd The ODD used for the translation. |
|||
* @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. |
|||
* @param targetVector The vector to which the translated DD-based vector is to be added. |
|||
*/ |
|||
template<typename ValueType> |
|||
void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const; |
|||
|
|||
/*! |
|||
* Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support, |
|||
* because they could be "don't cares"). Additionally, the indices are sorted to allow for easy access. |
|||
* |
|||
* @return The (sorted) indices of all DD variables that are contained in this DD. |
|||
*/ |
|||
std::vector<uint_fast64_t> getSortedVariableIndices() const; |
|||
|
|||
// A pointer to the manager responsible for this DD. |
|||
std::shared_ptr<DdManager<DdType::CUDD> const> ddManager; |
|||
|
|||
// The ADD created by CUDD. |
|||
boost::variant<BDD, ADD> cuddDd; |
|||
|
|||
// The meta variables that appear in this DD. |
|||
std::set<storm::expressions::Variable> containedMetaVariables; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_CUDDDD_H_ */ |
|||
@ -0,0 +1,321 @@ |
|||
#include <cstring>
|
|||
#include <algorithm>
|
|||
|
|||
#include "src/storage/dd/CuddBdd.h"
|
|||
#include "src/storage/dd/CuddAdd.h"
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
Bdd<DdType::CUDD>::Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
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(); |
|||
} |
|||
|
|||
Bdd<DdType::CUDD> Bdd<DdType::CUDD>::operator&&(Bdd<DdType::CUDD> const& other) const { |
|||
Dd<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 { |
|||
Dd<DdType::CUDD> cubeDd(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); |
|||
cubeDd &= ddMetaVariable.getCube(); |
|||
} |
|||
|
|||
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables); |
|||
} |
|||
|
|||
Dd<DdType::CUDD> Bdd<DdType::CUDD>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const { |
|||
Dd<DdType::CUDD> cubeDd(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); |
|||
cubeDd &= ddMetaVariable.getCube(); |
|||
} |
|||
|
|||
return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables); |
|||
} |
|||
|
|||
Dd<DdType::CUDD> Bdd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) { |
|||
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 { |
|||
STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); |
|||
|
|||
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne()); |
|||
for (auto const& metaVariable : existentialVariables) { |
|||
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); |
|||
cubeDd &= 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 Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables); |
|||
} |
|||
|
|||
Dd<DdType::CUDD> Bdd<DdType::CUDD>::constrain(Dd<DdType::CUDD> const& constraint) const { |
|||
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables()); |
|||
metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); |
|||
|
|||
if (this->isBdd() && constraint.isBdd()) { |
|||
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); |
|||
} else { |
|||
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables); |
|||
} |
|||
} |
|||
|
|||
Dd<DdType::CUDD> Bdd<DdType::CUDD>::restrict(Dd<DdType::CUDD> const& constraint) const { |
|||
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables()); |
|||
metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); |
|||
|
|||
if (this->isBdd() && constraint.isBdd()) { |
|||
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); |
|||
} else { |
|||
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables); |
|||
} |
|||
} |
|||
|
|||
Dd<DdType::CUDD> Bdd<DdType::CUDD>::getSupport() const { |
|||
if (this->isBdd()) { |
|||
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); |
|||
} else { |
|||
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().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(); |
|||
} |
|||
if (this->isBdd()) { |
|||
return static_cast<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables))); |
|||
} else { |
|||
return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountMinterm(static_cast<int>(numberOfDdVariables))); |
|||
} |
|||
} |
|||
|
|||
uint_fast64_t Bdd<DdType::CUDD>::getLeafCount() const { |
|||
if (this->isBdd()) { |
|||
return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves()); |
|||
} else { |
|||
return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountLeaves()); |
|||
} |
|||
} |
|||
|
|||
uint_fast64_t Bdd<DdType::CUDD>::getNodeCount() const { |
|||
if (this->isBdd()) { |
|||
return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount()); |
|||
} else { |
|||
return static_cast<uint_fast64_t>(this->getCuddMtbdd().nodeCount()); |
|||
} |
|||
} |
|||
|
|||
bool Bdd<DdType::CUDD>::isOne() const { |
|||
if (this->isBdd()) { |
|||
return this->getCuddBdd().IsOne(); |
|||
} else { |
|||
return this->getCuddMtbdd().IsOne(); |
|||
} |
|||
} |
|||
|
|||
bool Bdd<DdType::CUDD>::isZero() const { |
|||
if (this->isBdd()) { |
|||
return this->getCuddBdd().IsZero(); |
|||
} else { |
|||
return this->getCuddMtbdd().IsZero(); |
|||
} |
|||
} |
|||
|
|||
uint_fast64_t Bdd<DdType::CUDD>::getIndex() const { |
|||
if (this->isBdd()) { |
|||
return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex()); |
|||
} else { |
|||
return static_cast<uint_fast64_t>(this->getCuddMtbdd().NodeReadIndex()); |
|||
} |
|||
} |
|||
|
|||
std::vector<uint_fast64_t> Bdd<DdType::CUDD>::getSortedVariableIndices() const { |
|||
std::vector<uint_fast64_t> ddVariableIndices; |
|||
for (auto const& metaVariableName : this->getContainedMetaVariables()) { |
|||
auto const& metaVariable = this->getDdManager()->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; |
|||
} |
|||
|
|||
void Bdd<DdType::CUDD>::exportToDot(std::string const& filename) const { |
|||
if (filename.empty()) { |
|||
if (this->isBdd()) { |
|||
std::vector<BDD> cuddBddVector = { this->getCuddBdd() }; |
|||
this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); |
|||
} else { |
|||
std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() }; |
|||
this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); |
|||
} |
|||
} 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"); |
|||
if (this->isBdd()) { |
|||
std::vector<BDD> cuddBddVector = { this->getCuddBdd() }; |
|||
this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); |
|||
} else { |
|||
std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() }; |
|||
this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); |
|||
} |
|||
fclose(filePointer); |
|||
|
|||
// Finally, delete the names.
|
|||
for (char* element : ddNames) { |
|||
delete element; |
|||
} |
|||
for (char* element : ddVariableNames) { |
|||
delete element; |
|||
} |
|||
} |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) { |
|||
dd.exportToDot(); |
|||
return out; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,275 @@ |
|||
#ifndef STORM_STORAGE_DD_CUDDBDD_H_ |
|||
#define STORM_STORAGE_DD_CUDDBDD_H_ |
|||
|
|||
#include "src/storage/dd/Bdd.h" |
|||
#include "src/storage/dd/CuddDd.h" |
|||
#include "src/storage/dd/CuddAdd.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 Add; |
|||
|
|||
template<> |
|||
class Bdd<DdType::CUDD> : public Dd<DdType::CUDD> { |
|||
public: |
|||
// 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 Odd<DdType::CUDD>; |
|||
|
|||
// 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 |
|||
|
|||
/*! |
|||
* 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; |
|||
|
|||
/*! |
|||
* 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<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 |
|||
* 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<DdType::CUDD> ite(Bdd<DdType::CUDD> const& thenBdd, Bdd<DdType::CUDD> 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<DdType::CUDD> operator||(Bdd<DdType::CUDD> 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<DdType::CUDD>& operator|=(Bdd<DdType::CUDD> 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<DdType::CUDD> operator&&(Bdd<DdType::CUDD> 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<DdType::CUDD>& operator&=(Bdd<DdType::CUDD> 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<DdType::CUDD> iff(Bdd<DdType::CUDD> 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<DdType::CUDD> exclusiveOr(Bdd<DdType::CUDD> 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<DdType::CUDD> implies(Bdd<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Logically inverts the current BDD. |
|||
* |
|||
* @return The resulting BDD. |
|||
*/ |
|||
Bdd<DdType::CUDD> operator!() const; |
|||
|
|||
/*! |
|||
* Logically complements the current BDD. |
|||
* |
|||
* @return A reference to the current BDD after the operation. |
|||
*/ |
|||
Bdd<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; |
|||
|
|||
/*! |
|||
* 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; |
|||
|
|||
/*! |
|||
* 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<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs); |
|||
|
|||
/*! |
|||
* 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<DdType::CUDD> andExists(Bdd<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 |
|||
* 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<DdType::CUDD> constrain(Bdd<DdType::CUDD> 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<DdType::CUDD> restrict(Bdd<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; |
|||
|
|||
/*! |
|||
* 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; |
|||
|
|||
/*! |
|||
* 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; |
|||
|
|||
/*! |
|||
* 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; |
|||
|
|||
/*! |
|||
* Retrieves the index of the topmost variable in the BDD. |
|||
* |
|||
* @return The index of the topmost variable in BDD. |
|||
*/ |
|||
virtual uint_fast64_t getIndex() const override; |
|||
|
|||
/*! |
|||
* 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); |
|||
|
|||
/*! |
|||
* Converts a BDD to an equivalent ADD. |
|||
* |
|||
* @return The corresponding ADD. |
|||
*/ |
|||
Add<DdType::CUDD> toAdd() 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. |
|||
* |
|||
* @param ddManager The manager responsible for this DD. |
|||
* @param cuddDd The CUDD ADD to store. |
|||
* @param containedMetaVariables The meta variables that appear in the DD. |
|||
*/ |
|||
Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>()); |
|||
|
|||
// The BDD created by CUDD. |
|||
BDD cuddBdd; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_CUDDBDD_H_ */ |
|||
1158
src/storage/dd/CuddDd.cpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
Write
Preview
Loading…
Cancel
Save
Reference in new issue