ArrayEliminator.h

Go to the documentation of this file.

#pragma once
 
#include <boost/variant.hpp>
 
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/jani/Variable.h"
 
namespace storm {
namespace expressions {
class Expression;
}
 
namespace jani {
class Model;
class Property;
 
struct ArrayEliminatorData {
    class Replacement {
       public:
        Replacement(storm::jani::Variable const& variable);
        Replacement(std::vector<Replacement>&& replacements = {});
        bool isVariable() const;
        storm::jani::Variable const& getVariable() const;
        std::vector<Replacement> const& getReplacements() const;
        Replacement const& at(std::size_t const& index) const;                 
        Replacement& at(std::size_t const& index);                             
        Replacement const& at(std::vector<std::size_t> const& indices) const;  
        Replacement& at(std::vector<std::size_t> const& indices);              
        std::size_t size() const;                                              
        void grow(std::size_t const& minimumSize);                             
 
       private:
        boost::variant<storm::jani::Variable const*, std::vector<Replacement>> data;
    };
    std::vector<std::shared_ptr<Variable>> eliminatedArrayVariables;
    std::unordered_map<storm::expressions::Variable, Replacement> replacements;
 
    // Transforms the given expression (which might contain array expressions) to an equivalent expression without array variables.
    storm::expressions::Expression transformExpression(storm::expressions::Expression const& arrayExpression) const;
    // Transforms the given property (which might contain array expressions) to an equivalent property without array variables.
    void transformProperty(storm::jani::Property& property) const;
};
 
class ArrayEliminator {
   public:
    ArrayEliminator() = default;
 
    ArrayEliminatorData eliminate(Model& model, bool keepNonTrivialArrayAccess = false);
};
}  // namespace jani
}  // namespace storm