Adapted Z3ExpressionAdapter to deletion of constant expressions. Added functionality to autocreate variables in the solver. Added function to get variables and their types from an expression.

Former-commit-id: 29f8e2fb70

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 {
@@ -25,6 +27,9 @@ namespace storm {
             /*!
              * 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.
              * @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions.
@@ -41,10 +46,47 @@ 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;

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"
@@ -138,6 +139,13 @@ namespace storm {
              */
             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.
              *

src/storage/expressions/BinaryExpression.cpp

@@ -20,6 +20,13 @@ namespace storm {
 			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;
         }

src/storage/expressions/BinaryExpression.h

@@ -34,6 +34,7 @@ namespace storm {
             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::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
             
             /*!
              * Retrieves the first operand of the expression.

src/storage/expressions/BooleanLiteralExpression.cpp

@@ -26,6 +26,10 @@ namespace storm {
             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();
         }

src/storage/expressions/BooleanLiteralExpression.h

@@ -30,6 +30,7 @@ namespace storm {
             virtual bool isTrue() const override;
             virtual bool isFalse() 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;
             

src/storage/expressions/DoubleLiteralExpression.cpp

@@ -18,6 +18,10 @@ namespace storm {
             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();
         }

src/storage/expressions/DoubleLiteralExpression.h

@@ -28,6 +28,7 @@ namespace storm {
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual bool isLiteral() 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;
 

src/storage/expressions/Expression.cpp

@@ -91,6 +91,17 @@ namespace storm {
 			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;
         }

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.

src/storage/expressions/IfThenElseExpression.cpp

@@ -42,6 +42,15 @@ namespace storm {
 			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;
             if (conditionSimplified->isTrue()) {

src/storage/expressions/IfThenElseExpression.h

@@ -31,6 +31,7 @@ namespace storm {
             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::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
             

src/storage/expressions/IntegerLiteralExpression.cpp

@@ -22,6 +22,10 @@ namespace storm {
 			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();
         }

src/storage/expressions/IntegerLiteralExpression.h

@@ -29,6 +29,7 @@ namespace storm {
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual bool isLiteral() 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;
             

src/storage/expressions/UnaryExpression.cpp

@@ -17,6 +17,10 @@ namespace storm {
 			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;
         }

src/storage/expressions/UnaryExpression.h

@@ -30,6 +30,7 @@ namespace storm {
             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::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
             
             /*!
              * Retrieves the operand of the unary expression.

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();
         }

src/storage/expressions/VariableExpression.h

@@ -32,6 +32,7 @@ namespace storm {
             virtual std::string const& getIdentifier() const override;
             virtual bool containsVariables() 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;