InternalCuddBdd.h

Go to the documentation of this file.

#pragma once
 
#include "storm-config.h"
 
#include <functional>
#include <memory>
#include <set>
#include <unordered_map>
 
#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"
 
#ifdef STORM_HAVE_CUDD
// Include the C++-interface of CUDD.
#include "cuddObj.hh"
#endif
 
namespace storm {
namespace storage {
class BitVector;
}
 
namespace dd {
template<DdType LibraryType>
class InternalDdManager;
 
template<DdType LibraryType, typename ValueType>
class InternalAdd;
 
class Odd;
 
template<>
class InternalBdd<DdType::CUDD> {
   public:
    template<DdType LibraryType, typename ValueType>
    friend class InternalAdd;
 
#ifdef STORM_HAVE_CUDD
    InternalBdd(InternalDdManager<DdType::CUDD> const* ddManager, cudd::BDD cuddBdd);
#endif
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    InternalBdd() = default;
    InternalBdd(InternalBdd<DdType::CUDD> const& other) = default;
    InternalBdd& operator=(InternalBdd<DdType::CUDD> const& other) = default;
    InternalBdd(InternalBdd<DdType::CUDD>&& other) = default;
    InternalBdd& operator=(InternalBdd<DdType::CUDD>&& other) = default;

    static InternalBdd<storm::dd::DdType::CUDD> fromVector(InternalDdManager<DdType::CUDD> const* ddManager, Odd const& odd,
                                                           std::vector<uint_fast64_t> const& sortedDdVariableIndices,
                                                           std::function<bool(uint64_t)> const& filter);

    bool operator==(InternalBdd<DdType::CUDD> const& other) const;

    bool operator!=(InternalBdd<DdType::CUDD> const& other) const;

    InternalBdd<DdType::CUDD> relationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables,
                                                std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;

    InternalBdd<DdType::CUDD> inverseRelationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables,
                                                       std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;

    InternalBdd<DdType::CUDD> inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::CUDD> const& relation,
                                                                           std::vector<InternalBdd<DdType::CUDD>> const& rowVariables,
                                                                           std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;

    InternalBdd<DdType::CUDD> ite(InternalBdd<DdType::CUDD> const& thenBdd, InternalBdd<DdType::CUDD> const& elseBdd) const;

    template<typename ValueType>
    InternalAdd<DdType::CUDD, ValueType> ite(InternalAdd<DdType::CUDD, ValueType> const& thenAdd, InternalAdd<DdType::CUDD, ValueType> const& elseAdd) const;

    InternalBdd<DdType::CUDD> operator||(InternalBdd<DdType::CUDD> const& other) const;

    InternalBdd<DdType::CUDD>& operator|=(InternalBdd<DdType::CUDD> const& other);

    InternalBdd<DdType::CUDD> operator&&(InternalBdd<DdType::CUDD> const& other) const;

    InternalBdd<DdType::CUDD>& operator&=(InternalBdd<DdType::CUDD> const& other);

    InternalBdd<DdType::CUDD> iff(InternalBdd<DdType::CUDD> const& other) const;

    InternalBdd<DdType::CUDD> exclusiveOr(InternalBdd<DdType::CUDD> const& other) const;

    InternalBdd<DdType::CUDD> implies(InternalBdd<DdType::CUDD> const& other) const;

    InternalBdd<DdType::CUDD> operator!() const;

    InternalBdd<DdType::CUDD>& complement();

    InternalBdd<DdType::CUDD> existsAbstract(InternalBdd<DdType::CUDD> const& cube) const;

    InternalBdd<DdType::CUDD> existsAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const;

    InternalBdd<DdType::CUDD> universalAbstract(InternalBdd<DdType::CUDD> const& cube) const;

    InternalBdd<DdType::CUDD> swapVariables(std::vector<InternalBdd<DdType::CUDD>> const& from, std::vector<InternalBdd<DdType::CUDD>> const& to) const;

    InternalBdd<DdType::CUDD> andExists(InternalBdd<DdType::CUDD> const& other, InternalBdd<storm::dd::DdType::CUDD> const& cube) const;

    InternalBdd<DdType::CUDD> constrain(InternalBdd<DdType::CUDD> const& constraint) const;

    InternalBdd<DdType::CUDD> restrict(InternalBdd<DdType::CUDD> const& constraint) const;

    InternalBdd<DdType::CUDD> 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::CUDD, 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::CUDD>> splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
 
    friend struct std::hash<storm::dd::InternalBdd<storm::dd::DdType::CUDD>>;
 
#ifdef STORM_HAVE_CUDD
    cudd::BDD getCuddBdd() const;

    DdNode* getCuddDdNode() const;
#endif
 
   private:
#ifdef STORM_HAVE_CUDD
    static DdNode* fromVectorRec(::DdManager* manager, 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);

    void toVectorRec(DdNode const* dd, cudd::Cudd const& manager, 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;
 
    // 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<DdNode const*, bool> const& key) const;
    };

    static std::shared_ptr<Odd> createOddRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel,
                                             std::vector<uint_fast64_t> const& ddVariableIndices,
                                             std::vector<std::unordered_map<DdNode const*, std::shared_ptr<Odd>>>& uniqueTableForLevels);

    template<typename ValueType>
    static void filterExplicitVectorRec(DdNode const* dd, cudd::Cudd const& manager, 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(DdNode const* dd, cudd::Cudd const& manager, 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(
        DdNode const* dd, cudd::Cudd const& ddManager, 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<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex);
 
    void splitIntoGroupsRec(DdNode* dd, bool negated, std::vector<InternalBdd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices,
                            uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;
 
    InternalDdManager<DdType::CUDD> const* ddManager;
 
    cudd::BDD cuddBdd;
#endif
};
}  // namespace dd
}  // namespace storm
 
namespace std {
template<>
struct hash<storm::dd::InternalBdd<storm::dd::DdType::CUDD>> {
#ifdef STORM_HAVE_CUDD
    std::size_t operator()(storm::dd::InternalBdd<storm::dd::DdType::CUDD> const& key) const {
        return reinterpret_cast<std::size_t>(key.cuddBdd.getNode());
    }
#else
    std::size_t operator()(storm::dd::InternalBdd<storm::dd::DdType::CUDD> const&) const {
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with CUDD support.");
    }
#endif
};
}  // namespace std