Add.h

Go to the documentation of this file.

#pragma once
 
#include <map>
 
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/dd/Dd.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/InternalAdd.h"
#include "storm/storage/dd/InternalDdManager.h"
#include "storm/storage/dd/Odd.h"
#include "storm/storage/dd/cudd/CuddAddIterator.h"
#include "storm/storage/dd/cudd/InternalCuddAdd.h"
#include "storm/storage/dd/sylvan/InternalSylvanAdd.h"
#include "storm/storage/dd/sylvan/SylvanAddIterator.h"
 
namespace storm {
namespace dd {
template<DdType LibraryType>
class Bdd;
 
template<DdType LibraryType, typename ValueType>
class AddIterator;
 
namespace bisimulation {
template<DdType LibraryType, typename ValueType>
class InternalSignatureRefiner;
}
 
template<DdType LibraryType, typename ValueType = double>
class Add : public Dd<LibraryType> {
   public:
    friend class DdManager<LibraryType>;
    friend class Bdd<LibraryType>;
 
    template<DdType LibraryTypePrime, typename ValueTypePrime>
    friend class Add;
 
    friend class bisimulation::InternalSignatureRefiner<LibraryType, ValueType>;
 
    // Instantiate all copy/move constructors/assignments with the default implementation.
    Add() = default;
    Add(Add<LibraryType, ValueType> const& other) = default;
    Add& operator=(Add<LibraryType, ValueType> const& other) = default;
    Add(Add<LibraryType, ValueType>&& other) = default;
    Add& operator=(Add<LibraryType, ValueType>&& other) = default;
 
    static Add<LibraryType, ValueType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd,
                                                  std::set<storm::expressions::Variable> const& metaVariables);
 
    bool operator==(Add<LibraryType, ValueType> const& other) const;
 
