#include <DdManager.h>

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

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

Public Member Functions
	DdManager ()
	Creates an empty manager without any meta variables.

	DdManager (DdManager< LibraryType > const &other)=delete

DdManager< LibraryType > &	operator= (DdManager< LibraryType > const &other)=delete

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

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

std::shared_ptr< DdManager< LibraryType > >	asSharedPointer ()

std::shared_ptr< DdManager< LibraryType > const >	asSharedPointer () const

Bdd< LibraryType >	getBddOne () const
	Retrieves a BDD representing the constant one function.

template<typename ValueType >
Add< LibraryType, ValueType >	getAddOne () const
	Retrieves an ADD representing the constant one function.

Bdd< LibraryType >	getBddZero () const
	Retrieves a BDD representing the constant zero function.

template<typename ValueType >
Add< LibraryType, ValueType >	getAddZero () const
	Retrieves an ADD representing the constant zero function.

template<typename ValueType >
Add< LibraryType, ValueType >	getAddUndefined () const
	Retrieves an ADD representing an undefined value.

template<typename ValueType >
Add< LibraryType, ValueType >	getInfinity () const
	Retrieves an ADD representing the constant infinity function.

template<typename ValueType >
Add< LibraryType, ValueType >	getConstant (ValueType const &value) const
	Retrieves an ADD representing the constant function with the given value.

Bdd< LibraryType >	getEncoding (storm::expressions::Variable const &variable, int_fast64_t value, bool mostSignificantBitAtTop=true) const
	Retrieves the BDD representing the function that maps all inputs which have the given meta variable equal to the given value one.

Bdd< LibraryType >	getRange (storm::expressions::Variable const &variable) const
	Retrieves the BDD representing the range of the meta variable, i.e., a function that maps all legal values of the range of the meta variable to one.

template<typename ValueType >
Add< LibraryType, ValueType >	getIdentity (storm::expressions::Variable const &variable) const
	Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all legal values of the range of the meta variable to the values themselves.

Bdd< LibraryType >	getIdentity (std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &variablePairs, bool restrictToFirstRange=true) const
	Retrieves a BDD in which an encoding is mapped to true iff the meta variables of each pair encode the same value.

Bdd< LibraryType >	getIdentity (storm::expressions::Variable const &first, storm::expressions::Variable const &second, bool restrictToFirstRange=true) const
	Retrieves a BDD in which an encoding is mapped to true iff the two meta variables encode the same value.

Bdd< LibraryType >	getCube (storm::expressions::Variable const &variable) const
	Retrieves a BDD that is the cube of the variables representing the given meta variable.

Bdd< LibraryType >	getCube (std::set< storm::expressions::Variable > const &variables) const
	Retrieves a BDD that is the cube of the variables representing the given meta variables.

std::vector< storm::expressions::Variable >	cloneVariable (storm::expressions::Variable const &variable, std::string const &newVariableName, boost::optional< uint64_t > const &numberOfLayers=boost::none)
	Clones the given meta variable and optionally changes the number of layers of the variable.

std::pair< storm::expressions::Variable, storm::expressions::Variable >	addMetaVariable (std::string const &variableName, int_fast64_t low, int_fast64_t high, boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &position=boost::none)
	Adds an integer meta variable with the given range with two layers (a 'normal' and a 'primed' one).

std::vector< storm::expressions::Variable >	addMetaVariable (std::string const &variableName, int_fast64_t low, int_fast64_t high, uint64_t numberOfLayers, boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &position=boost::none)
	Creates a meta variable with the given number of layers.

std::vector< storm::expressions::Variable >	addBitVectorMetaVariable (std::string const &variableName, uint64_t bits, uint64_t numberOfLayers, boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &position=boost::none)
	Creates a meta variable with the given number of layers.

std::pair< storm::expressions::Variable, storm::expressions::Variable >	addMetaVariable (std::string const &variableName, boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &position=boost::none)
	Adds a boolean meta variable with two layers (a 'normal' and a 'primed' one).

