Expression.h

Go to the documentation of this file.

#pragma once
 
#include <functional>
#include <map>
#include <memory>
#include <set>
#include <unordered_map>
#include <vector>
 
#include "storm-config.h"
#include "storm/storage/expressions/BaseExpression.h"
#include "storm/storage/expressions/BinaryRelationExpression.h"
#include "storm/utility/OsDetection.h"
 
namespace storm {
namespace expressions {
// Foward-declare expression manager class.
class ExpressionManager;
class Variable;
class ExpressionVisitor;
class CompiledExpression;
 
class Expression {
   public:
    friend class ExpressionManager;
    friend class Variable;
    template<typename MapType>
    friend class SubstitutionVisitor;
 
    friend Expression operator+(Expression const& first, Expression const& second);
    friend Expression operator+(Expression const& first, int64_t second);
    friend Expression operator+(int64_t first, Expression const& second);
    friend Expression operator-(Expression const& first, Expression const& second);
    friend Expression operator-(Expression const& first, int64_t second);
    friend Expression operator-(int64_t first, Expression const& second);
    friend Expression operator-(Expression const& first);
    friend Expression operator*(Expression const& first, Expression const& second);
    friend Expression operator/(Expression const& first, Expression const& second);
    friend Expression operator%(Expression const& first, Expression const& second);
    friend Expression operator&&(Expression const& first, Expression const& second);
    friend Expression operator||(Expression const& first, Expression const& second);
    friend Expression operator!(Expression const& first);
    friend Expression operator==(Expression const& first, Expression const& second);
    friend Expression operator!=(Expression const& first, Expression const& second);
    friend Expression operator>(Expression const& first, Expression const& second);
    friend Expression operator>=(Expression const& first, Expression const& second);
    friend Expression operator<(Expression const& first, Expression const& second);
    friend Expression operator<=(Expression const& first, Expression const& second);
    friend Expression operator>(Expression const& first, int64_t second);
    friend Expression operator>=(Expression const& first, int64_t second);
    friend Expression operator<(Expression const& first, int64_t second);
    friend Expression operator<=(Expression const& first, int64_t second);
    friend Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression);
    friend Expression implies(Expression const& first, Expression const& second);
    friend Expression iff(Expression const& first, Expression const& second);
    friend Expression xclusiveor(Expression const& first, Expression const& second);
    friend Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType);
    friend Expression abs(Expression const& first);
    friend Expression truncate(Expression const& first);
    friend Expression sign(Expression const& first);
    friend Expression floor(Expression const& first);
    friend Expression ceil(Expression const& first);
    friend Expression round(Expression const& first);
    friend Expression minimum(Expression const& first, Expression const& second);
    friend Expression maximum(Expression const& first, Expression const& second);
 
    Expression() = default;
    ~Expression();

    Expression(Variable const& variable);

    Expression(std::shared_ptr<BaseExpression const> const& expressionPtr);
 
    // Instantiate constructors and assignments with their default implementations.
    Expression(Expression const& other) = default;
    Expression& operator=(Expression const& other) = default;
    Expression(Expression&&) = default;
    Expression& operator=(Expression&&) = default;

    Expression changeManager(ExpressionManager const& newExpressionManager) const;

    Expression substitute(std::map<Variable, Expression> const& variableToExpressionMap) const;

    Expression substituteNonStandardPredicates() const;
    Expression substitute(std::unordered_map<Variable, Expression> const& variableToExpressionMap) const;

    bool evaluateAsBool(Valuation const* valuation = nullptr) const;

    int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const;

    double evaluateAsDouble(Valuation const* valuation = nullptr) const;

    storm::RationalNumber evaluateAsRational() const;

    Expression simplify() const;

    Expression reduceNesting() const;

    OperatorType getOperator() const;

    bool isFunctionApplication() const;

    uint_fast64_t getArity() const;

    Expression getOperand(uint_fast64_t operandIndex) const;

    std::string const& getIdentifier() const;

    bool containsVariables() const;

    bool isLiteral() const;

    bool isVariable() const;

    bool isTrue() const;

    bool isFalse() const;

    bool areSame(storm::expressions::Expression const& other) const;

    bool isRelationalExpression() const;

    bool isLinear() const;

    std::set<storm::expressions::Variable> getVariables() const;

    void gatherVariables(std::set<storm::expressions::Variable>& variables) const;

    bool containsVariable(std::set<storm::expressions::Variable> const& variables) const;

    bool containsVariableInITEGuard(std::set<storm::expressions::Variable> const& variables) const;

    BaseExpression const& getBaseExpression() const;

    std::shared_ptr<BaseExpression const> const& getBaseExpressionPointer() const;

    ExpressionManager const& getManager() const;

    Type const& getType() const;

    bool hasNumericalType() const;

    bool hasRationalType() const;

    bool hasBooleanType() const;

    bool hasIntegerType() const;

    bool hasBitVectorType() const;

    boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const;

    std::string toString() const;

