InternalSylvanBdd.h

Go to the documentation of this file.

#pragma once
 
#include <functional>
#include <memory>
#include <unordered_map>
#include <vector>
 
#include "storm-config.h"
#include "storm/adapters/sylvan.h"
#include "storm/exceptions/MissingLibraryException.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/InternalAdd.h"
#include "storm/storage/dd/InternalBdd.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/ExpressionManager.h"
 
namespace storm {
namespace storage {
class BitVector;
}
 
namespace dd {
template<DdType LibraryType>
class InternalDdManager;
 
class Odd;
 
template<>
class InternalBdd<DdType::Sylvan> {
   public:
    template<DdType LibraryType, typename ValueType>
    friend class InternalAdd;
 
#ifdef STORM_HAVE_SYLVAN
    InternalBdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Bdd const& sylvanBdd);
#endif
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    InternalBdd();
    InternalBdd(InternalBdd<DdType::Sylvan> const& other) = default;
    InternalBdd& operator=(InternalBdd<DdType::Sylvan> const& other) = default;
    InternalBdd(InternalBdd<DdType::Sylvan>&& other) = default;
    InternalBdd& operator=(InternalBdd<DdType::Sylvan>&& other) = default;
 
    static InternalBdd<storm::dd::DdType::Sylvan> fromVector(InternalDdManager<DdType::Sylvan> const* ddManager, Odd const& odd,
                                                             std::vector<uint_fast64_t> const& sortedDdVariableIndices,
                                                             std::function<bool(uint64_t)> const& filter);
 
    bool operator==(InternalBdd<DdType::Sylvan> const& other) const;
 
    bool operator!=(InternalBdd<DdType::Sylvan> const& other) const;
 
    InternalBdd<DdType::Sylvan> relationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables,
                                                  std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const;
 
    InternalBdd<DdType::Sylvan> inverseRelationalProduct(InternalBdd<DdType::Sylvan> const& relation,
                                                         std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables,
                                                         std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const;
 
    InternalBdd<DdType::Sylvan> inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::Sylvan> const& relation,
                                                                             std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables,
                                                                             std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const;
 
    InternalBdd<DdType::Sylvan> ite(InternalBdd<DdType::Sylvan> const& thenBdd, InternalBdd<DdType::Sylvan> const& elseBdd) const;
 
    template<typename ValueType>
    InternalAdd<DdType::Sylvan, ValueType> ite(InternalAdd<DdType::Sylvan, ValueType> const& thenAdd,
                                               InternalAdd<DdType::Sylvan, ValueType> const& elseAdd) const;
 
    InternalBdd<DdType::Sylvan> operator||(InternalBdd<DdType::Sylvan> const& other) const;
 
    InternalBdd<DdType::Sylvan>& operator|=(InternalBdd<DdType::Sylvan> const& other);
 
    InternalBdd<DdType::Sylvan> operator&&(InternalBdd<DdType::Sylvan> const& other) const;
 
    InternalBdd<DdType::Sylvan>& operator&=(InternalBdd<DdType::Sylvan> const& other);
 
    InternalBdd<DdType::Sylvan> iff(InternalBdd<DdType::Sylvan> const& other) const;
 
    InternalBdd<DdType::Sylvan> exclusiveOr(InternalBdd<DdType::Sylvan> const& other) const;
 
    InternalBdd<DdType::Sylvan> implies(InternalBdd<DdType::Sylvan> const& other) const;
 
    InternalBdd<DdType::Sylvan> operator!() const;
 
    InternalBdd<DdType::Sylvan>& complement();
 
    InternalBdd<DdType::Sylvan> existsAbstract(InternalBdd<DdType::Sylvan> const& cube) const;
 
    InternalBdd<DdType::Sylvan> existsAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const;
 
    InternalBdd<DdType::Sylvan> universalAbstract(InternalBdd<DdType::Sylvan> const& cube) const;
 
    InternalBdd<DdType::Sylvan> swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const;
 
    InternalBdd<DdType::Sylvan> andExists(InternalBdd<DdType::Sylvan> const& other, InternalBdd<storm::dd::DdType::Sylvan> const& cube) const;
 
    InternalBdd<DdType::Sylvan> constrain(InternalBdd<DdType::Sylvan> const& constraint) const;
 
    InternalBdd<DdType::Sylvan> restrict(InternalBdd<DdType::Sylvan> const& constraint) const;
 
    InternalBdd<DdType::Sylvan> getSupport() const;
 
    uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
 
    uint_fast64_t getLeafCount() const;
 
    uint_fast64_t getNodeCount() const;
 
    bool isOne() const;
 
    bool isZero() const;
 
    uint_fast64_t getIndex() const;
 
    uint_fast64_t getLevel() const;
 
    void exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings, bool showVariablesIfPossible = true) const;
 
