Dd.h

Go to the documentation of this file.

#pragma once
 
#include <set>
#include <string>
#include <vector>
 
#include "storm/storage/dd/DdType.h"
#include "storm/storage/expressions/Variable.h"
 
namespace storm {
namespace dd {
// Forward-declare some classes.
template<DdType LibraryType>
class DdManager;
 
template<DdType LibraryType>
class Bdd;
 
template<DdType LibraryType>
class Dd {
   public:
    // Declare the DdManager so it can access the internals of a DD.
    friend class DdManager<LibraryType>;
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    Dd() = default;
    Dd(Dd<LibraryType> const& other) = default;
    Dd& operator=(Dd<LibraryType> const& other) = default;
    Dd(Dd<LibraryType>&& other) = default;
    Dd& operator=(Dd<LibraryType>&& other) = default;
 
    virtual ~Dd() = default;
 
    virtual Bdd<LibraryType> getSupport() const = 0;
 
    virtual uint_fast64_t getNonZeroCount() const = 0;
 
    virtual uint_fast64_t getLeafCount() const = 0;
 
    virtual uint_fast64_t getNodeCount() const = 0;
 
    virtual uint_fast64_t getIndex() const = 0;
 
    virtual uint_fast64_t getLevel() const = 0;
 
    bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const;
 
    bool containsMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    std::set<storm::expressions::Variable> const& getContainedMetaVariables() const;
 
    virtual void exportToDot(std::string const& filename, bool showVariablesIfPossible = true) const = 0;
 
    virtual void exportToText(std::string const& filename) const = 0;
 
    DdManager<LibraryType>& getDdManager() const;
 
    std::set<storm::expressions::Variable>& getContainedMetaVariables();
 
    void addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables);
 
    void addMetaVariable(storm::expressions::Variable const& metaVariable);
 
    void removeMetaVariable(storm::expressions::Variable const& metaVariable);
 
    void removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables);
 
   protected:
    std::vector<uint_fast64_t> getSortedVariableIndices() const;
 
    Dd(DdManager<LibraryType> const& ddManager,
       std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
 
    static std::set<storm::expressions::Variable> joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second);
 
    static std::set<storm::expressions::Variable> subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second);
 
   private:
    // A pointer to the manager responsible for this DD.
    DdManager<LibraryType>* ddManager;
 
    // The meta variables that appear in this DD.
    std::set<storm::expressions::Variable> containedMetaVariables;
};
}  // namespace dd
}  // namespace storm