    bool isInitialized() const;

    bool isSyntacticallyEqual(storm::expressions::Expression const& other) const;

    bool hasCompiledExpression() const;

    void setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const;

    CompiledExpression const& getCompiledExpression() const;
 
    friend std::ostream& operator<<(std::ostream& stream, Expression const& expression);
 
   private:
    // A pointer to the underlying base expression.
    std::shared_ptr<BaseExpression const> expressionPtr;
 
    // A pointer to an associated compiled expression object (if any).
    mutable std::shared_ptr<CompiledExpression> compiledExpression;
};
 
// Provide operator overloads to conveniently construct new expressions from other expressions.
Expression operator+(Expression const& first, Expression const& second);
Expression operator+(Expression const& first, int64_t second);
Expression operator+(int64_t first, Expression const& second);
Expression operator-(Expression const& first, Expression const& second);
Expression operator-(Expression const& first, int64_t second);
Expression operator-(int64_t first, Expression const& second);
Expression operator-(Expression const& first);
Expression operator*(Expression const& first, Expression const& second);
Expression operator/(Expression const& first, Expression const& second);
Expression operator&&(Expression const& first, Expression const& second);
Expression operator||(Expression const& first, Expression const& second);
Expression operator!(Expression const& first);
Expression operator==(Expression const& first, Expression const& second);
Expression operator!=(Expression const& first, Expression const& second);
Expression operator>(Expression const& first, Expression const& second);
Expression operator>=(Expression const& first, Expression const& second);
Expression operator<(Expression const& first, Expression const& second);
Expression operator<=(Expression const& first, Expression const& second);
Expression operator>(Expression const& first, int64_t second);
Expression operator>=(Expression const& first, int64_t second);
Expression operator<(Expression const& first, int64_t second);
Expression operator<=(Expression const& first, int64_t second);
Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression);
Expression implies(Expression const& first, Expression const& second);
Expression iff(Expression const& first, Expression const& second);
Expression xclusiveor(Expression const& first, Expression const& second);

Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType = false);
Expression abs(Expression const& first);
Expression truncate(Expression const& first);
Expression sign(Expression const& first);
Expression floor(Expression const& first);
Expression ceil(Expression const& first);
Expression round(Expression const& first);
Expression modulo(Expression const& first, Expression const& second);
Expression logarithm(Expression const& first, Expression const& second);
Expression cos(Expression const& first);
Expression sin(Expression const& first);
Expression minimum(Expression const& first, Expression const& second);
Expression maximum(Expression const& first, Expression const& second);
Expression atLeastOneOf(std::vector<storm::expressions::Expression> const& expressions);
Expression atMostOneOf(std::vector<storm::expressions::Expression> const& expressions);
Expression exactlyOneOf(std::vector<storm::expressions::Expression> const& expressions);
Expression disjunction(std::vector<storm::expressions::Expression> const& expressions);
Expression conjunction(std::vector<storm::expressions::Expression> const& expressions);
Expression sum(std::vector<storm::expressions::Expression> const& expressions);
Expression product(std::vector<storm::expressions::Expression> const& expressions);
Expression apply(std::vector<storm::expressions::Expression> const& expressions,
                 std::function<Expression(Expression const&, Expression const&)> const& function);
Expression applyAssociative(std::vector<storm::expressions::Expression> const& expressions,
                            std::function<Expression(Expression const&, Expression const&)> const& function);
Expression makeBinaryRelationExpression(Expression const& lhs, Expression const& rhs, RelationType const& reltype);
 
struct ExpressionLess {
    bool operator()(Expression const& lhs, Expression const& rhs) const {
        return std::less<BaseExpression const*>()(lhs.getBaseExpressionPointer().get(), rhs.getBaseExpressionPointer().get());
    }
};
}  // namespace expressions
}  // namespace storm
 
namespace std {
#ifndef STORM_WORKAROUND_LLVM_EXPRESSION_LESS_BUG
template<>
struct less<storm::expressions::Expression> {
    bool operator()(storm::expressions::Expression const& lhs, storm::expressions::Expression const& rhs) const {
        return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer();
    }
};
#endif
 
template<>
struct hash<storm::expressions::Expression> {
    size_t operator()(storm::expressions::Expression const& e) const {
        return reinterpret_cast<size_t>(e.getBaseExpressionPointer().get());
    }
};
 
template<>
struct equal_to<storm::expressions::Expression> {
    bool operator()(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2) const {
        return e1.areSame(e2);
    }
};
}  // namespace std
 
namespace storm {
namespace expressions {
#ifdef STORM_WORKAROUND_LLVM_EXPRESSION_LESS_BUG
using ExpressionComparator = ExpressionLess;
#else
using ExpressionComparator = std::less<Expression>;
#endif
using ExpressionSet = std::set<Expression, ExpressionComparator>;
template<typename Value>
using ExpressionMap = std::map<Expression, Value, ExpressionComparator>;
}  // namespace expressions
}  // namespace storm