Browse Source

done cleaining up

Former-commit-id: 4c732fc188
tempestpy_adaptions
dehnert 9 years ago
parent
commit
c36d869b3c
  1. 4
      src/storage/dd/Add.h
  2. 8
      src/storage/dd/Bdd.h
  3. 22
      src/storage/dd/DdManager.h
  4. 1
      src/storage/dd/Odd.cpp

4
src/storage/dd/Add.h

@ -626,10 +626,10 @@ namespace storm {
private: 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 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. * @param containedMetaVariables The meta variables that appear in the DD.
*/ */
Add(std::shared_ptr<DdManager<LibraryType> const> ddManager, InternalAdd<LibraryType, ValueType> const& internalAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>()); Add(std::shared_ptr<DdManager<LibraryType> const> ddManager, InternalAdd<LibraryType, ValueType> const& internalAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());

8
src/storage/dd/Bdd.h

@ -7,6 +7,10 @@
#include "src/storage/dd/cudd/InternalCuddBdd.h" #include "src/storage/dd/cudd/InternalCuddBdd.h"
namespace storm { namespace storm {
namespace logic {
enum class ComparisonType;
}
namespace dd { namespace dd {
template<DdType LibraryType, typename ValueType> template<DdType LibraryType, typename ValueType>
class Add; class Add;
@ -265,10 +269,10 @@ namespace storm {
operator InternalBdd<LibraryType>() const; operator InternalBdd<LibraryType>() 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 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. * @param containedMetaVariables The meta variables that appear in the DD.
*/ */
Bdd(std::shared_ptr<DdManager<LibraryType> const> ddManager, InternalBdd<LibraryType> const& internalBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>()); Bdd(std::shared_ptr<DdManager<LibraryType> const> ddManager, InternalBdd<LibraryType> const& internalBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());

22
src/storage/dd/DdManager.h

@ -146,21 +146,21 @@ namespace storm {
bool hasMetaVariable(std::string const& variableName) const; 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. * @param value If set to true, dynamic reordering is allowed and forbidden otherwise.
*/ */
void allowDynamicReordering(bool value); 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. * @return True iff dynamic reordering is currently allowed.
*/ */
bool isDynamicReorderingAllowed() const; 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(); void triggerReordering();
@ -179,6 +179,11 @@ namespace storm {
*/ */
std::shared_ptr<DdManager<LibraryType> const> asSharedPointer() const; std::shared_ptr<DdManager<LibraryType> const> asSharedPointer() const;
/*!
* Retrieves the set of meta variables contained in the DD.
*
* @return All contained meta variables.
*/
std::set<storm::expressions::Variable> getAllMetaVariables() const; std::set<storm::expressions::Variable> getAllMetaVariables() const;
/*! /*!
@ -242,7 +247,18 @@ namespace storm {
*/ */
storm::expressions::ExpressionManager& getExpressionManager(); storm::expressions::ExpressionManager& getExpressionManager();
/*!
* Retrieves a pointer to the internal DD manager.
*
* @return A pointer to the internal DD manager.
*/
InternalDdManager<LibraryType>* getInternalDdManagerPointer(); InternalDdManager<LibraryType>* getInternalDdManagerPointer();
/*!
* Retrieves a pointer to the internal DD manager.
*
* @return A pointer to the internal DD manager.
*/
InternalDdManager<LibraryType> const* getInternalDdManagerPointer() const; InternalDdManager<LibraryType> const* getInternalDdManagerPointer() const;
// A mapping from variables to the meta variable information. // A mapping from variables to the meta variable information.

1
src/storage/dd/Odd.cpp

@ -59,6 +59,7 @@ namespace storm {
if (this->isTerminalNode()) { if (this->isTerminalNode()) {
return 1; return 1;
} else { } else {
// Since both subtrees have the same height, we only count the height of the else-tree.
return 1 + this->getElseSuccessor().getHeight(); return 1 + this->getElseSuccessor().getHeight();
} }
} }

Loading…
Cancel
Save