#include <Bdd.h>

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

Collaboration diagram for storm::dd::Bdd< LibraryType >:

Public Member Functions
	Bdd (DdManager< LibraryType > const &ddManager, InternalBdd< LibraryType > const &internalBdd, std::set< storm::expressions::Variable > const &containedMetaVariables=std::set< storm::expressions::Variable >())
	Creates a DD that encapsulates the given internal BDD.

	Bdd ()=default

	Bdd (Bdd< LibraryType > const &other)=default

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

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

Bdd &	operator= (Bdd< LibraryType > &&other)=default

bool	operator== (Bdd< LibraryType > const &other) const
	Retrieves whether the two BDDs represent the same function.

bool	operator!= (Bdd< LibraryType > const &other) const
	Retrieves whether the two BDDs represent different functions.

Bdd< LibraryType >	ite (Bdd< LibraryType > const &thenBdd, Bdd< LibraryType > const &elseBdd) const
	Performs an if-then-else with the given operands, i.e.

template<typename ValueType >
Add< LibraryType, ValueType >	ite (Add< LibraryType, ValueType > const &thenAdd, Add< LibraryType, ValueType > const &elseAdd) const
	Performs an if-then-else with the given operands, i.e.

Bdd< LibraryType >	operator\|\| (Bdd< LibraryType > const &other) const
	Performs a logical or of the current and the given BDD.

Bdd< LibraryType > &	operator\|= (Bdd< LibraryType > const &other)
	Performs a logical or of the current and the given BDD and assigns it to the current BDD.

Bdd< LibraryType >	operator&& (Bdd< LibraryType > const &other) const
	Performs a logical and of the current and the given BDD.

Bdd< LibraryType > &	operator&= (Bdd< LibraryType > const &other)
	Performs a logical and of the current and the given BDD and assigns it to the current BDD.

Bdd< LibraryType >	iff (Bdd< LibraryType > const &other) const
	Performs a logical iff of the current and the given BDD.

Bdd< LibraryType >	exclusiveOr (Bdd< LibraryType > const &other) const
	Performs a logical exclusive-or of the current and the given BDD.

Bdd< LibraryType >	implies (Bdd< LibraryType > const &other) const
	Performs a logical implication of the current and the given BDD.

Bdd< LibraryType >	operator! () const
	Logically inverts the current BDD.

Bdd< LibraryType > &	complement ()
	Logically complements the current BDD.

Bdd< LibraryType >	existsAbstract (std::set< storm::expressions::Variable > const &metaVariables) const
	Existentially abstracts from the given meta variables.

Bdd< LibraryType >	existsAbstractRepresentative (std::set< storm::expressions::Variable > const &metaVariables) const
	Similar to `existsAbstract`, 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 that make the function evaluate to true.

Bdd< LibraryType >	universalAbstract (std::set< storm::expressions::Variable > const &metaVariables) const
	Universally abstracts from the given meta variables.

Bdd< LibraryType >	andExists (Bdd< LibraryType > const &other, std::set< storm::expressions::Variable > const &existentialVariables) const
	Computes the logical and of the current and the given BDD and existentially abstracts from the given set of variables.

Bdd< LibraryType >	constrain (Bdd< LibraryType > const &constraint) const
	Computes the constraint of the current BDD with the given constraint.

Bdd< LibraryType >	restrict (Bdd< LibraryType > const &constraint) const
	Computes the restriction of the current BDD with the given constraint.

Bdd< LibraryType >	relationalProduct (Bdd< LibraryType > const &relation, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables) const
	Computes the relational product of the current BDD and the given BDD representing a relation.

Bdd< LibraryType >	inverseRelationalProduct (Bdd< LibraryType > const &relation, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables) const
	Computes the inverse relational product of the current BDD and the given BDD representing a relation.

Bdd< LibraryType >	inverseRelationalProductWithExtendedRelation (Bdd< LibraryType > const &relation, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables) const
	Computes the inverse relational product of the current BDD and the given BDD representing a relation that contains more variables than just the row and column variables.

