DdManager.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <functional>
#include <set>
#include <unordered_map>
 
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdMetaVariable.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/InternalDdManager.h"
#include "storm/storage/dd/cudd/InternalCuddDdManager.h"
#include "storm/storage/dd/sylvan/InternalSylvanDdManager.h"
#include "storm/storage/expressions/Variable.h"
 
namespace storm {
class Environment;
}  // namespace storm
 
namespace storm {
namespace dd {
 
// Declare DdManager class so we can then specialize it for the different DD types.
template<DdType LibraryType>
class DdManager : public std::enable_shared_from_this<DdManager<LibraryType>> {
   public:
    friend class Bdd<LibraryType>;
 
    template<DdType LibraryTypePrime, typename ValueType>
    friend class Add;
 
    template<DdType LibraryTypePrime, typename ValueType>
    friend class AddIterator;

    explicit DdManager(storm::Environment const& env);

    static std::shared_ptr<DdManager<LibraryType>> createWithDefaultEnvironment();
 
    // Explicitly forbid copying a DdManager, but allow moving it.
    DdManager(DdManager<LibraryType> const& other) = delete;
    DdManager<LibraryType>& operator=(DdManager<LibraryType> const& other) = delete;
    DdManager(DdManager<LibraryType>&& other) = default;
    DdManager<LibraryType>& operator=(DdManager<LibraryType>&& other) = default;
 
    std::shared_ptr<DdManager<LibraryType>> asSharedPointer();
    std::shared_ptr<DdManager<LibraryType> const> asSharedPointer() const;

    Bdd<LibraryType> getBddOne() const;

    template<typename ValueType>
    Add<LibraryType, ValueType> getAddOne() const;

    Bdd<LibraryType> getBddZero() const;

    template<typename ValueType>
    Add<LibraryType, ValueType> getAddZero() const;

    template<typename ValueType>
    Add<LibraryType, ValueType> getAddUndefined() const;

    template<typename ValueType>
    Add<LibraryType, ValueType> getInfinity() const;

    template<typename ValueType>
    Add<LibraryType, ValueType> getConstant(ValueType const& value) const;

    Bdd<LibraryType> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool mostSignificantBitAtTop = true) const;

    Bdd<LibraryType> getRange(storm::expressions::Variable const& variable) const;

    template<typename ValueType>
    Add<LibraryType, ValueType> getIdentity(storm::expressions::Variable const& variable) const;

    Bdd<LibraryType> getIdentity(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& variablePairs,
                                 bool restrictToFirstRange = true) const;

    Bdd<LibraryType> getIdentity(storm::expressions::Variable const& first, storm::expressions::Variable const& second, bool restrictToFirstRange = true) const;

    Bdd<LibraryType> getCube(storm::expressions::Variable const& variable) const;

    Bdd<LibraryType> getCube(std::set<storm::expressions::Variable> const& variables) const;

    std::vector<storm::expressions::Variable> cloneVariable(storm::expressions::Variable const& variable, std::string const& newVariableName,
                                                            boost::optional<uint64_t> const& numberOfLayers = boost::none);

    std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(
        std::string const& variableName, int_fast64_t low, int_fast64_t high,
        boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);

    std::vector<storm::expressions::Variable> addMetaVariable(
        std::string const& variableName, int_fast64_t low, int_fast64_t high, uint64_t numberOfLayers,
        boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);

    std::vector<storm::expressions::Variable> addBitVectorMetaVariable(
        std::string const& variableName, uint64_t bits, uint64_t numberOfLayers,
        boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);

    std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(
        std::string const& variableName, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);

    std::vector<storm::expressions::Variable> addMetaVariable(
        std::string const& variableName, uint64_t numberOfLayers,
        boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);

    std::set<std::string> getAllMetaVariableNames() const;

    std::size_t getNumberOfMetaVariables() const;

    bool hasMetaVariable(std::string const& variableName) const;

    storm::expressions::Variable getMetaVariable(std::string const& variableName) const;

    bool supportsOrderedInsertion() const;

    void allowDynamicReordering(bool value);

    bool isDynamicReorderingAllowed() const;

    void triggerReordering();

    DdMetaVariable<LibraryType> const& getMetaVariable(storm::expressions::Variable const& variable) const;

    std::set<storm::expressions::Variable> getAllMetaVariables() const;

    std::vector<uint_fast64_t> getSortedVariableIndices() const;

    std::vector<uint_fast64_t> getSortedVariableIndices(std::set<storm::expressions::Variable> const& metaVariables) const;

    InternalDdManager<LibraryType>& getInternalDdManager();

    InternalDdManager<LibraryType> const& getInternalDdManager() const;

    void debugCheck() const;

    void execute(std::function<void()> const& f) const;
 
   private:
    std::vector<storm::expressions::Variable> addMetaVariableHelper(
        MetaVariableType const& type, std::string const& name, uint64_t numberOfDdVariables, uint64_t numberOfLayers,
        boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none,
        boost::optional<std::pair<int_fast64_t, int_fast64_t>> const& bounds = boost::none);

    std::vector<std::string> getDdVariableNames() const;

    std::vector<storm::expressions::Variable> getDdVariables() const;

    storm::expressions::ExpressionManager const& getExpressionManager() const;

    storm::expressions::ExpressionManager& getExpressionManager();

    InternalDdManager<LibraryType>* getInternalDdManagerPointer();

    InternalDdManager<LibraryType> const* getInternalDdManagerPointer() const;
 
    // ATTENTION: as the DD packages typically perform garbage collection, the order of members is crucial here:
    // First, the references to the DDs of the meta variables need to be disposed of and *then* the manager.
 
    // The DD manager that is customized according to the selected library type.
    InternalDdManager<LibraryType> internalDdManager;
 
    // A mapping from variables to the meta variable information.
    std::unordered_map<storm::expressions::Variable, DdMetaVariable<LibraryType>> metaVariableMap;
 
    // The manager responsible for the variables.
    std::shared_ptr<storm::expressions::ExpressionManager> manager;
};
}  // namespace dd
}  // namespace storm