std::vector< storm::expressions::Variable >	addMetaVariable (std::string const &variableName, uint64_t numberOfLayers, boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &position=boost::none)
	Creates a meta variable with the given number of layers.

std::set< std::string >	getAllMetaVariableNames () const
	Retrieves the names of all meta variables that have been added to the manager.

std::size_t	getNumberOfMetaVariables () const
	Retrieves the number of meta variables that are contained in this manager.

bool	hasMetaVariable (std::string const &variableName) const
	Retrieves whether the given meta variable name is already in use.

storm::expressions::Variable	getMetaVariable (std::string const &variableName) const
	Retrieves the given meta variable by name.

bool	supportsOrderedInsertion () const
	Checks whether this manager supports the ordered insertion of variables, i.e.

void	allowDynamicReordering (bool value)
	Sets whether dynamic reordering is allowed for the DDs managed by this manager (if supported).

bool	isDynamicReorderingAllowed () const
	Retrieves whether dynamic reordering is currently allowed (if supported).

void	triggerReordering ()
	Triggers a reordering of the DDs managed by this manager (if supported).

DdMetaVariable< LibraryType > const &	getMetaVariable (storm::expressions::Variable const &variable) const
	Retrieves the meta variable with the given name if it exists.

std::set< storm::expressions::Variable >	getAllMetaVariables () const
	Retrieves the set of meta variables contained in the DD.

std::vector< uint_fast64_t >	getSortedVariableIndices () const
	Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.

std::vector< uint_fast64_t >	getSortedVariableIndices (std::set< storm::expressions::Variable > const &metaVariables) const
	Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.

InternalDdManager< LibraryType > &	getInternalDdManager ()
	Retrieves the internal DD manager.

InternalDdManager< LibraryType > const &	getInternalDdManager () const
	Retrieves the internal DD manager.

void	debugCheck () const
	Performs a debug check if available.

void	execute (std::function< void()> const &f) const
	All code that manipulates DDs shall be called through this function.

Friends
class	Bdd< LibraryType >

template<DdType LibraryTypePrime, typename ValueType >
class	Add

template<DdType LibraryTypePrime, typename ValueType >
class	AddIterator

Detailed Description

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

Definition at line 22 of file DdManager.h.

Constructor & Destructor Documentation

◆ DdManager() [1/3]

template<DdType LibraryType>

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

Creates an empty manager without any meta variables.

Definition at line 17 of file DdManager.cpp.

◆ DdManager() [2/3]

template<DdType LibraryType>

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

delete

◆ DdManager() [3/3]

template<DdType LibraryType>

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

default

Member Function Documentation

◆ addBitVectorMetaVariable()

template<DdType LibraryType>

std::vector< storm::expressions::Variable > storm::dd::DdManager< LibraryType >::addBitVectorMetaVariable	(	std::string const &	variableName,
		uint64_t	bits,
		uint64_t	numberOfLayers,
		boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &	position = `boost::none`
	)

Creates a meta variable with the given number of layers.

Parameters

variableName	The name of the variable.
numberOfLayers	The number of layers of this variable (must be greater or equal 1).

Definition at line 231 of file DdManager.cpp.

◆ addMetaVariable() [1/4]

template<DdType LibraryType>

std::pair< storm::expressions::Variable, storm::expressions::Variable > storm::dd::DdManager< LibraryType >::addMetaVariable	(	std::string const &	variableName,
		boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &	position = `boost::none`
	)

Adds a boolean meta variable with two layers (a 'normal' and a 'primed' one).

Parameters

variableName The name of the new variable.

Definition at line 238 of file DdManager.cpp.

◆ addMetaVariable() [2/4]

template<DdType LibraryType>

std::pair< storm::expressions::Variable, storm::expressions::Variable > storm::dd::DdManager< LibraryType >::addMetaVariable	(	std::string const &	variableName,
		int_fast64_t	low,
		int_fast64_t	high,
		boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &	position = `boost::none`
	)

