InternalCuddAdd.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/adapters/RationalNumberAdapter.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/InternalAdd.h"
#include "storm/storage/dd/Odd.h"
#include "storm/storage/expressions/Variable.h"
 
#ifdef STORM_HAVE_CUDD
// Include the C++-interface of CUDD.
#include "cuddObj.hh"
#endif
 
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;
 
namespace bisimulation {
template<DdType LibraryType, typename ValueType>
class InternalSignatureRefiner;
}
 
template<typename ValueType>
class InternalAdd<DdType::CUDD, ValueType> {
   public:
    friend class InternalBdd<DdType::CUDD>;
 
    friend class bisimulation::InternalSignatureRefiner<DdType::CUDD, ValueType>;
 
#ifdef STORM_HAVE_CUDD
    InternalAdd(InternalDdManager<DdType::CUDD> const* ddManager, cudd::ADD cuddAdd);
#endif
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    InternalAdd() = default;
    InternalAdd(InternalAdd<DdType::CUDD, ValueType> const& other) = default;
    InternalAdd& operator=(InternalAdd<DdType::CUDD, ValueType> const& other) = default;
    InternalAdd(InternalAdd<DdType::CUDD, ValueType>&& other) = default;
    InternalAdd& operator=(InternalAdd<DdType::CUDD, ValueType>&& other) = default;
    virtual ~InternalAdd() = default;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    template<typename TargetValueType>
    typename std::enable_if<std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type toValueType() const;
    template<typename TargetValueType>
    typename std::enable_if<!std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type toValueType() const;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    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::CUDD, ValueType> begin(DdManager<DdType::CUDD> const& fullDdManager, InternalBdd<DdType::CUDD> const& variableCube,
                                               uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables,
                                               bool enumerateDontCareMetaVariables = true) const;

    AddIterator<DdType::CUDD, ValueType> end(DdManager<DdType::CUDD> 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 forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
                 std::function<void(uint64_t 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;

    std::vector<InternalAdd<DdType::CUDD, 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::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> splitIntoGroups(
        InternalAdd<DdType::CUDD, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;

    std::vector<std::vector<InternalAdd<DdType::CUDD, ValueType>>> splitIntoGroups(std::vector<InternalAdd<DdType::CUDD, 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::CUDD, ValueType> fromVector(InternalDdManager<DdType::CUDD> 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::CUDD> const& getInternalDdManager() const;
 
#ifdef STORM_HAVE_CUDD
    cudd::ADD getCuddAdd() const;

    DdNode* getCuddDdNode() const;
#endif

    std::string getStringId() const;
 
   private:
#ifdef STORM_HAVE_CUDD
    void forEachRec(DdNode const* 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 splitIntoGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices,
                            uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;

    void decodeGroupLabelsRec(DdNode* 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(DdNode* dd1, DdNode* dd2,
                            std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>>& groups,
                            std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;

    void splitIntoGroupsRec(std::vector<DdNode*> const& dds, std::vector<std::vector<InternalAdd<DdType::CUDD, ValueType>>>& groups,
                            std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;

    void toMatrixComponentsRec(DdNode const* dd, 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 DdNode* fromVectorRec(::DdManager* manager, 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);

    static std::shared_ptr<Odd> createOddRec(DdNode* 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*, std::shared_ptr<Odd>>>& uniqueTableForLevels);
 
    InternalDdManager<DdType::CUDD> const* ddManager;
 
    cudd::ADD cuddAdd;
#endif
};
}  // namespace dd
}  // namespace storm