CuddAddIterator.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <memory>
#include <set>
#include <tuple>
#include <utility>
 
#include "storm-config.h"
#include "storm/adapters/cudd.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::CUDD, ValueType> {
   public:
    friend class InternalAdd<DdType::CUDD, ValueType>;
 
    // Default-instantiate the constructor.
    AddIterator();
 
    // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then.
    AddIterator(AddIterator<DdType::CUDD, ValueType> const& other) = delete;
    AddIterator& operator=(AddIterator<DdType::CUDD, ValueType> const& other) = delete;
 
    // Provide move-construction and move-assignment, though.
    AddIterator(AddIterator<DdType::CUDD, ValueType>&& other);
    AddIterator& operator=(AddIterator<DdType::CUDD, ValueType>&& other);

    ~AddIterator();

    AddIterator<DdType::CUDD, ValueType>& operator++();

    std::pair<storm::expressions::SimpleValuation, ValueType> operator*() const;

    bool operator==(AddIterator<DdType::CUDD, ValueType> const& other) const;

    bool operator!=(AddIterator<DdType::CUDD, ValueType> const& other) const;
 
   private:
#ifdef STORM_HAVE_CUDD
    AddIterator(DdManager<DdType::CUDD> const& ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd,
                std::set<storm::expressions::Variable> const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true);

    void treatNewCube();

    void treatNextInCube();
 
    // The manager responsible for the meta variables (and therefore the underlying DD).
    DdManager<DdType::CUDD> const* ddManager;
 
    // The CUDD generator used to enumerate the cubes of the DD.
    DdGen* generator;
 
    // The currently considered cube of the DD.
    int* cube;
 
    // The function value of the current cube.
    double valueAsDouble;
 
    // 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 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