Adds an integer meta variable with the given range with two layers (a 'normal' and a 'primed' one).

Parameters

variableName	The name of the new variable.
low	The lowest value of the range of the variable.
high	The highest value of the range of the variable.

Definition at line 214 of file DdManager.cpp.

◆ addMetaVariable() [3/4]

template<DdType LibraryType>

std::vector< storm::expressions::Variable > storm::dd::DdManager< LibraryType >::addMetaVariable	(	std::string const &	variableName,
		int_fast64_t	low,
		int_fast64_t	high,
		uint64_t	numberOfLayers,
		boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &	position = `boost::none`
	)

Creates a meta variable with the given number of layers.

Parameters

variableName	The name of the variable.
numberOfLayers	The number of layers of this variable (must be greater or equal 1).

Definition at line 222 of file DdManager.cpp.

◆ addMetaVariable() [4/4]

template<DdType LibraryType>

std::vector< storm::expressions::Variable > storm::dd::DdManager< LibraryType >::addMetaVariable	(	std::string const &	variableName,
		uint64_t	numberOfLayers,
		boost::optional< std::pair< MetaVariablePosition, storm::expressions::Variable > > const &	position = `boost::none`
	)

Creates a meta variable with the given number of layers.

Parameters

variableName	The name of the variable.
numberOfLayers	The number of layers of this variable (must be greater or equal 1).

Definition at line 245 of file DdManager.cpp.

◆ allowDynamicReordering()

template<DdType LibraryType>

void storm::dd::DdManager< LibraryType >::allowDynamicReordering ( bool value )

Sets whether dynamic reordering is allowed for the DDs managed by this manager (if supported).

Parameters

value If set to true, dynamic reordering is allowed and forbidden otherwise.

Definition at line 440 of file DdManager.cpp.

◆ asSharedPointer() [1/2]

template<DdType LibraryType>

std::shared_ptr< DdManager< LibraryType > > storm::dd::DdManager< LibraryType >::asSharedPointer ( )

Definition at line 22 of file DdManager.cpp.

◆ asSharedPointer() [2/2]

template<DdType LibraryType>

std::shared_ptr< DdManager< LibraryType > const > storm::dd::DdManager< LibraryType >::asSharedPointer ( ) const

Definition at line 27 of file DdManager.cpp.

◆ cloneVariable()

template<DdType LibraryType>

std::vector< storm::expressions::Variable > storm::dd::DdManager< LibraryType >::cloneVariable	(	storm::expressions::Variable const &	variable,
		std::string const &	newVariableName,
		boost::optional< uint64_t > const &	numberOfLayers = `boost::none`
	)

Clones the given meta variable and optionally changes the number of layers of the variable.

Parameters

variable	The variable to clone.
newVariableName	The name of the variable to create.
numberOfLayers	The number of layers of the variable to create.

Definition at line 198 of file DdManager.cpp.

◆ debugCheck()

template<DdType LibraryType>

void storm::dd::DdManager< LibraryType >::debugCheck ( ) const

Performs a debug check if available.

Definition at line 503 of file DdManager.cpp.

◆ execute()

template<DdType LibraryType>

void storm::dd::DdManager< LibraryType >::execute ( std::function< void()> const & f ) const

All code that manipulates DDs shall be called through this function.

