diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 120aef683..3aedb86a4 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -626,10 +626,10 @@ namespace storm { private: /*! - * Creates a DD that encapsulates the given CUDD ADD. + * Creates a DD that encapsulates the given CUDD internal ADD. * * @param ddManager The manager responsible for this DD. - * @param cuddBdd The CUDD BDD to store. + * @param internalAdd The internal ADD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ Add(std::shared_ptr const> ddManager, InternalAdd const& internalAdd, std::set const& containedMetaVariables = std::set()); diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index e5c0fe5b3..65cf35f55 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -7,6 +7,10 @@ #include "src/storage/dd/cudd/InternalCuddBdd.h" namespace storm { + namespace logic { + enum class ComparisonType; + } + namespace dd { template class Add; @@ -265,10 +269,10 @@ namespace storm { operator InternalBdd() const; /*! - * Creates a DD that encapsulates the given CUDD ADD. + * Creates a DD that encapsulates the given internal BDD. * * @param ddManager The manager responsible for this DD. - * @param cuddBdd The CUDD BDD to store. + * @param internalBdd The internal BDD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables = std::set()); diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index fa7e5d3ea..1c068684e 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -146,21 +146,21 @@ namespace storm { bool hasMetaVariable(std::string const& variableName) const; /*! - * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. + * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager (if supported). * * @param value If set to true, dynamic reordering is allowed and forbidden otherwise. */ void allowDynamicReordering(bool value); /*! - * Retrieves whether dynamic reordering is currently allowed. + * Retrieves whether dynamic reordering is currently allowed (if supported). * * @return True iff dynamic reordering is currently allowed. */ bool isDynamicReorderingAllowed() const; /*! - * Triggers a reordering of the DDs managed by this manager. + * Triggers a reordering of the DDs managed by this manager (if supported). */ void triggerReordering(); @@ -179,6 +179,11 @@ namespace storm { */ std::shared_ptr const> asSharedPointer() const; + /*! + * Retrieves the set of meta variables contained in the DD. + * + * @return All contained meta variables. + */ std::set getAllMetaVariables() const; /*! @@ -242,7 +247,18 @@ namespace storm { */ storm::expressions::ExpressionManager& getExpressionManager(); + /*! + * Retrieves a pointer to the internal DD manager. + * + * @return A pointer to the internal DD manager. + */ InternalDdManager* getInternalDdManagerPointer(); + + /*! + * Retrieves a pointer to the internal DD manager. + * + * @return A pointer to the internal DD manager. + */ InternalDdManager const* getInternalDdManagerPointer() const; // A mapping from variables to the meta variable information. diff --git a/src/storage/dd/Odd.cpp b/src/storage/dd/Odd.cpp index 7bf0f18ab..bac7c2112 100644 --- a/src/storage/dd/Odd.cpp +++ b/src/storage/dd/Odd.cpp @@ -59,6 +59,7 @@ namespace storm { if (this->isTerminalNode()) { return 1; } else { + // Since both subtrees have the same height, we only count the height of the else-tree. return 1 + this->getElseSuccessor().getHeight(); } }