diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 727579dff..d4686bcff 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -572,7 +572,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { if (!this->secondRun) { LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename()); } @@ -580,7 +580,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { if (!this->secondRun) { LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename()); } @@ -588,7 +588,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { if (!this->secondRun) { LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename()); } @@ -596,7 +596,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename()); } @@ -604,7 +604,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename()); } @@ -612,7 +612,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename()); } diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index bb4ea0921..2aef5ab6e 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,30 @@ namespace storm { LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); } - bool BaseExpression::isConstant() const { + 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::isLiteral() 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..79dc09c1d 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/src/storage/expressions/BaseExpression.h @@ -74,11 +74,48 @@ 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 bool isConstant() const; + 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 a variable. + * + * @return The identifier associated with this expression. + */ + virtual std::string const& getIdentifier() 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 variable. + * + * @return True iff the expression is a variable. + */ + virtual bool isVariable() const; /*! * Checks if the expression is equal to the boolean literal true. @@ -101,13 +138,6 @@ namespace storm { */ virtual std::set getVariables() const = 0; - /*! - * Retrieves the set of all constants that appear in the expression. - * - * @return The set of all constants that appear in the expression. - */ - virtual std::set getConstants() const = 0; - /*! * Simplifies the expression according to some simple rules. * 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..0ca77aa0c 100644 --- a/src/storage/expressions/BinaryExpression.cpp +++ b/src/storage/expressions/BinaryExpression.cpp @@ -1,13 +1,16 @@ #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(); } std::set BinaryExpression::getVariables() const { @@ -17,13 +20,6 @@ namespace storm { return firstVariableSet; } - std::set BinaryExpression::getConstants() const { - std::set firstConstantSet = this->getFirstOperand()->getVariables(); - std::set secondConstantSet = this->getSecondOperand()->getVariables(); - firstConstantSet.insert(secondConstantSet.begin(), secondConstantSet.end()); - return firstConstantSet; - } - std::shared_ptr const& BinaryExpression::getFirstOperand() const { return this->firstOperand; } @@ -31,5 +27,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..dd81343ac 100644 --- a/src/storage/expressions/BinaryExpression.h +++ b/src/storage/expressions/BinaryExpression.h @@ -30,9 +30,10 @@ namespace storm { virtual ~BinaryExpression() = default; // Override base class methods. - virtual bool isConstant() const override; + virtual bool containsVariables() 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; /*! * Retrieves the first operand of the expression. diff --git a/src/storage/expressions/BooleanConstantExpression.cpp b/src/storage/expressions/BooleanConstantExpression.cpp deleted file mode 100644 index de87dab48..000000000 --- a/src/storage/expressions/BooleanConstantExpression.cpp +++ /dev/null @@ -1,23 +0,0 @@ -#include "src/storage/expressions/BooleanConstantExpression.h" -#include "src/exceptions/ExceptionMacros.h" - -namespace storm { - namespace expressions { - BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Bool, constantName) { - // Intentionally left empty. - } - - bool BooleanConstantExpression::evaluateAsBool(Valuation const* valuation) const { - LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation."); - return valuation->getBooleanValue(this->getConstantName()); - } - - void BooleanConstantExpression::accept(ExpressionVisitor* visitor) const { - visitor->visit(this); - } - - std::shared_ptr BooleanConstantExpression::simplify() const { - return this->shared_from_this(); - } - } -} \ No newline at end of file diff --git a/src/storage/expressions/BooleanConstantExpression.h b/src/storage/expressions/BooleanConstantExpression.h deleted file mode 100644 index dd204d7a5..000000000 --- a/src/storage/expressions/BooleanConstantExpression.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ -#define STORM_STORAGE_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ - -#include "src/storage/expressions/ConstantExpression.h" -#include "src/utility/OsDetection.h" - -namespace storm { - namespace expressions { - class BooleanConstantExpression : public ConstantExpression { - public: - /*! - * Creates a boolean constant expression with the given constant name. - * - * @param constantName The name of the boolean constant associated with this expression. - */ - BooleanConstantExpression(std::string const& constantName); - - // Instantiate constructors and assignments with their default implementations. - BooleanConstantExpression(BooleanConstantExpression const& other) = default; - BooleanConstantExpression& operator=(BooleanConstantExpression const& other) = default; -#ifndef WINDOWS - BooleanConstantExpression(BooleanConstantExpression&&) = default; - BooleanConstantExpression& operator=(BooleanConstantExpression&&) = default; -#endif - virtual ~BooleanConstantExpression() = default; - - // Override base class methods. - virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; - virtual void accept(ExpressionVisitor* visitor) const override; - virtual std::shared_ptr simplify() const override; - }; - } -} - -#endif /* STORM_STORAGE_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ */ diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp index 6ef15fe83..5112ec8a9 100644 --- a/src/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storage/expressions/BooleanLiteralExpression.cpp @@ -10,7 +10,7 @@ namespace storm { return this->getValue(); } - bool BooleanLiteralExpression::isConstant() const { + bool BooleanLiteralExpression::isLiteral() const { return true; } @@ -26,10 +26,6 @@ namespace storm { return std::set(); } - std::set BooleanLiteralExpression::getConstants() const { - return std::set(); - } - std::shared_ptr BooleanLiteralExpression::simplify() const { return this->shared_from_this(); } diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h index 6c0413236..fc299e60a 100644 --- a/src/storage/expressions/BooleanLiteralExpression.h +++ b/src/storage/expressions/BooleanLiteralExpression.h @@ -26,11 +26,10 @@ 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 isTrue() const override; virtual bool isFalse() const override; virtual std::set getVariables() const override; - virtual std::set getConstants() const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/ConstantExpression.cpp b/src/storage/expressions/ConstantExpression.cpp deleted file mode 100644 index d09a75573..000000000 --- a/src/storage/expressions/ConstantExpression.cpp +++ /dev/null @@ -1,25 +0,0 @@ -#include "src/storage/expressions/ConstantExpression.h" - -namespace storm { - namespace expressions { - ConstantExpression::ConstantExpression(ExpressionReturnType returnType, std::string const& constantName) : BaseExpression(returnType), constantName(constantName) { - // Intentionally left empty. - } - - std::set ConstantExpression::getVariables() const { - return std::set(); - } - - std::set ConstantExpression::getConstants() const { - return {this->getConstantName()}; - } - - std::string const& ConstantExpression::getConstantName() const { - return this->constantName; - } - - void ConstantExpression::printToStream(std::ostream& stream) const { - stream << this->getConstantName(); - } - } -} \ No newline at end of file diff --git a/src/storage/expressions/ConstantExpression.h b/src/storage/expressions/ConstantExpression.h deleted file mode 100644 index 50f00c235..000000000 --- a/src/storage/expressions/ConstantExpression.h +++ /dev/null @@ -1,50 +0,0 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_CONSTANTEXPRESSION_H_ -#define STORM_STORAGE_EXPRESSIONS_CONSTANTEXPRESSION_H_ - -#include "src/storage/expressions/BaseExpression.h" -#include "src/utility/OsDetection.h" - -namespace storm { - namespace expressions { - class ConstantExpression : public BaseExpression { - public: - /*! - * Creates a constant expression with the given return type and constant name. - * - * @param returnType The return type of the expression. - * @param constantName The name of the constant associated with this expression. - */ - ConstantExpression(ExpressionReturnType returnType, std::string const& constantName); - - // Instantiate constructors and assignments with their default implementations. - ConstantExpression(ConstantExpression const& other) = default; - ConstantExpression& operator=(ConstantExpression const& other) = default; -#ifndef WINDOWS - ConstantExpression(ConstantExpression&&) = default; - ConstantExpression& operator=(ConstantExpression&&) = default; -#endif - virtual ~ConstantExpression() = default; - - // Override base class methods. - virtual std::set getVariables() const override; - virtual std::set getConstants() const override; - - /*! - * Retrieves the name of the constant. - * - * @return The name of the constant. - */ - std::string const& getConstantName() const; - - protected: - // Override base class method. - virtual void printToStream(std::ostream& stream) const override; - - private: - // The name of the constant. - std::string constantName; - }; - } -} - -#endif /* STORM_STORAGE_EXPRESSIONS_CONSTANTEXPRESSION_H_ */ diff --git a/src/storage/expressions/DoubleConstantExpression.cpp b/src/storage/expressions/DoubleConstantExpression.cpp deleted file mode 100644 index e7d541975..000000000 --- a/src/storage/expressions/DoubleConstantExpression.cpp +++ /dev/null @@ -1,23 +0,0 @@ -#include "src/storage/expressions/DoubleConstantExpression.h" -#include "src/exceptions/ExceptionMacros.h" - -namespace storm { - namespace expressions { - DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Double, constantName) { - // Intentionally left empty. - } - - double DoubleConstantExpression::evaluateAsDouble(Valuation const* valuation) const { - LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation."); - return valuation->getDoubleValue(this->getConstantName()); - } - - std::shared_ptr DoubleConstantExpression::simplify() const { - return this->shared_from_this(); - } - - void DoubleConstantExpression::accept(ExpressionVisitor* visitor) const { - visitor->visit(this); - } - } -} \ No newline at end of file diff --git a/src/storage/expressions/DoubleConstantExpression.h b/src/storage/expressions/DoubleConstantExpression.h deleted file mode 100644 index b271bf6db..000000000 --- a/src/storage/expressions/DoubleConstantExpression.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ -#define STORM_STORAGE_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ - -#include "src/storage/expressions/ConstantExpression.h" -#include "src/utility/OsDetection.h" - -namespace storm { - namespace expressions { - class DoubleConstantExpression : public ConstantExpression { - public: - /*! - * Creates a double constant expression with the given constant name. - * - * @param constantName The name of the double constant associated with this expression. - */ - DoubleConstantExpression(std::string const& constantName); - - // Instantiate constructors and assignments with their default implementations. - DoubleConstantExpression(DoubleConstantExpression const& other) = default; - DoubleConstantExpression& operator=(DoubleConstantExpression const& other) = default; -#ifndef WINDOWS - DoubleConstantExpression(DoubleConstantExpression&&) = default; - DoubleConstantExpression& operator=(DoubleConstantExpression&&) = default; -#endif - virtual ~DoubleConstantExpression() = default; - - // Override base class methods. - virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; - virtual void accept(ExpressionVisitor* visitor) const override; - virtual std::shared_ptr simplify() const override; - }; - } -} - -#endif /* STORM_STORAGE_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ */ diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp index 642a1817f..b780a8862 100644 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ b/src/storage/expressions/DoubleLiteralExpression.cpp @@ -10,7 +10,7 @@ namespace storm { return this->getValue(); } - bool DoubleLiteralExpression::isConstant() const { + bool DoubleLiteralExpression::isLiteral() const { return true; } @@ -18,10 +18,6 @@ namespace storm { return std::set(); } - std::set DoubleLiteralExpression::getConstants() const { - return std::set(); - } - std::shared_ptr DoubleLiteralExpression::simplify() const { return this->shared_from_this(); } diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h index e4bc28b81..ad22ee3be 100644 --- a/src/storage/expressions/DoubleLiteralExpression.h +++ b/src/storage/expressions/DoubleLiteralExpression.h @@ -26,9 +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 std::set getVariables() const override; - virtual std::set getConstants() const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 51d085fe4..863d630f3 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -5,23 +5,10 @@ #include "src/storage/expressions/SubstitutionVisitor.h" #include "src/storage/expressions/IdentifierSubstitutionVisitor.h" #include "src/storage/expressions/TypeCheckVisitor.h" +#include "src/storage/expressions/Expressions.h" #include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/ExceptionMacros.h" -#include "src/storage/expressions/IfThenElseExpression.h" -#include "src/storage/expressions/BinaryBooleanFunctionExpression.h" -#include "src/storage/expressions/BinaryNumericalFunctionExpression.h" -#include "src/storage/expressions/BinaryRelationExpression.h" -#include "src/storage/expressions/BooleanConstantExpression.h" -#include "src/storage/expressions/IntegerConstantExpression.h" -#include "src/storage/expressions/DoubleConstantExpression.h" -#include "src/storage/expressions/BooleanLiteralExpression.h" -#include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" -#include "src/storage/expressions/VariableExpression.h" -#include "src/storage/expressions/UnaryBooleanFunctionExpression.h" -#include "src/storage/expressions/UnaryNumericalFunctionExpression.h" - namespace storm { namespace expressions { Expression::Expression(std::shared_ptr const& expressionPtr) : expressionPtr(expressionPtr) { @@ -68,8 +55,28 @@ namespace storm { return Expression(this->getBaseExpression().simplify()); } - bool Expression::isConstant() const { - return this->getBaseExpression().isConstant(); + 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::containsVariables() const { + return this->getBaseExpression().containsVariables(); + } + + bool Expression::isLiteral() const { + return this->getBaseExpression().isLiteral(); + } + + bool Expression::isVariable() const { + return this->getBaseExpression().isVariable(); } bool Expression::isTrue() const { @@ -84,17 +91,6 @@ namespace storm { return this->getBaseExpression().getVariables(); } - std::set Expression::getConstants() const { - return this->getBaseExpression().getConstants(); - } - - std::set Expression::getIdentifiers() const { - std::set result = this->getConstants(); - std::set variables = this->getVariables(); - result.insert(variables.begin(), variables.end()); - return result; - } - BaseExpression const& Expression::getBaseExpression() const { return *this->expressionPtr; } @@ -151,18 +147,6 @@ namespace storm { return Expression(std::shared_ptr(new VariableExpression(ExpressionReturnType::Undefined, variableName))); } - Expression Expression::createBooleanConstant(std::string const& constantName) { - return Expression(std::shared_ptr(new BooleanConstantExpression(constantName))); - } - - Expression Expression::createIntegerConstant(std::string const& constantName) { - return Expression(std::shared_ptr(new IntegerConstantExpression(constantName))); - } - - Expression Expression::createDoubleConstant(std::string const& constantName) { - return Expression(std::shared_ptr(new DoubleConstantExpression(constantName))); - } - Expression Expression::operator+(Expression const& other) const { LOG_THROW(this->hasNumericalReturnType() && other.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Operator '+' requires numerical operands."); return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Plus))); diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 36c367639..44f3e5728 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -39,9 +39,6 @@ namespace storm { static Expression createIntegerVariable(std::string const& variableName); static Expression createDoubleVariable(std::string const& variableName); static Expression createUndefinedVariable(std::string const& variableName); - static Expression createBooleanConstant(std::string const& constantName); - static Expression createIntegerConstant(std::string const& constantName); - static Expression createDoubleConstant(std::string const& constantName); // Provide operator overloads to conveniently construct new expressions from other expressions. Expression operator+(Expression const& other) const; @@ -127,9 +124,8 @@ namespace storm { void check(std::unordered_map const& identifierToTypeMap) const; /*! - * Evaluates the expression under the valuation of unknowns (variables and constants) given by the - * valuation and returns the resulting boolean value. If the return type of the expression is not a boolean - * an exception is thrown. + * Evaluates the expression under the valuation of variables given by the valuation and returns the + * resulting boolean value. If the return type of the expression is not a boolean an exception is thrown. * * @param valuation The valuation of unknowns under which to evaluate the expression. * @return The boolean value of the expression under the given valuation. @@ -137,9 +133,8 @@ namespace storm { bool evaluateAsBool(Valuation const* valuation = nullptr) const; /*! - * Evaluates the expression under the valuation of unknowns (variables and constants) given by the - * valuation and returns the resulting integer value. If the return type of the expression is not an integer - * an exception is thrown. + * Evaluates the expression under the valuation of variables given by the valuation and returns the + * resulting integer value. If the return type of the expression is not an integer an exception is thrown. * * @param valuation The valuation of unknowns under which to evaluate the expression. * @return The integer value of the expression under the given valuation. @@ -147,9 +142,8 @@ namespace storm { int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const; /*! - * Evaluates the expression under the valuation of unknowns (variables and constants) given by the - * valuation and returns the resulting double value. If the return type of the expression is not a double - * an exception is thrown. + * Evaluates the expression under the valuation of variables given by the valuation and returns the + * resulting double value. If the return type of the expression is not a double an exception is thrown. * * @param valuation The valuation of unknowns under which to evaluate the expression. * @return The double value of the expression under the given valuation. @@ -164,11 +158,48 @@ 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 a variable. + * + * @return The identifier associated with this expression. + */ + std::string const& getIdentifier() const; + + /*! + * Retrieves whether the expression contains a variable. + * + * @return True iff the expression contains a variable. + */ + bool containsVariables() const; + + /*! + * Retrieves whether the expression is a literal. + * + * @return True iff the expression is a literal. + */ + bool isLiteral() const; + + /*! + * Retrieves whether the expression is a variable. + * + * @return True iff the expression is a variable. + */ + bool isVariable() const; /*! * Checks if the expression is equal to the boolean literal true. @@ -191,20 +222,6 @@ namespace storm { */ std::set getVariables() const; - /*! - * Retrieves the set of all constants that appear in the expression. - * - * @return The set of all constants that appear in the expression. - */ - std::set getConstants() const; - - /*! - * Retrieves the set of all identifiers (constants and variables) that appear in the expression. - * - * @return The est of all identifiers that appear in the expression. - */ - std::set getIdentifiers() const; - /*! * Retrieves the base expression underlying this expression object. Note that prior to calling this, the * expression object must be properly initialized. diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index 928e6297c..1b417f6ed 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -8,10 +8,6 @@ namespace storm { class BinaryBooleanFunctionExpression; class BinaryNumericalFunctionExpression; class BinaryRelationExpression; - class BooleanConstantExpression; - class DoubleConstantExpression; - class IntegerConstantExpression; - class IntegerConstantExpression; class VariableExpression; class UnaryBooleanFunctionExpression; class UnaryNumericalFunctionExpression; @@ -25,9 +21,6 @@ namespace storm { virtual void visit(BinaryBooleanFunctionExpression const* expression) = 0; virtual void visit(BinaryNumericalFunctionExpression const* expression) = 0; virtual void visit(BinaryRelationExpression const* expression) = 0; - virtual void visit(BooleanConstantExpression const* expression) = 0; - virtual void visit(DoubleConstantExpression const* expression) = 0; - virtual void visit(IntegerConstantExpression const* expression) = 0; virtual void visit(VariableExpression const* expression) = 0; virtual void visit(UnaryBooleanFunctionExpression const* expression) = 0; virtual void visit(UnaryNumericalFunctionExpression const* expression) = 0; diff --git a/src/storage/expressions/Expressions.h b/src/storage/expressions/Expressions.h index df8bbd8ed..d670c29e3 100644 --- a/src/storage/expressions/Expressions.h +++ b/src/storage/expressions/Expressions.h @@ -2,12 +2,9 @@ #include "src/storage/expressions/BinaryBooleanFunctionExpression.h" #include "src/storage/expressions/BinaryNumericalFunctionExpression.h" #include "src/storage/expressions/BinaryRelationExpression.h" -#include "src/storage/expressions/BooleanConstantExpression.h" #include "src/storage/expressions/BooleanLiteralExpression.h" -#include "src/storage/expressions/DoubleConstantExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" -#include "src/storage/expressions/IntegerConstantExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" +#include "src/storage/expressions/DoubleLiteralExpression.h" #include "src/storage/expressions/UnaryBooleanFunctionExpression.h" #include "src/storage/expressions/UnaryNumericalFunctionExpression.h" #include "src/storage/expressions/VariableExpression.h" diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp index 1b058bed2..a2153af6d 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp @@ -3,20 +3,7 @@ #include #include "src/storage/expressions/IdentifierSubstitutionVisitor.h" - -#include "src/storage/expressions/IfThenElseExpression.h" -#include "src/storage/expressions/BinaryBooleanFunctionExpression.h" -#include "src/storage/expressions/BinaryNumericalFunctionExpression.h" -#include "src/storage/expressions/BinaryRelationExpression.h" -#include "src/storage/expressions/BooleanConstantExpression.h" -#include "src/storage/expressions/IntegerConstantExpression.h" -#include "src/storage/expressions/DoubleConstantExpression.h" -#include "src/storage/expressions/BooleanLiteralExpression.h" -#include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" -#include "src/storage/expressions/VariableExpression.h" -#include "src/storage/expressions/UnaryBooleanFunctionExpression.h" -#include "src/storage/expressions/UnaryNumericalFunctionExpression.h" +#include "src/storage/expressions/Expressions.h" namespace storm { namespace expressions { @@ -106,40 +93,7 @@ namespace storm { this->expressionStack.push(std::shared_ptr(new BinaryRelationExpression(expression->getReturnType(), firstExpression, secondExpression, expression->getRelationType()))); } } - - template - void IdentifierSubstitutionVisitor::visit(BooleanConstantExpression const* expression) { - // If the boolean constant is in the key set of the substitution, we need to replace it. - auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); - if (namePair != this->identifierToIdentifierMap.end()) { - this->expressionStack.push(std::shared_ptr(new BooleanConstantExpression(namePair->second))); - } else { - this->expressionStack.push(expression->getSharedPointer()); - } - } - - template - void IdentifierSubstitutionVisitor::visit(DoubleConstantExpression const* expression) { - // If the double constant is in the key set of the substitution, we need to replace it. - auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); - if (namePair != this->identifierToIdentifierMap.end()) { - this->expressionStack.push(std::shared_ptr(new DoubleConstantExpression(namePair->second))); - } else { - this->expressionStack.push(expression->getSharedPointer()); - } - } - - template - void IdentifierSubstitutionVisitor::visit(IntegerConstantExpression const* expression) { - // If the integer constant is in the key set of the substitution, we need to replace it. - auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); - if (namePair != this->identifierToIdentifierMap.end()) { - this->expressionStack.push(std::shared_ptr(new IntegerConstantExpression(namePair->second))); - } else { - this->expressionStack.push(expression->getSharedPointer()); - } - } - + template void IdentifierSubstitutionVisitor::visit(VariableExpression const* expression) { // If the variable is in the key set of the substitution, we need to replace it. diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.h b/src/storage/expressions/IdentifierSubstitutionVisitor.h index e8412d949..23dae79de 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.h +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.h @@ -32,9 +32,6 @@ namespace storm { virtual void visit(BinaryBooleanFunctionExpression const* expression) override; virtual void visit(BinaryNumericalFunctionExpression const* expression) override; virtual void visit(BinaryRelationExpression const* expression) override; - virtual void visit(BooleanConstantExpression const* expression) override; - virtual void visit(DoubleConstantExpression const* expression) override; - virtual void visit(IntegerConstantExpression const* expression) override; virtual void visit(VariableExpression const* expression) override; virtual void visit(UnaryBooleanFunctionExpression const* expression) override; virtual void visit(UnaryNumericalFunctionExpression const* expression) override; diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp index 81ebca670..4cc028b3c 100644 --- a/src/storage/expressions/IfThenElseExpression.cpp +++ b/src/storage/expressions/IfThenElseExpression.cpp @@ -33,10 +33,6 @@ namespace storm { } } - bool IfThenElseExpression::isConstant() const { - return this->condition->isConstant() && this->thenExpression->isConstant() && this->elseExpression->isConstant(); - } - std::set IfThenElseExpression::getVariables() const { std::set result = this->condition->getVariables(); std::set tmp = this->thenExpression->getVariables(); @@ -46,15 +42,6 @@ namespace storm { return result; } - std::set IfThenElseExpression::getConstants() const { - std::set result = this->condition->getConstants(); - std::set tmp = this->thenExpression->getConstants(); - result.insert(tmp.begin(), tmp.end()); - tmp = this->elseExpression->getConstants(); - result.insert(tmp.begin(), tmp.end()); - return result; - } - std::shared_ptr IfThenElseExpression::simplify() const { std::shared_ptr conditionSimplified; if (conditionSimplified->isTrue()) { diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h index 979cb08f0..b44de20be 100644 --- a/src/storage/expressions/IfThenElseExpression.h +++ b/src/storage/expressions/IfThenElseExpression.h @@ -30,9 +30,7 @@ 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 bool isConstant() const override; virtual std::set getVariables() const override; - virtual std::set getConstants() const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/IntegerConstantExpression.cpp b/src/storage/expressions/IntegerConstantExpression.cpp deleted file mode 100644 index 60ad8de89..000000000 --- a/src/storage/expressions/IntegerConstantExpression.cpp +++ /dev/null @@ -1,27 +0,0 @@ -#include "src/storage/expressions/IntegerConstantExpression.h" -#include "src/exceptions/ExceptionMacros.h" - -namespace storm { - namespace expressions { - IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Int, constantName) { - // Intentionally left empty. - } - - int_fast64_t IntegerConstantExpression::evaluateAsInt(Valuation const* valuation) const { - LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation."); - return valuation->getIntegerValue(this->getConstantName()); - } - - double IntegerConstantExpression::evaluateAsDouble(Valuation const* valuation) const { - return static_cast(this->evaluateAsInt(valuation)); - } - - std::shared_ptr IntegerConstantExpression::simplify() const { - return this->shared_from_this(); - } - - void IntegerConstantExpression::accept(ExpressionVisitor* visitor) const { - visitor->visit(this); - } - } -} \ No newline at end of file diff --git a/src/storage/expressions/IntegerConstantExpression.h b/src/storage/expressions/IntegerConstantExpression.h deleted file mode 100644 index fcf151ead..000000000 --- a/src/storage/expressions/IntegerConstantExpression.h +++ /dev/null @@ -1,36 +0,0 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ -#define STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ - -#include "src/storage/expressions/ConstantExpression.h" -#include "src/utility/OsDetection.h" - -namespace storm { - namespace expressions { - class IntegerConstantExpression : public ConstantExpression { - public: - /*! - * Creates an integer constant expression with the given constant name. - * - * @param constantName The name of the integer constant associated with this expression. - */ - IntegerConstantExpression(std::string const& constantName); - - // Instantiate constructors and assignments with their default implementations. - IntegerConstantExpression(IntegerConstantExpression const& other) = default; - IntegerConstantExpression& operator=(IntegerConstantExpression const& other) = default; -#ifndef WINDOWS - IntegerConstantExpression(IntegerConstantExpression&&) = default; - IntegerConstantExpression& operator=(IntegerConstantExpression&&) = default; -#endif - virtual ~IntegerConstantExpression() = default; - - // 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 std::shared_ptr simplify() const override; - virtual void accept(ExpressionVisitor* visitor) const; - }; - } -} - -#endif /* STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ */ diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp index 5e6404fc8..47341a771 100644 --- a/src/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storage/expressions/IntegerLiteralExpression.cpp @@ -14,7 +14,7 @@ namespace storm { return static_cast(this->evaluateAsInt(valuation)); } - bool IntegerLiteralExpression::isConstant() const { + bool IntegerLiteralExpression::isLiteral() const { return true; } @@ -22,10 +22,6 @@ namespace storm { return std::set(); } - std::set IntegerLiteralExpression::getConstants() const { - return std::set(); - } - std::shared_ptr IntegerLiteralExpression::simplify() const { return this->shared_from_this(); } diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h index 8d50fe688..4a9e8882f 100644 --- a/src/storage/expressions/IntegerLiteralExpression.h +++ b/src/storage/expressions/IntegerLiteralExpression.h @@ -27,9 +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 std::set getVariables() const override; - virtual std::set getConstants() const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index 7990ab4f9..2559b474b 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -94,39 +94,6 @@ namespace storm { } } - template - void SubstitutionVisitor::visit(BooleanConstantExpression const* expression) { - // If the boolean constant is in the key set of the substitution, we need to replace it. - auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); - if (nameExpressionPair != this->identifierToExpressionMap.end()) { - this->expressionStack.push(nameExpressionPair->second.getBaseExpressionPointer()); - } else { - this->expressionStack.push(expression->getSharedPointer()); - } - } - - template - void SubstitutionVisitor::visit(DoubleConstantExpression const* expression) { - // If the double constant is in the key set of the substitution, we need to replace it. - auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); - if (nameExpressionPair != this->identifierToExpressionMap.end()) { - this->expressionStack.push(nameExpressionPair->second.getBaseExpressionPointer()); - } else { - this->expressionStack.push(expression->getSharedPointer()); - } - } - - template - void SubstitutionVisitor::visit(IntegerConstantExpression const* expression) { - // If the integer constant is in the key set of the substitution, we need to replace it. - auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); - if (nameExpressionPair != this->identifierToExpressionMap.end()) { - this->expressionStack.push(nameExpressionPair->second.getBaseExpressionPointer()); - } else { - this->expressionStack.push(expression->getSharedPointer()); - } - } - template void SubstitutionVisitor::visit(VariableExpression const* expression) { // If the variable is in the key set of the substitution, we need to replace it. diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index d46d62cee..bc58148e3 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -32,9 +32,6 @@ namespace storm { virtual void visit(BinaryBooleanFunctionExpression const* expression) override; virtual void visit(BinaryNumericalFunctionExpression const* expression) override; virtual void visit(BinaryRelationExpression const* expression) override; - virtual void visit(BooleanConstantExpression const* expression) override; - virtual void visit(DoubleConstantExpression const* expression) override; - virtual void visit(IntegerConstantExpression const* expression) override; virtual void visit(VariableExpression const* expression) override; virtual void visit(UnaryBooleanFunctionExpression const* expression) override; virtual void visit(UnaryNumericalFunctionExpression const* expression) override; diff --git a/src/storage/expressions/TypeCheckVisitor.cpp b/src/storage/expressions/TypeCheckVisitor.cpp index d5cef0381..044b85237 100644 --- a/src/storage/expressions/TypeCheckVisitor.cpp +++ b/src/storage/expressions/TypeCheckVisitor.cpp @@ -40,28 +40,7 @@ namespace storm { expression->getFirstOperand()->accept(this); expression->getSecondOperand()->accept(this); } - - template - void TypeCheckVisitor::visit(BooleanConstantExpression const* expression) { - auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName()); - LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'."); - LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'bool', but found '" << expression->getReturnType() << "'."); - } - - template - void TypeCheckVisitor::visit(DoubleConstantExpression const* expression) { - auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName()); - LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'."); - LOG_THROW(identifierTypePair->second == ExpressionReturnType::Double, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'double', but found '" << expression->getReturnType() << "'."); - } - - template - void TypeCheckVisitor::visit(IntegerConstantExpression const* expression) { - auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName()); - LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'."); - LOG_THROW(identifierTypePair->second == ExpressionReturnType::Int, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'int', but found '" << expression->getReturnType() << "'."); - } - + template void TypeCheckVisitor::visit(VariableExpression const* expression) { auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName()); diff --git a/src/storage/expressions/TypeCheckVisitor.h b/src/storage/expressions/TypeCheckVisitor.h index e39a536a6..7772e0e7e 100644 --- a/src/storage/expressions/TypeCheckVisitor.h +++ b/src/storage/expressions/TypeCheckVisitor.h @@ -30,9 +30,6 @@ namespace storm { virtual void visit(BinaryBooleanFunctionExpression const* expression) override; virtual void visit(BinaryNumericalFunctionExpression const* expression) override; virtual void visit(BinaryRelationExpression const* expression) override; - virtual void visit(BooleanConstantExpression const* expression) override; - virtual void visit(DoubleConstantExpression const* expression) override; - virtual void visit(IntegerConstantExpression const* expression) override; virtual void visit(VariableExpression const* expression) override; virtual void visit(UnaryBooleanFunctionExpression const* expression) override; virtual void visit(UnaryNumericalFunctionExpression const* expression) override; diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp index 1e2d9135e..62ff442ed 100644 --- a/src/storage/expressions/UnaryExpression.cpp +++ b/src/storage/expressions/UnaryExpression.cpp @@ -1,25 +1,33 @@ #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(); } std::set UnaryExpression::getVariables() const { return this->getOperand()->getVariables(); } - std::set UnaryExpression::getConstants() const { - return this->getOperand()->getVariables(); - } - 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..8ad304ce1 100644 --- a/src/storage/expressions/UnaryExpression.h +++ b/src/storage/expressions/UnaryExpression.h @@ -26,9 +26,10 @@ namespace storm { virtual ~UnaryExpression() = default; // Override base class methods. - virtual bool isConstant() const override; + virtual bool containsVariables() 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; /*! * Retrieves the operand of the unary expression. diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp index d7765f14a..2062c58ee 100644 --- a/src/storage/expressions/VariableExpression.cpp +++ b/src/storage/expressions/VariableExpression.cpp @@ -41,12 +41,16 @@ namespace storm { return 0; } - std::set VariableExpression::getVariables() const { - return {this->getVariableName()}; + std::string const& VariableExpression::getIdentifier() const { + return this->getVariableName(); + } + + bool VariableExpression::containsVariables() const { + return true; } - std::set VariableExpression::getConstants() const { - return std::set(); + std::set VariableExpression::getVariables() const { + return {this->getVariableName()}; } std::shared_ptr VariableExpression::simplify() const { diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h index 2d83b7160..6eff8c794 100644 --- a/src/storage/expressions/VariableExpression.h +++ b/src/storage/expressions/VariableExpression.h @@ -29,8 +29,9 @@ 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; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index c29001b16..10a1114e6 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -343,11 +343,9 @@ namespace storm { // Check defining expressions of defined constants. if (constant.isDefined()) { - LOG_THROW(constant.getExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": definition of constant " << constant.getName() << " must not refer to variables."); - - std::set containedConstantNames = constant.getExpression().getConstants(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstantNames.begin(), containedConstantNames.end()); - LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown constants."); + std::set containedIdentifiers = constant.getExpression().getVariables(); + bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); + LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers."); // Now check that the constants appear with the right types. try { @@ -373,12 +371,11 @@ namespace storm { LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); // Check the initial value of the variable. - LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables."); - std::set containedConstants = variable.getInitialValueExpression().getConstants(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + std::set containedIdentifiers = variable.getInitialValueExpression().getVariables(); + bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); try { - variable.getInitialValueExpression().check(identifierToTypeMap); + variable.getInitialValueExpression().check(identifierToTypeMap); } catch (storm::exceptions::InvalidTypeException const& e) { LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what()); } @@ -396,9 +393,8 @@ namespace storm { LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); // Check that bound expressions of the range. - LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables."); - std::set containedConstants = variable.getLowerBoundExpression().getConstants(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + std::set containedIdentifiers = variable.getLowerBoundExpression().getVariables(); + bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants."); try { variable.getLowerBoundExpression().check(identifierToTypeMap); @@ -406,9 +402,8 @@ namespace storm { LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what()); } - LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables."); - containedConstants = variable.getLowerBoundExpression().getConstants(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + containedIdentifiers = variable.getLowerBoundExpression().getVariables(); + isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants."); try { variable.getUpperBoundExpression().check(identifierToTypeMap); @@ -417,9 +412,8 @@ namespace storm { } // Check the initial value of the variable. - LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables."); - containedConstants = variable.getInitialValueExpression().getConstants(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + containedIdentifiers = variable.getInitialValueExpression().getVariables(); + isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); try { variable.getInitialValueExpression().check(identifierToTypeMap); @@ -443,9 +437,8 @@ namespace storm { LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); // Check the initial value of the variable. - LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables."); - std::set containedConstants = variable.getInitialValueExpression().getConstants(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + std::set containedIdentifiers = variable.getInitialValueExpression().getVariables(); + bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); try { variable.getInitialValueExpression().check(identifierToTypeMap); @@ -468,9 +461,8 @@ namespace storm { identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int); // Check that bound expressions of the range. - LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables."); - std::set containedConstants = variable.getLowerBoundExpression().getConstants(); - bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + std::set containedIdentifiers = variable.getLowerBoundExpression().getVariables(); + bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants."); try { variable.getLowerBoundExpression().check(identifierToTypeMap); @@ -478,9 +470,8 @@ namespace storm { LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what()); } - LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables."); - containedConstants = variable.getLowerBoundExpression().getConstants(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + containedIdentifiers = variable.getLowerBoundExpression().getVariables(); + isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants."); try { variable.getUpperBoundExpression().check(identifierToTypeMap); @@ -489,9 +480,8 @@ namespace storm { } // Check the initial value of the variable. - LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables."); - containedConstants = variable.getInitialValueExpression().getConstants(); - isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end()); + containedIdentifiers = variable.getInitialValueExpression().getVariables(); + isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); try { variable.getInitialValueExpression().check(identifierToTypeMap); @@ -521,7 +511,7 @@ namespace storm { for (auto const& command : module.getCommands()) { // Check the guard. - std::set containedIdentifiers = command.getGuardExpression().getIdentifiers(); + std::set containedIdentifiers = command.getGuardExpression().getVariables(); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers."); try { @@ -533,7 +523,7 @@ namespace storm { // Check all updates. for (auto const& update : command.getUpdates()) { - containedIdentifiers = update.getLikelihoodExpression().getIdentifiers(); + containedIdentifiers = update.getLikelihoodExpression().getVariables(); isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers."); try { @@ -556,7 +546,7 @@ namespace storm { auto variableTypePair = identifierToTypeMap.find(assignment.getVariableName()); LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'."); - containedIdentifiers = assignment.getExpression().getIdentifiers(); + containedIdentifiers = assignment.getExpression().getVariables(); isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers."); try { @@ -575,7 +565,7 @@ namespace storm { // Now check the reward models. for (auto const& rewardModel : this->getRewardModels()) { for (auto const& stateReward : rewardModel.getStateRewards()) { - std::set containedIdentifiers = stateReward.getStatePredicateExpression().getIdentifiers(); + std::set containedIdentifiers = stateReward.getStatePredicateExpression().getVariables(); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward expression refers to unknown identifiers."); try { @@ -585,7 +575,7 @@ namespace storm { } LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'."); - containedIdentifiers = stateReward.getRewardValueExpression().getIdentifiers(); + containedIdentifiers = stateReward.getRewardValueExpression().getVariables(); isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward value expression refers to unknown identifiers."); try { @@ -597,7 +587,7 @@ namespace storm { } for (auto const& transitionReward : rewardModel.getTransitionRewards()) { - std::set containedIdentifiers = transitionReward.getStatePredicateExpression().getIdentifiers(); + std::set containedIdentifiers = transitionReward.getStatePredicateExpression().getVariables(); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers."); try { @@ -607,7 +597,7 @@ namespace storm { } LOG_THROW(transitionReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'."); - containedIdentifiers = transitionReward.getRewardValueExpression().getIdentifiers(); + containedIdentifiers = transitionReward.getRewardValueExpression().getVariables(); isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers."); try { @@ -620,7 +610,7 @@ namespace storm { } // Check the initial states expression. - std::set containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getIdentifiers(); + std::set containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables(); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial expression refers to unknown identifiers."); try { @@ -634,7 +624,7 @@ namespace storm { // Check for duplicate identifiers. LOG_THROW(allIdentifiers.find(label.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": duplicate identifier '" << label.getName() << "'."); - std::set containedIdentifiers = label.getStatePredicateExpression().getIdentifiers(); + std::set containedIdentifiers = label.getStatePredicateExpression().getVariables(); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers."); try { @@ -651,7 +641,7 @@ namespace storm { // Check for duplicate identifiers. LOG_THROW(allIdentifiers.find(formula.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": duplicate identifier '" << formula.getName() << "'."); - std::set containedIdentifiers = formula.getExpression().getIdentifiers(); + std::set containedIdentifiers = formula.getExpression().getVariables(); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers."); try { diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 89ca71e9b..26822190d 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -15,9 +15,6 @@ TEST(Expression, FactoryMethodTest) { EXPECT_NO_THROW(storm::expressions::Expression::createBooleanVariable("x")); EXPECT_NO_THROW(storm::expressions::Expression::createIntegerVariable("y")); EXPECT_NO_THROW(storm::expressions::Expression::createDoubleVariable("z")); - EXPECT_NO_THROW(storm::expressions::Expression::createBooleanConstant("a")); - EXPECT_NO_THROW(storm::expressions::Expression::createIntegerConstant("b")); - EXPECT_NO_THROW(storm::expressions::Expression::createDoubleConstant("c")); } TEST(Expression, AccessorTest) { @@ -28,9 +25,6 @@ TEST(Expression, AccessorTest) { storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; storm::expressions::Expression doubleVarExpression; - storm::expressions::Expression boolConstExpression; - storm::expressions::Expression intConstExpression; - storm::expressions::Expression doubleConstExpression; ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); @@ -39,79 +33,48 @@ TEST(Expression, AccessorTest) { ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); - ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a")); - ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b")); - ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c")); EXPECT_TRUE(trueExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - EXPECT_TRUE(trueExpression.isConstant()); + EXPECT_TRUE(trueExpression.isLiteral()); 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.isLiteral()); 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.isLiteral()); 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.isLiteral()); 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.isLiteral()); 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.isLiteral()); 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.isLiteral()); 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.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.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.isTrue()); - EXPECT_FALSE(doubleConstExpression.isFalse()); - EXPECT_TRUE(doubleConstExpression.getVariables() == std::set()); - EXPECT_TRUE(doubleConstExpression.getConstants() == std::set({"c"})); } TEST(Expression, OperatorTest) { @@ -122,9 +85,6 @@ TEST(Expression, OperatorTest) { storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; storm::expressions::Expression doubleVarExpression; - storm::expressions::Expression boolConstExpression; - storm::expressions::Expression intConstExpression; - storm::expressions::Expression doubleConstExpression; ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); @@ -133,18 +93,15 @@ TEST(Expression, OperatorTest) { ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); - ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a")); - ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b")); - ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c")); storm::expressions::Expression tempExpression; ASSERT_THROW(tempExpression = trueExpression.ite(falseExpression, piExpression), storm::exceptions::InvalidTypeException); - ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(threeExpression, doubleVarExpression)); + ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(threeExpression, doubleVarExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(threeExpression, intVarExpression)); + ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(threeExpression, intVarExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(trueExpression, falseExpression)); + ASSERT_NO_THROW(tempExpression = boolVarExpression.ite(trueExpression, falseExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression + piExpression, storm::exceptions::InvalidTypeException); @@ -152,7 +109,7 @@ TEST(Expression, OperatorTest) { EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); ASSERT_NO_THROW(tempExpression = threeExpression + piExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = doubleVarExpression + doubleConstExpression); + ASSERT_NO_THROW(tempExpression = doubleVarExpression + doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); ASSERT_THROW(tempExpression = trueExpression - piExpression, storm::exceptions::InvalidTypeException); @@ -160,7 +117,7 @@ TEST(Expression, OperatorTest) { EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); ASSERT_NO_THROW(tempExpression = threeExpression - piExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = doubleVarExpression - doubleConstExpression); + ASSERT_NO_THROW(tempExpression = doubleVarExpression - doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); ASSERT_THROW(tempExpression = -trueExpression, storm::exceptions::InvalidTypeException); @@ -176,7 +133,7 @@ TEST(Expression, OperatorTest) { EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); ASSERT_NO_THROW(tempExpression = threeExpression * piExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = intVarExpression * intConstExpression); + ASSERT_NO_THROW(tempExpression = intVarExpression * intVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); ASSERT_THROW(tempExpression = trueExpression / piExpression, storm::exceptions::InvalidTypeException); @@ -184,19 +141,19 @@ TEST(Expression, OperatorTest) { EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); ASSERT_NO_THROW(tempExpression = threeExpression / piExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); - ASSERT_NO_THROW(tempExpression = doubleVarExpression / intConstExpression); + ASSERT_NO_THROW(tempExpression = doubleVarExpression / intVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); ASSERT_THROW(tempExpression = trueExpression && piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression && falseExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = boolVarExpression && boolConstExpression); + ASSERT_NO_THROW(tempExpression = boolVarExpression && boolVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression || piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression || falseExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = boolVarExpression || boolConstExpression); + ASSERT_NO_THROW(tempExpression = boolVarExpression || boolVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = !threeExpression, storm::exceptions::InvalidTypeException); @@ -208,79 +165,79 @@ TEST(Expression, OperatorTest) { ASSERT_THROW(tempExpression = trueExpression == piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression == threeExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression == doubleConstExpression); + ASSERT_NO_THROW(tempExpression = intVarExpression == doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression != piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression != threeExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression != doubleConstExpression); + ASSERT_NO_THROW(tempExpression = intVarExpression != doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression > piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression > threeExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression > doubleConstExpression); + ASSERT_NO_THROW(tempExpression = intVarExpression > doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression >= piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression >= threeExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression >= doubleConstExpression); + ASSERT_NO_THROW(tempExpression = intVarExpression >= doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression < piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression < threeExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression < doubleConstExpression); + ASSERT_NO_THROW(tempExpression = intVarExpression < doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression <= piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression <= threeExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = intVarExpression <= doubleConstExpression); + ASSERT_NO_THROW(tempExpression = intVarExpression <= doubleVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = storm::expressions::Expression::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(threeExpression, threeExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(intVarExpression, doubleConstExpression)); + ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::minimum(intVarExpression, doubleVarExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); ASSERT_THROW(tempExpression = storm::expressions::Expression::maximum(trueExpression, piExpression), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(threeExpression, threeExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(intVarExpression, doubleConstExpression)); + ASSERT_NO_THROW(tempExpression = storm::expressions::Expression::maximum(intVarExpression, doubleVarExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); ASSERT_THROW(tempExpression = trueExpression.implies(piExpression), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression.implies(falseExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = boolVarExpression.implies(boolConstExpression)); + ASSERT_NO_THROW(tempExpression = boolVarExpression.implies(boolVarExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression.iff(piExpression), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression.iff(falseExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolConstExpression)); + ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolVarExpression)); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = trueExpression ^ falseExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); - ASSERT_NO_THROW(tempExpression = boolVarExpression ^ boolConstExpression); + ASSERT_NO_THROW(tempExpression = boolVarExpression ^ boolVarExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); ASSERT_THROW(tempExpression = trueExpression.floor(), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression.floor()); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = doubleConstExpression.floor()); + ASSERT_NO_THROW(tempExpression = doubleVarExpression.floor()); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); ASSERT_THROW(tempExpression = trueExpression.ceil(), storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression.ceil()); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); - ASSERT_NO_THROW(tempExpression = doubleConstExpression.ceil()); + ASSERT_NO_THROW(tempExpression = doubleVarExpression.ceil()); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); } @@ -292,9 +249,6 @@ TEST(Expression, SubstitutionTest) { storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; storm::expressions::Expression doubleVarExpression; - storm::expressions::Expression boolConstExpression; - storm::expressions::Expression intConstExpression; - storm::expressions::Expression doubleConstExpression; ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); @@ -303,14 +257,11 @@ TEST(Expression, SubstitutionTest) { ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); - ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a")); - ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b")); - ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c")); storm::expressions::Expression tempExpression; - ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolConstExpression); + ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); - std::map substution = { std::make_pair("y", doubleConstExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) }; + std::map substution = { std::make_pair("y", doubleVarExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) }; storm::expressions::Expression substitutedExpression; ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution)); EXPECT_TRUE(substitutedExpression.simplify().isTrue()); @@ -347,9 +298,6 @@ TEST(Expression, SimpleEvaluationTest) { storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; storm::expressions::Expression doubleVarExpression; - storm::expressions::Expression boolConstExpression; - storm::expressions::Expression intConstExpression; - storm::expressions::Expression doubleConstExpression; ASSERT_NO_THROW(trueExpression = storm::expressions::Expression::createTrue()); ASSERT_NO_THROW(falseExpression = storm::expressions::Expression::createFalse()); @@ -358,13 +306,10 @@ TEST(Expression, SimpleEvaluationTest) { ASSERT_NO_THROW(boolVarExpression = storm::expressions::Expression::createBooleanVariable("x")); ASSERT_NO_THROW(intVarExpression = storm::expressions::Expression::createIntegerVariable("y")); ASSERT_NO_THROW(doubleVarExpression = storm::expressions::Expression::createDoubleVariable("z")); - ASSERT_NO_THROW(boolConstExpression = storm::expressions::Expression::createBooleanConstant("a")); - ASSERT_NO_THROW(intConstExpression = storm::expressions::Expression::createIntegerConstant("b")); - ASSERT_NO_THROW(doubleConstExpression = storm::expressions::Expression::createDoubleConstant("c")); storm::expressions::Expression tempExpression; - ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolConstExpression); + ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation); storm::expressions::SimpleValuation valuation; @@ -379,7 +324,7 @@ TEST(Expression, SimpleEvaluationTest) { ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); ASSERT_NO_THROW(valuation.setBooleanValue("a", true)); - EXPECT_TRUE(tempExpression.evaluateAsBool(&valuation)); + EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); ASSERT_NO_THROW(valuation.setIntegerValue("y", 3)); EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation));