ExpressionManager.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONMANAGER_H_
#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONMANAGER_H_
 
#include <cstdint>
#include <iosfwd>
#include <iterator>
#include <unordered_map>
#include <unordered_set>
#include <vector>
 
#include <boost/optional.hpp>
 
#include "storm/adapters/RationalNumberForward.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/utility/OsDetection.h"
 
namespace storm {
namespace expressions {
// Forward-declare manager class for iterator class.
class ExpressionManager;
 
class VariableIterator {
   public:
    // Define iterator
    using iterator_category = std::input_iterator_tag;
    using value_type = std::pair<storm::expressions::Variable, storm::expressions::Type> const;
    using difference_type = std::ptrdiff_t;
    using pointer = std::pair<storm::expressions::Variable, storm::expressions::Type> const*;
    using reference = std::pair<storm::expressions::Variable, storm::expressions::Type> const&;
 
    enum class VariableSelection { OnlyRegularVariables, OnlyAuxiliaryVariables, AllVariables };
 
    VariableIterator(ExpressionManager const& manager, std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIterator,
                     std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIteratorEnd, VariableSelection const& selection);
    VariableIterator(VariableIterator&& other) = default;
 
    // Define the basic input iterator operations.
    bool operator==(VariableIterator const& other);
    bool operator!=(VariableIterator const& other);
    value_type& operator*();
    VariableIterator& operator++(int);
    VariableIterator& operator++();
 
   private:
    void moveUntilNextSelectedElement(bool atLeastOneStep = true);
 
    // The manager responsible for the variable to iterate over.
    ExpressionManager const& manager;
 
    // The underlying iterator that ranges over all names and the corresponding indices.
    std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIterator;
 
    // The iterator indicating the end of the underlying iterator range.
    std::unordered_map<std::string, uint_fast64_t>::const_iterator nameIndexIteratorEnd;
 
    // A field indicating which variables we are supposed to iterate over.
    VariableSelection selection;
 
    // The current element that is shown to the outside upon dereferencing.
    std::pair<storm::expressions::Variable, storm::expressions::Type> currentElement;
};
 
class ExpressionManager : public std::enable_shared_from_this<ExpressionManager> {
   public:
    friend class VariableIterator;
 
    typedef VariableIterator const_iterator;
 
    ExpressionManager();
 
    ~ExpressionManager();
 
    std::shared_ptr<ExpressionManager> clone() const;
 
    // Create default instantiations for the move construction/assignment.
    ExpressionManager(ExpressionManager&& other) = default;
    ExpressionManager& operator=(ExpressionManager&& other) = default;
 
    Expression boolean(bool value) const;
 
    Expression integer(int_fast64_t value) const;
 
    Expression rational(double value) const;
 
    Expression rational(storm::RationalNumber const& value) const;
 
    bool operator==(ExpressionManager const& other) const;
 
    Type const& getBooleanType() const;
 
    Type const& getIntegerType() const;
 
    Type const& getBitVectorType(std::size_t width) const;
 
    Type const& getRationalType() const;
 
    Type const& getArrayType(Type elementType) const;
 
    Type const& getTranscendentalNumberType() const;
 
    Variable declareVariableCopy(Variable const& variable);
 
    Variable declareVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary = false);
 
    Variable declareBooleanVariable(std::string const& name, bool auxiliary = false);
 
    Variable declareIntegerVariable(std::string const& name, bool auxiliary = false);
 
    Variable declareBitVectorVariable(std::string const& name, std::size_t width, bool auxiliary = false);
 
    Variable declareRationalVariable(std::string const& name, bool auxiliary = false);
 
    Variable declareArrayVariable(std::string const& name, Type const& elementType, bool auxiliary = false);
 
    Variable declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary = false);
 
    Variable getVariable(std::string const& name) const;
 
    std::set<Variable> const& getVariables() const;
 
    bool hasVariable(std::string const& name) const;
 
