From 83d2a1c3152ae18d5eeec33a8c8f951ae1195300 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Tue, 6 May 2014 16:08:17 +0200 Subject: [PATCH] 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: 29f8e2fb70968802447ab37f923263a165776dce --- src/adapters/Z3ExpressionAdapter.h | 62 ++++++++++++++----- src/storage/expressions/BaseExpression.h | 10 ++- src/storage/expressions/BinaryExpression.cpp | 23 ++++--- src/storage/expressions/BinaryExpression.h | 5 +- .../expressions/BooleanLiteralExpression.cpp | 6 +- .../expressions/BooleanLiteralExpression.h | 3 +- .../expressions/DoubleLiteralExpression.cpp | 6 +- .../expressions/DoubleLiteralExpression.h | 3 +- src/storage/expressions/Expression.cpp | 19 ++++-- src/storage/expressions/Expression.h | 13 ++++ .../expressions/IfThenElseExpression.cpp | 29 ++++++--- .../expressions/IfThenElseExpression.h | 3 +- .../expressions/IntegerLiteralExpression.cpp | 14 +++-- .../expressions/IntegerLiteralExpression.h | 3 +- src/storage/expressions/TypeCheckVisitor.cpp | 4 +- src/storage/expressions/UnaryExpression.cpp | 12 ++-- src/storage/expressions/UnaryExpression.h | 3 +- .../expressions/VariableExpression.cpp | 4 ++ src/storage/expressions/VariableExpression.h | 3 +- 19 files changed, 165 insertions(+), 60 deletions(-) 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 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(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 #include #include +#include #include #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 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 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 BinaryExpression::getVariables() const { - std::set firstVariableSet = this->getFirstOperand()->getVariables(); - std::set secondVariableSet = this->getSecondOperand()->getVariables(); - firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end()); - return firstVariableSet; - } + } + + std::set BinaryExpression::getVariables() const { + std::set firstVariableSet = this->getFirstOperand()->getVariables(); + std::set secondVariableSet = this->getSecondOperand()->getVariables(); + firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end()); + return firstVariableSet; + } + + std::map BinaryExpression::getVariablesAndTypes() const { + std::map firstVariableSet = this->getFirstOperand()->getVariablesAndTypes(); + std::map secondVariableSet = this->getSecondOperand()->getVariablesAndTypes(); + firstVariableSet.insert(secondVariableSet.begin(), secondVariableSet.end()); + return firstVariableSet; + } std::shared_ptr 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 getOperand(uint_fast64_t operandIndex) const override; - virtual std::set getVariables() const override; + virtual std::shared_ptr getOperand(uint_fast64_t operandIndex) const override; + virtual std::set getVariables() const override; + virtual std::map 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 BooleanLiteralExpression::getVariables() const { return std::set(); - } + } + + std::map BooleanLiteralExpression::getVariablesAndTypes() const { + return std::map(); + } std::shared_ptr BooleanLiteralExpression::simplify() const { return this->shared_from_this(); diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h index 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 getVariables() const override; + virtual std::set getVariables() const override; + virtual std::map getVariablesAndTypes() const override; virtual std::shared_ptr 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 DoubleLiteralExpression::getVariables() const { return std::set(); - } + } + + std::map DoubleLiteralExpression::getVariablesAndTypes() const { + return std::map(); + } std::shared_ptr DoubleLiteralExpression::simplify() const { return this->shared_from_this(); diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h index 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 getVariables() const override; + virtual std::set getVariables() const override; + virtual std::map getVariablesAndTypes() const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override; diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 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 Expression::getVariables() const { - return this->getBaseExpression().getVariables(); - } + + std::set Expression::getVariables() const { + return this->getBaseExpression().getVariables(); + } + + std::map Expression::getVariablesAndTypes(bool validate = true) const { + if (validate) { + std::map 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 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 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 IfThenElseExpression::getVariables() const { - std::set result = this->condition->getVariables(); - std::set tmp = this->thenExpression->getVariables(); - result.insert(tmp.begin(), tmp.end()); - tmp = this->elseExpression->getVariables(); - result.insert(tmp.begin(), tmp.end()); - return result; - } + } + + std::set IfThenElseExpression::getVariables() const { + std::set result = this->condition->getVariables(); + std::set tmp = this->thenExpression->getVariables(); + result.insert(tmp.begin(), tmp.end()); + tmp = this->elseExpression->getVariables(); + result.insert(tmp.begin(), tmp.end()); + return result; + } + + std::map IfThenElseExpression::getVariablesAndTypes() const { + std::map result = this->condition->getVariablesAndTypes(); + std::map 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 IfThenElseExpression::simplify() const { std::shared_ptr 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 getVariables() const override; + virtual std::set getVariables() const override; + virtual std::map getVariablesAndTypes() const override; virtual std::shared_ptr 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 IntegerLiteralExpression::getVariables() const { - return std::set(); - } + } + + std::set IntegerLiteralExpression::getVariables() const { + return std::set(); + } + + std::map IntegerLiteralExpression::getVariablesAndTypes() const { + return std::map(); + } std::shared_ptr IntegerLiteralExpression::simplify() const { return this->shared_from_this(); diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h index 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 getVariables() const override; + virtual std::set getVariables() const override; + virtual std::map getVariablesAndTypes() const override; virtual std::shared_ptr 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 void TypeCheckVisitor::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 UnaryExpression::getVariables() const { - return this->getOperand()->getVariables(); - } + + std::set UnaryExpression::getVariables() const { + return this->getOperand()->getVariables(); + } + + std::map UnaryExpression::getVariablesAndTypes() const { + return this->getOperand()->getVariablesAndTypes(); + } std::shared_ptr 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 getOperand(uint_fast64_t operandIndex) const override; - virtual std::set getVariables() const override; + virtual std::set getVariables() const override; + virtual std::map 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 VariableExpression::getVariablesAndTypes() const { + return{ std::make_pair(this->getVariableName(), this->getReturnType()) }; + } + std::shared_ptr 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 getVariables() const override; + virtual std::set getVariables() const override; + virtual std::map getVariablesAndTypes() const override; virtual std::shared_ptr simplify() const override; virtual void accept(ExpressionVisitor* visitor) const override;