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/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;
 
    InternalDdManager();
 
    ~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