#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

Add &	operator= (Add< LibraryType, ValueType > const &other)=default

	Add (Add< LibraryType, ValueType > &&other)=default

Add &	operator= (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

Dd &	operator= (Dd< LibraryType > const &other)=default

	Dd (Dd< LibraryType > &&other)=default

Dd &	operator= (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::Variable >	joinMetaVariables (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::Variable >	subtractMetaVariables (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

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.

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

constraint The 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

other	The ADD with which to compare.
precision	An upper bound on the maximal difference between any two function values that is to be tolerated.
relative	If 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

other The 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

filename The 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

filename The 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

ddManager	The manager responsible for the ADD.
values	The vector that is to be represented by the ADD.
odd	The ODD used for the translation.
metaVariables	The 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

metaVariableToValueMap A 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

other The 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

value The 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

other The 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

value The 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

other The 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

value The 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

other The 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

value The 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

metaVariables The 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

metaVariables The 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

other The 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

metaVariables The 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

metaVariables The 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

other The 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

otherMatrix	The matrix with which to multiply.
summationMetaVariables	The 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

otherMatrix	The matrix with which to multiply.
summationMetaVariables	The 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

other The 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

other The 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

other The 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

other The 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

other The 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

other The 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

other The 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

other The 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

other The 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

other The 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

other The 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

metaVariablePairs A 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

from	The meta variables to be renamed. The current ADD needs to contain all these meta variables.
to	The 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

from	The meta variables to be renamed. The current ADD needs to contain all these meta variables.
to	The 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

constraint The 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

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.
targetValue	The 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

metaVariable	The meta variable that has to be equal to the given value.
variableValue	The value that the meta variable is supposed to have. This must be within the range of the meta variable.
targetValue	The 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

metaVariable1	The first meta variable that has to be equal to the first given value.
variableValue1	The value that the first meta variable is supposed to have. This must be within the range of the meta variable.
metaVariable2	The second meta variable that has to be equal to the second given value.
variableValue2	The value that the second meta variable is supposed to have. This must be within the range of the meta variable.
targetValue	The 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

metaVariables The 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

metaVariablePairs A 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

groupMetaVariables	The meta variables that are used to distinguish different row groups.
rowOdd	The ODD used for determining the correct row.
columnOdd	The 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

rowMetaVariables	The meta variables that encode the rows of the matrix.
columnMetaVariables	The meta variables that encode the columns of the matrix.
rowOdd	The ODD used for determining the correct row.
columnOdd	The 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

rowOdd	The ODD used for determining the correct row.
columnOdd	The 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

vector	The symbolic vector to convert.
groupMetaVariables	The meta variables that are used to distinguish different row groups.
rowOdd	The ODD used for determining the correct row.
columnOdd	The 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

vectors	The symbolic vectors to convert.
groupMetaVariables	The meta variables that are used to distinguish different row groups.
rowOdd	The ODD used for determining the correct row.
columnOdd	The 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

matrix	The symbolic matrix whose row group sizes to respect.
rowGroupIndices	A vector specifying the sizes of the row groups.
rowMetaVariables	The meta variables that encode the rows of the matrix.
columnMetaVariables	The meta variables that encode the columns of the matrix.
groupMetaVariables	The meta variables that are used to distinguish different row groups.
rowOdd	The 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

rowOdd The 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:

src/storm-gamebased-ar/abstraction/jani/EdgeAbstractor.h
src/storm/storage/dd/Add.h
src/storm/storage/dd/Add.cpp

Classes

Public Member Functions

Static Public Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ Add() [1/3]

◆ Add() [2/3]

◆ Add() [3/3]

Member Function Documentation

◆ begin()

◆ ceil()

◆ constrain()

◆ createOdd()

◆ end()

◆ equalModuloPrecision()

◆ equals()

◆ exportToDot()

◆ exportToText()

◆ floor()

◆ fromVector()

◆ getIndex()

◆ getInternalAdd()

◆ getInternalDdManager()

◆ getLeafCount()

◆ getLevel()

◆ getMax()

◆ getMin()

◆ getNodeCount()

◆ getNonZeroCount()

◆ getSupport()

◆ getValue()

◆ greater() [1/2]

◆ greater() [2/2]

◆ greaterOrEqual() [1/2]

◆ greaterOrEqual() [2/2]

◆ isConstant()

◆ isOne()

◆ isZero()

◆ less() [1/2]

◆ less() [2/2]

◆ lessOrEqual() [1/2]

◆ lessOrEqual() [2/2]

◆ logxy()

◆ maxAbstract()

◆ maxAbstractRepresentative()

◆ maximum()

◆ minAbstract()

◆ minAbstractRepresentative()

◆ minimum()

◆ mod()

◆ multiplyMatrix() [1/2]

◆ multiplyMatrix() [2/2]

◆ notEquals()

◆ notZero()

◆ operator!=()

◆ operator*()

◆ operator*=()

◆ operator+()

◆ operator+=()

◆ operator-() [1/2]

◆ operator-() [2/2]

◆ operator-=()

◆ operator/()

◆ operator/=()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ permuteVariables()

◆ pow()

◆ renameVariables()

◆ renameVariablesAbstract()

◆ restrict()

◆ setValue() [1/3]

◆ setValue() [2/3]

◆ setValue() [3/3]

◆ sharpenKwekMehlhorn() [1/3]

◆ sharpenKwekMehlhorn() [2/3]

◆ sharpenKwekMehlhorn() [3/3]