Type.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_
#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_
 
#include <cstdint>
#include <iosfwd>
#include <memory>
 
namespace storm {
namespace expressions {
class ExpressionManager;
class BaseType;
 
class Type {
   public:
    friend bool operator<(storm::expressions::Type const& type1, storm::expressions::Type const& type2);
 
    Type();
 
    Type(std::shared_ptr<ExpressionManager const> const& manager, std::shared_ptr<BaseType> const& innerType);
 
    bool operator==(Type const& other) const;
 
    uint64_t getMask() const;
 
    std::string getStringRepresentation() const;
 
    bool isBooleanType() const;
 
    bool isIntegerType() const;
 
    bool isBitVectorType() const;
 
    bool isRationalType() const;
 
    bool isNumericalType() const;
 
    bool isArrayType() const;
 
    bool isTranscendentalNumberType() const;
 
    std::size_t getWidth() const;
 
    Type getElementType() const;
 
    storm::expressions::ExpressionManager const& getManager() const;
 
    // Functions that, given the input types, produce the output type of the corresponding function application.
    Type plusMinusTimes(Type const& other) const;
    Type minus() const;
    Type divide(Type const& other) const;
    Type modulo(Type const& other) const;
    Type logarithm(Type const& other) const;
    Type power(Type const& other, bool allowIntegerType = false) const;
    Type trigonometric() const;
    Type logicalConnective(Type const& other) const;
    Type logicalConnective() const;
    Type numericalComparison(Type const& other) const;
    Type ite(Type const& thenType, Type const& elseType) const;
    Type floorCeil() const;
    Type minimumMaximum(Type const& other) const;
 
   private:
    // The manager responsible for the type.
    std::shared_ptr<ExpressionManager const> manager;
 
    // The encapsulated type.
    std::shared_ptr<BaseType> innerType;
};
 
std::ostream& operator<<(std::ostream& stream, Type const& type);
 
bool operator<(storm::expressions::Type const& type1, storm::expressions::Type const& type2);
 
class BaseType {
   public:
    BaseType();
    virtual ~BaseType() = default;
 
    virtual uint64_t getMask() const = 0;
 
    virtual bool operator==(BaseType const& other) const;
 
    virtual std::string getStringRepresentation() const = 0;
 
    virtual bool isErrorType() const;
    virtual bool isBooleanType() const;
    virtual bool isIntegerType() const;
    virtual bool isBitVectorType() const;
    virtual bool isRationalType() const;
    virtual bool isArrayType() const;
    virtual bool isTranscendentalNumberType() const;
};
 
class BooleanType : public BaseType {
   public:
    virtual uint64_t getMask() const override;
    virtual std::string getStringRepresentation() const override;
    virtual bool isBooleanType() const override;
 
   private:
    static const uint64_t mask = (1ull << 56);
};
 
class IntegerType : public BaseType {
   public:
    virtual uint64_t getMask() const override;
    virtual std::string getStringRepresentation() const override;
    virtual bool isIntegerType() const override;
 
   private:
    static const uint64_t mask = (1ull << 58);
};
 
class BitVectorType : public BaseType {
   public:
    BitVectorType(std::size_t width);
 
    std::size_t getWidth() const;
 
    virtual bool operator==(BaseType const& other) const override;
    virtual uint64_t getMask() const override;
    virtual std::string getStringRepresentation() const override;
    virtual bool isIntegerType() const override;
    virtual bool isBitVectorType() const override;
 
   private:
    static const uint64_t mask = (1ull << 57);
 
    // The bit width of the type.
    std::size_t width;
};
 
class RationalType : public BaseType {
   public:
    virtual uint64_t getMask() const override;
    virtual std::string getStringRepresentation() const override;
    virtual bool isRationalType() const override;
 
   private:
    static const uint64_t mask = (1ull << 59);
};
 
class ArrayType : public BaseType {
   public:
    ArrayType(Type elementType);
 
    Type getElementType() const;
 
    virtual bool operator==(BaseType const& other) const override;
    virtual uint64_t getMask() const override;
    virtual std::string getStringRepresentation() const override;
    virtual bool isArrayType() const override;
 
   private:
    static const uint64_t mask = (1ull << 55);
 
    // The type of the array elements (can again be of type array).
    Type elementType;
};
 
class TranscendentalNumberType : public BaseType {
   public:
    virtual uint64_t getMask() const override;
    virtual std::string getStringRepresentation() const override;
    virtual bool isTranscendentalNumberType() const override;
 
   private:
    static const uint64_t mask = (1ull << 60);
};
 
class ErrorType : public BaseType {
   public:
    virtual uint64_t getMask() const override;
    virtual std::string getStringRepresentation() const override;
    virtual bool isErrorType() const override;
 
   private:
    static const uint64_t mask = 0;
};
 
bool operator<(BaseType const& first, BaseType const& second);
}  // namespace expressions
}  // namespace storm
 
namespace std {
// Provide a hashing operator, so we can put types in unordered collections.
template<>
struct hash<storm::expressions::Type> {
    std::size_t operator()(storm::expressions::Type const& type) const {
        return std::hash<uint64_t>()(type.getMask());
    }
};
}  // namespace std
 
#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONRETURNTYPE_H_ */