Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::dd::Add< LibraryType, ValueType > Class Template Reference

#include <Add.h>

Inheritance diagram for storm::dd::Add< LibraryType, ValueType >:
Collaboration diagram for storm::dd::Add< LibraryType, ValueType >:

Classes

struct  MatrixAndLabeling
 Converts the ADD to a row-grouped (sparse) matrix. More...
 

Public Member Functions

 Add ()=default
 
 Add (Add< LibraryType, ValueType > const &other)=default
 
Addoperator= (Add< LibraryType, ValueType > const &other)=default
 
 Add (Add< LibraryType, ValueType > &&other)=default
 
Addoperator= (Add< LibraryType, ValueType > &&other)=default
 
bool operator== (Add< LibraryType, ValueType > const &other) const
 Retrieves whether the two DDs represent the same function.
 
bool operator!= (Add< LibraryType, ValueType > const &other) const
 Retrieves whether the two DDs represent different functions.
 
Add< LibraryType, ValueType > operator+ (Add< LibraryType, ValueType > const &other) const
 Adds the two ADDs.
 
Add< LibraryType, ValueType > & operator+= (Add< LibraryType, ValueType > const &other)
 Adds the given ADD to the current one.
 
Add< LibraryType, ValueType > operator* (Add< LibraryType, ValueType > const &other) const
 Multiplies the two ADDs.
 
Add< LibraryType, ValueType > & operator*= (Add< LibraryType, ValueType > const &other)
 Multiplies the given ADD with the current one and assigns the result to the current ADD.
 
Add< LibraryType, ValueType > operator- (Add< LibraryType, ValueType > const &other) const
 Subtracts the given ADD from the current one.
 
Add< LibraryType, ValueType > operator- () const
 Subtracts the ADD from the constant zero function.
 
Add< LibraryType, ValueType > & operator-= (Add< LibraryType, ValueType > const &other)
 Subtracts the given ADD from the current one and assigns the result to the current ADD.
 
Add< LibraryType, ValueType > operator/ (Add< LibraryType, ValueType > const &other) const
 Divides the current ADD by the given one.
 
Add< LibraryType, ValueType > & operator/= (Add< LibraryType, ValueType > const &other)
 Divides the current ADD by the given one and assigns the result to the current ADD.
 
