SylvanAddIterator.h

Go to the documentation of this file.

#pragma once
 
#include <unordered_map>
 
#include "storm-config.h"
#include "storm/adapters/sylvan.h"
#include "storm/storage/dd/AddIterator.h"
#include "storm/storage/expressions/SimpleValuation.h"
 
namespace storm {
namespace dd {
// Forward-declare the DdManager class.
template<DdType Type>
class DdManager;
 
template<DdType Type, typename ValueType>
class InternalAdd;
 
template<typename ValueType>
class AddIterator<DdType::Sylvan, ValueType> {
   public:
    friend class InternalAdd<DdType::Sylvan, ValueType>;
 
    // Default-instantiate the constructor.
    AddIterator();
 
    // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then.
    AddIterator(AddIterator<DdType::Sylvan, ValueType> const& other) = delete;
    AddIterator& operator=(AddIterator<DdType::Sylvan, ValueType> const& other) = delete;
 
    // Provide move-construction and move-assignment, though.
    AddIterator(AddIterator<DdType::Sylvan, ValueType>&& other) = default;
    AddIterator& operator=(AddIterator<DdType::Sylvan, ValueType>&& other) = default;
 
    AddIterator<DdType::Sylvan, ValueType>& operator++();
 
    std::pair<storm::expressions::SimpleValuation, ValueType> operator*() const;
 
    bool operator==(AddIterator<DdType::Sylvan, ValueType> const& other) const;
 
    bool operator!=(AddIterator<DdType::Sylvan, ValueType> const& other) const;
 
   private:
#ifdef STORM_HAVE_SYLVAN
    AddIterator(DdManager<DdType::Sylvan> const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, bool isAtEnd,
                std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables);
 
    static AddIterator createBeginIterator(DdManager<DdType::Sylvan> const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables,
                                           uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const* metaVariables,
                                           bool enumerateDontCareMetaVariables = true);
 
    static AddIterator createEndIterator(DdManager<DdType::Sylvan> const& ddManager);
 
    void treatNewCube();
 
    void treatNextInCube();
 
    void createGlobalToLocalIndexMapping();
 
    // The manager responsible for the meta variables (and therefore the underlying DD).
    DdManager<DdType::Sylvan> const* ddManager;
 
    // The MTBDD over which to iterate.
    sylvan::Mtbdd mtbdd;
 
    // The cube of variables in the MTBDD.
    sylvan::Bdd variables;
 
    // The currently considered cube of the DD.
    std::vector<uint8_t> cube;
 
    // The function value of the current cube, represented by the corresponding leaf.
    MTBDD leaf;
 
    // A flag that indicates whether the iterator is at its end and may not be moved further. This is also used
    // for the check against the end iterator.
    bool isAtEnd;
 
    // The set of meta variables appearing in the DD.
    std::set<storm::expressions::Variable> const* metaVariables;
 
    // A mapping from global variable indices to local (i.e. appearing the MTBDD) ones.
    std::unordered_map<uint_fast64_t, uint_fast64_t> globalToLocalIndexMap;
 
    // A flag that indicates whether the iterator is supposed to enumerate meta variable valuations even if
    // they don't influence the function value.
    bool enumerateDontCareMetaVariables;
 
    // A number that represents how many assignments of the current cube have already been returned previously.
    // This is needed, because cubes may represent many assignments (if they have don't care variables).
    uint_fast64_t cubeCounter;
 
    // A vector of tuples of the form <metaVariable, bitIndex>.
    std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> relevantDontCareDdVariables;
 
    // The current valuation of meta variables.
    storm::expressions::SimpleValuation currentValuation;
#endif
};
}  // namespace dd
}  // namespace storm