Storm
A Modern Probabilistic Model Checker
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Public Member Functions | List of all members
storm::dd::InternalAdd< Type, ValueType > Class Template Reference

Public Member Functions

bool equalModuloPrecision (InternalAdd< DdType::CUDD, storm::RationalNumber > const &, storm::RationalNumber const &, bool) const
 
InternalBdd< DdType::CUDD > greater (storm::RationalNumber const &value) const
 
InternalBdd< DdType::CUDD > greaterOrEqual (storm::RationalNumber const &value) const
 
InternalBdd< DdType::CUDD > less (storm::RationalNumber const &value) const
 
InternalBdd< DdType::CUDD > lessOrEqual (storm::RationalNumber const &value) const
 
DdNode * fromVectorRec (::DdManager *manager, uint_fast64_t &currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector< storm::RationalNumber > const &values, Odd const &odd, std::vector< uint_fast64_t > const &ddVariableIndices)
 
storm::RationalNumber getValue (MTBDD const &node)
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > operator+ (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > & operator+= (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other)
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > operator* (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > & operator*= (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other)
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > operator- (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > & operator-= (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other)
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > operator/ (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > & operator/= (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other)
 
InternalBdd< DdType::Sylvan > equals (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalBdd< DdType::Sylvan > less (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalBdd< DdType::Sylvan > lessOrEqual (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > pow (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > mod (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > logxy (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > floor () const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > ceil () const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > minimum (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > maximum (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &other) const
 
InternalAdd< DdType::Sylvan, double > toValueType () const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > toValueType () const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > sumAbstract (InternalBdd< DdType::Sylvan > const &cube) const
 
InternalBdd< DdType::Sylvan > minAbstractRepresentative (InternalBdd< DdType::Sylvan > const &cube) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > minAbstract (InternalBdd< DdType::Sylvan > const &cube) const
 
InternalBdd< DdType::Sylvan > maxAbstractRepresentative (InternalBdd< DdType::Sylvan > const &cube) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > maxAbstract (InternalBdd< DdType::Sylvan > const &cube) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > multiplyMatrix (InternalAdd< DdType::Sylvan, storm::RationalNumber > const &otherMatrix, std::vector< InternalBdd< DdType::Sylvan > > const &summationDdVariables) const
 
InternalAdd< DdType::Sylvan, storm::RationalNumber > multiplyMatrix (InternalBdd< DdType::Sylvan > const &otherMatrix, std::vector< InternalBdd< DdType::Sylvan > > const &summationDdVariables) const
 
InternalBdd< DdType::Sylvan > greater (storm::RationalNumber const &value) const
 
InternalBdd< DdType::Sylvan > greaterOrEqual (storm::RationalNumber const &value) const
 
storm::RationalNumber getMin () const
 
storm::RationalNumber getMax () const
 

Detailed Description

template<DdType Type, typename ValueType>
class storm::dd::InternalAdd< Type, ValueType >

Definition at line 23 of file CuddAddIterator.h.

Member Function Documentation

◆ ceil()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::ceil ( ) const

Definition at line 411 of file InternalSylvanAdd.cpp.

◆ equalModuloPrecision()

bool storm::dd::InternalAdd< DdType::CUDD, storm::RationalNumber >::equalModuloPrecision ( InternalAdd< DdType::CUDD, storm::RationalNumber > const &  ,
storm::RationalNumber const &  ,
bool   
) const

Definition at line 200 of file InternalCuddAdd.cpp.

◆ equals()

InternalBdd< DdType::Sylvan > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::equals ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 267 of file InternalSylvanAdd.cpp.

◆ floor()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::floor ( ) const

Definition at line 394 of file InternalSylvanAdd.cpp.

◆ fromVectorRec()

DdNode * storm::dd::InternalAdd< DdType::CUDD, storm::RationalNumber >::fromVectorRec ( ::DdManager *  manager,
uint_fast64_t &  currentOffset,
uint_fast64_t  currentLevel,
uint_fast64_t  maxLevel,
std::vector< storm::RationalNumber > const &  values,
Odd const &  odd,
std::vector< uint_fast64_t > const &  ddVariableIndices 
)

Definition at line 871 of file InternalCuddAdd.cpp.

◆ getMax()

storm::RationalNumber storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::getMax ( ) const

Definition at line 816 of file InternalSylvanAdd.cpp.

◆ getMin()

storm::RationalNumber storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::getMin ( ) const

Definition at line 799 of file InternalSylvanAdd.cpp.

◆ getValue()

storm::RationalNumber storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::getValue ( MTBDD const &  node)

Definition at line 58 of file InternalSylvanAdd.cpp.

◆ greater() [1/2]

InternalBdd< DdType::CUDD > storm::dd::InternalAdd< DdType::CUDD, storm::RationalNumber >::greater ( storm::RationalNumber const &  value) const

Definition at line 263 of file InternalCuddAdd.cpp.

◆ greater() [2/2]

InternalBdd< DdType::Sylvan > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::greater ( storm::RationalNumber const &  value) const

Definition at line 717 of file InternalSylvanAdd.cpp.

◆ greaterOrEqual() [1/2]

InternalBdd< DdType::CUDD > storm::dd::InternalAdd< DdType::CUDD, storm::RationalNumber >::greaterOrEqual ( storm::RationalNumber const &  value) const

Definition at line 273 of file InternalCuddAdd.cpp.

◆ greaterOrEqual() [2/2]

InternalBdd< DdType::Sylvan > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::greaterOrEqual ( storm::RationalNumber const &  value) const

Definition at line 734 of file InternalSylvanAdd.cpp.

◆ less() [1/2]

InternalBdd< DdType::Sylvan > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::less ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 290 of file InternalSylvanAdd.cpp.

◆ less() [2/2]

InternalBdd< DdType::CUDD > storm::dd::InternalAdd< DdType::CUDD, storm::RationalNumber >::less ( storm::RationalNumber const &  value) const

Definition at line 283 of file InternalCuddAdd.cpp.

◆ lessOrEqual() [1/2]

InternalBdd< DdType::Sylvan > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::lessOrEqual ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 308 of file InternalSylvanAdd.cpp.

◆ lessOrEqual() [2/2]

InternalBdd< DdType::CUDD > storm::dd::InternalAdd< DdType::CUDD, storm::RationalNumber >::lessOrEqual ( storm::RationalNumber const &  value) const

Definition at line 293 of file InternalCuddAdd.cpp.

◆ logxy()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::logxy ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  ) const

Definition at line 375 of file InternalSylvanAdd.cpp.

◆ maxAbstract()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::maxAbstract ( InternalBdd< DdType::Sylvan > const &  cube) const

Definition at line 565 of file InternalSylvanAdd.cpp.

◆ maxAbstractRepresentative()

InternalBdd< DdType::Sylvan > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::maxAbstractRepresentative ( InternalBdd< DdType::Sylvan > const &  cube) const

Definition at line 560 of file InternalSylvanAdd.cpp.

◆ maximum()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::maximum ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 459 of file InternalSylvanAdd.cpp.

◆ minAbstract()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::minAbstract ( InternalBdd< DdType::Sylvan > const &  cube) const

Definition at line 536 of file InternalSylvanAdd.cpp.

◆ minAbstractRepresentative()

InternalBdd< DdType::Sylvan > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::minAbstractRepresentative ( InternalBdd< DdType::Sylvan > const &  cube) const

Definition at line 531 of file InternalSylvanAdd.cpp.

◆ minimum()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::minimum ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 440 of file InternalSylvanAdd.cpp.

◆ mod()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::mod ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 356 of file InternalSylvanAdd.cpp.

◆ multiplyMatrix() [1/2]

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::multiplyMatrix ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  otherMatrix,
std::vector< InternalBdd< DdType::Sylvan > > const &  summationDdVariables 
) const

Definition at line 662 of file InternalSylvanAdd.cpp.

◆ multiplyMatrix() [2/2]

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::multiplyMatrix ( InternalBdd< DdType::Sylvan > const &  otherMatrix,
std::vector< InternalBdd< DdType::Sylvan > > const &  summationDdVariables 
) const

Definition at line 700 of file InternalSylvanAdd.cpp.

◆ operator*()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator* ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 144 of file InternalSylvanAdd.cpp.

◆ operator*=()

InternalAdd< DdType::Sylvan, storm::RationalNumber > & storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator*= ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other)

Definition at line 164 of file InternalSylvanAdd.cpp.

◆ operator+()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator+ ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 103 of file InternalSylvanAdd.cpp.

◆ operator+=()

InternalAdd< DdType::Sylvan, storm::RationalNumber > & storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator+= ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other)

Definition at line 123 of file InternalSylvanAdd.cpp.

◆ operator-()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator- ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 185 of file InternalSylvanAdd.cpp.

◆ operator-=()

InternalAdd< DdType::Sylvan, storm::RationalNumber > & storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator-= ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other)

Definition at line 205 of file InternalSylvanAdd.cpp.

◆ operator/()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator/ ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 226 of file InternalSylvanAdd.cpp.

◆ operator/=()

InternalAdd< DdType::Sylvan, storm::RationalNumber > & storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::operator/= ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other)

Definition at line 246 of file InternalSylvanAdd.cpp.

◆ pow()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::pow ( InternalAdd< DdType::Sylvan, storm::RationalNumber > const &  other) const

Definition at line 337 of file InternalSylvanAdd.cpp.

◆ sumAbstract()

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::sumAbstract ( InternalBdd< DdType::Sylvan > const &  cube) const

Definition at line 507 of file InternalSylvanAdd.cpp.

◆ toValueType() [1/2]

InternalAdd< DdType::Sylvan, double > storm::dd::InternalAdd< DdType::Sylvan, storm::RationalNumber >::toValueType ( ) const

Definition at line 483 of file InternalSylvanAdd.cpp.

◆ toValueType() [2/2]

InternalAdd< DdType::Sylvan, storm::RationalNumber > storm::dd::InternalAdd< DdType::Sylvan, double >::toValueType ( ) const

Definition at line 489 of file InternalSylvanAdd.cpp.

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