Bdd< LibraryType > equals (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to one that have identical function values.
 
Bdd< LibraryType > notEquals (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to one that have distinct function values.
 
Bdd< LibraryType > less (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to one whose function value in the first ADD are less than the one in the given ADD.
 
Bdd< LibraryType > lessOrEqual (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or equal than the one in the given ADD.
 
Bdd< LibraryType > greater (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater than the one in the given ADD.
 
Bdd< LibraryType > greaterOrEqual (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater or equal than the one in the given ADD.
 
Add< LibraryType, ValueType > pow (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that represents the current ADD to the power of the given ADD.
 
Add< LibraryType, ValueType > mod (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that represents the current ADD modulo the given ADD.
 
Add< LibraryType, ValueType > logxy (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that represents the logarithm of the current ADD to the bases given by the second ADD.
 
Add< LibraryType, ValueType > floor () const
 Retrieves the function that floors all values in the current ADD.
 
Add< LibraryType, ValueType > ceil () const
 Retrieves the function that ceils all values in the current ADD.
 
Add< LibraryType, storm::RationalNumber > sharpenKwekMehlhorn (uint64_t precision) const
 Retrieves the function that sharpens all values in the current ADD with the Kwek-Mehlhorn algorithm.
 
Add< LibraryType, ValueType > minimum (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs.
 
Add< LibraryType, ValueType > maximum (Add< LibraryType, ValueType > const &other) const
 Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs.
 
template<typename TargetValueType >
std::enable_if< std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type toValueType () const
 Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else.
 
template<typename TargetValueType >
std::enable_if<!std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type toValueType () const
 
Add< LibraryType, ValueType > sumAbstract (std::set< storm::expressions::Variable > const &metaVariables) const
 Sum-abstracts from the given meta variables.
 
Add< LibraryType, ValueType > minAbstract (std::set< storm::expressions::Variable > const &metaVariables) const
 Min-abstracts from the given meta variables.
 
Bdd< LibraryType > minAbstractRepresentative (std::set< storm::expressions::Variable > const &metaVariables) const
 Similar to minAbstract, but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the minimal value.
 
Add< LibraryType, ValueType > maxAbstract (std::set< storm::expressions::Variable > const &metaVariables) const
 Max-abstracts from the given meta variables.
 
Bdd< LibraryType > maxAbstractRepresentative (std::set< storm::expressions::Variable > const &metaVariables) const
 Similar to maxAbstract, but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the maximal value.
 
bool equalModuloPrecision (Add< LibraryType, ValueType > const &other, ValueType const &precision, bool relative=true) const
 Checks whether the current and the given ADD represent the same function modulo some given precision.
 
Add< LibraryType, ValueType > renameVariables (std::set< storm::expressions::Variable > const &from, std::set< storm::expressions::Variable > const &to) const
 Renames the given meta variables in the ADD.
 
Add< LibraryType, ValueType > renameVariablesAbstract (std::set< storm::expressions::Variable > const &from, std::set< storm::expressions::Variable > const &to) const
 Renames the given meta variables in the ADD.
 
Add< LibraryType, ValueType > swapVariables (std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
 Swaps the given pairs of meta variables in the ADD.
 
Add< LibraryType, ValueType > permuteVariables (std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
 Permutes the given pairs of meta variables in the ADD.
 
Add< LibraryType, ValueType > multiplyMatrix (Add< LibraryType, ValueType > const &otherMatrix, std::set< storm::expressions::Variable > const &summationMetaVariables) const
 Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta variables.
 
Add< LibraryType, ValueType > multiplyMatrix (Bdd< LibraryType > const &otherMatrix, std::set< storm::expressions::Variable > const &summationMetaVariables) const
 Multiplies the current ADD (representing a matrix) with the given matrix (given by a BDD) by summing over the given meta variables.
 
Bdd< LibraryType > greater (ValueType const &value) const
 Computes a BDD 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.
 
Bdd< LibraryType > greaterOrEqual (ValueType const &value) const
 Computes a BDD 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.
 
Bdd< LibraryType > less (ValueType const &value) const
 Computes a BDD that represents the function in which all assignments with a function value strictly lower than the given value are mapped to one and all others to zero.
 
Bdd< LibraryType > lessOrEqual (ValueType const &value) const
 Computes a BDD that represents the function in which all assignments with a function value less or equal to the given value are mapped to one and all others to zero.
 
Bdd< LibraryType > notZero () const
 Computes a BDD that represents the function in which all assignments with a function value unequal to zero are mapped to one and all others to zero.
 
Add< LibraryType, ValueType > constrain (Add< LibraryType, ValueType > const &constraint) const
 Computes the constraint of the current ADD with the given constraint.
 
Add< LibraryType, ValueType > restrict (Add< LibraryType, ValueType > const &constraint) const
 Computes the restriction of the current ADD with the given constraint.
 
Bdd< LibraryType > getSupport () const override
 Retrieves the support of the current ADD.
 
virtual uint_fast64_t getNonZeroCount () const override
 Retrieves the number of encodings that are mapped to a non-zero value.
 
virtual uint_fast64_t getLeafCount () const override
 Retrieves the number of leaves of the ADD.
 
virtual uint_fast64_t getNodeCount () const override
 Retrieves the number of nodes necessary to represent the DD.
 
ValueType getMin () const
 Retrieves the lowest function value of any encoding.
 
ValueType getMax () const
 Retrieves the highest function value of any encoding.
 
void setValue (storm::expressions::Variable const &metaVariable, int_fast64_t variableValue, ValueType const &targetValue)
 Sets the function values of all encodings that have the given value of the meta variable to the given target value.
 
void setValue (storm::expressions::Variable const &metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const &metaVariable2, int_fast64_t variableValue2, ValueType const &targetValue)
 Sets the function values of all encodings that have the given values of the two meta variables to the given target value.
 
void setValue (std::map< storm::expressions::Variable, int_fast64_t > const &metaVariableToValueMap=std::map< storm::expressions::Variable, int_fast64_t >(), ValueType const &targetValue=0)
 Sets the function values of all encodings that have the given values of the given meta variables to the given target value.
 
ValueType getValue (std::map< storm::expressions::Variable, int_fast64_t > const &metaVariableToValueMap=std::map< storm::expressions::Variable, int_fast64_t >()) const
 Retrieves the value of the function when all meta variables are assigned the values of the given mapping.
 
bool isOne () const
 Retrieves whether this ADD represents the constant one function.
 
bool isZero () const
 Retrieves whether this ADD represents the constant zero function.
 
bool isConstant () const
 Retrieves whether this ADD represents a constant function.
 
virtual uint_fast64_t getIndex () const override
 Retrieves the index of the topmost variable in the DD.
 
virtual uint_fast64_t getLevel () const override
 Retrieves the level of the topmost variable in the DD.
 
std::vector< ValueType > toVector () const
 Converts the ADD to a vector.
 
std::vector< ValueType > toVector (storm::dd::Odd const &rowOdd) const
 Converts the ADD to a vector.
 
std::vector< ValueType > toVector (storm::dd::Add< LibraryType, ValueType > const &matrix, std::vector< uint_fast64_t > const &rowGroupIndices, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd) const
 Converts the ADD to a row-grouped vector while respecting the row group sizes of the provided matrix.
 
storm::storage::SparseMatrix< ValueType > toMatrix () const
 Converts the ADD to a (sparse) matrix.
 
storm::storage::SparseMatrix< ValueType > toMatrix (storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const
 Converts the ADD to a (sparse) matrix.
 
storm::storage::SparseMatrix< ValueType > toMatrix (std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const
 Converts the ADD to a (sparse) matrix.
 
storm::storage::SparseMatrix< ValueType > toMatrix (std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const
 Converts the ADD to a row-grouped (sparse) matrix.
 
MatrixAndLabeling toLabeledMatrix (std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd, std::vector< std::set< storm::expressions::Variable > > const &labelMetaVariables=std::vector< std::set< storm::expressions::Variable > >()) const
 
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > toMatrixVector (storm::dd::Add< LibraryType, ValueType > const &vector, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const
 Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector.
 
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > toMatrixVector (std::vector< uint_fast64_t > &&rowGroupSizes, storm::dd::Add< LibraryType, ValueType > const &vector, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const
 
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > toMatrixVectors (std::vector< storm::dd::Add< LibraryType, ValueType > > const &vectors, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const
 Converts the ADD to a row-grouped (sparse) matrix and the given vectors to row-grouped vectors.
 
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > toMatrixVectors (std::vector< uint_fast64_t > &&rowGroupSizes, std::vector< storm::dd::Add< LibraryType, ValueType > > const &vectors, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::set< storm::expressions::Variable > const &groupMetaVariables, storm::dd::Odd const &rowOdd, storm::dd::Odd const &columnOdd) const
 
void exportToDot (std::string const &filename, bool showVariablesIfPossible=true) const override
 Exports the DD to the given file in the dot format.
 
virtual void exportToText (std::string const &filename) const override
 Exports the DD to the given file in the dot format.
 
AddIterator< LibraryType, ValueType > begin (bool enumerateDontCareMetaVariables=true) const
 Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
 
AddIterator< LibraryType, ValueType > end () const
 Retrieves an iterator that points past the end of the container.
 
Bdd< LibraryType > toBdd () const
 Converts the ADD to a BDD by mapping all values unequal to zero to 1.
 
Odd createOdd () const
 Creates an ODD based on the current ADD.
 
InternalAdd< LibraryType, ValueType > const & getInternalAdd () const
 Retrieves the internal ADD.
 
InternalDdManager< LibraryType > const & getInternalDdManager () const
 Retrieves the internal ADD.
 
Add< storm::dd::DdType::Sylvan, storm::RationalNumber > sharpenKwekMehlhorn (uint64_t precision) const
 
Add< storm::dd::DdType::Sylvan, storm::RationalNumber > sharpenKwekMehlhorn (uint64_t precision) const
 
- Public Member Functions inherited from storm::dd::Dd< LibraryType >
 Dd ()=default
 
 Dd (Dd< LibraryType > const &other)=default
 
Ddoperator= (Dd< LibraryType > const &other)=default
 
 Dd (Dd< LibraryType > &&other)=default
 
Ddoperator= (Dd< LibraryType > &&other)=default
 
virtual ~Dd ()=default
 
bool containsMetaVariable (storm::expressions::Variable const &metaVariable) const
 Retrieves whether the given meta variable is contained in the DD.
 
bool containsMetaVariables (std::set< storm::expressions::Variable > const &metaVariables) const
 Retrieves whether the given meta variables are all contained in the DD.
 
std::set< storm::expressions::Variable > const & getContainedMetaVariables () const
 Retrieves the set of all meta variables contained in the DD.
 
DdManager< LibraryType > & getDdManager () const
 Retrieves the manager that is responsible for this DD.
 
std::set< storm::expressions::Variable > & getContainedMetaVariables ()
 Retrieves the set of all meta variables contained in the DD.
 
void addMetaVariables (std::set< storm::expressions::Variable > const &metaVariables)
 Adds the given set of meta variables to the DD.
 
void addMetaVariable (storm::expressions::Variable const &metaVariable)
 Adds the given meta variable to the set of meta variables that are contained in this DD.
 
void removeMetaVariable (storm::expressions::Variable const &metaVariable)
 Removes the given meta variable to the set of meta variables that are contained in this DD.
 
void removeMetaVariables (std::set< storm::expressions::Variable > const &metaVariables)
 Removes the given set of meta variables from the DD.
 

Static Public Member Functions

static Add< LibraryType, ValueType > fromVector (DdManager< LibraryType > const &ddManager, std::vector< ValueType > const &values, Odd const &odd, std::set< storm::expressions::Variable > const &metaVariables)
 Builds an ADD representing the given vector.
 

Friends

class DdManager< LibraryType >
 
class Bdd< LibraryType >
 
template<DdType LibraryTypePrime, typename ValueTypePrime >
class Add
 
class bisimulation::InternalSignatureRefiner< LibraryType, ValueType >
 
template<DdType LibraryTypePrime, typename ValueTypePrime >
std::ostream & operator<< (std::ostream &out, Add< LibraryTypePrime, ValueTypePrime > const &add)
 

Additional Inherited Members

- Protected Member Functions inherited from storm::dd::Dd< LibraryType >
std::vector< uint_fast64_t > getSortedVariableIndices () const
 Retrieves the (sorted) list of the variable indices of DD variables contained in this DD.
 
 Dd (DdManager< LibraryType > const &ddManager, std::set< storm::expressions::Variable > const &containedMetaVariables=std::set< storm::expressions::Variable >())
 Creates a DD with the given manager and meta variables.
 
- Static Protected Member Functions inherited from storm::dd::Dd< LibraryType >
static std::set< storm::expressions::VariablejoinMetaVariables (storm::dd::Dd< LibraryType > const &first, storm::dd::Dd< LibraryType > const &second)
 Retrieves the set of meta variables contained in both DDs.
 
static std::set< storm::expressions::VariablesubtractMetaVariables (storm::dd::Dd< LibraryType > const &first, storm::dd::Dd< LibraryType > const &second)
 Retrieves the set of meta variables that are contained in the first but not the second DD.
 

Detailed Description

template<DdType LibraryType, typename ValueType = double>
class storm::dd::Add< LibraryType, ValueType >

Definition at line 33 of file Add.h.

Constructor & Destructor Documentation

◆ Add() [1/3]

template<DdType LibraryType, typename ValueType = double>
storm::dd::Add< LibraryType, ValueType >::Add ( )
default

◆ Add() [2/3]

template<DdType LibraryType, typename ValueType = double>
storm::dd::Add< LibraryType, ValueType >::Add ( Add< LibraryType, ValueType > const &  other)
default

◆ Add() [3/3]

template<DdType LibraryType, typename ValueType = double>
storm::dd::Add< LibraryType, ValueType >::Add ( Add< LibraryType, ValueType > &&  other)
default

Member Function Documentation

◆ begin()

template<DdType LibraryType, typename ValueType >
AddIterator< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::begin ( bool  enumerateDontCareMetaVariables = true) const

Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.

Parameters
enumerateDontCareMetaVariablesIf set to true, all meta variable assignments are enumerated, even if a meta variable does not at all influence the the function value.
Returns
An iterator that points to the first meta variable assignment with a non-zero function value.

Definition at line 1149 of file Add.cpp.

◆ ceil()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::ceil ( ) const

Retrieves the function that ceils all values in the current ADD.

@retur The resulting ADD.

Definition at line 146 of file Add.cpp.

◆ constrain()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::constrain ( Add< LibraryType, ValueType > const &  constraint) const

Computes the constraint of the current ADD with the given constraint.

That is, the function value of the resulting ADD will be the same as the current ones for all assignments mapping to one in the constraint and may be different otherwise.

Parameters
constraintThe constraint to use for the operation.
Returns
The resulting ADD.

Definition at line 436 of file Add.cpp.

◆ createOdd()

template<DdType LibraryType, typename ValueType >
Odd storm::dd::Add< LibraryType, ValueType >::createOdd ( ) const

Creates an ODD based on the current ADD.

Returns
The corresponding ODD.

Definition at line 1192 of file Add.cpp.

◆ end()

template<DdType LibraryType, typename ValueType >
AddIterator< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::end ( ) const

Retrieves an iterator that points past the end of the container.

Returns
An iterator that points past the end of the container.

Definition at line 1161 of file Add.cpp.

◆ equalModuloPrecision()

template<DdType LibraryType, typename ValueType >
bool storm::dd::Add< LibraryType, ValueType >::equalModuloPrecision ( Add< LibraryType, ValueType > const &  other,
ValueType const &  precision,
bool  relative = true 
) const

Checks whether the current and the given ADD represent the same function modulo some given precision.

Parameters
otherThe ADD with which to compare.
precisionAn upper bound on the maximal difference between any two function values that is to be tolerated.
relativeIf set to true, not the absolute values have to be within the precision, but the relative values.

Definition at line 211 of file Add.cpp.

◆ equals()

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::equals ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to one that have identical function values.

Parameters
otherThe ADD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 96 of file Add.cpp.

◆ exportToDot()

template<DdType LibraryType, typename ValueType >
void storm::dd::Add< LibraryType, ValueType >::exportToDot ( std::string const &  filename,
bool  showVariablesIfPossible = true 
) const
overridevirtual

Exports the DD to the given file in the dot format.

Parameters
filenameThe name of the file to which the DD is to be exported.

Implements storm::dd::Dd< LibraryType >.

Definition at line 1139 of file Add.cpp.

◆ exportToText()

template<DdType LibraryType, typename ValueType >
void storm::dd::Add< LibraryType, ValueType >::exportToText ( std::string const &  filename) const
overridevirtual

Exports the DD to the given file in the dot format.

Parameters
filenameThe name of the file to which the DD is to be exported.

Implements storm::dd::Dd< LibraryType >.

Definition at line 1144 of file Add.cpp.

◆ floor()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::floor ( ) const

Retrieves the function that floors all values in the current ADD.

@retur The resulting ADD.

Definition at line 141 of file Add.cpp.

◆ fromVector()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::fromVector ( DdManager< LibraryType > const &  ddManager,
std::vector< ValueType > const &  values,
Odd const &  odd,
std::set< storm::expressions::Variable > const &  metaVariables 
)
static

Builds an ADD representing the given vector.

Parameters
ddManagerThe manager responsible for the ADD.
valuesThe vector that is to be represented by the ADD.
oddThe ODD used for the translation.
metaVariablesThe meta variables used for the translation.
Returns
The resulting ADD.

Definition at line 1178 of file Add.cpp.

◆ getIndex()

template<DdType LibraryType, typename ValueType >
uint_fast64_t storm::dd::Add< LibraryType, ValueType >::getIndex ( ) const
overridevirtual

Retrieves the index of the topmost variable in the DD.

Returns
The index of the topmost variable in DD.

Implements storm::dd::Dd< LibraryType >.

Definition at line 542 of file Add.cpp.

◆ getInternalAdd()

template<DdType LibraryType, typename ValueType >
InternalAdd< LibraryType, ValueType > const & storm::dd::Add< LibraryType, ValueType >::getInternalAdd ( ) const

Retrieves the internal ADD.

Definition at line 1197 of file Add.cpp.

◆ getInternalDdManager()

template<DdType LibraryType, typename ValueType >
InternalDdManager< LibraryType > const & storm::dd::Add< LibraryType, ValueType >::getInternalDdManager ( ) const

Retrieves the internal ADD.

Definition at line 1202 of file Add.cpp.

◆ getLeafCount()

template<DdType LibraryType, typename ValueType >
uint_fast64_t storm::dd::Add< LibraryType, ValueType >::getLeafCount ( ) const
overridevirtual

Retrieves the number of leaves of the ADD.

Returns
The number of leaves of the ADD.

Implements storm::dd::Dd< LibraryType >.

Definition at line 460 of file Add.cpp.

◆ getLevel()

template<DdType LibraryType, typename ValueType >
uint_fast64_t storm::dd::Add< LibraryType, ValueType >::getLevel ( ) const
overridevirtual

Retrieves the level of the topmost variable in the DD.

Returns
The level of the topmost variable in DD.

Implements storm::dd::Dd< LibraryType >.

Definition at line 547 of file Add.cpp.

◆ getMax()

template<DdType LibraryType, typename ValueType >
ValueType storm::dd::Add< LibraryType, ValueType >::getMax ( ) const

Retrieves the highest function value of any encoding.

Returns
The highest function value of any encoding.

Definition at line 475 of file Add.cpp.

◆ getMin()

template<DdType LibraryType, typename ValueType >
ValueType storm::dd::Add< LibraryType, ValueType >::getMin ( ) const

Retrieves the lowest function value of any encoding.

Returns
The lowest function value of any encoding.

Definition at line 470 of file Add.cpp.

◆ getNodeCount()

template<DdType LibraryType, typename ValueType >
uint_fast64_t storm::dd::Add< LibraryType, ValueType >::getNodeCount ( ) const
overridevirtual

Retrieves the number of nodes necessary to represent the DD.

Returns
The number of nodes in this DD.

Implements storm::dd::Dd< LibraryType >.

Definition at line 465 of file Add.cpp.

◆ getNonZeroCount()

template<DdType LibraryType, typename ValueType >
uint_fast64_t storm::dd::Add< LibraryType, ValueType >::getNonZeroCount ( ) const
overridevirtual

Retrieves the number of encodings that are mapped to a non-zero value.

Returns
The number of encodings that are mapped to a non-zero value.

Implements storm::dd::Dd< LibraryType >.

Definition at line 451 of file Add.cpp.

◆ getSupport()

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::getSupport ( ) const
overridevirtual

Retrieves the support of the current ADD.

Returns
The support represented as a BDD.

Implements storm::dd::Dd< LibraryType >.

Definition at line 446 of file Add.cpp.

◆ getValue()

template<DdType LibraryType, typename ValueType >
ValueType storm::dd::Add< LibraryType, ValueType >::getValue ( std::map< storm::expressions::Variable, int_fast64_t > const &  metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>()) const

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.

Parameters
metaVariableToValueMapA mapping of meta variables to their values.
Returns
The value of the function evaluated with the given input.

Definition at line 508 of file Add.cpp.

◆ greater() [1/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greater ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater than the one in the given ADD.

Parameters
otherThe ADD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 116 of file Add.cpp.

◆ greater() [2/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greater ( ValueType const &  value) const

Computes a BDD 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.

Parameters
valueThe value used for the comparison.
Returns
The resulting BDD.

Definition at line 411 of file Add.cpp.

◆ greaterOrEqual() [1/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greaterOrEqual ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater or equal than the one in the given ADD.

Parameters
otherThe ADD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 121 of file Add.cpp.

◆ greaterOrEqual() [2/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::greaterOrEqual ( ValueType const &  value) const

Computes a BDD 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.

Parameters
valueThe value used for the comparison.
Returns
The resulting BDD.

Definition at line 416 of file Add.cpp.

◆ isConstant()

template<DdType LibraryType, typename ValueType >
bool storm::dd::Add< LibraryType, ValueType >::isConstant ( ) const

Retrieves whether this ADD represents a constant function.

Returns
True if this ADD represents a constants function.

Definition at line 537 of file Add.cpp.

◆ isOne()

template<DdType LibraryType, typename ValueType >
bool storm::dd::Add< LibraryType, ValueType >::isOne ( ) const

Retrieves whether this ADD represents the constant one function.

Returns
True if this ADD represents the constant one function.

Definition at line 527 of file Add.cpp.

◆ isZero()

template<DdType LibraryType, typename ValueType >
bool storm::dd::Add< LibraryType, ValueType >::isZero ( ) const

Retrieves whether this ADD represents the constant zero function.

Returns
True if this ADD represents the constant zero function.

Definition at line 532 of file Add.cpp.

◆ less() [1/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::less ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to one whose function value in the first ADD are less than the one in the given ADD.

Parameters
otherThe ADD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 106 of file Add.cpp.

◆ less() [2/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::less ( ValueType const &  value) const

Computes a BDD that represents the function in which all assignments with a function value strictly lower than the given value are mapped to one and all others to zero.

Parameters
valueThe value used for the comparison.
Returns
The resulting BDD.

Definition at line 421 of file Add.cpp.

◆ lessOrEqual() [1/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::lessOrEqual ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or equal than the one in the given ADD.

Parameters
otherThe DD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 111 of file Add.cpp.

◆ lessOrEqual() [2/2]

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::lessOrEqual ( ValueType const &  value) const

Computes a BDD that represents the function in which all assignments with a function value less or equal to the given value are mapped to one and all others to zero.

Parameters
valueThe value used for the comparison.
Returns
The resulting BDD.

Definition at line 426 of file Add.cpp.

◆ logxy()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::logxy ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that represents the logarithm of the current ADD to the bases given by the second ADD.

@other The base function (given as an ADD). @retur The resulting ADD.

Definition at line 136 of file Add.cpp.

◆ maxAbstract()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::maxAbstract ( std::set< storm::expressions::Variable > const &  metaVariables) const

Max-abstracts from the given meta variables.

Parameters
metaVariablesThe meta variables from which to abstract.

Definition at line 198 of file Add.cpp.

◆ maxAbstractRepresentative()

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::maxAbstractRepresentative ( std::set< storm::expressions::Variable > const &  metaVariables) const

Similar to maxAbstract, but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the maximal value.

Parameters
metaVariablesThe meta variables from which to abstract.

Definition at line 205 of file Add.cpp.

◆ maximum()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::maximum ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs.

Parameters
otherThe ADD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 173 of file Add.cpp.

◆ minAbstract()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::minAbstract ( std::set< storm::expressions::Variable > const &  metaVariables) const

Min-abstracts from the given meta variables.

Parameters
metaVariablesThe meta variables from which to abstract.

Definition at line 185 of file Add.cpp.

◆ minAbstractRepresentative()

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::minAbstractRepresentative ( std::set< storm::expressions::Variable > const &  metaVariables) const

Similar to minAbstract, but does not abstract from the variables but rather picks a valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a valuation (of the other variables) that make the function evaluate to the minimal value.

Parameters
metaVariablesThe meta variables from which to abstract.

Definition at line 192 of file Add.cpp.

◆ minimum()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::minimum ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs.

Parameters
otherThe ADD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 168 of file Add.cpp.

◆ mod()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::mod ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that represents the current ADD modulo the given ADD.

@other The modul function (given as an ADD). @retur The resulting ADD.

Definition at line 131 of file Add.cpp.

◆ multiplyMatrix() [1/2]

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::multiplyMatrix ( Add< LibraryType, ValueType > const &  otherMatrix,
std::set< storm::expressions::Variable > const &  summationMetaVariables 
) const

Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta variables.

Parameters
otherMatrixThe matrix with which to multiply.
summationMetaVariablesThe names of the meta variables over which to sum during the matrix- matrix multiplication.
Returns
An ADD representing the result of the matrix-matrix multiplication.

Definition at line 372 of file Add.cpp.

◆ multiplyMatrix() [2/2]

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::multiplyMatrix ( Bdd< LibraryType > const &  otherMatrix,
std::set< storm::expressions::Variable > const &  summationMetaVariables 
) const

Multiplies the current ADD (representing a matrix) with the given matrix (given by a BDD) by summing over the given meta variables.

Parameters
otherMatrixThe matrix with which to multiply.
summationMetaVariablesThe names of the meta variables over which to sum during the matrix- matrix multiplication.
Returns
An ADD representing the result of the matrix-matrix multiplication.

Definition at line 391 of file Add.cpp.

◆ notEquals()

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::notEquals ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that maps all evaluations to one that have distinct function values.

Parameters
otherThe ADD with which to perform the operation.
Returns
The resulting function represented as an ADD.

Definition at line 101 of file Add.cpp.

◆ notZero()

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::notZero ( ) const

Computes a BDD that represents the function in which all assignments with a function value unequal to zero are mapped to one and all others to zero.

Returns
The resulting DD.

Definition at line 431 of file Add.cpp.

◆ operator!=()

template<DdType LibraryType, typename ValueType >
bool storm::dd::Add< LibraryType, ValueType >::operator!= ( Add< LibraryType, ValueType > const &  other) const

Retrieves whether the two DDs represent different functions.

Parameters
otherThe DD that is to be compared with the current one.
Returns
True if the DDs represent the different functions.

Definition at line 38 of file Add.cpp.

◆ operator*()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator* ( Add< LibraryType, ValueType > const &  other) const

Multiplies the two ADDs.

Parameters
otherThe ADD to multiply with the current one.
Returns
The result of the multiplication.

Definition at line 55 of file Add.cpp.

◆ operator*=()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator*= ( Add< LibraryType, ValueType > const &  other)

Multiplies the given ADD with the current one and assigns the result to the current ADD.

Parameters
otherThe ADD to multiply with the current one.
Returns
A reference to the current ADD after the operation.

Definition at line 60 of file Add.cpp.

◆ operator+()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator+ ( Add< LibraryType, ValueType > const &  other) const

Adds the two ADDs.

Parameters
otherThe ADD to add to the current one.
Returns
The result of the addition.

Definition at line 43 of file Add.cpp.

◆ operator+=()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator+= ( Add< LibraryType, ValueType > const &  other)

Adds the given ADD to the current one.

Parameters
otherThe ADD to add to the current one.
Returns
A reference to the current ADD after the operation.

Definition at line 48 of file Add.cpp.

◆ operator-() [1/2]

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator- ( ) const

Subtracts the ADD from the constant zero function.

Returns
The resulting function represented as a ADD.

Definition at line 72 of file Add.cpp.

◆ operator-() [2/2]

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator- ( Add< LibraryType, ValueType > const &  other) const

Subtracts the given ADD from the current one.

Parameters
otherThe ADD to subtract from the current one.
Returns
The result of the subtraction.

Definition at line 67 of file Add.cpp.

◆ operator-=()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator-= ( Add< LibraryType, ValueType > const &  other)

Subtracts the given ADD from the current one and assigns the result to the current ADD.

Parameters
otherThe ADD to subtract from the current one.
Returns
A reference to the current ADD after the operation.

Definition at line 77 of file Add.cpp.

◆ operator/()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::operator/ ( Add< LibraryType, ValueType > const &  other) const

Divides the current ADD by the given one.

Parameters
otherThe ADD by which to divide the current one.
Returns
The result of the division.

Definition at line 84 of file Add.cpp.

◆ operator/=()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > & storm::dd::Add< LibraryType, ValueType >::operator/= ( Add< LibraryType, ValueType > const &  other)

Divides the current ADD by the given one and assigns the result to the current ADD.

Parameters
otherThe ADD by which to divide the current one.
Returns
A reference to the current ADD after the operation.

Definition at line 89 of file Add.cpp.

◆ operator=() [1/2]

template<DdType LibraryType, typename ValueType = double>
Add & storm::dd::Add< LibraryType, ValueType >::operator= ( Add< LibraryType, ValueType > &&  other)
default

◆ operator=() [2/2]

template<DdType LibraryType, typename ValueType = double>
Add & storm::dd::Add< LibraryType, ValueType >::operator= ( Add< LibraryType, ValueType > const &  other)
default

◆ operator==()

template<DdType LibraryType, typename ValueType >
bool storm::dd::Add< LibraryType, ValueType >::operator== ( Add< LibraryType, ValueType > const &  other) const

Retrieves whether the two DDs represent the same function.

Parameters
otherThe DD that is to be compared with the current one.
Returns
True if the DDs represent the same function.

Definition at line 33 of file Add.cpp.

◆ permuteVariables()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::permuteVariables ( std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &  metaVariablePairs) const

Permutes the given pairs of meta variables in the ADD.

The pairs of meta variables must be guaranteed to have the same number of underlying ADD variables. The first component of the i-th entry is substituted by the second component.

Parameters
metaVariablePairsA vector of meta variable pairs that are to be permuted.
Returns
The resulting ADD.

Definition at line 337 of file Add.cpp.

◆ pow()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::pow ( Add< LibraryType, ValueType > const &  other) const

Retrieves the function that represents the current ADD to the power of the given ADD.

@other The exponent function (given as an ADD). @retur The resulting ADD.

Definition at line 126 of file Add.cpp.

◆ renameVariables()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::renameVariables ( std::set< storm::expressions::Variable > const &  from,
std::set< storm::expressions::Variable > const &  to 
) const

Renames the given meta variables in the ADD.

The number of the underlying DD variables of the both meta variable sets needs to agree.

Parameters
fromThe meta variables to be renamed. The current ADD needs to contain all these meta variables.
toThe meta variables that are the target of the renaming process. The current ADD must not contain any of these meta variables.
Returns
The resulting ADD.

Definition at line 216 of file Add.cpp.

◆ renameVariablesAbstract()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::renameVariablesAbstract ( std::set< storm::expressions::Variable > const &  from,
std::set< storm::expressions::Variable > const &  to 
) const

Renames the given meta variables in the ADD.

The number of the underlying DD variables of the from meta variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide, this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables and then performs the renaming.

Parameters
fromThe meta variables to be renamed. The current ADD needs to contain all these meta variables.
toThe meta variables that are the target of the renaming process. The current ADD must not contain any of these meta variables.
Returns
The resulting ADD.

Definition at line 247 of file Add.cpp.

◆ restrict()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::restrict ( Add< LibraryType, ValueType > const &  constraint) const

Computes the restriction of the current ADD 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.

Parameters
constraintThe constraint to use for the operation.
Returns
The resulting ADD.

Definition at line 441 of file Add.cpp.

◆ setValue() [1/3]

template<DdType LibraryType, typename ValueType >
void storm::dd::Add< LibraryType, ValueType >::setValue ( std::map< storm::expressions::Variable, int_fast64_t > const &  metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>(),
ValueType const &  targetValue = 0 
)

Sets the function values of all encodings that have the given values of the given meta variables to the given target value.

Parameters
metaVariableToValueMapA mapping of meta variables to the values they are supposed to have. All values must be within the range of the respective meta variable.
targetValueThe new function value of the modified encodings.

Definition at line 496 of file Add.cpp.

◆ setValue() [2/3]

template<DdType LibraryType, typename ValueType >
void storm::dd::Add< LibraryType, ValueType >::setValue ( storm::expressions::Variable const &  metaVariable,
int_fast64_t  variableValue,
ValueType const &  targetValue 
)

Sets the function values of all encodings that have the given value of the meta variable to the given target value.

Parameters
metaVariableThe meta variable that has to be equal to the given value.
variableValueThe value that the meta variable is supposed to have. This must be within the range of the meta variable.
targetValueThe new function value of the modified encodings.

Definition at line 480 of file Add.cpp.

◆ setValue() [3/3]

template<DdType LibraryType, typename ValueType >
void storm::dd::Add< LibraryType, ValueType >::setValue ( storm::expressions::Variable const &  metaVariable1,
int_fast64_t  variableValue1,
storm::expressions::Variable const &  metaVariable2,
int_fast64_t  variableValue2,
ValueType const &  targetValue 
)

Sets the function values of all encodings that have the given values of the two meta variables to the given target value.

Parameters
metaVariable1The first meta variable that has to be equal to the first given value.
variableValue1The value that the first meta variable is supposed to have. This must be within the range of the meta variable.
metaVariable2The second meta variable that has to be equal to the second given value.
variableValue2The value that the second meta variable is supposed to have. This must be within the range of the meta variable.
targetValueThe new function value of the modified encodings.

Definition at line 487 of file Add.cpp.

◆ sharpenKwekMehlhorn() [1/3]

Add< storm::dd::DdType::Sylvan, storm::RationalNumber > storm::dd::Add< storm::dd::DdType::Sylvan, double >::sharpenKwekMehlhorn ( uint64_t  precision) const

Definition at line 156 of file Add.cpp.

◆ sharpenKwekMehlhorn() [2/3]

Add< storm::dd::DdType::Sylvan, storm::RationalNumber > storm::dd::Add< storm::dd::DdType::Sylvan, storm::RationalNumber >::sharpenKwekMehlhorn ( uint64_t  precision) const

Definition at line 162 of file Add.cpp.

◆ sharpenKwekMehlhorn() [3/3]

template<DdType LibraryType, typename ValueType >
Add< LibraryType, storm::RationalNumber > storm::dd::Add< LibraryType, ValueType >::sharpenKwekMehlhorn ( uint64_t  precision) const

Retrieves the function that sharpens all values in the current ADD with the Kwek-Mehlhorn algorithm.

Returns
The resulting ADD.

Definition at line 151 of file Add.cpp.

◆ sumAbstract()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::sumAbstract ( std::set< storm::expressions::Variable > const &  metaVariables) const

Sum-abstracts from the given meta variables.

Parameters
metaVariablesThe meta variables from which to abstract.

Definition at line 178 of file Add.cpp.

◆ swapVariables()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType > storm::dd::Add< LibraryType, ValueType >::swapVariables ( std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &  metaVariablePairs) const

Swaps the given pairs of meta variables in the ADD.

The pairs of meta variables must be guaranteed to have the same number of underlying ADD variables.

Parameters
metaVariablePairsA vector of meta variable pairs that are to be swapped for one another.
Returns
The resulting ADD.

Definition at line 292 of file Add.cpp.

◆ toBdd()

template<DdType LibraryType, typename ValueType >
Bdd< LibraryType > storm::dd::Add< LibraryType, ValueType >::toBdd ( ) const

Converts the ADD to a BDD by mapping all values unequal to zero to 1.

This effectively does the same as a call to notZero().

Returns
The corresponding BDD.

Definition at line 1187 of file Add.cpp.

◆ toLabeledMatrix()

template<DdType LibraryType, typename ValueType >
Add< LibraryType, ValueType >::MatrixAndLabeling storm::dd::Add< LibraryType, ValueType >::toLabeledMatrix ( std::set< storm::expressions::Variable > const &  rowMetaVariables,
std::set< storm::expressions::Variable > const &  columnMetaVariables,
std::set< storm::expressions::Variable > const &  groupMetaVariables,
storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd,
std::vector< std::set< storm::expressions::Variable > > const &  labelMetaVariables = std::vector<std::set<storm::expressions::Variable>>() 
) const

Definition at line 752 of file Add.cpp.

◆ toMatrix() [1/4]

template<DdType LibraryType, typename ValueType >
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix ( ) const

Converts the ADD to a (sparse) matrix.

All contained non-primed variables are assumed to encode the row, whereas all primed variables are assumed to encode the column.

Returns
The matrix that is represented by this ADD.

Definition at line 634 of file Add.cpp.

◆ toMatrix() [2/4]

template<DdType LibraryType, typename ValueType >
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix ( std::set< storm::expressions::Variable > const &  groupMetaVariables,
storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd 
) const

Converts the ADD to a row-grouped (sparse) 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 ADD.

Note
: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods.
Parameters
groupMetaVariablesThe meta variables that are used to distinguish different row groups.
rowOddThe ODD used for determining the correct row.
columnOddThe ODD used for determining the correct column.
Returns
The matrix that is represented by this ADD.

Definition at line 729 of file Add.cpp.

◆ toMatrix() [3/4]

template<DdType LibraryType, typename ValueType >
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix ( std::set< storm::expressions::Variable > const &  rowMetaVariables,
std::set< storm::expressions::Variable > const &  columnMetaVariables,
storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd 
) const

Converts the ADD to a (sparse) matrix.

The given offset-labeled DDs are used to determine the correct row and column, respectively, for each entry.

Parameters
rowMetaVariablesThe meta variables that encode the rows of the matrix.
columnMetaVariablesThe meta variables that encode the columns of the matrix.
rowOddThe ODD used for determining the correct row.
columnOddThe ODD used for determining the correct column.
Returns
The matrix that is represented by this ADD.

Definition at line 666 of file Add.cpp.

◆ toMatrix() [4/4]

template<DdType LibraryType, typename ValueType >
storm::storage::SparseMatrix< ValueType > storm::dd::Add< LibraryType, ValueType >::toMatrix ( storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd 
) const

Converts the ADD to a (sparse) 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.

Parameters
rowOddThe ODD used for determining the correct row.
columnOddThe ODD used for determining the correct column.
Returns
The matrix that is represented by this ADD.

Definition at line 650 of file Add.cpp.

◆ toMatrixVector() [1/2]

template<DdType LibraryType, typename ValueType >
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > storm::dd::Add< LibraryType, ValueType >::toMatrixVector ( std::vector< uint_fast64_t > &&  rowGroupSizes,
storm::dd::Add< LibraryType, ValueType > const &  vector,
std::set< storm::expressions::Variable > const &  rowMetaVariables,
std::set< storm::expressions::Variable > const &  columnMetaVariables,
std::set< storm::expressions::Variable > const &  groupMetaVariables,
storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd 
) const

Definition at line 953 of file Add.cpp.

◆ toMatrixVector() [2/2]

template<DdType LibraryType, typename ValueType >
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > storm::dd::Add< LibraryType, ValueType >::toMatrixVector ( storm::dd::Add< LibraryType, ValueType > const &  vector,
std::set< storm::expressions::Variable > const &  groupMetaVariables,
storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd 
) const

Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector.

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 ADD.

Note
: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods.
Parameters
vectorThe symbolic vector to convert.
groupMetaVariablesThe meta variables that are used to distinguish different row groups.
rowOddThe ODD used for determining the correct row.
columnOddThe ODD used for determining the correct column.
Returns
The matrix that is represented by this ADD.

Definition at line 916 of file Add.cpp.

◆ toMatrixVectors() [1/2]

template<DdType LibraryType, typename ValueType >
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > storm::dd::Add< LibraryType, ValueType >::toMatrixVectors ( std::vector< storm::dd::Add< LibraryType, ValueType > > const &  vectors,
std::set< storm::expressions::Variable > const &  groupMetaVariables,
storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd 
) const

Converts the ADD to a row-grouped (sparse) matrix and the given vectors to row-grouped vectors.

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 ADD.

Note
: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods.
Parameters
vectorsThe symbolic vectors to convert.
groupMetaVariablesThe meta variables that are used to distinguish different row groups.
rowOddThe ODD used for determining the correct row.
columnOddThe ODD used for determining the correct column.
Returns
The matrix that is represented by this ADD.

Definition at line 962 of file Add.cpp.

◆ toMatrixVectors() [2/2]

template<DdType LibraryType, typename ValueType >
std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< std::vector< ValueType > > > storm::dd::Add< LibraryType, ValueType >::toMatrixVectors ( std::vector< uint_fast64_t > &&  rowGroupSizes,
std::vector< storm::dd::Add< LibraryType, ValueType > > const &  vectors,
std::set< storm::expressions::Variable > const &  rowMetaVariables,
std::set< storm::expressions::Variable > const &  columnMetaVariables,
std::set< storm::expressions::Variable > const &  groupMetaVariables,
storm::dd::Odd const &  rowOdd,
storm::dd::Odd const &  columnOdd 
) const

Definition at line 993 of file Add.cpp.

◆ toValueType() [1/2]

template<DdType LibraryType, typename ValueType >
template<typename TargetValueType >
std::enable_if<!std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type storm::dd::Add< LibraryType, ValueType >::toValueType ( ) const

Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else.

Returns
The resulting function represented as an ADD.

Definition at line 1213 of file Add.cpp.

◆ toValueType() [2/2]

template<DdType LibraryType, typename ValueType = double>
template<typename TargetValueType >
std::enable_if<!std::is_same< TargetValueType, ValueType >::value, Add< LibraryType, TargetValueType > >::type storm::dd::Add< LibraryType, ValueType >::toValueType ( ) const

◆ toVector() [1/3]

template<DdType LibraryType, typename ValueType >
std::vector< ValueType > storm::dd::Add< LibraryType, ValueType >::toVector ( ) const

Converts the ADD to a vector.

Returns
The vector that is represented by this ADD.

Definition at line 552 of file Add.cpp.

◆ toVector() [2/3]

template<DdType LibraryType, typename ValueType >
std::vector< ValueType > storm::dd::Add< LibraryType, ValueType >::toVector ( storm::dd::Add< LibraryType, ValueType > const &  matrix,
std::vector< uint_fast64_t > const &  rowGroupIndices,
std::set< storm::expressions::Variable > const &  rowMetaVariables,
std::set< storm::expressions::Variable > const &  columnMetaVariables,
std::set< storm::expressions::Variable > const &  groupMetaVariables,
storm::dd::Odd const &  rowOdd 
) const

Converts the ADD to a row-grouped vector while respecting the row group sizes of the provided matrix.

That is, if the vector has a zero entry for some row in a row group for which the matrix has a non-zero row, the value at the vector will be correctly set to zero.

Note
: This function assumes that the meta variables used to distinguish different row groups are at the very top of the ADD.
: The order of the rows within the groups could be inconsistent with the order obtained by other toMatrix/toVector methods.
Parameters
matrixThe symbolic matrix whose row group sizes to respect.
rowGroupIndicesA vector specifying the sizes of the row groups.
rowMetaVariablesThe meta variables that encode the rows of the matrix.
columnMetaVariablesThe meta variables that encode the columns of the matrix.
groupMetaVariablesThe meta variables that are used to distinguish different row groups.
rowOddThe ODD used for determining the correct row.
Returns
The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector (if it was given).
The vector that is represented by this ADD.

Definition at line 565 of file Add.cpp.

◆ toVector() [3/3]

template<DdType LibraryType, typename ValueType >
std::vector< ValueType > storm::dd::Add< LibraryType, ValueType >::toVector ( storm::dd::Odd const &  rowOdd) const

Converts the ADD to a vector.

The given offset-labeled DD is used to determine the correct row of each entry.

Parameters
rowOddThe ODD used for determining the correct row.
Returns
The vector that is represented by this ADD.

Definition at line 557 of file Add.cpp.

Friends And Related Symbol Documentation

◆ Add

template<DdType LibraryType, typename ValueType = double>
template<DdType LibraryTypePrime, typename ValueTypePrime >
friend class Add
friend

Definition at line 39 of file Add.h.

◆ Bdd< LibraryType >

template<DdType LibraryType, typename ValueType = double>
friend class Bdd< LibraryType >
friend

Definition at line 1 of file Add.h.

◆ bisimulation::InternalSignatureRefiner< LibraryType, ValueType >

template<DdType LibraryType, typename ValueType = double>
friend class bisimulation::InternalSignatureRefiner< LibraryType, ValueType >
friend

Definition at line 39 of file Add.h.

◆ DdManager< LibraryType >

template<DdType LibraryType, typename ValueType = double>
friend class DdManager< LibraryType >
friend

Definition at line 1 of file Add.h.

◆ operator<<

template<DdType LibraryType, typename ValueType = double>
template<DdType LibraryTypePrime, typename ValueTypePrime >
std::ostream & operator<< ( std::ostream &  out,
Add< LibraryTypePrime, ValueTypePrime > const &  add 
)
friend

The documentation for this class was generated from the following files: