InternalSylvanAdd.h

Go to the documentation of this file.

#pragma once
 
#include <set>
#include <unordered_map>
 
#include "storm-config.h"
#include "storm/adapters/RationalFunctionForward.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/InternalAdd.h"
#include "storm/storage/dd/Odd.h"
#include "storm/storage/dd/sylvan/InternalSylvanBdd.h"
#include "storm/storage/dd/sylvan/SylvanAddIterator.h"
#include "storm/storage/expressions/Variable.h"
 
namespace storm {
namespace storage {
template<typename T>
class SparseMatrix;
 
class BitVector;
 
template<typename E, typename V>
class MatrixEntry;
}  // namespace storage
 
namespace dd {
template<DdType LibraryType>
class DdManager;
 
template<DdType LibraryType>
class InternalDdManager;
 
template<DdType LibraryType>
class InternalBdd;
 
template<DdType LibraryType, typename ValueType>
class AddIterator;
 
template<typename ValueType>
class InternalAdd<DdType::Sylvan, ValueType> {
   public:
    friend class AddIterator<DdType::Sylvan, ValueType>;
    friend class InternalBdd<DdType::Sylvan>;
 
#ifdef STORM_HAVE_SYLVAN
    InternalAdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Mtbdd const& sylvanMtbdd);
#endif
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    InternalAdd();
    InternalAdd(InternalAdd<DdType::Sylvan, ValueType> const& other) = default;
    InternalAdd& operator=(InternalAdd<DdType::Sylvan, ValueType> const& other) = default;
    InternalAdd(InternalAdd<DdType::Sylvan, ValueType>&& other) = default;
    InternalAdd& operator=(InternalAdd<DdType::Sylvan, ValueType>&& other) = default;
    virtual ~InternalAdd() = default;

