diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index bb4ea0921..346871b01 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -1,6 +1,7 @@ #include "src/storage/expressions/BaseExpression.h" #include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/InvalidTypeException.h" +#include "src/exceptions/InvalidAccessException.h" namespace storm { namespace expressions { @@ -36,10 +37,38 @@ namespace storm { LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); } + uint_fast64_t BaseExpression::getArity() const { + return 0; + } + + std::shared_ptr BaseExpression::getOperand(uint_fast64_t operandIndex) const { + LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 0."); + } + + std::string const& BaseExpression::getIdentifier() const { + LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to access identifier of non-constant, non-variable expression."); + } + + bool BaseExpression::containsVariables() const { + return false; + } + + bool BaseExpression::hasConstantValue() const { + return false; + } + + bool BaseExpression::isLiteral() const { + return false; + } + bool BaseExpression::isConstant() const { return false; } - + + bool BaseExpression::isVariable() const { + return false; + } + bool BaseExpression::isTrue() const { return false; } diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index fb3df4514..fb88ffae8 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/src/storage/expressions/BaseExpression.h @@ -74,12 +74,63 @@ namespace storm { virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const; /*! - * Retrieves whether the expression is constant, i.e., contains no variables or undefined constants. + * Returns the arity of the expression. * - * @return True iff the expression is constant. + * @return The arity of the expression. + */ + virtual uint_fast64_t getArity() const; + + /*! + * Retrieves the given operand from the expression. + * + * @param operandIndex The index of the operand to retrieve. This must be lower than the arity of the expression. + * @return The operand at the given index. + */ + virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const; + + /*! + * Retrieves the identifier associated with this expression. This is only legal to call if the expression + * is either a constant or a variable. + * + * @return The identifier associated with this expression. + */ + virtual std::string const& getIdentifier() const; + + /*! + * Retrieves whether the expression has a constant value, i.e., does not involve variables or constants. + * + * @return True iff the expression has a constant value. + */ + virtual bool hasConstantValue() const; + + /*! + * Retrieves whether the expression contains a variable. + * + * @return True iff the expression contains a variable. + */ + virtual bool containsVariables() const; + + /*! + * Retrieves whether the expression is a literal. + * + * @return True iff the expression is a literal. + */ + virtual bool isLiteral() const; + + /*! + * Retrieves whether the expression is a constant. + * + * @return True iff the expression is a constant. */ virtual bool isConstant() const; + /*! + * Retrieves whether the expression is a variable. + * + * @return True iff the expression is a variable. + */ + virtual bool isVariable() const; + /*! * Checks if the expression is equal to the boolean literal true. * diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 02cd9686b..e270293a8 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -30,7 +30,7 @@ namespace storm { return result; } - + std::shared_ptr BinaryBooleanFunctionExpression::simplify() const { std::shared_ptr firstOperandSimplified = this->getFirstOperand()->simplify(); std::shared_ptr secondOperandSimplified = this->getSecondOperand()->simplify(); diff --git a/src/storage/expressions/BinaryExpression.cpp b/src/storage/expressions/BinaryExpression.cpp index cfd18447c..bdb885993 100644 --- a/src/storage/expressions/BinaryExpression.cpp +++ b/src/storage/expressions/BinaryExpression.cpp @@ -1,13 +1,20 @@ #include "src/storage/expressions/BinaryExpression.h" +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/InvalidAccessException.h" + namespace storm { namespace expressions { BinaryExpression::BinaryExpression(ExpressionReturnType returnType, std::shared_ptr const& firstOperand, std::shared_ptr const& secondOperand) : BaseExpression(returnType), firstOperand(firstOperand), secondOperand(secondOperand) { // Intentionally left empty. } - - bool BinaryExpression::isConstant() const { - return this->getFirstOperand()->isConstant() && this->getSecondOperand()->isConstant(); + + bool BinaryExpression::containsVariables() const { + return this->getFirstOperand()->containsVariables() || this->getSecondOperand()->containsVariables(); + } + + bool BinaryExpression::hasConstantValue() const { + return this->getFirstOperand()->hasConstantValue() && this->getSecondOperand()->hasConstantValue(); } std::set BinaryExpression::getVariables() const { @@ -31,5 +38,18 @@ namespace storm { std::shared_ptr const& BinaryExpression::getSecondOperand() const { return this->secondOperand; } + + uint_fast64_t BinaryExpression::getArity() const { + return 2; + } + + std::shared_ptr BinaryExpression::getOperand(uint_fast64_t operandIndex) const { + LOG_THROW(operandIndex < 2, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2."); + if (operandIndex == 1) { + return this->getFirstOperand(); + } else { + return this->getSecondOperand(); + } + } } } \ No newline at end of file diff --git a/src/storage/expressions/BinaryExpression.h b/src/storage/expressions/BinaryExpression.h index 640297a91..5016bd247 100644 --- a/src/storage/expressions/BinaryExpression.h +++ b/src/storage/expressions/BinaryExpression.h @@ -30,7 +30,10 @@ namespace storm { virtual ~BinaryExpression() = default; // Override base class methods. - virtual bool isConstant() const override; + virtual bool containsVariables() const override; + virtual bool hasConstantValue() const override; + virtual uint_fast64_t getArity() const override; + virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; virtual std::set getVariables() const override; virtual std::set getConstants() const override; diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp index 6ef15fe83..b0a65594c 100644 --- a/src/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storage/expressions/BooleanLiteralExpression.cpp @@ -10,7 +10,11 @@ namespace storm { return this->getValue(); } - bool BooleanLiteralExpression::isConstant() const { + bool BooleanLiteralExpression::isLiteral() const { + return true; + } + + bool BooleanLiteralExpression::hasConstantValue() const { return true; } diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h index 6c0413236..31a7d5dca 100644 --- a/src/storage/expressions/BooleanLiteralExpression.h +++ b/src/storage/expressions/BooleanLiteralExpression.h @@ -26,7 +26,8 @@ namespace storm { // Override base class methods. virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; - virtual bool isConstant() const override; + virtual bool isLiteral() const override; + virtual bool hasConstantValue() const override; virtual bool isTrue() const override; virtual bool isFalse() const override; virtual std::set getVariables() const override; diff --git a/src/storage/expressions/ConstantExpression.cpp b/src/storage/expressions/ConstantExpression.cpp index d09a75573..ec1efc11a 100644 --- a/src/storage/expressions/ConstantExpression.cpp +++ b/src/storage/expressions/ConstantExpression.cpp @@ -18,6 +18,18 @@ namespace storm { return this->constantName; } + bool ConstantExpression::isConstant() const { + return true; + } + + bool ConstantExpression::hasConstantValue() const { + return false; + } + + std::string const& ConstantExpression::getIdentifier() const { + return this->getConstantName(); + } + void ConstantExpression::printToStream(std::ostream& stream) const { stream << this->getConstantName(); } diff --git a/src/storage/expressions/ConstantExpression.h b/src/storage/expressions/ConstantExpression.h index 50f00c235..fd79fd51e 100644 --- a/src/storage/expressions/ConstantExpression.h +++ b/src/storage/expressions/ConstantExpression.h @@ -26,6 +26,9 @@ namespace storm { virtual ~ConstantExpression() = default; // Override base class methods. + virtual bool isConstant() const override; + virtual bool hasConstantValue() const override; + virtual std::string const& getIdentifier() const override; virtual std::set getVariables() const override; virtual std::set getConstants() const override; diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp index 642a1817f..a319c40d8 100644 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ b/src/storage/expressions/DoubleLiteralExpression.cpp @@ -10,7 +10,11 @@ namespace storm { return this->getValue(); } - bool DoubleLiteralExpression::isConstant() const { + bool DoubleLiteralExpression::isLiteral() const { + return true; + } + + bool DoubleLiteralExpression::hasConstantValue() const { return true; } diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h index e4bc28b81..5395a34a8 100644 --- a/src/storage/expressions/DoubleLiteralExpression.h +++ b/src/storage/expressions/DoubleLiteralExpression.h @@ -26,7 +26,8 @@ namespace storm { // Override base class methods. virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; - virtual bool isConstant() const override; + virtual bool isLiteral() const override; + virtual bool hasConstantValue() const override; virtual std::set getVariables() const override; virtual std::set getConstants() const override; virtual std::shared_ptr simplify() const override; diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 51d085fe4..ae787faed 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -68,10 +68,38 @@ namespace storm { return Expression(this->getBaseExpression().simplify()); } + uint_fast64_t Expression::getArity() const { + return this->getBaseExpression().getArity(); + } + + Expression Expression::getOperand(uint_fast64_t operandIndex) const { + return Expression(this->getBaseExpression().getOperand(operandIndex)); + } + + std::string const& Expression::getIdentifier() const { + return this->getBaseExpression().getIdentifier(); + } + + bool Expression::hasConstantValue() const { + return this->getBaseExpression().hasConstantValue(); + } + + bool Expression::containsVariables() const { + return this->getBaseExpression().containsVariables(); + } + + bool Expression::isLiteral() const { + return this->isLiteral(); + } + bool Expression::isConstant() const { return this->getBaseExpression().isConstant(); } + bool Expression::isVariable() const { + return this->getBaseExpression().isVariable(); + } + bool Expression::isTrue() const { return this->getBaseExpression().isTrue(); } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 36c367639..11636521b 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -164,11 +164,62 @@ namespace storm { Expression simplify(); /*! - * Retrieves whether the expression is constant, i.e., contains no variables or undefined constants. + * Retrieves the arity of the expression. * - * @return True iff the expression is constant. + * @return The arity of the expression. */ - bool isConstant() const; + uint_fast64_t getArity() const; + + /*! + * Retrieves the given operand from the expression. + * + * @param operandIndex The index of the operand to retrieve. This must be lower than the arity of the expression. + * @return The operand at the given index. + */ + Expression getOperand(uint_fast64_t operandIndex) const; + + /*! + * Retrieves the identifier associated with this expression. This is only legal to call if the expression + * is either a constant or a variable. + * + * @return The identifier associated with this expression. + */ + virtual std::string const& getIdentifier() const; + + /*! + * Retrieves whether the expression has a constant value, i.e., does not involve variables. + * + * @return True iff the expression has a constant value. + */ + virtual bool hasConstantValue() const; + + /*! + * Retrieves whether the expression contains a variable. + * + * @return True iff the expression contains a variable. + */ + virtual bool containsVariables() const; + + /*! + * Retrieves whether the expression is a literal. + * + * @return True iff the expression is a literal. + */ + virtual bool isLiteral() const; + + /*! + * Retrieves whether the expression is a constant. + * + * @return True iff the expression is a constant. + */ + virtual bool isConstant() const; + + /*! + * Retrieves whether the expression is a variable. + * + * @return True iff the expression is a variable. + */ + virtual bool isVariable() const; /*! * Checks if the expression is equal to the boolean literal true. diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp index 5e6404fc8..5bdb9c1a9 100644 --- a/src/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storage/expressions/IntegerLiteralExpression.cpp @@ -14,7 +14,11 @@ namespace storm { return static_cast(this->evaluateAsInt(valuation)); } - bool IntegerLiteralExpression::isConstant() const { + bool IntegerLiteralExpression::isLiteral() const { + return true; + } + + bool IntegerLiteralExpression::hasConstantValue() const { return true; } diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h index 8d50fe688..2a45eb5cc 100644 --- a/src/storage/expressions/IntegerLiteralExpression.h +++ b/src/storage/expressions/IntegerLiteralExpression.h @@ -27,7 +27,8 @@ namespace storm { // Override base class methods. virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override; virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; - virtual bool isConstant() const override; + virtual bool isLiteral() const override; + virtual bool hasConstantValue() const override; virtual std::set getVariables() const override; virtual std::set getConstants() const override; virtual std::shared_ptr simplify() const override; diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp index 1e2d9135e..8349a8aac 100644 --- a/src/storage/expressions/UnaryExpression.cpp +++ b/src/storage/expressions/UnaryExpression.cpp @@ -1,13 +1,20 @@ #include "src/storage/expressions/UnaryExpression.h" +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/InvalidAccessException.h" + namespace storm { namespace expressions { UnaryExpression::UnaryExpression(ExpressionReturnType returnType, std::shared_ptr const& operand) : BaseExpression(returnType), operand(operand) { // Intentionally left empty. } - bool UnaryExpression::isConstant() const { - return this->getOperand()->isConstant(); + bool UnaryExpression::containsVariables() const { + return this->getOperand()->containsVariables(); + } + + bool UnaryExpression::hasConstantValue() const { + return this->getOperand()->hasConstantValue(); } std::set UnaryExpression::getVariables() const { @@ -21,5 +28,14 @@ namespace storm { std::shared_ptr const& UnaryExpression::getOperand() const { return this->operand; } + + uint_fast64_t UnaryExpression::getArity() const { + return 1; + } + + std::shared_ptr UnaryExpression::getOperand(uint_fast64_t operandIndex) const { + LOG_THROW(operandIndex == 0, storm::exceptions::InvalidAccessException, "Unable to access operand " << operandIndex << " in expression of arity 2."); + return this->getOperand(); + } } } \ No newline at end of file diff --git a/src/storage/expressions/UnaryExpression.h b/src/storage/expressions/UnaryExpression.h index f81bc08ad..e071aa979 100644 --- a/src/storage/expressions/UnaryExpression.h +++ b/src/storage/expressions/UnaryExpression.h @@ -26,7 +26,10 @@ namespace storm { virtual ~UnaryExpression() = default; // Override base class methods. - virtual bool isConstant() const override; + virtual bool containsVariables() const override; + virtual bool hasConstantValue() const override; + virtual uint_fast64_t getArity() const override; + virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; virtual std::set getVariables() const override; virtual std::set getConstants() const override; diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp index d7765f14a..88cb7ba86 100644 --- a/src/storage/expressions/VariableExpression.cpp +++ b/src/storage/expressions/VariableExpression.cpp @@ -41,6 +41,14 @@ namespace storm { return 0; } + std::string const& VariableExpression::getIdentifier() const { + return this->getVariableName(); + } + + bool VariableExpression::containsVariables() const { + return true; + } + std::set VariableExpression::getVariables() const { return {this->getVariableName()}; } diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h index 2d83b7160..e6d9366f7 100644 --- a/src/storage/expressions/VariableExpression.h +++ b/src/storage/expressions/VariableExpression.h @@ -29,6 +29,8 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override; virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; + virtual std::string const& getIdentifier() const override; + virtual bool containsVariables() const override; virtual std::set getVariables() const override; virtual std::set getConstants() const override; virtual std::shared_ptr simplify() const override; diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 89ca71e9b..893149a23 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -44,70 +44,70 @@ TEST(Expression, AccessorTest) { ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c")); EXPECT_TRUE(trueExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - EXPECT_TRUE(trueExpression.isConstant()); + EXPECT_TRUE(trueExpression.hasConstantValue()); EXPECT_TRUE(trueExpression.isTrue()); EXPECT_FALSE(trueExpression.isFalse()); EXPECT_TRUE(trueExpression.getVariables() == std::set()); EXPECT_TRUE(trueExpression.getConstants() == std::set()); EXPECT_TRUE(falseExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - EXPECT_TRUE(falseExpression.isConstant()); + EXPECT_TRUE(falseExpression.hasConstantValue()); EXPECT_FALSE(falseExpression.isTrue()); EXPECT_TRUE(falseExpression.isFalse()); EXPECT_TRUE(falseExpression.getVariables() == std::set()); EXPECT_TRUE(falseExpression.getConstants() == std::set()); EXPECT_TRUE(threeExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - EXPECT_TRUE(threeExpression.isConstant()); + EXPECT_TRUE(threeExpression.hasConstantValue()); EXPECT_FALSE(threeExpression.isTrue()); EXPECT_FALSE(threeExpression.isFalse()); EXPECT_TRUE(threeExpression.getVariables() == std::set()); EXPECT_TRUE(threeExpression.getConstants() == std::set()); EXPECT_TRUE(piExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - EXPECT_TRUE(piExpression.isConstant()); + EXPECT_TRUE(piExpression.hasConstantValue()); EXPECT_FALSE(piExpression.isTrue()); EXPECT_FALSE(piExpression.isFalse()); EXPECT_TRUE(piExpression.getVariables() == std::set()); EXPECT_TRUE(piExpression.getConstants() == std::set()); EXPECT_TRUE(boolVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - EXPECT_FALSE(boolVarExpression.isConstant()); + EXPECT_FALSE(boolVarExpression.hasConstantValue()); EXPECT_FALSE(boolVarExpression.isTrue()); EXPECT_FALSE(boolVarExpression.isFalse()); EXPECT_TRUE(boolVarExpression.getVariables() == std::set({"x"})); EXPECT_TRUE(boolVarExpression.getConstants() == std::set()); EXPECT_TRUE(intVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - EXPECT_FALSE(intVarExpression.isConstant()); + EXPECT_FALSE(intVarExpression.hasConstantValue()); EXPECT_FALSE(intVarExpression.isTrue()); EXPECT_FALSE(intVarExpression.isFalse()); EXPECT_TRUE(intVarExpression.getVariables() == std::set({"y"})); EXPECT_TRUE(intVarExpression.getConstants() == std::set()); EXPECT_TRUE(doubleVarExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - EXPECT_FALSE(doubleVarExpression.isConstant()); + EXPECT_FALSE(doubleVarExpression.hasConstantValue()); EXPECT_FALSE(doubleVarExpression.isTrue()); EXPECT_FALSE(doubleVarExpression.isFalse()); EXPECT_TRUE(doubleVarExpression.getVariables() == std::set({"z"})); EXPECT_TRUE(doubleVarExpression.getConstants() == std::set()); EXPECT_TRUE(boolConstExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - EXPECT_FALSE(boolConstExpression.isConstant()); + EXPECT_FALSE(boolConstExpression.hasConstantValue()); EXPECT_FALSE(boolConstExpression.isTrue()); EXPECT_FALSE(boolConstExpression.isFalse()); EXPECT_TRUE(boolConstExpression.getVariables() == std::set()); EXPECT_TRUE(boolConstExpression.getConstants() == std::set({"a"})); EXPECT_TRUE(intConstExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - EXPECT_FALSE(intConstExpression.isConstant()); + EXPECT_FALSE(intConstExpression.hasConstantValue()); EXPECT_FALSE(intConstExpression.isTrue()); EXPECT_FALSE(intConstExpression.isFalse()); EXPECT_TRUE(intConstExpression.getVariables() == std::set()); EXPECT_TRUE(intConstExpression.getConstants() == std::set({"b"})); EXPECT_TRUE(doubleConstExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - EXPECT_FALSE(doubleConstExpression.isConstant()); + EXPECT_FALSE(doubleConstExpression.hasConstantValue()); EXPECT_FALSE(doubleConstExpression.isTrue()); EXPECT_FALSE(doubleConstExpression.isFalse()); EXPECT_TRUE(doubleConstExpression.getVariables() == std::set());