#include <Dd.h>

Inheritance diagram for storm::dd::Dd< LibraryType >:

[legend]

Public Member Functions
	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

virtual Bdd< LibraryType >	getSupport () const =0
	Retrieves the support of the current DD.

virtual uint_fast64_t	getNonZeroCount () const =0
	Retrieves the number of encodings that are mapped to a non-zero value.

virtual uint_fast64_t	getLeafCount () const =0
	Retrieves the number of leaves of the DD.

virtual uint_fast64_t	getNodeCount () const =0
	Retrieves the number of nodes necessary to represent the DD.

virtual uint_fast64_t	getIndex () const =0
	Retrieves the index of the topmost variable in the DD.

virtual uint_fast64_t	getLevel () const =0
	Retrieves the level of the topmost variable in the DD.

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.

virtual void	exportToDot (std::string const &filename, bool showVariablesIfPossible=true) const =0
	Exports the DD to the given file in the dot format.

virtual void	exportToText (std::string const &filename) const =0
	Exports the DD to the given file in the dot format.

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.

Protected Member Functions
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
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.

Friends
class	DdManager< LibraryType >

Detailed Description

template<DdType LibraryType>
class storm::dd::Dd< LibraryType >

Definition at line 21 of file Dd.h.

Constructor & Destructor Documentation

◆ Dd() [1/4]

template<DdType LibraryType>

storm::dd::Dd< LibraryType >::Dd ( )

default

◆ Dd() [2/4]

template<DdType LibraryType>

storm::dd::Dd< LibraryType >::Dd ( Dd< LibraryType > const & other )

default

◆ Dd() [3/4]

template<DdType LibraryType>

storm::dd::Dd< LibraryType >::Dd ( Dd< LibraryType > && other )

default

◆ ~Dd()

template<DdType LibraryType>

virtual storm::dd::Dd< LibraryType >::~Dd ( )

virtualdefault

◆ Dd() [4/4]

template<DdType LibraryType>

Dd< LibraryType >::Dd	(	DdManager< LibraryType > const &	ddManager,
		std::set< storm::expressions::Variable > const &	containedMetaVariables = `std::set<storm::expressions::Variable>()`
	)

protected

Creates a DD with the given manager and meta variables.

Parameters

ddManager	The manager responsible for this DD.
containedMetaVariables	The meta variables that appear in the DD.

Definition at line 13 of file Dd.cpp.

Member Function Documentation

◆ addMetaVariable()

template<DdType LibraryType>

void Dd< LibraryType >::addMetaVariable ( storm::expressions::Variable const & metaVariable )

Adds the given meta variable to the set of meta variables that are contained in this DD.

Parameters

metaVariable The name of the meta variable to add.

Definition at line 52 of file Dd.cpp.

◆ addMetaVariables()

template<DdType LibraryType>

void Dd< LibraryType >::addMetaVariables ( std::set< storm::expressions::Variable > const & metaVariables )

Adds the given set of meta variables to the DD.

Parameters

metaVariables The set of meta variables to add.

Definition at line 44 of file Dd.cpp.

◆ containsMetaVariable()

template<DdType LibraryType>

bool Dd< LibraryType >::containsMetaVariable ( storm::expressions::Variable const & metaVariable ) const

Retrieves whether the given meta variable is contained in the DD.

Parameters

metaVariable The meta variable for which to query membership.

Returns: True iff the meta variable is contained in the DD.

Definition at line 19 of file Dd.cpp.

◆ containsMetaVariables()

template<DdType LibraryType>

bool Dd< LibraryType >::containsMetaVariables ( std::set< storm::expressions::Variable > const & metaVariables ) const

Retrieves whether the given meta variables are all contained in the DD.

Parameters

metaVariables The meta variables for which to query membership.

Returns: True iff all meta variables are contained in the DD.

Definition at line 24 of file Dd.cpp.

◆ exportToDot()

template<DdType LibraryType>

virtual void storm::dd::Dd< LibraryType >::exportToDot	(	std::string const &	filename,
		bool	showVariablesIfPossible = `true`
	)		const

pure virtual

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.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ exportToText()

template<DdType LibraryType>

virtual void storm::dd::Dd< LibraryType >::exportToText ( std::string const & filename ) const

pure virtual

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.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ getContainedMetaVariables() [1/2]

template<DdType LibraryType>

std::set< storm::expressions::Variable > & Dd< LibraryType >::getContainedMetaVariables ( )

Retrieves the set of all meta variables contained in the DD.

Returns: The set of all meta variables contained in the DD.

Definition at line 34 of file Dd.cpp.

◆ getContainedMetaVariables() [2/2]

template<DdType LibraryType>

std::set< storm::expressions::Variable > const & Dd< LibraryType >::getContainedMetaVariables ( ) const

Retrieves the set of all meta variables contained in the DD.

Returns: The set of all meta variables contained in the DD.

Definition at line 29 of file Dd.cpp.

◆ getDdManager()

template<DdType LibraryType>

DdManager< LibraryType > & Dd< LibraryType >::getDdManager ( ) const

Retrieves the manager that is responsible for this DD.

A pointer to the manager that is responsible for this DD.

Definition at line 39 of file Dd.cpp.

◆ getIndex()

template<DdType LibraryType>

virtual uint_fast64_t storm::dd::Dd< LibraryType >::getIndex ( ) const