    void exportToText(std::string const& filename) const;
 
    template<typename ValueType>
    InternalAdd<DdType::Sylvan, ValueType> toAdd() const;
 
    storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd, std::vector<uint_fast64_t> const& ddVariableIndices) const;
 
    std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<uint_fast64_t, storm::expressions::Variable>> toExpression(
        storm::expressions::ExpressionManager& manager) const;
 
    Odd createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const;
 
    template<typename ValueType>
    void filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType> const& sourceValues,
                              std::vector<ValueType>& targetValues) const;
 
    void filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, storm::storage::BitVector const& sourceValues,
                              storm::storage::BitVector& targetValues) const;
 
    std::vector<InternalBdd<DdType::Sylvan>> splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
 
    friend struct std::hash<storm::dd::InternalBdd<storm::dd::DdType::Sylvan>>;
 
#ifdef STORM_HAVE_SYLVAN
    sylvan::Bdd& getSylvanBdd();
 
    sylvan::Bdd const& getSylvanBdd() const;
#endif
 
   private:
#ifdef STORM_HAVE_SYLVAN
    static BDD fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, Odd const& odd,
                             std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool(uint64_t)> const& filter);
 
    // Declare a hash functor that is used for the unique tables in the construction process of ODDs.
    class HashFunctor {
       public:
        std::size_t operator()(std::pair<BDD, bool> const& key) const;
    };
 
    static std::shared_ptr<Odd> createOddRec(BDD dd, bool complement, uint_fast64_t currentLevel, uint_fast64_t maxLevel,
                                             std::vector<uint_fast64_t> const& ddVariableIndices,
                                             std::vector<std::unordered_map<std::pair<BDD, bool>, std::shared_ptr<Odd>, HashFunctor>>& uniqueTableForLevels);
 
    void toVectorRec(BDD dd, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel,
                     uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
 
    template<typename ValueType>
    static void filterExplicitVectorRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel,
                                        std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd,
                                        std::vector<ValueType>& result, uint_fast64_t& currentIndex, std::vector<ValueType> const& values);
 
    static void filterExplicitVectorRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel,
                                        std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd,
                                        storm::storage::BitVector& result, uint_fast64_t& currentIndex, storm::storage::BitVector const& values);
 
    static storm::expressions::Variable toExpressionRec(
        BDD dd, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions,
        std::unordered_map<uint_fast64_t, storm::expressions::Variable>& indexToVariableMap,
        std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair,
        std::unordered_map<BDD, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex);
 
    void splitIntoGroupsRec(BDD dd, std::vector<InternalBdd<DdType::Sylvan>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices,
                            uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;
 
    // The internal manager responsible for this BDD.
    InternalDdManager<DdType::Sylvan> const* ddManager;
 
    // The sylvan BDD.
    sylvan::Bdd sylvanBdd;
#endif
};
}  // namespace dd
}  // namespace storm
 
namespace std {
template<>
struct hash<storm::dd::InternalBdd<storm::dd::DdType::Sylvan>> {
#ifdef STORM_HAVE_SYLVAN
    std::size_t operator()(storm::dd::InternalBdd<storm::dd::DdType::Sylvan> const& key) const {
        return static_cast<std::size_t>(key.sylvanBdd.GetBDD());
    }
#else
    std::size_t operator()(storm::dd::InternalBdd<storm::dd::DdType::Sylvan> const&) const {
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
    }
#endif
};
}  // namespace std