storm::dd Namespace Reference

Namespaces
namespace	bisimulation

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

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)

Variables
template<DdType LibraryType, typename ValueType>
Add< LibraryType, storm::RationalNumber >	Add< LibraryType, ValueType >::sharpenKwekMehlhorn (uint64_t) const
template<typename ValueType>
InternalAdd< DdType::CUDD, storm::RationalNumber >	InternalAdd< DdType::CUDD, ValueType >::sharpenKwekMehlhorn (size_t) const

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 23 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 172 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 1159 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 )

Variable Documentation

Add< LibraryType, ValueType >::sharpenKwekMehlhorn

template<DdType LibraryType, typename ValueType>

Add< LibraryType, storm::RationalNumber > storm::dd::Add< LibraryType, ValueType >::sharpenKwekMehlhorn(uint64_t) const

(

uint64_t

)

const

Definition at line 144 of file Add.cpp.

InternalAdd< DdType::CUDD, ValueType >::sharpenKwekMehlhorn

template<typename ValueType>

InternalAdd< DdType::CUDD, storm::RationalNumber > storm::dd::InternalAdd< DdType::CUDD, ValueType >::sharpenKwekMehlhorn(size_t) const

(

size_t

)

const

Definition at line 1026 of file InternalCuddAdd.cpp.