pure virtual

Retrieves the index of the topmost variable in the DD.

Returns: The index of the topmost variable in DD.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ getLeafCount()

template<DdType LibraryType>

virtual uint_fast64_t storm::dd::Dd< LibraryType >::getLeafCount ( ) const

pure virtual

Retrieves the number of leaves of the DD.

Returns: The number of leaves of the DD.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ getLevel()

template<DdType LibraryType>

virtual uint_fast64_t storm::dd::Dd< LibraryType >::getLevel ( ) const

pure virtual

Retrieves the level of the topmost variable in the DD.

Returns: The level of the topmost variable in DD.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ getNodeCount()

template<DdType LibraryType>

virtual uint_fast64_t storm::dd::Dd< LibraryType >::getNodeCount ( ) const

pure virtual

Retrieves the number of nodes necessary to represent the DD.

Returns: The number of nodes in this DD.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ getNonZeroCount()

template<DdType LibraryType>

virtual uint_fast64_t storm::dd::Dd< LibraryType >::getNonZeroCount ( ) const

pure virtual

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.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ getSortedVariableIndices()

template<DdType LibraryType>

std::vector< uint_fast64_t > Dd< LibraryType >::getSortedVariableIndices ( ) const

protected

Retrieves the (sorted) list of the variable indices of DD variables contained in this DD.

Returns: The sorted list of variable indices.

Definition at line 70 of file Dd.cpp.

◆ getSupport()

template<DdType LibraryType>

virtual Bdd< LibraryType > storm::dd::Dd< LibraryType >::getSupport ( ) const

pure virtual

Retrieves the support of the current DD.

Returns: The support represented as a BDD.

Implemented in storm::dd::Add< LibraryType, ValueType >, storm::dd::Add< DdType, double >, storm::dd::Add< DdType, ValueType >, storm::dd::Add< Type, double >, storm::dd::Add< Type, ValueType >, storm::dd::Bdd< LibraryType >, storm::dd::Bdd< DdType >, storm::dd::Bdd< storm::dd::DdType::CUDD >, storm::dd::Bdd< storm::dd::DdType::Sylvan >, and storm::dd::Bdd< Type >.

◆ joinMetaVariables()

template<DdType LibraryType>

std::set< storm::expressions::Variable > Dd< LibraryType >::joinMetaVariables	(	storm::dd::Dd< LibraryType > const &	first,
		storm::dd::Dd< LibraryType > const &	second
	)

staticprotected

Retrieves the set of meta variables contained in both DDs.

Parameters

first	The first DD.
second	The second DD.

Returns: The set of all contained meta variables.

Definition at line 75 of file Dd.cpp.

◆ operator=() [1/2]

template<DdType LibraryType>

Dd & storm::dd::Dd< LibraryType >::operator= ( Dd< LibraryType > && other )

default

◆ operator=() [2/2]

template<DdType LibraryType>

Dd & storm::dd::Dd< LibraryType >::operator= ( Dd< LibraryType > const & other )

default

◆ removeMetaVariable()

template<DdType LibraryType>

void Dd< LibraryType >::removeMetaVariable ( storm::expressions::Variable const & metaVariable )

Removes the given meta variable to the set of meta variables that are contained in this DD.

Parameters

metaVariable The name of the meta variable to remove.

Definition at line 57 of file Dd.cpp.

◆ removeMetaVariables()

template<DdType LibraryType>

void Dd< LibraryType >::removeMetaVariables ( std::set< storm::expressions::Variable > const & metaVariables )

Removes the given set of meta variables from the DD.

Parameters

metaVariables The set of meta variables to remove.

Definition at line 62 of file Dd.cpp.

◆ subtractMetaVariables()

template<DdType LibraryType>

std::set< storm::expressions::Variable > Dd< LibraryType >::subtractMetaVariables	(	storm::dd::Dd< LibraryType > const &	first,
		storm::dd::Dd< LibraryType > const &	second
	)

staticprotected

Retrieves the set of meta variables that are contained in the first but not the second DD.

Parameters

first	The first DD.
second	The second DD.

Returns: The resulting set of meta variables.

Definition at line 83 of file Dd.cpp.

Friends And Related Symbol Documentation

◆ DdManager< LibraryType >

template<DdType LibraryType>

friend class DdManager< LibraryType >

friend

Definition at line 1 of file Dd.h.

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

src/storm/models/symbolic/Model.h
src/storm/storage/dd/Dd.h
src/storm/storage/dd/Dd.cpp

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Dd() [1/4]

◆ Dd() [2/4]

◆ Dd() [3/4]

◆ ~Dd()

◆ Dd() [4/4]

Member Function Documentation

◆ addMetaVariable()

◆ addMetaVariables()

◆ containsMetaVariable()

◆ containsMetaVariables()

◆ exportToDot()

◆ exportToText()

◆ getContainedMetaVariables() [1/2]

◆ getContainedMetaVariables() [2/2]

◆ getDdManager()

◆ getIndex()

◆ getLeafCount()

◆ getLevel()

◆ getNodeCount()

◆ getNonZeroCount()

◆ getSortedVariableIndices()

◆ getSupport()

◆ joinMetaVariables()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ removeMetaVariable()

◆ removeMetaVariables()

◆ subtractMetaVariables()

Friends And Related Symbol Documentation

◆ DdManager< LibraryType >