DdMetaVariable.h

Go to the documentation of this file.

#pragma once
 
#include <vector>
 
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdType.h"
 
namespace storm {
namespace dd {
 
template<DdType LibraryType>
class DdManager;
 
template<DdType LibraryType, typename ValueTpe>
class Add;
 
// An enumeration for all legal types of meta variables.
enum class MetaVariableType { Bool, Int, BitVector };
// An enum that expresses the relation of two meta variables relative to each other.
enum class MetaVariablePosition { Above, Below };
 
// Declare DdMetaVariable class so we can then specialize it for the different DD types.
template<DdType LibraryType>
class DdMetaVariable {
   public:
    friend class DdManager<LibraryType>;
    friend class Bdd<LibraryType>;
 
    template<DdType LibraryTypePrime, typename ValueTypePrime>
    friend class Add;
 
    template<DdType LibraryTypePrime, typename ValueTypePrime>
    friend class AddIterator;
 
    std::string const& getName() const;
 
    MetaVariableType getType() const;
 
    int_fast64_t getLow() const;
 
    bool hasHigh() const;
 
    int_fast64_t getHigh() const;
 
    bool canRepresent(int_fast64_t value) const;
 
    std::size_t getNumberOfDdVariables() const;
 
    Bdd<LibraryType> const& getCube() const;
 
    uint64_t getLowestIndex() const;
 
    uint64_t getHighestLevel() const;
 
    std::vector<uint64_t> getIndices(bool sortedByLevel = true) const;
 
    std::vector<std::pair<uint64_t, uint64_t>> getIndicesAndLevels() const;
 
   private:
    DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<LibraryType>> const& ddVariables);
 
    DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables);
 
    void precomputeLowestIndex();
 
    std::vector<Bdd<LibraryType>> const& getDdVariables() const;
 
    void createCube();
 
    // The name of the meta variable.
    std::string name;
 
    // The type of the variable.
    MetaVariableType type;
 
    // The lowest value of the range of the variable.
    int_fast64_t low;
 
    // The highest value of the range of the variable.
    boost::optional<int_fast64_t> high;
 
    // The vector of variables that are used to encode the meta variable.
    std::vector<Bdd<LibraryType>> ddVariables;
 
    // The cube consisting of all variables that encode the meta variable.
    Bdd<LibraryType> cube;
 
    // The lowest index of any DD variable of this meta variable.
    uint64_t lowestIndex;
};
}  // namespace dd
}  // namespace storm