    bool operator!=(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType> operator+(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType>& operator+=(Add<LibraryType, ValueType> const& other);
 
    Add<LibraryType, ValueType> operator*(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType>& operator*=(Add<LibraryType, ValueType> const& other);
 
    Add<LibraryType, ValueType> operator-(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType> operator-() const;
 
    Add<LibraryType, ValueType>& operator-=(Add<LibraryType, ValueType> const& other);
 
    Add<LibraryType, ValueType> operator/(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType>& operator/=(Add<LibraryType, ValueType> const& other);
 
    Bdd<LibraryType> equals(Add<LibraryType, ValueType> const& other) const;
 
    Bdd<LibraryType> notEquals(Add<LibraryType, ValueType> const& other) const;
 
    Bdd<LibraryType> less(Add<LibraryType, ValueType> const& other) const;
 
    Bdd<LibraryType> lessOrEqual(Add<LibraryType, ValueType> const& other) const;
 
    Bdd<LibraryType> greater(Add<LibraryType, ValueType> const& other) const;
 
    Bdd<LibraryType> greaterOrEqual(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType> pow(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType> mod(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType> logxy(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType> floor() const;
 
    Add<LibraryType, ValueType> ceil() const;
 
    Add<LibraryType, storm::RationalNumber> sharpenKwekMehlhorn(uint64_t precision) const;
 
    Add<LibraryType, ValueType> minimum(Add<LibraryType, ValueType> const& other) const;
 
    Add<LibraryType, ValueType> maximum(Add<LibraryType, ValueType> const& other) const;
 
    template<typename TargetValueType>
    typename std::enable_if_t<std::is_same_v<TargetValueType, ValueType>, Add<LibraryType, TargetValueType>> toValueType() const;
    template<typename TargetValueType>
    typename std::enable_if_t<!std::is_same_v<TargetValueType, ValueType>, Add<LibraryType, TargetValueType>> toValueType() const;
 
    Add<LibraryType, ValueType> sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    Add<LibraryType, ValueType> minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    Bdd<LibraryType> minAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    Add<LibraryType, ValueType> maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    Bdd<LibraryType> maxAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const;
 
    bool equalModuloPrecision(Add<LibraryType, ValueType> const& other, ValueType const& precision, bool relative = true) const;
 
    Add<LibraryType, ValueType> renameVariables(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
 
    Add<LibraryType, ValueType> renameVariablesAbstract(std::set<storm::expressions::Variable> const& from,
                                                        std::set<storm::expressions::Variable> const& to) const;
 
    Add<LibraryType, ValueType> swapVariables(
        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
 
    Add<LibraryType, ValueType> permuteVariables(
        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
 
    Add<LibraryType, ValueType> multiplyMatrix(Add<LibraryType, ValueType> const& otherMatrix,
                                               std::set<storm::expressions::Variable> const& summationMetaVariables) const;
 
    Add<LibraryType, ValueType> multiplyMatrix(Bdd<LibraryType> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const;
 
    Bdd<LibraryType> greater(ValueType const& value) const;
 
    Bdd<LibraryType> greaterOrEqual(ValueType const& value) const;
 
    Bdd<LibraryType> less(ValueType const& value) const;
 
    Bdd<LibraryType> lessOrEqual(ValueType const& value) const;
 
    Bdd<LibraryType> notZero() const;
 
    Add<LibraryType, ValueType> constrain(Add<LibraryType, ValueType> const& constraint) const;
 
    Add<LibraryType, ValueType> restrict(Add<LibraryType, ValueType> const& constraint) const;
 
    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;
 
    ValueType getMin() const;
 
    ValueType getMax() const;
 
    void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, ValueType const& targetValue);
 
    void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2,
                  int_fast64_t variableValue2, ValueType const& targetValue);
 
    void setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>(),
                  ValueType const& targetValue = 0);
 
    ValueType getValue(
        std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>()) const;
 
    bool isOne() const;
 
    bool isZero() const;
 
    bool isConstant() const;
 
    virtual uint_fast64_t getIndex() const override;
 
    virtual uint_fast64_t getLevel() const override;
 
    std::vector<ValueType> toVector() const;
 
    std::vector<ValueType> toVector(storm::dd::Odd const& rowOdd) const;
 
    std::vector<ValueType> toVector(storm::dd::Add<LibraryType, ValueType> const& matrix, std::vector<uint_fast64_t> const& rowGroupIndices,
                                    std::set<storm::expressions::Variable> const& rowMetaVariables,
                                    std::set<storm::expressions::Variable> const& columnMetaVariables,
                                    std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd) const;
 
    storm::storage::SparseMatrix<ValueType> toMatrix() const;
 
    storm::storage::SparseMatrix<ValueType> toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
 
    storm::storage::SparseMatrix<ValueType> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables,
                                                     std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd const& rowOdd,
                                                     storm::dd::Odd const& columnOdd) const;
 
    storm::storage::SparseMatrix<ValueType> toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd,
                                                     storm::dd::Odd const& columnOdd) const;
 
    struct MatrixAndLabeling {
        MatrixAndLabeling() = default;
 
        MatrixAndLabeling(storm::storage::SparseMatrix<ValueType> const& matrix) : matrix(matrix) {
            // Intentionally left empty.
        }
 
        MatrixAndLabeling(storm::storage::SparseMatrix<ValueType>&& matrix) : matrix(std::move(matrix)) {
            // Intentionally left empty.
        }
 
        storm::storage::SparseMatrix<ValueType> matrix;
        std::vector<std::vector<uint64_t>> labelings;
    };
 
    MatrixAndLabeling toLabeledMatrix(
        std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd,
        std::vector<std::set<storm::expressions::Variable>> const& labelMetaVariables = std::vector<std::set<storm::expressions::Variable>>()) const;
 
    std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector,
                                                                                              std::set<storm::expressions::Variable> const& groupMetaVariables,
                                                                                              storm::dd::Odd const& rowOdd,
                                                                                              storm::dd::Odd const& columnOdd) const;
    std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> toMatrixVector(
        std::vector<uint_fast64_t>&& rowGroupSizes, storm::dd::Add<LibraryType, ValueType> const& vector,
        std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
 
    std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<std::vector<ValueType>>> toMatrixVectors(
        std::vector<storm::dd::Add<LibraryType, ValueType>> const& vectors, std::set<storm::expressions::Variable> const& groupMetaVariables,
        storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
    std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<std::vector<ValueType>>> toMatrixVectors(
        std::vector<uint_fast64_t>&& rowGroupSizes, std::vector<storm::dd::Add<LibraryType, ValueType>> const& vectors,
        std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables,
        std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
 
    void exportToDot(std::string const& filename, bool showVariablesIfPossible = true) const override;
 
    virtual void exportToText(std::string const& filename) const override;
 
    AddIterator<LibraryType, ValueType> begin(bool enumerateDontCareMetaVariables = true) const;
 
    AddIterator<LibraryType, ValueType> end() const;
 
    template<DdType LibraryTypePrime, typename ValueTypePrime>
    friend std::ostream& operator<<(std::ostream& out, Add<LibraryTypePrime, ValueTypePrime> const& add);
 
    Bdd<LibraryType> toBdd() const;
 
    Odd createOdd() const;
 
    InternalAdd<LibraryType, ValueType> const& getInternalAdd() const;
 
    InternalDdManager<LibraryType> const& getInternalDdManager() const;
 
   private:
    Add(DdManager<LibraryType> const& ddManager, InternalAdd<LibraryType, ValueType> const& internalAdd,
        std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
 
    operator InternalAdd<LibraryType, ValueType>() const;
 
    std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector,
                                                                                              std::set<storm::expressions::Variable> const& rowMetaVariables,
                                                                                              std::set<storm::expressions::Variable> const& columnMetaVariables,
                                                                                              std::set<storm::expressions::Variable> const& groupMetaVariables,
                                                                                              storm::dd::Odd const& rowOdd,
                                                                                              storm::dd::Odd const& columnOdd) const;
 
    // The internal ADD that depends on the chosen library.
    InternalAdd<LibraryType, ValueType> internalAdd;
};
}  // namespace dd
}  // namespace storm