Bdd.h

Go to the documentation of this file.

#pragma once
 
#include <functional>
 
#include "storm/storage/BitVector.h"
#include "storm/storage/PairHash.h"
#include "storm/storage/dd/Dd.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/cudd/InternalCuddBdd.h"
#include "storm/storage/dd/sylvan/InternalSylvanBdd.h"
 
namespace storm {
namespace logic {
enum class ComparisonType;
}
 
namespace dd {
template<DdType LibraryType, typename ValueType>
class Add;
 
class Odd;
 
template<DdType LibraryType>
class Bdd : public Dd<LibraryType> {
   public:
    friend class DdManager<LibraryType>;
 
    template<DdType LibraryTypePrime, typename ValueTypePrime>
    friend class Add;
 
    Bdd(DdManager<LibraryType> const& ddManager, InternalBdd<LibraryType> const& internalBdd,
        std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    Bdd() = default;
    Bdd(Bdd<LibraryType> const& other) = default;
    Bdd& operator=(Bdd<LibraryType> const& other) = default;
    Bdd(Bdd<LibraryType>&& other) = default;
    Bdd& operator=(Bdd<LibraryType>&& other) = default;
 
    static Bdd<LibraryType> getEncoding(DdManager<LibraryType> const& ddManager, uint64_t targetOffset, storm::dd::Odd const& odd,
                                        std::set<storm::expressions::Variable> const& metaVariables);
 
    static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, storm::storage::BitVector const& truthValues, storm::dd::Odd const& odd,
                                       std::set<storm::expressions::Variable> const& metaVariables);
 
    template<typename ValueType>
    static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& explicitValues, storm::dd::Odd const& odd,
                                       std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType,
                                       ValueType value);
 
    bool operator==(Bdd<LibraryType> const& other) const;
 
    bool operator!=(Bdd<LibraryType> const& other) const;
 
    Bdd<LibraryType> ite(Bdd<LibraryType> const& thenBdd, Bdd<LibraryType> const& elseBdd) const;
 
    template<typename ValueType>
    Add<LibraryType, ValueType> ite(Add<LibraryType, ValueType> const& thenAdd, Add<LibraryType, ValueType> const& elseAdd) const;
 
    Bdd<LibraryType> operator||(Bdd<LibraryType> const& other) const;
 
    Bdd<LibraryType>& operator|=(Bdd<LibraryType> const& other);
 
    Bdd<LibraryType> operator&&(Bdd<LibraryType> const& other) const;
 
    Bdd<LibraryType>& operator&=(Bdd<LibraryType> const& other);
 
    Bdd<LibraryType> iff(Bdd<LibraryType> const& other) const;
 
    Bdd<LibraryType> exclusiveOr(Bdd<LibraryType> const& other) const;
 
    Bdd<LibraryType> implies(Bdd<LibraryType> const& other) const;
 
    Bdd<LibraryType> operator!() const;
 
    Bdd<LibraryType>& complement();
 
    Bdd<LibraryType> existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    Bdd<LibraryType> existsAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    Bdd<LibraryType> universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    Bdd<LibraryType> andExists(Bdd<LibraryType> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
 
    Bdd<LibraryType> constrain(Bdd<LibraryType> const& constraint) const;
 
    Bdd<LibraryType> restrict(Bdd<LibraryType> const& constraint) const;
 
    Bdd<LibraryType> relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables,
                                       std::set<storm::expressions::Variable> const& columnMetaVariables) const;
 
    Bdd<LibraryType> inverseRelationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables,
                                              std::set<storm::expressions::Variable> const& columnMetaVariables) const;
 
    Bdd<LibraryType> inverseRelationalProductWithExtendedRelation(Bdd<LibraryType> const& relation,
                                                                  std::set<storm::expressions::Variable> const& rowMetaVariables,
                                                                  std::set<storm::expressions::Variable> const& columnMetaVariables) const;
 
    Bdd<LibraryType> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
 
    Bdd<LibraryType> renameVariables(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
 
    Bdd<LibraryType> renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
 
    Bdd<LibraryType> renameVariablesConcretize(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
 
    bool isOne() const;
 
    bool isZero() const;
 
    template<typename ValueType>
    Add<LibraryType, ValueType> toAdd() const;
 
    std::vector<Bdd<LibraryType>> split(std::set<storm::expressions::Variable> const& variables) const;
 
    storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd) const;
 
    std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<uint_fast64_t, storm::expressions::Variable>> toExpression(
        storm::expressions::ExpressionManager& manager) const;
 
    virtual Bdd<LibraryType> getSupport() const override;
 
    virtual uint_fast64_t getNonZeroCount() const override;
 
    virtual uint_fast64_t getLeafCount() const override;
 
    virtual uint_fast64_t getNodeCount() const override;
 
    virtual uint_fast64_t getIndex() const override;
 
    virtual uint_fast64_t getLevel() const override;
 
    virtual void exportToDot(std::string const& filename, bool showVariablesIfPossible = true) const override;
 
    virtual void exportToText(std::string const& filename) const override;
 
    static Bdd<LibraryType> getCube(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables);
 
    Odd createOdd() const;
 
    template<typename ValueType>
    std::vector<ValueType> filterExplicitVector(Odd const& odd, std::vector<ValueType> const& values) const;
 
    storm::storage::BitVector filterExplicitVector(Odd const& odd, storm::storage::BitVector const& values) const;
 
    InternalBdd<LibraryType> const& getInternalBdd() const;
 
    friend struct std::hash<storm::dd::Bdd<LibraryType>>;
 
    template<DdType LibraryTypePrime, typename ValueType>
    friend struct FromVectorHelper;
 
   private:
    // The internal BDD that depends on the chosen library.
    InternalBdd<LibraryType> internalBdd;
};
}  // namespace dd
}  // namespace storm
 
namespace std {
template<storm::dd::DdType LibraryType>
struct hash<storm::dd::Bdd<LibraryType>> {
    std::size_t operator()(storm::dd::Bdd<LibraryType> const& key) const {
        return std::hash<storm::dd::InternalBdd<LibraryType>>().operator()(key.internalBdd);
    }
};
}  // namespace std