InternalSylvanDdManager.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
 
#include "storm-config.h"
#include "storm/adapters/RationalFunctionForward.h"
#include "storm/environment/dd/SylvanDdManagerEnvironment.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/InternalDdManager.h"
#include "storm/storage/dd/sylvan/InternalSylvanAdd.h"
#include "storm/storage/dd/sylvan/InternalSylvanBdd.h"
 
namespace storm {
namespace dd {
template<DdType LibraryType, typename ValueType>
class InternalAdd;
 
template<DdType LibraryType>
class InternalBdd;
 
template<>
class InternalDdManager<DdType::Sylvan> {
   public:
    friend class InternalBdd<DdType::Sylvan>;
 
    template<DdType LibraryType, typename ValueType>
    friend class InternalAdd;

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

    ~InternalDdManager();

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

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

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

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

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

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

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

    std::vector<InternalBdd<DdType::Sylvan>> 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;
 
   private:
#ifdef STORM_HAVE_SYLVAN
 
    // Helper function to create the BDD whose encodings are below a given bound.
    BDD getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, BDD cube, uint64_t remainingDdVariables) const;
 
    // A counter for the number of instances of this class. This is used to determine when to initialize and
    // quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a
    // 'global' manager.
    static uint_fast64_t numberOfInstances;
 
    // Since the sylvan (more specifically: lace) processes do busy waiting, we suspend them as long as
    // sylvan is not used. This flag keeps track of whether we are currently suspending.
    static bool suspended;
 
    // The index of the next free variable index. This needs to be shared across all instances since the sylvan
    // manager is implicitly 'global'.
    static uint_fast64_t nextFreeVariableIndex;
#endif
};
 
}  // namespace dd
}  // namespace storm