Bdd< LibraryType >	swapVariables (std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
	Swaps the given pairs of meta variables in the BDD.

Bdd< LibraryType >	renameVariables (std::set< storm::expressions::Variable > const &from, std::set< storm::expressions::Variable > const &to) const
	Renames the given meta variables in the BDD.

Bdd< LibraryType >	renameVariablesAbstract (std::set< storm::expressions::Variable > const &from, std::set< storm::expressions::Variable > const &to) const
	Renames the given meta variables in the BDD.

Bdd< LibraryType >	renameVariablesConcretize (std::set< storm::expressions::Variable > const &from, std::set< storm::expressions::Variable > const &to) const
	Renames the given meta variables in the BDD.

bool	isOne () const
	Retrieves whether this DD represents the constant one function.

bool	isZero () const
	Retrieves whether this DD represents the constant zero function.

template<typename ValueType >
Add< LibraryType, ValueType >	toAdd () const
	Converts a BDD to an equivalent ADD.

std::vector< Bdd< LibraryType > >	split (std::set< storm::expressions::Variable > const &variables) const
	Splits the BDD along the given variables (must be at the top).

storm::storage::BitVector	toVector (storm::dd::Odd const &rowOdd) const
	Converts the BDD to a bit vector.

std::pair< std::vector< storm::expressions::Expression >, std::unordered_map< uint_fast64_t, storm::expressions::Variable > >	toExpression (storm::expressions::ExpressionManager &manager) const
	Translates the function the BDD is representing to a set of expressions that characterize the function.

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

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

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

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.

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

Odd	createOdd () const
	Creates an ODD based on the current BDD.

template<typename ValueType >
std::vector< ValueType >	filterExplicitVector (Odd const &odd, std::vector< ValueType > const &values) const
	Filters the given explicit vector using the symbolic representation of which values to select.

storm::storage::BitVector	filterExplicitVector (Odd const &odd, storm::storage::BitVector const &values) const
	Filters the given explicit vector using the symbolic representation of which values to select.

InternalBdd< LibraryType > const &	getInternalBdd () const
	Retrieves the internal BDD.

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 Bdd< LibraryType >	getEncoding (DdManager< LibraryType > const &ddManager, uint64_t targetOffset, storm::dd::Odd const &odd, std::set< storm::expressions::Variable > const &metaVariables)
	Constructs the BDD representation of the encoding with the given offset.

static Bdd< LibraryType >	fromVector (DdManager< LibraryType > const &ddManager, storm::storage::BitVector const &truthValues, storm::dd::Odd const &odd, std::set< storm::expressions::Variable > const &metaVariables)
	Constructs a BDD representation of all encodings whose value is true in the given list of truth values.

template<typename ValueType >
static Bdd< LibraryType >	fromVector (DdManager< LibraryType > const &ddManager, std::vector< ValueType > const &explicitValues, storm::dd::Odd const &odd, std::set< storm::expressions::Variable > const &metaVariables, storm::logic::ComparisonType comparisonType, ValueType value)
	Constructs a BDD representation of all encodings that are in the requested relation with the given value.

static Bdd< LibraryType >	getCube (DdManager< LibraryType > const &manager, std::set< storm::expressions::Variable > const &metaVariables)
	Retrieves the cube of all given meta variables.

Friends
class	DdManager< LibraryType >

template<DdType LibraryTypePrime, typename ValueTypePrime >
class	Add

struct	std::hash< storm::dd::Bdd< LibraryType > >

template<DdType LibraryTypePrime, typename ValueType >
struct	FromVectorHelper

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>
class storm::dd::Bdd< LibraryType >

Definition at line 25 of file Bdd.h.

Constructor & Destructor Documentation

◆ Bdd() [1/4]

template<DdType LibraryType>

storm::dd::Bdd< LibraryType >::Bdd	(	DdManager< LibraryType > const &	ddManager,
		InternalBdd< LibraryType > const &	internalBdd,
		std::set< storm::expressions::Variable > const &	containedMetaVariables = `std::set<storm::expressions::Variable>()`
	)

Creates a DD that encapsulates the given internal BDD.

Parameters

ddManager	The manager responsible for this DD.
internalBdd	The internal BDD to store.
containedMetaVariables	The meta variables that appear in the DD.

Definition at line 26 of file Bdd.cpp.

◆ Bdd() [2/4]

template<DdType LibraryType>

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

default

◆ Bdd() [3/4]

template<DdType LibraryType>

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

default

◆ Bdd() [4/4]

template<DdType LibraryType>

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

default

Member Function Documentation

◆ andExists()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::andExists	(	Bdd< LibraryType > const &	other,
		std::set< storm::expressions::Variable > const &	existentialVariables
	)		const

Computes the logical and of the current and the given BDD and existentially abstracts from the given set of variables.

Parameters

other	The second BDD for the logical and.
existentialVariables	The variables from which to existentially abstract.

Returns: A BDD representing the result.

Definition at line 196 of file Bdd.cpp.

◆ complement()

template<DdType LibraryType>

Bdd< LibraryType > & storm::dd::Bdd< LibraryType >::complement ( )

Logically complements the current BDD.

Returns: A reference to the current BDD after the operation.

Definition at line 172 of file Bdd.cpp.

◆ constrain()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::constrain ( Bdd< LibraryType > const & constraint ) const

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

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

Parameters

constraint The constraint to use for the operation.

Returns: The resulting BDD.

Definition at line 210 of file Bdd.cpp.

◆ createOdd()

template<DdType LibraryType>

Odd storm::dd::Bdd< LibraryType >::createOdd ( ) const

Creates an ODD based on the current BDD.

Returns: The corresponding ODD.

Definition at line 571 of file Bdd.cpp.

◆ exclusiveOr()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::exclusiveOr ( Bdd< LibraryType > const & other ) const

Performs a logical exclusive-or of the current and the given BDD.

Parameters

other The second BDD used for the operation.

Returns: The logical exclusive-or of the operands.

Definition at line 157 of file Bdd.cpp.

◆ existsAbstract()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::existsAbstract ( std::set< storm::expressions::Variable > const & metaVariables ) const

Existentially abstracts from the given meta variables.

Parameters

metaVariables The meta variables from which to abstract.

Definition at line 178 of file Bdd.cpp.

◆ existsAbstractRepresentative()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::existsAbstractRepresentative ( std::set< storm::expressions::Variable > const & metaVariables ) const

Similar to existsAbstract, 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 that make the function evaluate to true.

Parameters

metaVariables The meta variables from which to abstract.

Definition at line 184 of file Bdd.cpp.

◆ exportToDot()

template<DdType LibraryType>

void storm::dd::Bdd< LibraryType >::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 552 of file Bdd.cpp.

◆ exportToText()

template<DdType LibraryType>

void storm::dd::Bdd< LibraryType >::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 557 of file Bdd.cpp.

◆ filterExplicitVector() [1/2]

template<DdType LibraryType>

template<typename ValueType >

std::vector< ValueType > storm::dd::Bdd< LibraryType >::filterExplicitVector	(	Odd const &	odd,
		std::vector< ValueType > const &	values
	)		const

Filters the given explicit vector using the symbolic representation of which values to select.

Parameters

odd	The ODD used for the translation from symbolic to explicit.
values	The value vector from which to select the values.

Returns: The resulting vector.

Definition at line 582 of file Bdd.cpp.

◆ filterExplicitVector() [2/2]

template<DdType LibraryType>

storm::storage::BitVector storm::dd::Bdd< LibraryType >::filterExplicitVector	(	Odd const &	odd,
		storm::storage::BitVector const &	values
	)		const

Filters the given explicit vector using the symbolic representation of which values to select.

Parameters

odd	The ODD used for the translation from symbolic to explicit.
values	The value vector from which to select the values.

Returns: The resulting vector.

Definition at line 589 of file Bdd.cpp.

◆ fromVector() [1/2]

template<DdType LibraryType>

template<typename ValueType >

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::fromVector	(	DdManager< LibraryType > const &	ddManager,
		std::vector< ValueType > const &	explicitValues,
		storm::dd::Odd const &	odd,
		std::set< storm::expressions::Variable > const &	metaVariables,
		storm::logic::ComparisonType	comparisonType,
		ValueType	value
	)

static

Constructs a BDD representation of all encodings that are in the requested relation with the given value.

Parameters

ddManager	The DD manager responsible for the resulting BDD.
explicitValues	The explicit values to compare to the given value.
odd	The ODD used for the translation from the explicit representation to a symbolic one.
metaVariables	The meta variables to use for the symbolic encoding.
comparisonType	The relation that needs to hold for the values (wrt. to the given value).
value	The value to compare with.

Definition at line 78 of file Bdd.cpp.

◆ fromVector() [2/2]

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::fromVector	(	DdManager< LibraryType > const &	ddManager,
		storm::storage::BitVector const &	truthValues,
		storm::dd::Odd const &	odd,
		std::set< storm::expressions::Variable > const &	metaVariables
	)

static

Constructs a BDD representation of all encodings whose value is true in the given list of truth values.

Parameters

ddManager	The DD manager responsible for the resulting BDD.
truthValues	The truth values.
odd	The ODD used for the translation from the explicit representation to a symbolic one.
metaVariables	The meta variables to use for the symbolic encoding.

Definition at line 85 of file Bdd.cpp.

◆ getCube()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::getCube	(	DdManager< LibraryType > const &	manager,
		std::set< storm::expressions::Variable > const &	metaVariables
	)

static

Retrieves the cube of all given meta variables.

Parameters

metaVariables The variables for which to create the cube.

Returns: The resulting cube.

Definition at line 562 of file Bdd.cpp.

◆ getEncoding()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::getEncoding	(	DdManager< LibraryType > const &	ddManager,
		uint64_t	targetOffset,
		storm::dd::Odd const &	odd,
		std::set< storm::expressions::Variable > const &	metaVariables
	)

static

Constructs the BDD representation of the encoding with the given offset.

Parameters

ddManager	The DD manager responsible for the resulting BDD.
targetOffset	The offset to encode (interpreted within the ODD).
odd	The ODD used for the translation from the explicit representation to a symbolic one.
metaVariables	The meta variables to use for the symbolic encoding.

Definition at line 94 of file Bdd.cpp.

◆ getIndex()

template<DdType LibraryType>

uint_fast64_t storm::dd::Bdd< LibraryType >::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 532 of file Bdd.cpp.

◆ getInternalBdd()

template<DdType LibraryType>

InternalBdd< LibraryType > const & storm::dd::Bdd< LibraryType >::getInternalBdd ( ) const

Retrieves the internal BDD.

Definition at line 576 of file Bdd.cpp.

◆ getLeafCount()

template<DdType LibraryType>

uint_fast64_t storm::dd::Bdd< LibraryType >::getLeafCount ( ) const

overridevirtual

Retrieves the number of leaves of the DD.

Returns: The number of leaves of the DD.

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

Definition at line 522 of file Bdd.cpp.

◆ getLevel()

template<DdType LibraryType>

uint_fast64_t storm::dd::Bdd< LibraryType >::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 537 of file Bdd.cpp.

◆ getNodeCount()

template<DdType LibraryType>

uint_fast64_t storm::dd::Bdd< LibraryType >::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 527 of file Bdd.cpp.

◆ getNonZeroCount()

template<DdType LibraryType>

uint_fast64_t storm::dd::Bdd< LibraryType >::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 513 of file Bdd.cpp.

◆ getSupport()

template<DdType LibraryType>

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

overridevirtual

Retrieves the support of the current DD.

Returns: The support represented as a BDD.

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

Definition at line 508 of file Bdd.cpp.

◆ iff()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::iff ( Bdd< LibraryType > const & other ) const

Performs a logical iff of the current and the given BDD.

Parameters

other The second BDD used for the operation.

Returns: The logical iff of the operands.

Definition at line 152 of file Bdd.cpp.

◆ implies()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::implies ( Bdd< LibraryType > const & other ) const

Performs a logical implication of the current and the given BDD.

Parameters

other The second BDD used for the operation.

Returns: The logical implication of the operands.

Definition at line 162 of file Bdd.cpp.

◆ inverseRelationalProduct()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::inverseRelationalProduct	(	Bdd< LibraryType > const &	relation,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)		const

Computes the inverse relational product of the current BDD and the given BDD representing a relation.

Note that this operation assumes that the row and column variables are interleaved and that the relation only contains the row and column variables.

Parameters

relation	The relation to use.
rowMetaVariables	The row meta variables used in the relation.
columnMetaVariables	The row meta variables used in the relation.

Returns: The inverse relational product.

Definition at line 246 of file Bdd.cpp.

◆ inverseRelationalProductWithExtendedRelation()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::inverseRelationalProductWithExtendedRelation	(	Bdd< LibraryType > const &	relation,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)		const

Computes the inverse relational product of the current BDD and the given BDD representing a relation that contains more variables than just the row and column variables.

Note that this operation assumes that the row and column variables are interleaved.

Parameters

relation	The relation to use.
rowMetaVariables	The row meta variables used in the relation.
columnMetaVariables	The row meta variables used in the relation.

Returns: The inverse relational product.

Definition at line 273 of file Bdd.cpp.

◆ isOne()

template<DdType LibraryType>

bool storm::dd::Bdd< LibraryType >::isOne ( ) const

Retrieves whether this DD represents the constant one function.

Returns: True if this DD represents the constant one function.

Definition at line 542 of file Bdd.cpp.

◆ isZero()

template<DdType LibraryType>

bool storm::dd::Bdd< LibraryType >::isZero ( ) const

Retrieves whether this DD represents the constant zero function.

Returns: True if this DD represents the constant zero function.

Definition at line 547 of file Bdd.cpp.

◆ ite() [1/2]

template<DdType LibraryType>

template<typename ValueType >

Add< LibraryType, ValueType > storm::dd::Bdd< LibraryType >::ite	(	Add< LibraryType, ValueType > const &	thenAdd,
		Add< LibraryType, ValueType > const &	elseAdd
	)		const

Performs an if-then-else with the given operands, i.e.

maps all valuations that are mapped to true to the function values specified by the first DD and all others to the function values specified by the second DD.

Parameters

thenAdd	The ADD defining the 'then' part.
elseAdd	The ADD defining the 'else' part.

Returns: The resulting ADD.

Definition at line 121 of file Bdd.cpp.

◆ ite() [2/2]

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::ite	(	Bdd< LibraryType > const &	thenBdd,
		Bdd< LibraryType > const &	elseBdd
	)		const

Performs an if-then-else with the given operands, i.e.

maps all valuations that are mapped to a non-zero function value to the function values specified by the first DD and all others to the function values specified by the second DD.

Parameters

thenBdd	The BDD defining the 'then' part.
elseBdd	The BDD defining the 'else' part.

Returns: The resulting BDD.

Definition at line 113 of file Bdd.cpp.

◆ operator!()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::operator! ( ) const

Logically inverts the current BDD.

Returns: The resulting BDD.

Definition at line 167 of file Bdd.cpp.

◆ operator!=()

template<DdType LibraryType>

bool storm::dd::Bdd< LibraryType >::operator!= ( Bdd< LibraryType > const & other ) const

Retrieves whether the two BDDs represent different functions.

Parameters

other The BDD that is to be compared with the current one.

Returns: True if the BDDs represent the different functions.

Definition at line 108 of file Bdd.cpp.

◆ operator&&()

template<DdType LibraryType>

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

Performs a logical and of the current and the given BDD.

Parameters

other The second BDD used for the operation.

Returns: The logical and of the operands.

Definition at line 140 of file Bdd.cpp.

◆ operator&=()

template<DdType LibraryType>

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

Performs a logical and of the current and the given BDD and assigns it to the current BDD.

Parameters

other The second BDD used for the operation.

Returns: A reference to the current BDD after the operation

Definition at line 145 of file Bdd.cpp.

◆ operator=() [1/2]

template<DdType LibraryType>

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

default

◆ operator=() [2/2]

template<DdType LibraryType>

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

default

◆ operator==()

template<DdType LibraryType>

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

Retrieves whether the two BDDs represent the same function.

Parameters

other The BDD that is to be compared with the current one.

Returns: True if the BDDs represent the same function.

Definition at line 103 of file Bdd.cpp.

◆ operator|=()

template<DdType LibraryType>

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

Performs a logical or of the current and the given BDD and assigns it to the current BDD.

Parameters

other The second BDD used for the operation.

Returns: A reference to the current BDD after the operation

Definition at line 133 of file Bdd.cpp.

◆ operator||()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::operator|| ( Bdd< LibraryType > const & other ) const

Performs a logical or of the current and the given BDD.

Parameters

other The second BDD used for the operation.

Returns: The logical or of the operands.

Definition at line 128 of file Bdd.cpp.

◆ relationalProduct()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::relationalProduct	(	Bdd< LibraryType > const &	relation,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)		const

Computes the relational product of the current BDD and the given BDD representing a relation.

Note that this operation assumes that the row and column variables are interleaved and that the relation only contains the row and column variables.

Parameters

relation	The relation to use.
rowMetaVariables	The row meta variables used in the relation.
columnMetaVariables	The row meta variables used in the relation.

Returns: The relational product.

Definition at line 220 of file Bdd.cpp.

◆ renameVariables()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::renameVariables	(	std::set< storm::expressions::Variable > const &	from,
		std::set< storm::expressions::Variable > const &	to
	)		const

Renames the given meta variables in the BDD.

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 BDD needs to contain all these meta variables.
to	The meta variables that are the target of the renaming process. The current BDD must not contain any of these meta variables.

Returns: The resulting BDD.

Definition at line 347 of file Bdd.cpp.

◆ renameVariablesAbstract()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::renameVariablesAbstract	(	std::set< storm::expressions::Variable > const &	from,
		std::set< storm::expressions::Variable > const &	to
	)		const

Renames the given meta variables in the BDD.

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 377 of file Bdd.cpp.

◆ renameVariablesConcretize()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::renameVariablesConcretize	(	std::set< storm::expressions::Variable > const &	from,
		std::set< storm::expressions::Variable > const &	to
	)		const

Renames the given meta variables in the BDD.

The number of the underlying DD variables of the from meta variable set needs to be at most as large as the to meta variable set. If the amount of variables coincide, this operation coincides with renameVariables. Otherwise, it first adds a unique encoding in terms of 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 422 of file Bdd.cpp.

◆ restrict()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::restrict ( Bdd< LibraryType > const & constraint ) const

Computes the restriction of the current BDD with the given constraint.

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

Parameters

constraint The constraint to use for the operation.

Returns: The resulting BDD.

Definition at line 215 of file Bdd.cpp.

◆ split()

template<DdType LibraryType>

std::vector< Bdd< LibraryType > > storm::dd::Bdd< LibraryType >::split ( std::set< storm::expressions::Variable > const & variables ) const

Splits the BDD along the given variables (must be at the top).

Definition at line 473 of file Bdd.cpp.

◆ swapVariables()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::swapVariables ( std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & metaVariablePairs ) const

Swaps the given pairs of meta variables in the BDD.

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

Parameters

metaVariablePairs A vector of meta variable pairs that are to be swapped for one another.

Returns: The resulting BDD.

Definition at line 302 of file Bdd.cpp.

◆ toAdd()

template<DdType LibraryType>

template<typename ValueType >

template Add< DdType::Sylvan, uint_fast64_t > storm::dd::Bdd< LibraryType >::toAdd ( ) const

Converts a BDD to an equivalent ADD.

Returns: The corresponding ADD.

Definition at line 468 of file Bdd.cpp.

◆ toExpression()

template<DdType LibraryType>

std::pair< std::vector< storm::expressions::Expression >, std::unordered_map< uint_fast64_t, storm::expressions::Variable > > storm::dd::Bdd< LibraryType >::toExpression ( storm::expressions::ExpressionManager & manager ) const

Translates the function the BDD is representing to a set of expressions that characterize the function.

Parameters

manager The manager that is used to build the expression and, in particular, create new variables in.

Returns: A list of expressions representing the function of the BDD and a mapping of DD variable indices to the variables that represent these variables in the expressions.

Definition at line 502 of file Bdd.cpp.

◆ toVector()

template<DdType LibraryType>

storm::storage::BitVector storm::dd::Bdd< LibraryType >::toVector ( storm::dd::Odd const & rowOdd ) const

Converts the BDD to a bit 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 bit vector that is represented by this BDD.

Definition at line 497 of file Bdd.cpp.

◆ universalAbstract()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::Bdd< LibraryType >::universalAbstract ( std::set< storm::expressions::Variable > const & metaVariables ) const

Universally abstracts from the given meta variables.

Parameters

metaVariables The meta variables from which to abstract.

Definition at line 190 of file Bdd.cpp.

Friends And Related Symbol Documentation

◆ Add

template<DdType LibraryType>

template<DdType LibraryTypePrime, typename ValueTypePrime >

friend class Add

friend

Definition at line 30 of file Bdd.h.

◆ DdManager< LibraryType >

template<DdType LibraryType>

friend class DdManager< LibraryType >

friend

Definition at line 1 of file Bdd.h.

◆ FromVectorHelper

template<DdType LibraryType>

template<DdType LibraryTypePrime, typename ValueType >

friend struct FromVectorHelper

friend

Definition at line 437 of file Bdd.h.

◆ std::hash< storm::dd::Bdd< LibraryType > >

template<DdType LibraryType>

friend struct std::hash< storm::dd::Bdd< LibraryType > >

friend

Definition at line 432 of file Bdd.h.

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

src/storm-gamebased-ar/abstraction/ExpressionTranslator.h
src/storm/storage/dd/Bdd.h
src/storm/storage/dd/Bdd.cpp

Public Member Functions

Static Public Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ Bdd() [1/4]

◆ Bdd() [2/4]

◆ Bdd() [3/4]

◆ Bdd() [4/4]

Member Function Documentation

◆ andExists()

◆ complement()

◆ constrain()

◆ createOdd()

◆ exclusiveOr()

◆ existsAbstract()

◆ existsAbstractRepresentative()

◆ exportToDot()

◆ exportToText()

◆ filterExplicitVector() [1/2]

◆ filterExplicitVector() [2/2]

◆ fromVector() [1/2]

◆ fromVector() [2/2]

◆ getCube()

◆ getEncoding()

◆ getIndex()

◆ getInternalBdd()

◆ getLeafCount()

◆ getLevel()

◆ getNodeCount()

◆ getNonZeroCount()

◆ getSupport()

◆ iff()

◆ implies()

◆ inverseRelationalProduct()

◆ inverseRelationalProductWithExtendedRelation()

◆ isOne()

◆ isZero()

◆ ite() [1/2]

◆ ite() [2/2]

◆ operator!()

◆ operator!=()

◆ operator&&()

◆ operator&=()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ operator|=()

◆ operator||()

◆ relationalProduct()

◆ renameVariables()

◆ renameVariablesAbstract()

◆ renameVariablesConcretize()

◆ restrict()

◆ split()

◆ swapVariables()

◆ toAdd()

◆ toExpression()

◆ toVector()

◆ universalAbstract()

Friends And Related Symbol Documentation

◆ Add

◆ DdManager< LibraryType >

◆ FromVectorHelper

◆ std::hash< storm::dd::Bdd< LibraryType > >