From ae06c7d677fe7903a415f9a33abfea6ead6d8f70 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 4 Apr 2014 15:11:25 +0200
Subject: [PATCH] Commit to switch workplace.
Former-commit-id: d828f3d2550a4acf933e3e066d10070b257c3ffc
---
src/storage/expressions/BaseExpression.cpp | 12 ++++
src/storage/expressions/BaseExpression.h | 19 ++++++-
.../BinaryBooleanFunctionExpression.cpp | 24 +++-----
.../BinaryBooleanFunctionExpression.h | 10 ++--
.../BinaryNumericalFunctionExpression.cpp | 44 ++++++---------
.../BinaryNumericalFunctionExpression.h | 10 ++--
.../expressions/BinaryRelationExpression.cpp | 26 +++------
.../expressions/BinaryRelationExpression.h | 10 ++--
.../expressions/BooleanConstantExpression.cpp | 15 +----
.../expressions/BooleanConstantExpression.h | 11 ++--
.../expressions/BooleanLiteralExpression.cpp | 49 +++++++++++++++++
.../expressions/BooleanLiteralExpression.h | 49 +++++++++++++++++
.../expressions/ConstantExpression.cpp | 24 --------
src/storage/expressions/ConstantExpression.h | 11 +---
.../expressions/DoubleConstantExpression.cpp | 14 ++++-
.../expressions/DoubleConstantExpression.h | 16 ++++++
.../expressions/DoubleLiteralExpression.cpp | 41 ++++++++++++++
.../expressions/DoubleLiteralExpression.h | 47 ++++++++++++++++
src/storage/expressions/ExpressionVisitor.h | 28 ++++++++--
.../expressions/IntegerConstantExpression.cpp | 18 +++++-
.../expressions/IntegerConstantExpression.h | 18 ++++++
.../expressions/IntegerLiteralExpression.cpp | 45 +++++++++++++++
.../expressions/IntegerLiteralExpression.h | 48 ++++++++++++++++
src/storage/expressions/SimpleValuation.h | 53 +++++++++++++++++-
src/storage/expressions/SubstitutionVisitor.h | 2 -
.../UnaryBooleanFunctionExpression.cpp | 35 +++++++++++-
.../UnaryBooleanFunctionExpression.h | 35 +++++++++++-
src/storage/expressions/UnaryExpression.cpp | 26 ++++++++-
src/storage/expressions/UnaryExpression.h | 34 +++++++++++-
.../UnaryNumericalFunctionExpression.cpp | 34 +++++++++++-
.../UnaryNumericalFunctionExpression.h | 36 +++++++++++-
src/storage/expressions/Valuation.h | 24 ++++++++
.../expressions/VariableExpression.cpp | 43 ++++++---------
src/storage/expressions/VariableExpression.h | 55 ++++++++-----------
34 files changed, 751 insertions(+), 215 deletions(-)
create mode 100644 src/storage/expressions/BooleanLiteralExpression.cpp
create mode 100644 src/storage/expressions/BooleanLiteralExpression.h
create mode 100644 src/storage/expressions/DoubleLiteralExpression.cpp
create mode 100644 src/storage/expressions/DoubleLiteralExpression.h
create mode 100644 src/storage/expressions/IntegerLiteralExpression.cpp
create mode 100644 src/storage/expressions/IntegerLiteralExpression.h
diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp
index 550e2209f..ca2db09f1 100644
--- a/src/storage/expressions/BaseExpression.cpp
+++ b/src/storage/expressions/BaseExpression.cpp
@@ -11,6 +11,14 @@ namespace storm {
return this->returnType;
}
+ bool BaseExpression::hasNumericalReturnType() const {
+ return this->getReturnType() == ExpressionReturnType::Double || this->getReturnType() == ExpressionReturnType::Int;
+ }
+
+ bool BaseExpression::hasBooleanReturnType() const {
+ return this->getReturnType() == ExpressionReturnType::Bool;
+ }
+
int_fast64_t BaseExpression::evaluateAsInt(Valuation const& evaluation) const {
LOG_ASSERT(false, "Unable to evaluate expression as integer.");
}
@@ -23,6 +31,10 @@ namespace storm {
LOG_ASSERT(false, "Unable to evaluate expression as double.");
}
+ bool BaseExpression::isConstant() const {
+ return false;
+ }
+
bool BaseExpression::isTrue() const {
return false;
}
diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h
index 545289b08..0698278da 100644
--- a/src/storage/expressions/BaseExpression.h
+++ b/src/storage/expressions/BaseExpression.h
@@ -1,6 +1,7 @@
#ifndef STORM_STORAGE_EXPRESSIONS_BASEEXPRESSION_H_
#define STORM_STORAGE_EXPRESSIONS_BASEEXPRESSION_H_
+#include <cstdint>
#include <memory>
#include <set>
@@ -13,7 +14,7 @@ namespace storm {
/*!
* Each node in an expression tree has a uniquely defined type from this enum.
*/
- enum ExpressionReturnType {undefined, bool_, int_, double_};
+ enum class ExpressionReturnType {Undefined, Bool, Int, Double};
/*!
* The base class of all expression classes.
@@ -71,7 +72,7 @@ namespace storm {
*
* @return True iff the expression is constant.
*/
- virtual bool isConstant() const = 0;
+ virtual bool isConstant() const;
/*!
* Checks if the expression is equal to the boolean literal true.
@@ -122,6 +123,20 @@ namespace storm {
*/
virtual std::unique_ptr<BaseExpression> clone() const = 0;
+ /*!
+ * Retrieves whether the expression has a numerical return type, i.e., integer or double.
+ *
+ * @return True iff the expression has a numerical return type.
+ */
+ bool hasNumericalReturnType() const;
+
+ /*!
+ * Retrieves whether the expression has a boolean return type.
+ *
+ * @return True iff the expression has a boolean return type.
+ */
+ bool hasBooleanReturnType() const;
+
/*!
* Retrieves the return type of the expression.
*
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
index 749b1d1e1..e4034794e 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
@@ -10,26 +10,14 @@ namespace storm {
return this->operatorType;
}
- BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) : BinaryExpression(other), operatorType(other.getOperatorType()) {
- // Intentionally left empty.
- }
-
- BinaryBooleanFunctionExpression& BinaryBooleanFunctionExpression::operator=(BinaryBooleanFunctionExpression const& other) {
- if (this != &other) {
- BinaryExpression::operator=(other);
- this->operatorType = other.getOperatorType();
- }
- return *this;
- }
-
bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const& valuation) const {
bool firstOperandEvaluation = this->getFirstOperand()->evaluateAsBool(valuation);
bool secondOperandEvaluation = this->getSecondOperand()->evaluateAsBool(valuation);
bool result;
switch (this->getOperatorType()) {
- case AND: result = firstOperandEvaluation && secondOperandEvaluation; break;
- case OR: result = firstOperandEvaluation || secondOperandEvaluation; break;
+ case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break;
+ case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break;
}
return result;
@@ -40,7 +28,7 @@ namespace storm {
std::unique_ptr<BaseExpression> secondOperandSimplified = this->getSecondOperand()->simplify();
switch (this->getOperatorType()) {
- case AND: if (firstOperandSimplified->isTrue()) {
+ case OperatorType::And: if (firstOperandSimplified->isTrue()) {
return secondOperandSimplified;
} else if (firstOperandSimplified->isFalse()) {
return firstOperandSimplified;
@@ -50,7 +38,7 @@ namespace storm {
return secondOperandSimplified;
}
break;
- case OR: if (firstOperandSimplified->isTrue()) {
+ case OperatorType::Or: if (firstOperandSimplified->isTrue()) {
return firstOperandSimplified;
} else if (firstOperandSimplified->isFalse()) {
return secondOperandSimplified;
@@ -68,6 +56,8 @@ namespace storm {
visitor->visit(this);
}
- virtual std::unique_ptr<BaseExpression> clone() const override;
+ std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(*this));
+ }
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h
index f476550d0..eaabd1d56 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.h
+++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h
@@ -10,7 +10,7 @@ namespace storm {
/*!
* An enum type specifying the different operators applicable.
*/
- enum OperatorType {AND, OR};
+ enum class OperatorType {And, Or};
/*!
* Creates a binary boolean function expression with the given return type, operands and operator.
@@ -22,11 +22,9 @@ namespace storm {
*/
BinaryBooleanFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& fistOperand, std::unique_ptr<BaseExpression>&& secondOperand, OperatorType operatorType);
- // Provide custom versions of copy construction and assignment.
- BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other);
- BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other);
-
- // Create default variants of move construction/assignment and virtual destructor.
+ // Instantiate constructors and assignments with their default implementations.
+ BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) = default;
+ BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other) = default;
BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression&&) = default;
BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression&&) = default;
virtual ~BinaryBooleanFunctionExpression() = default;
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
index 61e491650..7139db695 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
@@ -9,43 +9,31 @@ namespace storm {
// Intentionally left empty.
}
- BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) : BinaryExpression(other), operatorType(this->getOperatorType()) {
- // Intentionally left empty.
- }
-
- BinaryNumericalFunctionExpression& BinaryNumericalFunctionExpression::operator=(BinaryNumericalFunctionExpression const& other) {
- if (this != &other) {
- BinaryExpression::operator=(other);
- this->operatorType = other.getOperatorType();
- }
- return *this;
- }
-
int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const& valuation) const {
- LOG_ASSERT(this->getReturnType() == ExpressionReturnType::int_, "Unable to evaluate expression as integer.");
+ LOG_ASSERT(this->getReturnType() == ExpressionReturnType::Int, "Unable to evaluate expression as integer.");
int_fast64_t firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
int_fast64_t secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation);
switch (this->getOperatorType()) {
- case PLUS: return firstOperandEvaluation + secondOperandEvaluation; break;
- case MINUS: return firstOperandEvaluation - secondOperandEvaluation; break;
- case TIMES: return firstOperandEvaluation * secondOperandEvaluation; break;
- case DIVIDE: return firstOperandEvaluation / secondOperandEvaluation; break;
- case MIN: return std::min(firstOperandEvaluation, secondOperandEvaluation); break;
- case MAX: return std::max(firstOperandEvaluation, secondOperandEvaluation); break;
+ case OperatorType::Plus: return firstOperandEvaluation + secondOperandEvaluation; break;
+ case OperatorType::Minus: return firstOperandEvaluation - secondOperandEvaluation; break;
+ case OperatorType::Times: return firstOperandEvaluation * secondOperandEvaluation; break;
+ case OperatorType::Divide: return firstOperandEvaluation / secondOperandEvaluation; break;
+ case OperatorType::Min: return std::min(firstOperandEvaluation, secondOperandEvaluation); break;
+ case OperatorType::Max: return std::max(firstOperandEvaluation, secondOperandEvaluation); break;
}
}
double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const& valuation) const {
- LOG_ASSERT(this->getReturnType() == ExpressionReturnType::int_, "Unable to evaluate expression as integer.");
- double firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
- double secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation);
+ LOG_ASSERT(this->getReturnType() == ExpressionReturnType::Double, "Unable to evaluate expression as double.");
+ double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation);
+ double secondOperandEvaluation = this->getSecondOperand()->evaluateAsDouble(valuation);
switch (this->getOperatorType()) {
- case PLUS: return firstOperandEvaluation + secondOperandEvaluation; break;
- case MINUS: return firstOperandEvaluation - secondOperandEvaluation; break;
- case TIMES: return firstOperandEvaluation * secondOperandEvaluation; break;
- case DIVIDE: return firstOperandEvaluation / secondOperandEvaluation; break;
- case MIN: return std::min(firstOperandEvaluation, secondOperandEvaluation); break;
- case MAX: return std::max(firstOperandEvaluation, secondOperandEvaluation); break;
+ case OperatorType::Plus: return static_cast<double>(firstOperandEvaluation + secondOperandEvaluation); break;
+ case OperatorType::Minus: return static_cast<double>(firstOperandEvaluation - secondOperandEvaluation); break;
+ case OperatorType::Times: return static_cast<double>(firstOperandEvaluation * secondOperandEvaluation); break;
+ case OperatorType::Divide: return static_cast<double>(firstOperandEvaluation / secondOperandEvaluation); break;
+ case OperatorType::Min: return static_cast<double>(std::min(firstOperandEvaluation, secondOperandEvaluation)); break;
+ case OperatorType::Max: return static_cast<double>(std::max(firstOperandEvaluation, secondOperandEvaluation)); break;
}
}
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storage/expressions/BinaryNumericalFunctionExpression.h
index 56ae3b55d..92d4bc0d2 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.h
+++ b/src/storage/expressions/BinaryNumericalFunctionExpression.h
@@ -10,7 +10,7 @@ namespace storm {
/*!
* An enum type specifying the different operators applicable.
*/
- enum OperatorType {PLUS, MINUS, TIMES, DIVIDE, MIN, MAX};
+ enum class OperatorType {Plus, Minus, Times, Divide, Min, Max};
/*!
* Constructs a binary numerical function expression with the given return type, operands and operator.
@@ -22,11 +22,9 @@ namespace storm {
*/
BinaryNumericalFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& firstOperand, std::unique_ptr<BaseExpression>&& secondOperand, OperatorType operatorType);
- // Provide custom versions of copy construction and assignment.
- BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other);
- BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other);
-
- // Create default variants of move construction/assignment and virtual destructor.
+ // Instantiate constructors and assignments with their default implementations.
+ BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) = default;
+ BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other) = default;
BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression&&) = default;
BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression&&) = default;
virtual ~BinaryNumericalFunctionExpression() = default;
diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp
index a203ec2fb..fb4123fca 100644
--- a/src/storage/expressions/BinaryRelationExpression.cpp
+++ b/src/storage/expressions/BinaryRelationExpression.cpp
@@ -5,29 +5,17 @@ namespace storm {
BinaryRelationExpression::BinaryRelationExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& firstOperand, std::unique_ptr<BaseExpression>&& secondOperand, RelationType relationType) : BinaryExpression(returnType, std::move(firstOperand), std::move(secondOperand)), relationType(relationType) {
// Intentionally left empty.
}
-
- BinaryRelationExpression::BinaryRelationExpression(BinaryRelationExpression const& other) : BinaryExpression(other), relationType(other.getRelationType()) {
- // Intentionally left empty.
- }
-
- BinaryRelationExpression& BinaryRelationExpression::operator=(BinaryRelationExpression const& other) {
- if (this != &other) {
- BinaryExpression::operator=(other);
- this->relationType = other.getRelationType();
- }
- return *this;
- }
-
+
bool BinaryRelationExpression::evaluateAsBool(Valuation const& valuation) const {
double firstOperandEvaluated = this->getFirstOperand()->evaluateAsDouble(valuation);
double secondOperandEvaluated = this->getSecondOperand()->evaluateAsDouble(valuation);
switch (this->getRelationType()) {
- case EQUAL: return firstOperandEvaluated == secondOperandEvaluated; break;
- case NOT_EQUAL: return firstOperandEvaluated != secondOperandEvaluated; break;
- case GREATER: return firstOperandEvaluated > secondOperandEvaluated; break;
- case GREATER_OR_EQUAL: return firstOperandEvaluated >= secondOperandEvaluated; break;
- case LESS: return firstOperandEvaluated < secondOperandEvaluated; break;
- case LESS_OR_EQUAL: return firstOperandEvaluated <= secondOperandEvaluated; break;
+ case RelationType::Equal: return firstOperandEvaluated == secondOperandEvaluated; break;
+ case RelationType::NotEqual: return firstOperandEvaluated != secondOperandEvaluated; break;
+ case RelationType::Greater: return firstOperandEvaluated > secondOperandEvaluated; break;
+ case RelationType::GreaterOrEqual: return firstOperandEvaluated >= secondOperandEvaluated; break;
+ case RelationType::Less: return firstOperandEvaluated < secondOperandEvaluated; break;
+ case RelationType::LessOrEqual: return firstOperandEvaluated <= secondOperandEvaluated; break;
}
}
diff --git a/src/storage/expressions/BinaryRelationExpression.h b/src/storage/expressions/BinaryRelationExpression.h
index 7b45cc1c1..31145ec30 100644
--- a/src/storage/expressions/BinaryRelationExpression.h
+++ b/src/storage/expressions/BinaryRelationExpression.h
@@ -10,7 +10,7 @@ namespace storm {
/*!
* An enum type specifying the different relations applicable.
*/
- enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
+ enum class RelationType {Equal, NotEqual, Less, LessOrEqual, Greater, GreaterOrEqual};
/*!
* Creates a binary relation expression with the given return type, operands and relation type.
@@ -22,11 +22,9 @@ namespace storm {
*/
BinaryRelationExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& firstOperand, std::unique_ptr<BaseExpression>&& secondOperand, RelationType relationType);
- // Provide custom versions of copy construction and assignment.
- BinaryRelationExpression(BinaryRelationExpression const& other);
- BinaryRelationExpression& operator=(BinaryRelationExpression const& other);
-
- // Create default variants of move construction/assignment and virtual destructor.
+ // Instantiate constructors and assignments with their default implementations.
+ BinaryRelationExpression(BinaryRelationExpression const& other) = default;
+ BinaryRelationExpression& operator=(BinaryRelationExpression const& other) = default;
BinaryRelationExpression(BinaryRelationExpression&&) = default;
BinaryRelationExpression& operator=(BinaryRelationExpression&&) = default;
virtual ~BinaryRelationExpression() = default;
diff --git a/src/storage/expressions/BooleanConstantExpression.cpp b/src/storage/expressions/BooleanConstantExpression.cpp
index b9fa340b0..c20d8a8b7 100644
--- a/src/storage/expressions/BooleanConstantExpression.cpp
+++ b/src/storage/expressions/BooleanConstantExpression.cpp
@@ -2,21 +2,10 @@
namespace storm {
namespace expressions {
- BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::bool_, constantName) {
+ BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Bool, constantName) {
// Intentionally left empty.
}
-
- BooleanConstantExpression::BooleanConstantExpression(BooleanConstantExpression const& other) : ConstantExpression(other) {
- // Intentionally left empty.
- }
-
- BooleanConstantExpression& BooleanConstantExpression::operator=(BooleanConstantExpression const& other) {
- if (this != &other) {
- ConstantExpression::operator=(other);
- }
- return *this;
- }
-
+
bool BooleanConstantExpression::evaluateAsBool(Valuation const& valuation) const {
return valuation.getBooleanValue(this->getConstantName());
}
diff --git a/src/storage/expressions/BooleanConstantExpression.h b/src/storage/expressions/BooleanConstantExpression.h
index 1ff4a157a..7b72fdc4e 100644
--- a/src/storage/expressions/BooleanConstantExpression.h
+++ b/src/storage/expressions/BooleanConstantExpression.h
@@ -8,18 +8,15 @@ namespace storm {
class BooleanConstantExpression : public ConstantExpression {
public:
/*!
- * Creates a boolean constant expression with the given return type and constant name.
+ * Creates a boolean constant expression with the given constant name.
*
- * @param returnType The return type of the expression.
* @param constantName The name of the boolean constant associated with this expression.
*/
BooleanConstantExpression(std::string const& constantName);
- // Provide custom versions of copy construction and assignment.
- BooleanConstantExpression(BooleanConstantExpression const& other);
- BooleanConstantExpression& operator=(BooleanConstantExpression const& other);
-
- // Create default variants of move construction/assignment and virtual destructor.
+ // Instantiate constructors and assignments with their default implementations.
+ BooleanConstantExpression(BooleanConstantExpression const& other) = default;
+ BooleanConstantExpression& operator=(BooleanConstantExpression const& other) = default;
BooleanConstantExpression(BooleanConstantExpression&&) = default;
BooleanConstantExpression& operator=(BooleanConstantExpression&&) = default;
virtual ~BooleanConstantExpression() = default;
diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp
new file mode 100644
index 000000000..371e9f7e9
--- /dev/null
+++ b/src/storage/expressions/BooleanLiteralExpression.cpp
@@ -0,0 +1,49 @@
+#include "src/storage/expressions/BooleanLiteralExpression.h"
+
+namespace storm {
+ namespace expressions {
+ BooleanLiteralExpression::BooleanLiteralExpression(bool value) : value(value) {
+ // Intentionally left empty.
+ }
+
+ bool BooleanLiteralExpression::evaluateAsBool(Valuation const& valuation) const {
+ return this->getValue();
+ }
+
+ bool BooleanLiteralExpression::isConstant() const {
+ return true;
+ }
+
+ bool BooleanLiteralExpression::isTrue() const {
+ return this->getValue() == true;
+ }
+
+ bool BooleanLiteralExpression::isFalse() const {
+ return this->getValue() == false;
+ }
+
+ std::set<std::string> BooleanLiteralExpression::getVariables() const {
+ return {};
+ }
+
+ std::set<std::string> BooleanLiteralExpression::getConstants() const {
+ return {};
+ }
+
+ std::unique_ptr<BaseExpression> BooleanLiteralExpression::simplify() const {
+ return this->clone();
+ }
+
+ void BooleanLiteralExpression::accept(ExpressionVisitor* visitor) const {
+ visitor->visit(this);
+ }
+
+ std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
+ }
+
+ bool BooleanLiteralExpression::getValue() const {
+ return this->value;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h
new file mode 100644
index 000000000..837190c95
--- /dev/null
+++ b/src/storage/expressions/BooleanLiteralExpression.h
@@ -0,0 +1,49 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_
+#define STORM_STORAGE_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_
+
+#include "src/storage/expressions/BaseExpression.h"
+
+namespace storm {
+ namespace expressions {
+ class BooleanLiteralExpression : BaseExpression {
+ public:
+ /*!
+ * Creates a boolean literal expression with the given value.
+ *
+ * @param value The value of the boolean literal.
+ */
+ BooleanLiteralExpression(bool value);
+
+ // Instantiate constructors and assignments with their default implementations.
+ BooleanLiteralExpression(BooleanLiteralExpression const& other) = default;
+ BooleanLiteralExpression& operator=(BooleanLiteralExpression const& other) = default;
+ BooleanLiteralExpression(BooleanLiteralExpression&&) = default;
+ BooleanLiteralExpression& operator=(BooleanLiteralExpression&&) = default;
+ virtual ~BooleanLiteralExpression() = default;
+
+ // Override base class methods.
+ virtual bool evaluateAsBool(Valuation const& valuation) const override;
+ virtual bool isConstant() const override;
+ virtual bool isTrue() const override;
+ virtual bool isFalse() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getConstants() const override;
+ virtual std::unique_ptr<BaseExpression> simplify() const override;
+ virtual void accept(ExpressionVisitor* visitor) const override;
+ virtual std::unique_ptr<BaseExpression> clone() const override;
+
+ /*!
+ * Retrieves the value of the boolean literal.
+ *
+ * @return The value of the boolean literal.
+ */
+ bool getValue() const;
+
+ private:
+ // The value of the boolean literal.
+ bool value;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/ConstantExpression.cpp b/src/storage/expressions/ConstantExpression.cpp
index 9fcef7338..08bd26a95 100644
--- a/src/storage/expressions/ConstantExpression.cpp
+++ b/src/storage/expressions/ConstantExpression.cpp
@@ -6,30 +6,6 @@ namespace storm {
// Intentionally left empty.
}
- ConstantExpression::ConstantExpression(ConstantExpression const& other) : BaseExpression(other), constantName(other.getConstantName()) {
- // Intentionally left empty.
- }
-
- ConstantExpression& ConstantExpression::operator=(ConstantExpression const& other) {
- if (this != &other) {
- BaseExpression::operator=(other);
- this->constantName = other.getConstantName();
- }
- return *this;
- }
-
- bool ConstantExpression::isConstant() const {
- return false;
- }
-
- bool ConstantExpression::isTrue() const {
- return false;
- }
-
- bool ConstantExpression::isFalse() const {
- return false;
- }
-
std::set<std::string> ConstantExpression::getVariables() const {
return std::set<std::string>();
}
diff --git a/src/storage/expressions/ConstantExpression.h b/src/storage/expressions/ConstantExpression.h
index 8049c12cd..b8b985ac2 100644
--- a/src/storage/expressions/ConstantExpression.h
+++ b/src/storage/expressions/ConstantExpression.h
@@ -15,19 +15,14 @@ namespace storm {
*/
ConstantExpression(ExpressionReturnType returnType, std::string const& constantName);
- // Provide custom versions of copy construction and assignment.
- ConstantExpression(ConstantExpression const& other);
- ConstantExpression& operator=(ConstantExpression const& other);
-
- // Create default variants of move construction/assignment and virtual destructor.
+ // Instantiate constructors and assignments with their default implementations.
+ ConstantExpression(ConstantExpression const& other) = default;
+ ConstantExpression& operator=(ConstantExpression const& other) = default;
ConstantExpression(ConstantExpression&&) = default;
ConstantExpression& operator=(ConstantExpression&&) = default;
virtual ~ConstantExpression() = default;
// Override base class methods.
- virtual bool isConstant() const override;
- virtual bool isTrue() const override;
- virtual bool isFalse() const override;
virtual std::set<std::string> getVariables() const override;
virtual std::set<std::string> getConstants() const override;
virtual std::unique_ptr<BaseExpression> simplify() const override;
diff --git a/src/storage/expressions/DoubleConstantExpression.cpp b/src/storage/expressions/DoubleConstantExpression.cpp
index 25fa035d4..c0c7925dc 100644
--- a/src/storage/expressions/DoubleConstantExpression.cpp
+++ b/src/storage/expressions/DoubleConstantExpression.cpp
@@ -2,8 +2,20 @@
namespace storm {
namespace expressions {
- DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(ReturnType::double_, constantName) {
+ DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Double, constantName) {
// Intentionally left empty.
}
+
+ double DoubleConstantExpression::evaluateAsDouble(Valuation const& valuation) const {
+ return valuation.getDoubleValue(this->getConstantName());
+ }
+
+ std::unique_ptr<BaseExpression> DoubleConstantExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*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
index fc5725642..28455190f 100644
--- a/src/storage/expressions/DoubleConstantExpression.h
+++ b/src/storage/expressions/DoubleConstantExpression.h
@@ -7,8 +7,24 @@ 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;
+ DoubleConstantExpression(DoubleConstantExpression&&) = default;
+ DoubleConstantExpression& operator=(DoubleConstantExpression&&) = default;
virtual ~DoubleConstantExpression() = default;
+
+ // Override base class methods.
+ virtual double evaluateAsDouble(Valuation const& valuation) const;
+ virtual std::unique_ptr<BaseExpression> clone() const;
+ virtual void accept(ExpressionVisitor* visitor) const;
};
}
}
diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp
new file mode 100644
index 000000000..a96bdcdd9
--- /dev/null
+++ b/src/storage/expressions/DoubleLiteralExpression.cpp
@@ -0,0 +1,41 @@
+#include "src/storage/expressions/DoubleLiteralExpression.h"
+
+namespace storm {
+ namespace expressions {
+ DoubleLiteralExpression::DoubleLiteralExpression(double value) : value(value) {
+ // Intentionally left empty.
+ }
+
+ double DoubleLiteralExpression::evaluateAsDouble(Valuation const& valuation) const {
+ return this->getValue();
+ }
+
+ bool DoubleLiteralExpression::isConstant() const {
+ return true;
+ }
+
+ std::set<std::string> DoubleLiteralExpression::getVariables() const {
+ return {};
+ }
+
+ std::set<std::string> DoubleLiteralExpression::getConstants() const {
+ return {};
+ }
+
+ std::unique_ptr<BaseExpression> DoubleLiteralExpression::simplify() const {
+ return this->clone();
+ }
+
+ void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) const {
+ visitor->visit(this);
+ }
+
+ std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
+ }
+
+ double DoubleLiteralExpression::getValue() const {
+ return this->value;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h
new file mode 100644
index 000000000..b15e5e013
--- /dev/null
+++ b/src/storage/expressions/DoubleLiteralExpression.h
@@ -0,0 +1,47 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
+#define STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
+
+#include "src/storage/expressions/BaseExpression.h"
+
+namespace storm {
+ namespace expressions {
+ class DoubleLiteralExpression : BaseExpression {
+ public:
+ /*!
+ * Creates an double literal expression with the given value.
+ *
+ * @param value The value of the double literal.
+ */
+ DoubleLiteralExpression(double value);
+
+ // Instantiate constructors and assignments with their default implementations.
+ DoubleLiteralExpression(DoubleLiteralExpression const& other) = default;
+ DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = default;
+ DoubleLiteralExpression(DoubleLiteralExpression&&) = default;
+ DoubleLiteralExpression& operator=(DoubleLiteralExpression&&) = default;
+ virtual ~DoubleLiteralExpression() = default;
+
+ // Override base class methods.
+ virtual double evaluateAsDouble(Valuation const& valuation) const override;
+ virtual bool isConstant() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getConstants() const override;
+ virtual std::unique_ptr<BaseExpression> simplify() const override;
+ virtual void accept(ExpressionVisitor* visitor) const override;
+ virtual std::unique_ptr<BaseExpression> clone() const override;
+
+ /*!
+ * Retrieves the value of the double literal.
+ *
+ * @return The value of the double literal.
+ */
+ double getValue() const;
+
+ private:
+ // The value of the double literal.
+ double value;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h
index 94898e1a2..4bd2e8d29 100644
--- a/src/storage/expressions/ExpressionVisitor.h
+++ b/src/storage/expressions/ExpressionVisitor.h
@@ -1,18 +1,36 @@
#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_
#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_
-#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
-#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/storage/expressions/BooleanConstantExpression.h"
-
namespace storm {
namespace expressions {
+ // Forward-declare all expression classes.
+ class BinaryBooleanFunctionExpression;
+ class BinaryNumericalFunctionExpression;
+ class BinaryRelationExpression;
+ class BooleanConstantExpression;
+ class DoubleConstantExpression;
+ class IntegerConstantExpression;
+ class IntegerConstantExpression;
+ class VariableExpression;
+ class UnaryBooleanFunctionExpression;
+ class UnaryNumericalFunctionExpression;
+ class BooleanLiteralExpression;
+ class IntegerLiteralExpression;
+ class DoubleLiteralExpression;
+
class ExpressionVisitor {
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;
+ virtual void visit(BooleanLiteralExpression const* expression) = 0;
+ virtual void visit(IntegerLiteralExpression const* expression) = 0;
+ virtual void visit(DoubleLiteralExpression const* expression) = 0;
};
}
}
diff --git a/src/storage/expressions/IntegerConstantExpression.cpp b/src/storage/expressions/IntegerConstantExpression.cpp
index 0cbf541a7..87e109423 100644
--- a/src/storage/expressions/IntegerConstantExpression.cpp
+++ b/src/storage/expressions/IntegerConstantExpression.cpp
@@ -2,8 +2,24 @@
namespace storm {
namespace expressions {
- IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(ReturnType::int_, constantName) {
+ IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Int, constantName) {
// Intentionally left empty.
}
+
+ int_fast64_t IntegerConstantExpression::evaluateAsInteger(Valuation const& valuation) const {
+ return valuation.getIntegerValue(this->getConstantName());
+ }
+
+ double IntegerConstantExpression::evaluateAsDouble(Valuation const& valuation) const {
+ return static_cast<double>(valuation.getIntegerValue(this->getConstantName()));
+ }
+
+ std::unique_ptr<BaseExpression> IntegerConstantExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*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
index c39df1c77..402679163 100644
--- a/src/storage/expressions/IntegerConstantExpression.h
+++ b/src/storage/expressions/IntegerConstantExpression.h
@@ -1,13 +1,31 @@
#ifndef STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
#define STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
+#include "src/storage/expressions/ConstantExpression.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;
+ IntegerConstantExpression(IntegerConstantExpression&&) = default;
+ IntegerConstantExpression& operator=(IntegerConstantExpression&&) = default;
virtual ~IntegerConstantExpression() = default;
+ // Override base class methods.
+ virtual int_fast64_t evaluateAsInteger(Valuation const& valuation) const;
+ virtual double evaluateAsDouble(Valuation const& valuation) const;
+ virtual std::unique_ptr<BaseExpression> clone() const;
+ virtual void accept(ExpressionVisitor* visitor) const;
};
}
}
diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp
new file mode 100644
index 000000000..ad74e58bd
--- /dev/null
+++ b/src/storage/expressions/IntegerLiteralExpression.cpp
@@ -0,0 +1,45 @@
+#include "src/storage/expressions/IntegerLiteralExpression.h"
+
+namespace storm {
+ namespace expressions {
+ IntegerLiteralExpression::IntegerLiteralExpression(int_fast64_t value) : value(value) {
+ // Intentionally left empty.
+ }
+
+ int_fast64_t IntegerLiteralExpression::evaluateAsInt(Valuation const& valuation) const {
+ return this->getValue();
+ }
+
+ double IntegerLiteralExpression::evaluateAsDouble(Valuation const& valuation) const {
+ return static_cast<double>(this->getValue());
+ }
+
+ bool IntegerLiteralExpression::isConstant() const {
+ return true;
+ }
+
+ std::set<std::string> IntegerLiteralExpression::getVariables() const {
+ return {};
+ }
+
+ std::set<std::string> IntegerLiteralExpression::getConstants() const {
+ return {};
+ }
+
+ std::unique_ptr<BaseExpression> IntegerLiteralExpression::simplify() const {
+ return this->clone();
+ }
+
+ void IntegerLiteralExpression::accept(ExpressionVisitor* visitor) const {
+ visitor->visit(this);
+ }
+
+ std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
+ }
+
+ int_fast64_t IntegerLiteralExpression::getValue() const {
+ return this->value;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h
new file mode 100644
index 000000000..1fc1b03f7
--- /dev/null
+++ b/src/storage/expressions/IntegerLiteralExpression.h
@@ -0,0 +1,48 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
+#define STORM_STORAGE_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
+
+#include "src/storage/expressions/BaseExpression.h"
+
+namespace storm {
+ namespace expressions {
+ class IntegerLiteralExpression : BaseExpression {
+ public:
+ /*!
+ * Creates an integer literal expression with the given value.
+ *
+ * @param value The value of the integer literal.
+ */
+ IntegerLiteralExpression(int_fast64_t value);
+
+ // Instantiate constructors and assignments with their default implementations.
+ IntegerLiteralExpression(IntegerLiteralExpression const& other) = default;
+ IntegerLiteralExpression& operator=(IntegerLiteralExpression const& other) = default;
+ IntegerLiteralExpression(IntegerLiteralExpression&&) = default;
+ IntegerLiteralExpression& operator=(IntegerLiteralExpression&&) = default;
+ virtual ~IntegerLiteralExpression() = default;
+
+ // Override base class methods.
+ virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
+ virtual double evaluateAsDouble(Valuation const& valuation) const override;
+ virtual bool isConstant() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getConstants() const override;
+ virtual std::unique_ptr<BaseExpression> simplify() const override;
+ virtual void accept(ExpressionVisitor* visitor) const override;
+ virtual std::unique_ptr<BaseExpression> clone() const override;
+
+ /*!
+ * Retrieves the value of the integer literal.
+ *
+ * @return The value of the integer literal.
+ */
+ int_fast64_t getValue() const;
+
+ private:
+ // The value of the integer literal.
+ int_fast64_t value;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h
index 399a6d7f4..f4808face 100644
--- a/src/storage/expressions/SimpleValuation.h
+++ b/src/storage/expressions/SimpleValuation.h
@@ -3,7 +3,6 @@
#include <memory>
#include <vector>
-#include <string>
#include <unordered_map>
#include "src/storage/expressions/Valuation.h"
@@ -12,30 +11,82 @@ namespace storm {
namespace expressions {
class SimpleValuation : public Valuation {
public:
+ /*!
+ * Creates a simple valuation that can hold the given number of boolean, integer and double variables.
+ *
+ * @param booleanVariableCount The number of boolean variables in the valuation.
+ * @param integerVariableCount The number of integer variables in the valuation.
+ * @param doubleVariableCount The number of double variables in the valuation.
+ */
SimpleValuation(std::size_t booleanVariableCount, std::size_t integerVariableCount, std::size_t doubleVariableCount);
+ /*!
+ * Creates a simple evaluation based on the given identifier to index map and value containers for the
+ * different types of variables.
+ *
+ * @param identifierToIndexMap A shared pointer to a mapping from identifier to their local indices in the
+ * value containers.
+ * @param booleanValues The value container for all boolean identifiers.
+ * @param integerValues The value container for all integer identifiers.
+ * @param doubleValues The value container for all double identifiers.
+ */
SimpleValuation(std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap, std::vector<bool> booleanValues, std::vector<int_fast64_t> integerValues, std::vector<double> doubleValues);
+ // Instantiate some constructors and assignments with their default implementations.
SimpleValuation() = default;
SimpleValuation(SimpleValuation const&) = default;
SimpleValuation(SimpleValuation&&) = default;
SimpleValuation& operator=(SimpleValuation const&) = default;
SimpleValuation& operator=(SimpleValuation&&) = default;
+ /*!
+ * Sets the index of the identifier with the given name to the given value.
+ *
+ * @param name The name of the identifier for which to set the index.
+ * @param index The new index of the identifier.
+ */
void setIdentifierIndex(std::string const& name, uint_fast64_t index);
+ /*!
+ * Sets the value of the boolean identifier with the given name to the given value.
+ *
+ * @param name The name of the boolean identifier whose value to set.
+ * @param value The new value of the boolean identifier.
+ */
void setBooleanValue(std::string const& name, bool value);
+
+ /*!
+ * Sets the value of the integer identifier with the given name to the given value.
+ *
+ * @param name The name of the integer identifier whose value to set.
+ * @param value The new value of the integer identifier.
+ */
void setIntegerValue(std::string const& name, int_fast64_t value);
+
+ /*!
+ * Sets the value of the double identifier with the given name to the given value.
+ *
+ * @param name The name of the double identifier whose value to set.
+ * @param value The new value of the double identifier.
+ */
void setDoubleValue(std::string const& name, double value);
+ // Override base class methods.
virtual bool getBooleanValue(std::string const& name) const override;
virtual int_fast64_t getIntegerValue(std::string const& name) const override;
virtual double getDoubleValue(std::string const& name) const override;
private:
+ // A mapping of identifiers to their local indices in the value containers.
std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap;
+
+ // The value container for all boolean identifiers.
std::vector<bool> booleanValues;
+
+ // The value container for all integer identifiers.
std::vector<int_fast64_t> integerValues;
+
+ // The value container for all double identifiers.
std::vector<double> doubleValues;
};
}
diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h
index f65482e3c..db2947e2e 100644
--- a/src/storage/expressions/SubstitutionVisitor.h
+++ b/src/storage/expressions/SubstitutionVisitor.h
@@ -10,8 +10,6 @@ namespace storm {
public:
template<template<typename... Arguments> class MapType>
Expression substitute(BaseExpression const* expression, MapType<std::string, Expression> const& identifierToExpressionMap);
-
-
};
}
}
diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
index 1d97ebf41..d25460c3c 100644
--- a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
@@ -1,9 +1,42 @@
#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
+#include "src/storage/expressions/BooleanLiteralExpression.h"
namespace storm {
namespace expressions {
- UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType) : UnaryExpression(returnType, std::move(argument)), functionType(functionType) {
+ UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType) : UnaryExpression(returnType, std::move(operand)), operatorType(operatorType) {
// Intentionally left empty.
}
+
+ OperatorType UnaryBooleanFunctionExpression::getOperatorType() const {
+ return this->operatorType;
+ }
+
+ bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const& valuation) const {
+ bool operandEvaluated = this->getOperand()->evaluateAsBool(valuation);
+ switch (this->getOperatorType()) {
+ case OperatorType::Not: return !operandEvaluated; break;
+ }
+ }
+
+ std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::simplify() const {
+ std::unique_ptr<BaseExpression> operandSimplified = this->getOperand()->simplify();
+ switch (this->getOperatorType()) {
+ case OperatorType::Not: if (operandSimplified->isTrue()) {
+ return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(false));
+ } else {
+ return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(true));
+ }
+ }
+
+ return UnaryBooleanFunctionExpression(this->getReturnType(), std::move(operandSimplified), this->getOperatorType());
+ }
+
+ void UnaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) const {
+ visitor->visit(this);
+ }
+
+ std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(*this));
+ }
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storage/expressions/UnaryBooleanFunctionExpression.h
index 277ea6637..8453f99e0 100644
--- a/src/storage/expressions/UnaryBooleanFunctionExpression.h
+++ b/src/storage/expressions/UnaryBooleanFunctionExpression.h
@@ -1,19 +1,48 @@
#ifndef STORM_STORAGE_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
#define STORM_STORAGE_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
+#include "src/storage/expressions/UnaryExpression.h"
+
namespace storm {
namespace expressions {
class UnaryBooleanFunctionExpression : public UnaryExpression {
/*!
* An enum type specifying the different functions applicable.
*/
- enum FunctionType {NOT};
+ enum class OperatorType {Not};
- UnaryBooleanFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType);
+ /*!
+ * Creates a unary boolean function expression with the given return type, operand and operator.
+ *
+ * @param returnType The return type of the expression.
+ * @param operand The operand of the expression.
+ * @param operatorType The operator of the expression.
+ */
+ UnaryBooleanFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType);
+
+ // Instantiate constructors and assignments with their default implementations.
+ UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& other) = default;
+ UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression const& other) = default;
+ UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression&&) = default;
+ UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression&&) = default;
virtual ~UnaryBooleanFunctionExpression() = default;
+ // Override base class methods.
+ virtual bool evaluateAsBool(Valuation const& valuation) const override;
+ virtual std::unique_ptr<BaseExpression> simplify() const override;
+ virtual void accept(ExpressionVisitor* visitor) const override;
+ virtual std::unique_ptr<BaseExpression> clone() const override;
+
+ /*!
+ * Retrieves the operator associated with this expression.
+ *
+ * @return The operator associated with this expression.
+ */
+ OperatorType getOperatorType() const;
+
private:
- FunctionType FunctionType;
+ // The operator of this expression.
+ OperatorType operatorType;
};
}
}
diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp
index bf8ab5972..e0573d813 100644
--- a/src/storage/expressions/UnaryExpression.cpp
+++ b/src/storage/expressions/UnaryExpression.cpp
@@ -2,8 +2,32 @@
namespace storm {
namespace expressions {
- UnaryExpression::UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& argument) : BaseExpression(returnType), argument(std::move(argument)) {
+ UnaryExpression::UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand) : BaseExpression(returnType), operand(std::move(operand)) {
// Intentionally left empty.
}
+
+ UnaryExpression::UnaryExpression(UnaryExpression const& other) : BaseExpression(other), operand(other.getOperand()->clone()) {
+ // Intentionally left empty.
+ }
+
+ UnaryExpression& UnaryExpression::operator=(UnaryExpression const& other) {
+ if (this != &other) {
+ BaseExpression::operator=(other);
+ this->operand = other.getOperand()->clone();
+ }
+ return *this;
+ }
+
+ bool UnaryExpression::isConstant() const {
+ return this->getOperand()->isConstant();
+ }
+
+ std::set<std::string> UnaryExpression::getVariables() const {
+ return this->getOperand()->getVariables();
+ }
+
+ std::set<std::string> UnaryExpression::getConstants() const {
+ return this->getOperand()->getVariables();
+ }
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/UnaryExpression.h b/src/storage/expressions/UnaryExpression.h
index 1aee2b349..c0d4acf33 100644
--- a/src/storage/expressions/UnaryExpression.h
+++ b/src/storage/expressions/UnaryExpression.h
@@ -1,16 +1,44 @@
#ifndef STORM_STORAGE_EXPRESSIONS_UNARYEXPRESSION_H_
#define STORM_STORAGE_EXPRESSIONS_UNARYEXPRESSION_H_
+#include "src/storage/expressions/BaseExpression.h"
+
namespace storm {
namespace expressions {
class UnaryExpression : public BaseExpression {
public:
- UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& argument);
+ /*!
+ * Creates a unary expression with the given return type and operand.
+ *
+ * @param returnType The return type of the expression.
+ * @param operand The operand of the unary expression.
+ */
+ UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand);
+
+ // Provide custom versions of copy construction and assignment.
+ UnaryExpression(UnaryExpression const& other);
+ UnaryExpression& operator=(UnaryExpression const& other);
+
+ // Create default variants of move construction/assignment and virtual destructor.
+ UnaryExpression(UnaryExpression&&) = default;
+ UnaryExpression& operator=(UnaryExpression&&) = default;
virtual ~UnaryExpression() = default;
- std::unique_ptr<BaseExpression> const& getArgument() const;
+ // Override base class methods.
+ virtual bool isConstant() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getConstants() const override;
+
+ /*!
+ * Retrieves the operand of the unary expression.
+ *
+ * @return The operand of the unary expression.
+ */
+ std::unique_ptr<BaseExpression> const& getOperand() const;
+
private:
- std::unique_ptr<BaseExpression> argument;
+ // The operand of the unary expression.
+ std::unique_ptr<BaseExpression> operand;
};
}
}
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
index e3cc93fdb..fc8ef625b 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -1,9 +1,41 @@
+#include <cmath>
+
#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
namespace storm {
namespace expressions {
- UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType) : UnaryExpression(returnType, std::move(argument)), functionType(functionType) {
+ UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType) : UnaryExpression(returnType, std::move(operand)), operatorType(operatorType) {
// Intentionally left empty.
}
+
+ int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const& valuation) const {
+ int_fast64_t operandEvaluated = this->getOperand()->evaluateAsInt(valuation);
+ switch (this->getOperatorType()) {
+ case OperatorType::Minus: return -operandEvaluated; break;
+ case OperatorType::Floor: return std::floor(operandEvaluated); break;
+ case OperatorType::Ceil: return std::ceil(operandEvaluated); break;
+ }
+ }
+
+ double UnaryNumericalFunctionExpression::evaluateAsDouble(Valuation const& valuation) const {
+ double operandEvaluated = this->getOperand()->evaluateAsDouble(valuation);
+ switch (this->getOperatorType()) {
+ case OperatorType::Minus: return -operandEvaluated; break;
+ case OperatorType::Floor: return std::floor(operandEvaluated); break;
+ case OperatorType::Ceil: return std::ceil(operandEvaluated); break;
+ }
+ }
+
+ std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::simplify() const {
+ return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getReturnType(), this->getOperand()->simplify(), this->getOperatorType()));
+ }
+
+ void UnaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) const {
+ visitor->visit(this);
+ }
+
+ std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(*this));
+ }
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storage/expressions/UnaryNumericalFunctionExpression.h
index 5dce0b84f..7bbba69ca 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.h
+++ b/src/storage/expressions/UnaryNumericalFunctionExpression.h
@@ -1,19 +1,49 @@
#ifndef STORM_STORAGE_EXPRESSIONS_UNARYNUMERICALFUNCTIONEXPRESSION_H_
#define STORM_STORAGE_EXPRESSIONS_UNARYNUMERICALFUNCTIONEXPRESSION_H_
+#include "src/storage/expressions/UnaryExpression.h"
+
namespace storm {
namespace expressions {
class UnaryNumericalFunctionExpression : public UnaryExpression {
/*!
* An enum type specifying the different functions applicable.
*/
- enum FunctionType {MINUS, FLOOR, CEIL};
+ enum class OperatorType {Minus, Floor, Ceil};
+
+ /*!
+ * Creates a unary numerical function expression with the given return type, operand and operator.
+ *
+ * @param returnType The return type of the expression.
+ * @param operand The operand of the expression.
+ * @param operatorType The operator of the expression.
+ */
+ UnaryNumericalFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType);
- UnaryNumericalFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType);
+ // Instantiate constructors and assignments with their default implementations.
+ UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& other) = default;
+ UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression const& other) = default;
+ UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression&&) = default;
+ UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression&&) = default;
virtual ~UnaryNumericalFunctionExpression() = default;
+ // Override base class methods.
+ virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
+ virtual double evaluateAsDouble(Valuation const& valuation) const override;
+ virtual std::unique_ptr<BaseExpression> simplify() const override;
+ virtual void accept(ExpressionVisitor* visitor) const override;
+ virtual std::unique_ptr<BaseExpression> clone() const override;
+
+ /*!
+ * Retrieves the operator associated with this expression.
+ *
+ * @return The operator associated with this expression.
+ */
+ OperatorType getOperatorType() const;
+
private:
- FunctionType FunctionType;
+ // The operator of this expression.
+ OperatorType operatorType;
};
}
}
diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h
index 5a1a470ce..7aa32a859 100644
--- a/src/storage/expressions/Valuation.h
+++ b/src/storage/expressions/Valuation.h
@@ -5,10 +5,34 @@
namespace storm {
namespace expressions {
+ /*!
+ * The base class of all valuations where a valuation assigns a concrete value to all identifiers. This is, for
+ * example, used for evaluating expressions.
+ */
class Valuation {
public:
+ /*!
+ * Retrieves the boolean value of the identifier with the given name.
+ *
+ * @param name The name of the boolean identifier whose value to retrieve.
+ * @return The value of the boolean identifier.
+ */
virtual bool getBooleanValue(std::string const& name) const = 0;
+
+ /*!
+ * Retrieves the integer value of the identifier with the given name.
+ *
+ * @param name The name of the integer identifier whose value to retrieve.
+ * @return The value of the integer identifier.
+ */
virtual int_fast64_t getIntegerValue(std::string const& name) const = 0;
+
+ /*!
+ * Retrieves the double value of the identifier with the given name.
+ *
+ * @param name The name of the double identifier whose value to retrieve.
+ * @return The value of the double identifier.
+ */
virtual double getDoubleValue(std::string const& name) const = 0;
};
}
diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp
index 7b64707fd..6cc96f799 100644
--- a/src/storage/expressions/VariableExpression.cpp
+++ b/src/storage/expressions/VariableExpression.cpp
@@ -12,47 +12,38 @@ namespace storm {
}
int_fast64_t VariableExpression::evaluateAsInt(Valuation const& evaluation) const {
- LOG_ASSERT((this->getReturnType() == ExpressionReturnType::int_), "Cannot evaluate expression as integer: return type is not an integer.");
+ LOG_ASSERT((this->getReturnType() == ExpressionReturnType::Int), "Cannot evaluate expression as integer: return type is not an integer.");
return evaluation.getIntegerValue(this->getVariableName());
}
bool VariableExpression::evaluateAsBool(Valuation const& evaluation) const {
- LOG_ASSERT((this->getReturnType() == ExpressionReturnType::bool_), "Cannot evaluate expression as integer: return type is not a boolean.");
+ LOG_ASSERT((this->getReturnType() == ExpressionReturnType::Bool), "Cannot evaluate expression as integer: return type is not a boolean.");
return evaluation.getBooleanValue(this->getVariableName());
}
double VariableExpression::evaluateAsDouble(Valuation const& evaluation) const {
- LOG_ASSERT((this->getReturnType() == ExpressionReturnType::double_), "Cannot evaluate expression as integer: return type is not a double.");
+ LOG_ASSERT((this->getReturnType() == ExpressionReturnType::Double), "Cannot evaluate expression as integer: return type is not a double.");
return evaluation.getDoubleValue(this->getVariableName());
}
- std::unique_ptr<BaseExpression> VariableExpression::operator+(BaseExpression const& other) const {
- // FIXME
- return nullptr;
+ std::set<std::string> VariableExpression::getVariables() const {
+ return {this->getVariableName()};
}
- std::unique_ptr<BaseExpression> operator-(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> operator-() const;
- std::unique_ptr<BaseExpression> operator*(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> operator/(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> operator&(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> operator|(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> operator~() const;
+ std::set<std::string> VariableExpression::getConstants() const {
+ return std::set<std::string>();
+ }
- std::unique_ptr<BaseExpression> equals(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> notEquals(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> greater(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> greaterOrEqual(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> less(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> lessOrEqual(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> minimum(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> maximum(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> mod(BaseExpression const& other) const;
- std::unique_ptr<BaseExpression> floor() const;
- std::unique_ptr<BaseExpression> ceil() const;
+ std::unique_ptr<BaseExpression> VariableExpression::simplify() const {
+ return this->clone();
+ }
- void visit(ExpressionVisitor* visitor) const;
+ void VariableExpression::accept(ExpressionVisitor* visitor) const {
+ visitor->visit(this);
+ }
- virtual std::unique_ptr<BaseExpression> clonse() const;
+ std::unique_ptr<BaseExpression> VariableExpression::clone() const {
+ return std::unique_ptr<BaseExpression>(new VariableExpression(*this));
+ }
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h
index d4d57907b..5aa89e4ce 100644
--- a/src/storage/expressions/VariableExpression.h
+++ b/src/storage/expressions/VariableExpression.h
@@ -7,40 +7,33 @@ namespace storm {
namespace expressions {
class VariableExpression : public BaseExpression {
VariableExpression(ExpressionReturnType returnType, std::string const& variableName);
- virtual ~VariableExpression() = default;
+ // Instantiate constructors and assignments with their default implementations.
+ VariableExpression(VariableExpression const&) = default;
+ VariableExpression(VariableExpression&&) = default;
+ VariableExpression& operator=(VariableExpression const&) = default;
+ VariableExpression& operator=(VariableExpression&&) = default;
+ virtual ~VariableExpression() = default;
+
+ // Override base class methods.
+ virtual bool evaluateAsBool(Valuation const& valuation) const override;
+ virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
+ virtual double evaluateAsDouble(Valuation const& valuation) const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getConstants() const override;
+ virtual std::unique_ptr<BaseExpression> simplify() const override;
+ virtual void accept(ExpressionVisitor* visitor) const override;
+ virtual std::unique_ptr<BaseExpression> clone() const override;
+
+ /*!
+ * Retrieves the name of the variable associated with this expression.
+ *
+ * @return The name of the variable.
+ */
std::string const& getVariableName() const;
-
- virtual int_fast64_t evaluateAsInt(Valuation const& evaluation) const;
- virtual bool evaluateAsBool(Valuation const& evaluation) const;
- virtual double evaluateAsDouble(Valuation const& evaluation) const;
-
- virtual std::unique_ptr<BaseExpression> operator+(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> operator-(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> operator-() const;
- virtual std::unique_ptr<BaseExpression> operator*(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> operator/(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> operator&(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> operator|(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> operator~() const;
-
- virtual std::unique_ptr<BaseExpression> equals(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> notEquals(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> greater(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> greaterOrEqual(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> less(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> lessOrEqual(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> minimum(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> maximum(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> mod(BaseExpression const& other) const;
- virtual std::unique_ptr<BaseExpression> floor() const;
- virtual std::unique_ptr<BaseExpression> ceil() const;
-
- virtual void visit(ExpressionVisitor* visitor) const;
-
- virtual std::unique_ptr<BaseExpression> clonse() const;
-
+
private:
+ // The variable name associated with this expression.
std::string variableName;
};
}