    bool operator==(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    bool operator!=(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType> operator+(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType>& operator+=(InternalAdd<DdType::Sylvan, ValueType> const& other);

    InternalAdd<DdType::Sylvan, ValueType> operator*(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType>& operator*=(InternalAdd<DdType::Sylvan, ValueType> const& other);

    InternalAdd<DdType::Sylvan, ValueType> operator-(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType>& operator-=(InternalAdd<DdType::Sylvan, ValueType> const& other);

    InternalAdd<DdType::Sylvan, ValueType> operator/(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType>& operator/=(InternalAdd<DdType::Sylvan, ValueType> const& other);

    InternalBdd<DdType::Sylvan> equals(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalBdd<DdType::Sylvan> notEquals(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalBdd<DdType::Sylvan> less(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalBdd<DdType::Sylvan> lessOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalBdd<DdType::Sylvan> greater(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalBdd<DdType::Sylvan> greaterOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType> pow(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType> mod(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType> logxy(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType> floor() const;

    InternalAdd<DdType::Sylvan, ValueType> ceil() const;

    InternalAdd<DdType::Sylvan, storm::RationalNumber> sharpenKwekMehlhorn(size_t precision) const;

    InternalAdd<DdType::Sylvan, ValueType> minimum(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    InternalAdd<DdType::Sylvan, ValueType> maximum(InternalAdd<DdType::Sylvan, ValueType> const& other) const;

    template<typename TargetValueType>
    InternalAdd<DdType::Sylvan, TargetValueType> toValueType() const;

    InternalAdd<DdType::Sylvan, ValueType> sumAbstract(InternalBdd<DdType::Sylvan> const& cube) const;

    InternalAdd<DdType::Sylvan, ValueType> minAbstract(InternalBdd<DdType::Sylvan> const& cube) const;

    InternalBdd<DdType::Sylvan> minAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const;

    InternalAdd<DdType::Sylvan, ValueType> maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const;

    InternalBdd<DdType::Sylvan> maxAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const;

    bool equalModuloPrecision(InternalAdd<DdType::Sylvan, ValueType> const& other, ValueType const& precision, bool relative = true) const;

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

    InternalAdd<DdType::Sylvan, ValueType> permuteVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from,
                                                            std::vector<InternalBdd<DdType::Sylvan>> const& to) const;

    InternalAdd<DdType::Sylvan, ValueType> multiplyMatrix(InternalAdd<DdType::Sylvan, ValueType> const& otherMatrix,
                                                          std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const;

    InternalAdd<DdType::Sylvan, ValueType> multiplyMatrix(InternalBdd<DdType::Sylvan> const& otherMatrix,
                                                          std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const;

    InternalBdd<DdType::Sylvan> greater(ValueType const& value) const;

    InternalBdd<DdType::Sylvan> greaterOrEqual(ValueType const& value) const;

    InternalBdd<DdType::Sylvan> less(ValueType const& value) const;

    InternalBdd<DdType::Sylvan> lessOrEqual(ValueType const& value) const;

    InternalBdd<DdType::Sylvan> notZero() const;

    InternalAdd<DdType::Sylvan, ValueType> constrain(InternalAdd<DdType::Sylvan, ValueType> const& constraint) const;

    InternalAdd<DdType::Sylvan, ValueType> restrict(InternalAdd<DdType::Sylvan, ValueType> const& constraint) const;

    InternalBdd<DdType::Sylvan> getSupport() const;

    virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;

    virtual uint_fast64_t getLeafCount() const;

    virtual uint_fast64_t getNodeCount() const;

    ValueType getMin() const;

    ValueType getMax() const;

    ValueType getValue() const;

    bool isOne() const;

    bool isZero() const;

    bool isConstant() 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;

    AddIterator<DdType::Sylvan, ValueType> begin(DdManager<DdType::Sylvan> const& fullDdManager, InternalBdd<DdType::Sylvan> const& variableCube,
                                                 uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables,
                                                 bool enumerateDontCareMetaVariables = true) const;

    AddIterator<DdType::Sylvan, ValueType> end(DdManager<DdType::Sylvan> const& fullDdManager) const;

    void composeWithExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector,
                                   std::function<ValueType(ValueType const&, ValueType const&)> const& function) const;

    void composeWithExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets,
                                   std::vector<ValueType>& targetVector, std::function<ValueType(ValueType const&, ValueType const&)> const& function) const;

    void forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
                 std::function<void(uint64_t const&, ValueType const&)> const& function) const;

    std::vector<InternalAdd<DdType::Sylvan, ValueType>> splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;

    std::vector<uint64_t> decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices,
                                            storm::storage::BitVector const& ddLabelVariableIndices) const;

    std::vector<std::pair<InternalAdd<DdType::Sylvan, ValueType>, InternalAdd<DdType::Sylvan, ValueType>>> splitIntoGroups(
        InternalAdd<DdType::Sylvan, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;

    std::vector<std::vector<InternalAdd<DdType::Sylvan, ValueType>>> splitIntoGroups(std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& vectors,
                                                                                     std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;

    void toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications,
                            std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd,
                            std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices,
                            bool writeValues) const;

    static InternalAdd<DdType::Sylvan, ValueType> fromVector(InternalDdManager<DdType::Sylvan> const* ddManager, std::vector<ValueType> const& values,
                                                             storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices);

    Odd createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const;
 
    InternalDdManager<DdType::Sylvan> const& getInternalDdManager() const;
 
#ifdef STORM_HAVE_SYLVAN
    sylvan::Mtbdd getSylvanMtbdd() const;

    static ValueType getValue(MTBDD const& node);
#endif
 
    std::string getStringId() const;
 
   private:
#ifdef STORM_HAVE_SYLVAN
    static std::shared_ptr<Odd> createOddRec(BDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices,
                                             std::vector<std::unordered_map<BDD, std::shared_ptr<Odd>>>& uniqueTableForLevels);

    void forEachRec(MTBDD dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd,
                    std::vector<uint_fast64_t> const& ddVariableIndices, std::function<void(uint64_t const&, ValueType const&)> const& function) const;

    void decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices,
                              storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel,
                              uint64_t label) const;

    void splitIntoGroupsRec(MTBDD dd, bool negated, std::vector<InternalAdd<DdType::Sylvan, ValueType>>& groups,
                            std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;

    void splitIntoGroupsRec(MTBDD dd1, bool negated1, MTBDD dd2, bool negated2,
                            std::vector<std::pair<InternalAdd<DdType::Sylvan, ValueType>, InternalAdd<DdType::Sylvan, ValueType>>>& groups,
                            std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;

    void splitIntoGroupsRec(std::vector<MTBDD> const& dds, storm::storage::BitVector const& negatedDds,
                            std::vector<std::vector<InternalAdd<DdType::Sylvan, ValueType>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices,
                            uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;

    static MTBDD fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values,
                               Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices);

    void toMatrixComponentsRec(MTBDD dd, bool negated, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications,
                               std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd,
                               uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset,
                               uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices,
                               std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const;

    static MTBDD getLeaf(double value);

    static MTBDD getLeaf(uint_fast64_t value);

    static MTBDD getLeaf(storm::RationalNumber const& value);

    static MTBDD getLeaf(storm::RationalFunction const& value);
 
    // The manager responsible for this MTBDD.
    InternalDdManager<DdType::Sylvan> const* ddManager;
 
    // The underlying sylvan MTBDD.
    sylvan::Mtbdd sylvanMtbdd;
#endif
};
}  // namespace dd
}  // namespace storm