storm::dd Namespace Reference

Namespaces
namespace	bisimulation

Classes
class	Add
class	AddIterator
class	AddIterator< DdType::CUDD, ValueType >
class	AddIterator< DdType::Sylvan, ValueType >
class	Bdd
class	BisimulationDecomposition
class	Dd
class	DdManager
class	DdMetaVariable
struct	FromVectorHelper
struct	FromVectorHelper< LibraryType, storm::RationalFunction >
class	InternalAdd
class	InternalAdd< DdType::CUDD, ValueType >
class	InternalAdd< DdType::Sylvan, ValueType >
class	InternalBdd
class	InternalBdd< DdType::CUDD >
class	InternalBdd< DdType::Sylvan >
class	InternalDdManager
class	InternalDdManager< DdType::CUDD >
class	InternalDdManager< DdType::Sylvan >
class	Odd

Enumerations
enum class	MetaVariableType { Bool , Int , BitVector }
enum class	MetaVariablePosition { Above , Below }
enum class	DdType { CUDD , Sylvan }

Functions
template<DdType LibraryType, typename ValueType >
std::ostream &	operator<< (std::ostream &out, Add< LibraryType, ValueType > const &add)
template std::ostream &	operator<< (std::ostream &out, Add< storm::dd::DdType::CUDD, double > const &add)
template std::ostream &	operator<< (std::ostream &out, Add< storm::dd::DdType::Sylvan, double > const &add)
template std::ostream &	operator<< (std::ostream &out, Add< storm::dd::DdType::CUDD, storm::RationalNumber > const &add)
template std::ostream &	operator<< (std::ostream &out, Add< storm::dd::DdType::Sylvan, storm::RationalNumber > const &add)
template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< PartitionRefiner< DdType, ValueType > >	createRefiner (storm::models::symbolic::Model< DdType, ValueType > const &model, Partition< DdType, ValueType > const &initialPartition)
void	getEncodingRec (Odd const &odd, uint64_t index, uint64_t offset, storm::storage::BitVector &result)

Enumeration Type Documentation

DdType

enum class storm::dd::DdType

strong

Enumerator
CUDD
Sylvan

Definition at line 5 of file DdType.h.

MetaVariablePosition

enum class storm::dd::MetaVariablePosition

strong

Enumerator
Above
Below

Definition at line 20 of file DdMetaVariable.h.

MetaVariableType

enum class storm::dd::MetaVariableType

strong

Enumerator
Bool
Int
BitVector

Definition at line 18 of file DdMetaVariable.h.

Function Documentation

createRefiner()

template<storm::dd::DdType DdType, typename ValueType >

std::unique_ptr< PartitionRefiner< DdType, ValueType > > storm::dd::createRefiner	(	storm::models::symbolic::Model< DdType, ValueType > const &	model,
		Partition< DdType, ValueType > const &	initialPartition
	)

Definition at line 26 of file BisimulationDecomposition.cpp.

getEncodingRec()

void storm::dd::getEncodingRec	(	Odd const &	odd,
		uint64_t	index,
		uint64_t	offset,
		storm::storage::BitVector &	result
	)

Definition at line 173 of file Odd.cpp.

operator<<() [1/5]

template<DdType LibraryType, typename ValueType >

std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< LibraryType, ValueType > const &	add
	)

Definition at line 1162 of file Add.cpp.

operator<<() [2/5]

template std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< storm::dd::DdType::CUDD, double > const &	add
	)

operator<<() [3/5]

template std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< storm::dd::DdType::CUDD, storm::RationalNumber > const &	add
	)

operator<<() [4/5]

template std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< storm::dd::DdType::Sylvan, double > const &	add
	)

operator<<() [5/5]

template std::ostream & storm::dd::operator<<	(	std::ostream &	out,
		Add< storm::dd::DdType::Sylvan, storm::RationalNumber > const &	add
	)