    Expression getVariableExpression(std::string const& name) const;
 
    Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false, std::string const& prefix = "_x");
 
    Variable declareFreshRationalVariable(bool auxiliary = false, std::string const& prefix = "_x");
 
    Variable declareFreshBooleanVariable(bool auxiliary = false, std::string const& prefix = "_x");
 
    Variable declareFreshIntegerVariable(bool auxiliary = false, std::string const& prefix = "_x");
 
    uint_fast64_t getNumberOfVariables() const;
 
    uint_fast64_t getNumberOfBooleanVariables() const;
 
    uint_fast64_t getNumberOfIntegerVariables() const;
 
    uint_fast64_t getNumberOfBitVectorVariables() const;
 
    uint_fast64_t getNumberOfRationalVariables() const;
 
    uint_fast64_t getNumberOfArrayVariables() const;
 
    std::string const& getVariableName(uint_fast64_t index) const;
 
    Type const& getVariableType(uint_fast64_t index) const;
 
    uint_fast64_t getOffset(uint_fast64_t index) const;
 
    const_iterator begin() const;
 
    const_iterator end() const;
 
    std::shared_ptr<ExpressionManager> getSharedPointer();
 
    std::shared_ptr<ExpressionManager const> getSharedPointer() const;
 
    friend std::ostream& operator<<(std::ostream& out, ExpressionManager const& manager);
 
   private:
    // Explicitly make copy construction/assignment private, since the manager is supposed to be stored as a pointer
    // of some sort. This is because the expression classes store a reference to the manager and it must
    // therefore be guaranteed that they do not become invalid, because the manager has been copied.
    ExpressionManager(ExpressionManager const& other) = default;
    ExpressionManager& operator=(ExpressionManager const& other) = default;
 
    static bool isValidVariableName(std::string const& name);
 
    bool variableExists(std::string const& name) const;
 
    Variable declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary, bool checkName);
 
    uint_fast64_t getNumberOfVariables(storm::expressions::Type const& variableType) const;
 
    uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const;
 
    // The set of all known variables.
    std::set<Variable> variableSet;
 
    // A mapping from all variable names (auxiliary + normal) to their indices.
    std::unordered_map<std::string, uint_fast64_t> nameToIndexMapping;
 
    // A mapping from all variable indices to their names.
    std::unordered_map<uint64_t, std::string> indexToNameMapping;
 
    // A mapping from all variable indices to their types.
    std::unordered_map<uint64_t, Type> indexToTypeMapping;
 
    // Store counts for variables.
    uint_fast64_t numberOfBooleanVariables;
    uint_fast64_t numberOfIntegerVariables;
    uint_fast64_t numberOfBitVectorVariables;
    uint_fast64_t numberOfRationalVariables;
    uint_fast64_t numberOfArrayVariables;
 
    // The number of declared auxiliary variables.
    uint_fast64_t numberOfAuxiliaryVariables;
 
    // Store counts for auxiliary variables.
    uint_fast64_t numberOfAuxiliaryBooleanVariables;
    uint_fast64_t numberOfAuxiliaryIntegerVariables;
    uint_fast64_t numberOfAuxiliaryBitVectorVariables;
    uint_fast64_t numberOfAuxiliaryRationalVariables;
    uint_fast64_t numberOfAuxiliaryArrayVariables;
 
    // A counter used to create fresh variables.
    uint_fast64_t freshVariableCounter;
 
    // The types managed by this manager.
    mutable boost::optional<Type> booleanType;
    mutable boost::optional<Type> integerType;
    mutable std::unordered_set<Type> bitvectorTypes;
    mutable boost::optional<Type> rationalType;
    mutable std::unordered_set<Type> arrayTypes;
    mutable boost::optional<Type> transcendentalNumberType;
 
    // A mask that can be used to query whether a variable is an auxiliary variable.
    static const uint64_t auxiliaryMask = (1ull << 50);
 
    // A mask that can be used to project a variable index to its offset (with the group of equally typed variables).
    static const uint64_t offsetMask = (1ull << 50) - 1;
};
 
std::ostream& operator<<(std::ostream& out, ExpressionManager const& manager);
}  // namespace expressions
}  // namespace storm
 
#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONMANAGER_H_ */