diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h
index 8237fbce6..8d780f218 100644
--- a/src/adapters/Z3ExpressionAdapter.h
+++ b/src/adapters/Z3ExpressionAdapter.h
@@ -14,7 +14,9 @@
#include "z3.h"
#include "src/storage/expressions/Expressions.h"
+#include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/ExpressionEvaluationException.h"
+#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
@@ -24,6 +26,9 @@ namespace storm {
public:
/*!
* Creates a Z3ExpressionAdapter over the given Z3 context.
+ *
+ * @remark The adapter internally creates helper variables prefixed with `__z3adapter_`. Avoid having variables with
+ * this prefix in the variableToExpressionMap, as this might lead to unexpected results.
*
* @param context A reference to the Z3 context over which to build the expressions. Be careful to guarantee
* the lifetime of the context as long as the instance of this adapter is used.
@@ -40,11 +45,48 @@ namespace storm {
/*!
* Translates the given expression to an equivalent expression for Z3.
- *
+ *
+ * @remark The adapter internally creates helper variables prefixed with `__z3adapter_`. Avoid having variables with
+ * this prefix in the expression, as this might lead to unexpected results.
+ *
* @param expression The expression to translate.
+ * @param createZ3Variables If set to true a solver variable is created for each variable in expression that is not
+ * yet known to the adapter. (i.e. values from the variableToExpressionMap passed to the constructor
+ * are not overwritten)
* @return An equivalent expression for Z3.
*/
- z3::expr translateExpression(storm::expressions::Expression const& expression) {
+ z3::expr translateExpression(storm::expressions::Expression const& expression, bool createZ3Variables = false) {
+ if (createZ3Variables) {
+ std::map<std::string, storm::expressions::ExpressionReturnType> variables;
+
+ try {
+ variables = expression.getVariablesAndTypes();
+ }
+ catch (storm::exceptions::InvalidTypeException* e) {
+ LOG_THROW(true, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e);
+ }
+
+ for (auto variableAndType : variables) {
+ if (this->variableToExpressionMap.find(variableAndType.first) == this->variableToExpressionMap.end()) {
+ switch (variableAndType.second)
+ {
+ case storm::expressions::ExpressionReturnType::Bool:
+ this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.bool_const(variableAndType.first.c_str())));
+ break;
+ case storm::expressions::ExpressionReturnType::Int:
+ this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.int_const(variableAndType.first.c_str())));
+ break;
+ case storm::expressions::ExpressionReturnType::Double:
+ this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.real_const(variableAndType.first.c_str())));
+ break;
+ default:
+ LOG_THROW(true, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first);
+ break;
+ }
+ }
+ }
+ }
+
expression.getBaseExpression().accept(this);
z3::expr result = stack.top();
stack.pop();
@@ -154,28 +196,16 @@ namespace storm {
}
}
- virtual void visit(storm::expressions::BooleanConstantExpression const* expression) override {
- throw storm::exceptions::NotImplementedException() << "BooleanConstantExpression is not supported by Z3ExpressionAdapter.";
- }
-
virtual void visit(storm::expressions::BooleanLiteralExpression const* expression) override {
stack.push(context.bool_val(expression->evaluateAsBool()));
}
- virtual void visit(storm::expressions::DoubleConstantExpression const* expression) override {
- throw storm::exceptions::NotImplementedException() << "DoubleConstantExpression is not supported by Z3ExpressionAdapter.";
- }
-
virtual void visit(storm::expressions::DoubleLiteralExpression const* expression) override {
std::stringstream fractionStream;
fractionStream << expression->evaluateAsDouble();
stack.push(context.real_val(fractionStream.str().c_str()));
}
- virtual void visit(storm::expressions::IntegerConstantExpression const* expression) override {
- throw storm::exceptions::NotImplementedException() << "IntegerConstantExpression is not supported by Z3ExpressionAdapter.";
- }
-
virtual void visit(storm::expressions::IntegerLiteralExpression const* expression) override {
stack.push(context.int_val(static_cast<int>(expression->evaluateAsInt())));
}
@@ -206,13 +236,13 @@ namespace storm {
stack.push(0 - childResult);
break;
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: {
- z3::expr floorVariable = context.int_const(("__floor_" + std::to_string(additionalVariableCounter++)).c_str());
+ z3::expr floorVariable = context.int_const(("__z3adapter_floor_" + std::to_string(additionalVariableCounter++)).c_str());
additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, floorVariable)) <= childResult < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1));
throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter.";
break;
}
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{
- z3::expr ceilVariable = context.int_const(("__floor_" + std::to_string(additionalVariableCounter++)).c_str());
+ z3::expr ceilVariable = context.int_const(("__z3adapter_ceil_" + std::to_string(additionalVariableCounter++)).c_str());
additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= childResult < z3::expr(context, Z3_mk_int2real(context, ceilVariable)));
throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter.";
break;
diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h
index 79dc09c1d..5a9cdba75 100644
--- a/src/storage/expressions/BaseExpression.h
+++ b/src/storage/expressions/BaseExpression.h
@@ -4,6 +4,7 @@
#include <cstdint>
#include <memory>
#include <set>
+#include <map>
#include <iostream>
#include "src/storage/expressions/Valuation.h"
@@ -137,7 +138,14 @@ namespace storm {
* @return The set of all variables that appear in the expression.
*/
virtual std::set<std::string> getVariables() const = 0;
-
+
+ /*!
+ * Retrieves the mapping of all variables that appear in the expression to their return type.
+ *
+ * @return The mapping of all variables that appear in the expression to their return type.
+ */
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const = 0;
+
/*!
* Simplifies the expression according to some simple rules.
*
diff --git a/src/storage/expressions/BinaryExpression.cpp b/src/storage/expressions/BinaryExpression.cpp
index 0ca77aa0c..09fb1cf70 100644
--- a/src/storage/expressions/BinaryExpression.cpp
+++ b/src/storage/expressions/BinaryExpression.cpp
@@ -11,14 +11,21 @@ namespace storm {
bool BinaryExpression::containsVariables() const {
return this->getFirstOperand()->containsVariables() || this->getSecondOperand()->containsVariables();
- }
-
- std::set<std::string> BinaryExpression::getVariables() const {
- std::set<std::string> firstVariableSet = this->getFirstOperand()->getVariables();
- std::set<std::string> secondVariableSet = this->getSecondOperand()->getVariables();
- firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end());
- return firstVariableSet;
- }
+ }
+
+ std::set<std::string> BinaryExpression::getVariables() const {
+ std::set<std::string> firstVariableSet = this->getFirstOperand()->getVariables();
+ std::set<std::string> secondVariableSet = this->getSecondOperand()->getVariables();
+ firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end());
+ return firstVariableSet;
+ }
+
+ std::map<std::string, ExpressionReturnType> BinaryExpression::getVariablesAndTypes() const {
+ std::map<std::string, ExpressionReturnType> firstVariableSet = this->getFirstOperand()->getVariablesAndTypes();
+ std::map<std::string, ExpressionReturnType> secondVariableSet = this->getSecondOperand()->getVariablesAndTypes();
+ firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end());
+ return firstVariableSet;
+ }
std::shared_ptr<BaseExpression const> const& BinaryExpression::getFirstOperand() const {
return this->firstOperand;
diff --git a/src/storage/expressions/BinaryExpression.h b/src/storage/expressions/BinaryExpression.h
index dd81343ac..9daf9505d 100644
--- a/src/storage/expressions/BinaryExpression.h
+++ b/src/storage/expressions/BinaryExpression.h
@@ -32,8 +32,9 @@ namespace storm {
// Override base class methods.
virtual bool containsVariables() const override;
virtual uint_fast64_t getArity() const override;
- virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;
- virtual std::set<std::string> getVariables() const override;
+ virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
/*!
* Retrieves the first operand of the expression.
diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp
index 5112ec8a9..d510c6f45 100644
--- a/src/storage/expressions/BooleanLiteralExpression.cpp
+++ b/src/storage/expressions/BooleanLiteralExpression.cpp
@@ -24,7 +24,11 @@ namespace storm {
std::set<std::string> BooleanLiteralExpression::getVariables() const {
return std::set<std::string>();
- }
+ }
+
+ std::map<std::string, ExpressionReturnType> BooleanLiteralExpression::getVariablesAndTypes() const {
+ return std::map<std::string, ExpressionReturnType>();
+ }
std::shared_ptr<BaseExpression const> BooleanLiteralExpression::simplify() const {
return this->shared_from_this();
diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h
index fc299e60a..57c19677c 100644
--- a/src/storage/expressions/BooleanLiteralExpression.h
+++ b/src/storage/expressions/BooleanLiteralExpression.h
@@ -29,7 +29,8 @@ namespace storm {
virtual bool isLiteral() 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> getVariables() const override;
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual void accept(ExpressionVisitor* visitor) const override;
diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp
index b780a8862..00471b533 100644
--- a/src/storage/expressions/DoubleLiteralExpression.cpp
+++ b/src/storage/expressions/DoubleLiteralExpression.cpp
@@ -16,7 +16,11 @@ namespace storm {
std::set<std::string> DoubleLiteralExpression::getVariables() const {
return std::set<std::string>();
- }
+ }
+
+ std::map<std::string, ExpressionReturnType> DoubleLiteralExpression::getVariablesAndTypes() const {
+ return std::map<std::string, ExpressionReturnType>();
+ }
std::shared_ptr<BaseExpression const> DoubleLiteralExpression::simplify() const {
return this->shared_from_this();
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h
index ad22ee3be..515326b8b 100644
--- a/src/storage/expressions/DoubleLiteralExpression.h
+++ b/src/storage/expressions/DoubleLiteralExpression.h
@@ -27,7 +27,8 @@ namespace storm {
// Override base class methods.
virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
virtual bool isLiteral() const override;
- virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
virtual std::shared_ptr<BaseExpression const> 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 863d630f3..ca2616b95 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -86,10 +86,21 @@ namespace storm {
bool Expression::isFalse() const {
return this->getBaseExpression().isFalse();
}
-
- std::set<std::string> Expression::getVariables() const {
- return this->getBaseExpression().getVariables();
- }
+
+ std::set<std::string> Expression::getVariables() const {
+ return this->getBaseExpression().getVariables();
+ }
+
+ std::map<std::string, ExpressionReturnType> Expression::getVariablesAndTypes(bool validate = true) const {
+ if (validate) {
+ std::map<std::string, ExpressionReturnType> result = this->getBaseExpression().getVariablesAndTypes();
+ this->check(result);
+ return result;
+ }
+ else {
+ return this->getBaseExpression().getVariablesAndTypes();
+ }
+ }
BaseExpression const& Expression::getBaseExpression() const {
return *this->expressionPtr;
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index 44f3e5728..6ad063c91 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -222,6 +222,19 @@ namespace storm {
*/
std::set<std::string> getVariables() const;
+ /*!
+ * Retrieves the mapping of all variables that appear in the expression to their return type.
+ *
+ * @param validate If this parameter is true, check() is called with the returnvalue before
+ * it is returned.
+ *
+ * @throws storm::exceptions::InvalidTypeException If a variables with the same name but different
+ * types occur somewhere withing the expression.
+ *
+ * @return The mapping of all variables that appear in the expression to their return type.
+ */
+ std::map<std::string, ExpressionReturnType> getVariablesAndTypes(bool validate = true) 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/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp
index 4cc028b3c..6b84cde84 100644
--- a/src/storage/expressions/IfThenElseExpression.cpp
+++ b/src/storage/expressions/IfThenElseExpression.cpp
@@ -31,16 +31,25 @@ namespace storm {
} else {
return this->elseExpression->evaluateAsDouble(valuation);
}
- }
-
- std::set<std::string> IfThenElseExpression::getVariables() const {
- std::set<std::string> result = this->condition->getVariables();
- std::set<std::string> tmp = this->thenExpression->getVariables();
- result.insert(tmp.begin(), tmp.end());
- tmp = this->elseExpression->getVariables();
- result.insert(tmp.begin(), tmp.end());
- return result;
- }
+ }
+
+ std::set<std::string> IfThenElseExpression::getVariables() const {
+ std::set<std::string> result = this->condition->getVariables();
+ std::set<std::string> tmp = this->thenExpression->getVariables();
+ result.insert(tmp.begin(), tmp.end());
+ tmp = this->elseExpression->getVariables();
+ result.insert(tmp.begin(), tmp.end());
+ return result;
+ }
+
+ std::map<std::string, ExpressionReturnType> IfThenElseExpression::getVariablesAndTypes() const {
+ std::map<std::string, ExpressionReturnType> result = this->condition->getVariablesAndTypes();
+ std::map<std::string, ExpressionReturnType> tmp = this->thenExpression->getVariablesAndTypes();
+ result.insert(tmp.begin(), tmp.end());
+ tmp = this->elseExpression->getVariablesAndTypes();
+ result.insert(tmp.begin(), tmp.end());
+ return result;
+ }
std::shared_ptr<BaseExpression const> IfThenElseExpression::simplify() const {
std::shared_ptr<BaseExpression const> conditionSimplified;
diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h
index b44de20be..0e59c097a 100644
--- a/src/storage/expressions/IfThenElseExpression.h
+++ b/src/storage/expressions/IfThenElseExpression.h
@@ -30,7 +30,8 @@ namespace storm {
virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
- virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual void accept(ExpressionVisitor* visitor) const override;
diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp
index 47341a771..b05ab5a67 100644
--- a/src/storage/expressions/IntegerLiteralExpression.cpp
+++ b/src/storage/expressions/IntegerLiteralExpression.cpp
@@ -16,11 +16,15 @@ namespace storm {
bool IntegerLiteralExpression::isLiteral() const {
return true;
- }
-
- std::set<std::string> IntegerLiteralExpression::getVariables() const {
- return std::set<std::string>();
- }
+ }
+
+ std::set<std::string> IntegerLiteralExpression::getVariables() const {
+ return std::set<std::string>();
+ }
+
+ std::map<std::string,ExpressionReturnType> IntegerLiteralExpression::getVariablesAndTypes() const {
+ return std::map<std::string, ExpressionReturnType>();
+ }
std::shared_ptr<BaseExpression const> IntegerLiteralExpression::simplify() const {
return this->shared_from_this();
diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h
index 4a9e8882f..5d6c731a5 100644
--- a/src/storage/expressions/IntegerLiteralExpression.h
+++ b/src/storage/expressions/IntegerLiteralExpression.h
@@ -28,7 +28,8 @@ namespace storm {
virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
virtual bool isLiteral() const override;
- virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual void accept(ExpressionVisitor* visitor) const override;
diff --git a/src/storage/expressions/TypeCheckVisitor.cpp b/src/storage/expressions/TypeCheckVisitor.cpp
index 044b85237..1c5899d61 100644
--- a/src/storage/expressions/TypeCheckVisitor.cpp
+++ b/src/storage/expressions/TypeCheckVisitor.cpp
@@ -43,8 +43,8 @@ namespace storm {
template<typename MapType>
void TypeCheckVisitor<MapType>::visit(VariableExpression const* expression) {
- auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName());
- LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getVariableName() << "'.");
+ auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName());
+ LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getVariableName() << "'.");
LOG_THROW(identifierTypePair->second == expression->getReturnType(), storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected '" << identifierTypePair->first << "', but found '" << expression->getReturnType() << "'.");
}
diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp
index 62ff442ed..cc75e6fa3 100644
--- a/src/storage/expressions/UnaryExpression.cpp
+++ b/src/storage/expressions/UnaryExpression.cpp
@@ -12,10 +12,14 @@ namespace storm {
bool UnaryExpression::containsVariables() const {
return this->getOperand()->containsVariables();
}
-
- std::set<std::string> UnaryExpression::getVariables() const {
- return this->getOperand()->getVariables();
- }
+
+ std::set<std::string> UnaryExpression::getVariables() const {
+ return this->getOperand()->getVariables();
+ }
+
+ std::map<std::string, ExpressionReturnType> UnaryExpression::getVariablesAndTypes() const {
+ return this->getOperand()->getVariablesAndTypes();
+ }
std::shared_ptr<BaseExpression const> const& UnaryExpression::getOperand() const {
return this->operand;
diff --git a/src/storage/expressions/UnaryExpression.h b/src/storage/expressions/UnaryExpression.h
index 8ad304ce1..27b903638 100644
--- a/src/storage/expressions/UnaryExpression.h
+++ b/src/storage/expressions/UnaryExpression.h
@@ -29,7 +29,8 @@ namespace storm {
virtual bool containsVariables() const override;
virtual uint_fast64_t getArity() const override;
virtual std::shared_ptr<BaseExpression const> getOperand(uint_fast64_t operandIndex) const override;
- virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
/*!
* Retrieves the operand of the unary expression.
diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp
index 2062c58ee..e28bbc7cd 100644
--- a/src/storage/expressions/VariableExpression.cpp
+++ b/src/storage/expressions/VariableExpression.cpp
@@ -53,6 +53,10 @@ namespace storm {
return {this->getVariableName()};
}
+ std::map<std::string, ExpressionReturnType> VariableExpression::getVariablesAndTypes() const {
+ return{ std::make_pair(this->getVariableName(), this->getReturnType()) };
+ }
+
std::shared_ptr<BaseExpression const> VariableExpression::simplify() const {
return this->shared_from_this();
}
diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h
index 6eff8c794..439cd3155 100644
--- a/src/storage/expressions/VariableExpression.h
+++ b/src/storage/expressions/VariableExpression.h
@@ -31,7 +31,8 @@ namespace storm {
virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
virtual std::string const& getIdentifier() const override;
virtual bool containsVariables() const override;
- virtual std::set<std::string> getVariables() const override;
+ virtual std::set<std::string> getVariables() const override;
+ virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual void accept(ExpressionVisitor* visitor) const override;