InternalCuddDdManager.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <functional>
 
#include "storm-config.h"
#include "storm/environment/dd/CuddDdManagerEnvironment.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/InternalDdManager.h"
#include "storm/storage/dd/cudd/InternalCuddAdd.h"
#include "storm/storage/dd/cudd/InternalCuddBdd.h"
 
#ifdef STORM_HAVE_CUDD
#include "cuddObj.hh"
#endif
 
namespace storm {
namespace dd {
template<DdType LibraryType, typename ValueType>
class InternalAdd;
 
template<DdType LibraryType>
class InternalBdd;
 
template<>
class InternalDdManager<DdType::CUDD> {
   public:
    friend class InternalBdd<DdType::CUDD>;
 
    template<DdType LibraryType, typename ValueType>
    friend class InternalAdd;

    explicit InternalDdManager(storm::CuddDdManagerEnvironment const& environment);

    ~InternalDdManager();

    InternalBdd<DdType::CUDD> getBddOne() const;

    template<typename ValueType>
    InternalAdd<DdType::CUDD, ValueType> getAddOne() const;

    InternalBdd<DdType::CUDD> getBddZero() const;

    InternalBdd<DdType::CUDD> getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube, uint64_t numberOfDdVariables) const;

    template<typename ValueType>
    InternalAdd<DdType::CUDD, ValueType> getAddZero() const;

    template<typename ValueType>
    InternalAdd<DdType::CUDD, ValueType> getAddUndefined() const;

    template<typename ValueType>
    InternalAdd<DdType::CUDD, ValueType> getConstant(ValueType const& value) const;

    std::vector<InternalBdd<DdType::CUDD>> createDdVariables(uint64_t numberOfLayers, boost::optional<uint_fast64_t> const& position = boost::none);

    bool supportsOrderedInsertion() const;

    void allowDynamicReordering(bool value);

    bool isDynamicReorderingAllowed() const;

    void triggerReordering();

    void debugCheck() const;

    void execute(std::function<void()> const& f) const;

    uint_fast64_t getNumberOfDdVariables() const;
 
#ifdef STORM_HAVE_CUDD
    cudd::Cudd& getCuddManager();

    cudd::Cudd const& getCuddManager() const;
#endif
 
   private:
#ifdef STORM_HAVE_CUDD
    // Helper function to create the BDD whose encodings are below a given bound.
    DdNodePtr getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube,
                                               uint64_t remainingDdVariables) const;
 
    // The manager responsible for the DDs created/modified with this DdManager.
    cudd::Cudd cuddManager;
 
    // The technique that is used for dynamic reordering.
    Cudd_ReorderingType reorderingTechnique;
 
    // Keeps track of the number of registered DD variables.
    uint_fast64_t numberOfDdVariables;
#endif
};
}  // namespace dd
}  // namespace storm