This is generally needed to set up the correct context. Specifically for sylvan, this is required to make sure that DD-manipulating code is executed as a LACE task. Example usage: manager->execute([&]() { bar = foo(arg1,arg2); }

Parameters

f	the function that is executed

Definition at line 508 of file DdManager.cpp.

◆ getAddOne()

template<DdType LibraryType>

template<typename ValueType >

template Add< DdType::Sylvan, storm::RationalFunction > storm::dd::DdManager< LibraryType >::getAddOne ( ) const

Retrieves an ADD representing the constant one function.

Returns: An ADD representing the constant one function.

Definition at line 38 of file DdManager.cpp.

◆ getAddUndefined()

template<DdType LibraryType>

template<typename ValueType >

template Add< DdType::Sylvan, storm::RationalFunction > storm::dd::DdManager< LibraryType >::getAddUndefined ( ) const

Retrieves an ADD representing an undefined value.

Returns: An ADD representing an undefined value.

Definition at line 55 of file DdManager.cpp.

◆ getAddZero()

template<DdType LibraryType>

template<typename ValueType >

template Add< DdType::Sylvan, storm::RationalFunction > storm::dd::DdManager< LibraryType >::getAddZero ( ) const

Retrieves an ADD representing the constant zero function.

Returns: An ADD representing the constant zero function.

Definition at line 49 of file DdManager.cpp.

◆ getAllMetaVariableNames()

template<DdType LibraryType>

std::set< std::string > storm::dd::DdManager< LibraryType >::getAllMetaVariableNames ( ) const

Retrieves the names of all meta variables that have been added to the manager.

Returns: The set of all meta variable names of the manager.

Definition at line 335 of file DdManager.cpp.

◆ getAllMetaVariables()

template<DdType LibraryType>

std::set< storm::expressions::Variable > storm::dd::DdManager< LibraryType >::getAllMetaVariables ( ) const

Retrieves the set of meta variables contained in the DD.

Returns: All contained meta variables.

Definition at line 455 of file DdManager.cpp.

◆ getBddOne()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::DdManager< LibraryType >::getBddOne ( ) const

Retrieves a BDD representing the constant one function.

Returns: A BDD representing the constant one function.

Definition at line 32 of file DdManager.cpp.

◆ getBddZero()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::DdManager< LibraryType >::getBddZero ( ) const

Retrieves a BDD representing the constant zero function.

Returns: A BDD representing the constant zero function.

Definition at line 43 of file DdManager.cpp.

◆ getConstant()

template<DdType LibraryType>

template<typename ValueType >

template Add< DdType::Sylvan, storm::RationalFunction > storm::dd::DdManager< LibraryType >::getConstant ( ValueType const & value ) const

Retrieves an ADD representing the constant function with the given value.

Returns: An ADD representing the constant function with the given value.

Definition at line 67 of file DdManager.cpp.

◆ getCube() [1/2]

template<DdType LibraryType>

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

Retrieves a BDD that is the cube of the variables representing the given meta variables.

Parameters

variables The expression variables associated with the meta variables.

Returns: The cube of the meta variables.

Definition at line 188 of file DdManager.cpp.

◆ getCube() [2/2]

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::DdManager< LibraryType >::getCube ( storm::expressions::Variable const & variable ) const

Retrieves a BDD that is the cube of the variables representing the given meta variable.

Parameters

variable The expression variable associated with the meta variable.

Returns: The cube of the meta variable.

Definition at line 182 of file DdManager.cpp.

◆ getEncoding()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::DdManager< LibraryType >::getEncoding	(	storm::expressions::Variable const &	variable,
		int_fast64_t	value,
		bool	mostSignificantBitAtTop = `true`
	)		const

Retrieves the BDD representing the function that maps all inputs which have the given meta variable equal to the given value one.

Parameters

variable	The expression variable associated with the meta variable.
value	The value the meta variable is supposed to have.
mostSignificantBitAtTop	A flag indicating whether the most significant bit of the value is to be encoded with the topmost variable or the bottommost.

Returns: The DD representing the function that maps all inputs which have the given meta variable equal to the given value one.

Definition at line 72 of file DdManager.cpp.

◆ getIdentity() [1/3]

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::DdManager< LibraryType >::getIdentity	(	std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	variablePairs,
		bool	restrictToFirstRange = `true`
	)		const

Retrieves a BDD in which an encoding is mapped to true iff the meta variables of each pair encode the same value.

Parameters

variablePairs	The variable pairs for which to compute the identity.
restrictToFirstRange	If set, the identity will be restricted to the legal range of the first variable.

Definition at line 150 of file DdManager.cpp.

◆ getIdentity() [2/3]

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::DdManager< LibraryType >::getIdentity	(	storm::expressions::Variable const &	first,
		storm::expressions::Variable const &	second,
		bool	restrictToFirstRange = `true`
	)		const

Retrieves a BDD in which an encoding is mapped to true iff the two meta variables encode the same value.

Parameters

first	The first meta variable in the identity.
second	The second meta variable in the identity.
restrictToFirstRange	If set, the identity will be restricted to the legal range of the first variable.

Definition at line 160 of file DdManager.cpp.

◆ getIdentity() [3/3]

template<DdType LibraryType>

template<typename ValueType >

template Add< DdType::Sylvan, storm::RationalFunction > storm::dd::DdManager< LibraryType >::getIdentity ( storm::expressions::Variable const & variable ) const

Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all legal values of the range of the meta variable to the values themselves.

Parameters

variable The expression variable associated with the meta variable.

Returns: The identity of the meta variable.

Definition at line 138 of file DdManager.cpp.

◆ getInfinity()

template<DdType LibraryType>

template<typename ValueType >

template Add< DdType::Sylvan, storm::RationalFunction > storm::dd::DdManager< LibraryType >::getInfinity< storm::RationalFunction > ( ) const

Retrieves an ADD representing the constant infinity function.

Returns: An ADD representing the constant infinity function.

Definition at line 61 of file DdManager.cpp.

◆ getInternalDdManager() [1/2]

template<DdType LibraryType>

InternalDdManager< LibraryType > & storm::dd::DdManager< LibraryType >::getInternalDdManager ( )

Retrieves the internal DD manager.

Returns: The internal DD manager.

Definition at line 483 of file DdManager.cpp.

◆ getInternalDdManager() [2/2]

template<DdType LibraryType>

InternalDdManager< LibraryType > const & storm::dd::DdManager< LibraryType >::getInternalDdManager ( ) const

Retrieves the internal DD manager.

Returns: The internal DD manager.

Definition at line 488 of file DdManager.cpp.

◆ getMetaVariable() [1/2]

template<DdType LibraryType>

storm::expressions::Variable storm::dd::DdManager< LibraryType >::getMetaVariable ( std::string const & variableName ) const

Retrieves the given meta variable by name.

Parameters

variableName The name of the variable.

Returns: The meta variable.

Definition at line 354 of file DdManager.cpp.

◆ getMetaVariable() [2/2]

template<DdType LibraryType>

DdMetaVariable< LibraryType > const & storm::dd::DdManager< LibraryType >::getMetaVariable ( storm::expressions::Variable const & variable ) const

Retrieves the meta variable with the given name if it exists.

Parameters

variable The expression variable associated with the meta variable.

Returns: The corresponding meta variable.

Definition at line 324 of file DdManager.cpp.

◆ getNumberOfMetaVariables()

template<DdType LibraryType>

std::size_t storm::dd::DdManager< LibraryType >::getNumberOfMetaVariables ( ) const

Retrieves the number of meta variables that are contained in this manager.

Returns: The number of meta variables contained in this manager.

Definition at line 344 of file DdManager.cpp.

◆ getRange()

template<DdType LibraryType>

Bdd< LibraryType > storm::dd::DdManager< LibraryType >::getRange ( storm::expressions::Variable const & variable ) const

Retrieves the BDD representing the range of the meta variable, i.e., a function that maps all legal values of the range of the meta variable to one.

Parameters

variable The expression variable associated with the meta variable.

Returns: The range of the meta variable.

Definition at line 120 of file DdManager.cpp.

◆ getSortedVariableIndices() [1/2]

template<DdType LibraryType>

std::vector< uint_fast64_t > storm::dd::DdManager< LibraryType >::getSortedVariableIndices ( ) const

Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.

Returns: The sorted list of variable indices.

Definition at line 464 of file DdManager.cpp.

◆ getSortedVariableIndices() [2/2]

template<DdType LibraryType>

std::vector< uint_fast64_t > storm::dd::DdManager< LibraryType >::getSortedVariableIndices ( std::set< storm::expressions::Variable > const & metaVariables ) const

Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.

Parameters

metaVariables The set of meta variables for which to retrieve the index list.

Returns: The sorted list of variable indices.

Definition at line 469 of file DdManager.cpp.

◆ hasMetaVariable()

template<DdType LibraryType>

bool storm::dd::DdManager< LibraryType >::hasMetaVariable ( std::string const & variableName ) const

Retrieves whether the given meta variable name is already in use.

Parameters

variableName The name of the variable.

Returns: True if the given meta variable name is managed by this manager.

Definition at line 349 of file DdManager.cpp.

◆ isDynamicReorderingAllowed()

template<DdType LibraryType>

bool storm::dd::DdManager< LibraryType >::isDynamicReorderingAllowed ( ) const

Retrieves whether dynamic reordering is currently allowed (if supported).

Returns: True iff dynamic reordering is currently allowed.

Definition at line 445 of file DdManager.cpp.

◆ operator=() [1/2]

template<DdType LibraryType>

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

default

◆ operator=() [2/2]

template<DdType LibraryType>

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

delete

◆ supportsOrderedInsertion()

template<DdType LibraryType>

bool storm::dd::DdManager< LibraryType >::supportsOrderedInsertion ( ) const

Checks whether this manager supports the ordered insertion of variables, i.e.

inserting variables at positions between already existing variables.

Returns: True iff the manager supports ordered insertion.

Definition at line 362 of file DdManager.cpp.

◆ triggerReordering()

template<DdType LibraryType>

void storm::dd::DdManager< LibraryType >::triggerReordering ( )

Triggers a reordering of the DDs managed by this manager (if supported).

Definition at line 450 of file DdManager.cpp.

Friends And Related Symbol Documentation

◆ Add

template<DdType LibraryType>

template<DdType LibraryTypePrime, typename ValueType >

friend class Add

friend

Definition at line 27 of file DdManager.h.

◆ AddIterator

template<DdType LibraryType>

template<DdType LibraryTypePrime, typename ValueType >

friend class AddIterator

friend

Definition at line 30 of file DdManager.h.

◆ Bdd< LibraryType >

template<DdType LibraryType>

friend class Bdd< LibraryType >

friend

Definition at line 1 of file DdManager.h.

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

src/storm-gamebased-ar/abstraction/AbstractionInformation.h
src/storm/storage/dd/DdManager.h
src/storm/storage/dd/DdManager.cpp

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ DdManager() [1/3]

◆ DdManager() [2/3]

◆ DdManager() [3/3]

Member Function Documentation

◆ addBitVectorMetaVariable()

◆ addMetaVariable() [1/4]

◆ addMetaVariable() [2/4]

◆ addMetaVariable() [3/4]

◆ addMetaVariable() [4/4]

◆ allowDynamicReordering()

◆ asSharedPointer() [1/2]

◆ asSharedPointer() [2/2]

◆ cloneVariable()

◆ debugCheck()

◆ execute()

◆ getAddOne()

◆ getAddUndefined()

◆ getAddZero()

◆ getAllMetaVariableNames()

◆ getAllMetaVariables()

◆ getBddOne()

◆ getBddZero()

◆ getConstant()

◆ getCube() [1/2]

◆ getCube() [2/2]

◆ getEncoding()

◆ getIdentity() [1/3]

◆ getIdentity() [2/3]

◆ getIdentity() [3/3]

◆ getInfinity()

◆ getInternalDdManager() [1/2]

◆ getInternalDdManager() [2/2]

◆ getMetaVariable() [1/2]

◆ getMetaVariable() [2/2]

◆ getNumberOfMetaVariables()

◆ getRange()

◆ getSortedVariableIndices() [1/2]

◆ getSortedVariableIndices() [2/2]

◆ hasMetaVariable()

◆ isDynamicReorderingAllowed()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ supportsOrderedInsertion()

◆ triggerReordering()

Friends And Related Symbol Documentation

◆ Add

◆ AddIterator

◆ Bdd< LibraryType >