Odd.h

Go to the documentation of this file.

#pragma once
 
#include <functional>
#include <map>
#include <memory>
#include <unordered_set>
#include <vector>
 
namespace storm {
namespace storage {
class BitVector;
}
 
namespace dd {
class Odd {
   public:
    Odd(std::shared_ptr<Odd> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd> thenNode, uint_fast64_t thenOffset);
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    Odd() = default;
    Odd(Odd const& other) = default;
    Odd& operator=(Odd const& other) = default;
    Odd(Odd&& other) = default;
    Odd& operator=(Odd&& other) = default;
 
    Odd const& getThenSuccessor() const;
 
    Odd const& getElseSuccessor() const;
 
    uint_fast64_t getElseOffset() const;
 
    void setElseOffset(uint_fast64_t newOffset);
 
    uint_fast64_t getThenOffset() const;
 
    void setThenOffset(uint_fast64_t newOffset);
 
    uint_fast64_t getTotalOffset() const;
 
    uint_fast64_t getNodeCount() const;
 
    uint_fast64_t getHeight() const;
 
    bool isTerminalNode() const;
 
    template<typename ValueType>
    void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<ValueType> const& oldValues, std::vector<ValueType>& newValues) const;
 
    void oldToNewIndex(storm::dd::Odd const& newOdd, std::function<void(uint64_t oldOffset, uint64_t newOffset)> const& callback) const;
 
    void exportToDot(std::string const& filename) const;
 
    void exportToText(std::string const& filename) const;
 
    storm::storage::BitVector getEncoding(uint64_t offset, uint64_t variableCount = 0) const;
 
   private:
    void addToLevelToOddNodesMap(std::map<uint_fast64_t, std::unordered_set<storm::dd::Odd const*>>& levelToOddNodesMap, uint_fast64_t level = 0) const;
 
    template<typename ValueType>
    static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<ValueType> const& oldValues, uint_fast64_t newOffset,
                                        storm::dd::Odd const& newOdd, std::vector<ValueType>& newValues);
 
    static void oldToNewIndexRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, uint_fast64_t newOffset, storm::dd::Odd const& newOdd,
                                 std::function<void(uint64_t oldOffset, uint64_t newOffset)> const& callback);
 
    // The then- and else-nodes.
    std::shared_ptr<Odd> elseNode;
    std::shared_ptr<Odd> thenNode;
 
    // The offsets that need to be added if the then- or else-successor is taken, respectively.
    uint_fast64_t elseOffset;
    uint_fast64_t thenOffset;
};
}  // namespace dd
}  // namespace storm