LocalExpressionInformation.h

Go to the documentation of this file.

#pragma once
 
#include <ostream>
#include <set>
#include <unordered_map>
#include <vector>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
 
#include "storm/storage/dd/DdType.h"
 
namespace storm::gbar {
namespace abstraction {
 
template<storm::dd::DdType DdType>
class AbstractionInformation;
 
template<storm::dd::DdType DdType>
class LocalExpressionInformation {
   public:
    LocalExpressionInformation(AbstractionInformation<DdType> const& abstractionInformation);
 
    std::map<uint64_t, uint64_t> addExpression(uint_fast64_t globalExpressionIndex);
 
    bool areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable);
 
    std::map<uint64_t, uint64_t> relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable);
 
    std::map<uint64_t, uint64_t> relate(std::set<storm::expressions::Variable> const& variables);
 
    std::set<storm::expressions::Variable> const& getBlockOfVariable(storm::expressions::Variable const& variable) const;
 
    uint_fast64_t getBlockIndexOfVariable(storm::expressions::Variable const& variable) const;
 
    std::set<uint_fast64_t> getBlockIndicesOfVariables(std::set<storm::expressions::Variable> const& variables) const;
 
    uint_fast64_t getNumberOfBlocks() const;
 
    std::set<storm::expressions::Variable> const& getVariableBlockWithIndex(uint_fast64_t blockIndex) const;
 
    std::set<uint_fast64_t> const& getRelatedExpressions(storm::expressions::Variable const& variable) const;
 
    std::set<uint_fast64_t> getRelatedExpressions(std::set<storm::expressions::Variable> const& variables) const;
 
    std::set<uint_fast64_t> const& getExpressionsUsingVariable(storm::expressions::Variable const& variable) const;
 
    std::set<uint_fast64_t> getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const;
 
    std::set<uint_fast64_t> const& getExpressionBlock(uint64_t index) const;
 
    template<storm::dd::DdType DdTypePrime>
    friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<DdTypePrime> const& partition);
 
   private:
    std::map<uint64_t, uint64_t> mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge);
 
    // The set of variables relevant for this partition.
    std::set<storm::expressions::Variable> relevantVariables;
 
    // A mapping from variables to their blocks.
    std::unordered_map<storm::expressions::Variable, uint_fast64_t> variableToBlockMapping;
 
    // The variable blocks of the partition.
    std::vector<std::set<storm::expressions::Variable>> variableBlocks;
 
    // The expression blocks of the partition.
    std::vector<std::set<uint_fast64_t>> expressionBlocks;
 
    // A mapping from variables to the indices of all expressions they appear in.
    std::unordered_map<storm::expressions::Variable, std::set<uint_fast64_t>> variableToExpressionsMapping;
 
    // The object storing the abstraction information.
    std::reference_wrapper<AbstractionInformation<DdType> const> abstractionInformation;
};
 
template<storm::dd::DdType DdType>
std::ostream& operator<<(std::ostream& out, LocalExpressionInformation<DdType> const& partition);
 
}  // namespace abstraction
}  // namespace storm::gbar