Variable.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_EXPRESSIONS_VARIABLE_H_
#define STORM_STORAGE_EXPRESSIONS_VARIABLE_H_
 
#include <cstdint>
#include <functional>
#include <memory>
 
#include "storm/utility/OsDetection.h"
#include "storm/utility/macros.h"
 
namespace storm {
namespace expressions {
class ExpressionManager;
class Expression;
class Type;
 
// This class captures a simple variable.
class Variable {
   public:
    Variable();
    ~Variable();
 
    Variable(std::shared_ptr<ExpressionManager const> const& manager, uint_fast64_t index);
 
    // Default-instantiate some copy/move construction/assignment.
    Variable(Variable const& other) = default;
    Variable& operator=(Variable const& other) = default;
    Variable(Variable&& other) = default;
    Variable& operator=(Variable&& other) = default;
 
    bool operator==(Variable const& other) const;
 
    bool operator!=(Variable const& other) const;
 
    bool operator<(Variable const& other) const;
 
    std::string const& getName() const;
 
    Type const& getType() const;
 
    storm::expressions::Expression getExpression() const;
 
    ExpressionManager const& getManager() const;
 
    uint_fast64_t getIndex() const;
 
    uint_fast64_t getOffset() const;
 
    bool hasBooleanType() const;
 
    bool hasIntegerType() const;
 
    bool hasBitVectorType() const;
 
    bool hasRationalType() const;
 
    bool hasNumericalType() const;
 
   private:
    // The manager that is responsible for this variable.
    ExpressionManager const* manager;
 
    // The index of the variable.
    uint_fast64_t index;
};
}  // namespace expressions
}  // namespace storm
 
namespace std {
// Provide a hashing operator, so we can put variables in unordered collections.
template<>
struct hash<storm::expressions::Variable> {
    std::size_t operator()(storm::expressions::Variable const& variable) const {
        return std::hash<uint_fast64_t>()(variable.getIndex());
    }
};
}  // namespace std
 
#endif /* STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ */