From 3d426798b3850cb239cf3c71f54c0920d0e86add Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 6 Sep 2016 15:28:16 +0200 Subject: [PATCH] added visitor that checks for syntatical equality of expressions Former-commit-id: b6753a48919f06e9bd6289c4c09e81221a2e371c [formerly 2b36b42bfae4b847781ff9bd504f0392ad4c30a1] Former-commit-id: f693de5f3067436af61304b5f412a5bc1226bcf3 --- src/adapters/AddExpressionAdapter.cpp | 54 +++--- src/adapters/AddExpressionAdapter.h | 20 +-- src/adapters/MathsatExpressionAdapter.h | 44 ++--- src/adapters/Z3ExpressionAdapter.cpp | 44 ++--- src/adapters/Z3ExpressionAdapter.h | 20 +-- src/storage/expressions/BaseExpression.cpp | 82 +++++++++ src/storage/expressions/BaseExpression.h | 46 +++++- .../BinaryBooleanFunctionExpression.cpp | 4 +- .../BinaryBooleanFunctionExpression.h | 2 +- .../BinaryNumericalFunctionExpression.cpp | 4 +- .../BinaryNumericalFunctionExpression.h | 2 +- .../expressions/BinaryRelationExpression.cpp | 4 +- .../expressions/BinaryRelationExpression.h | 2 +- .../expressions/BooleanLiteralExpression.cpp | 4 +- .../expressions/BooleanLiteralExpression.h | 2 +- src/storage/expressions/Expression.cpp | 13 +- src/storage/expressions/Expression.h | 9 +- src/storage/expressions/ExpressionVisitor.h | 20 +-- .../expressions/IfThenElseExpression.cpp | 4 +- .../expressions/IfThenElseExpression.h | 2 +- .../expressions/IntegerLiteralExpression.cpp | 4 +- .../expressions/IntegerLiteralExpression.h | 2 +- .../expressions/LinearCoefficientVisitor.cpp | 28 ++-- .../expressions/LinearCoefficientVisitor.h | 20 +-- .../expressions/LinearityCheckVisitor.cpp | 28 ++-- .../expressions/LinearityCheckVisitor.h | 20 +-- .../expressions/RationalLiteralExpression.cpp | 4 +- .../expressions/RationalLiteralExpression.h | 2 +- .../expressions/SubstitutionVisitor.cpp | 44 ++--- src/storage/expressions/SubstitutionVisitor.h | 20 +-- .../SyntacticalEqualityCheckVisitor.cpp | 155 ++++++++++++++++++ .../SyntacticalEqualityCheckVisitor.h | 27 +++ .../expressions/ToExprtkStringVisitor.cpp | 108 ++++++------ .../expressions/ToExprtkStringVisitor.h | 20 +-- .../expressions/ToRationalFunctionVisitor.cpp | 26 +-- .../expressions/ToRationalFunctionVisitor.h | 20 +-- .../expressions/ToRationalNumberVisitor.cpp | 26 +-- .../expressions/ToRationalNumberVisitor.h | 20 +-- .../UnaryBooleanFunctionExpression.cpp | 4 +- .../UnaryBooleanFunctionExpression.h | 2 +- .../UnaryNumericalFunctionExpression.cpp | 4 +- .../UnaryNumericalFunctionExpression.h | 2 +- .../expressions/VariableExpression.cpp | 4 +- src/storage/expressions/VariableExpression.h | 2 +- src/storage/jani/Assignment.cpp | 4 + src/storage/jani/Assignment.h | 2 + src/storage/jani/Edge.cpp | 8 + src/storage/jani/Edge.h | 16 ++ 48 files changed, 677 insertions(+), 327 deletions(-) create mode 100644 src/storage/expressions/SyntacticalEqualityCheckVisitor.cpp create mode 100644 src/storage/expressions/SyntacticalEqualityCheckVisitor.h diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index 2f0dc7190..f8a8f200e 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -19,37 +19,37 @@ namespace storm { template storm::dd::Add AddExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { if (expression.hasBooleanType()) { - return boost::any_cast>(expression.accept(*this)).template toAdd(); + return boost::any_cast>(expression.accept(*this, boost::none)).template toAdd(); } else { - return boost::any_cast>(expression.accept(*this)); + return boost::any_cast>(expression.accept(*this, boost::none)); } } template storm::dd::Bdd AddExpressionAdapter::translateBooleanExpression(storm::expressions::Expression const& expression) { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected expression of boolean type."); - return boost::any_cast>(expression.accept(*this)); + return boost::any_cast>(expression.accept(*this, boost::none)); } template - boost::any AddExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { if (expression.hasBooleanType()) { - storm::dd::Bdd elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); - storm::dd::Bdd thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); - storm::dd::Bdd conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); + storm::dd::Bdd elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this, data)); + storm::dd::Bdd thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this, data)); + storm::dd::Bdd conditionDd = boost::any_cast>(expression.getCondition()->accept(*this, data)); return conditionDd.ite(thenDd, elseDd); } else { - storm::dd::Add elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); - storm::dd::Add thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); - storm::dd::Bdd conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); + storm::dd::Add elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this, data)); + storm::dd::Add thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this, data)); + storm::dd::Bdd conditionDd = boost::any_cast>(expression.getCondition()->accept(*this, data)); return conditionDd.ite(thenDd, elseDd); } } template - boost::any AddExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { - storm::dd::Bdd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Bdd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + storm::dd::Bdd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + storm::dd::Bdd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); storm::dd::Bdd result; switch (expression.getOperatorType()) { @@ -74,9 +74,9 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { - storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); storm::dd::Add result; switch (expression.getOperatorType()) { @@ -109,9 +109,9 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { - storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) { + storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); storm::dd::Bdd result; switch (expression.getRelationType()) { @@ -139,7 +139,7 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) { auto const& variablePair = variableMapping->find(expression.getVariable()); STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); if (expression.hasBooleanType()) { @@ -150,8 +150,8 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { - storm::dd::Bdd result = boost::any_cast>(expression.getOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + storm::dd::Bdd result = boost::any_cast>(expression.getOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: @@ -163,8 +163,8 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { - storm::dd::Add result = boost::any_cast>(expression.getOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + storm::dd::Add result = boost::any_cast>(expression.getOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: @@ -184,17 +184,17 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) { return expression.getValue() ? ddManager->getBddOne() : ddManager->getBddZero(); } template - boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) { return ddManager->getConstant(static_cast(expression.getValue())); } template - boost::any AddExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) { return ddManager->getConstant(static_cast(expression.getValueAsDouble())); } diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h index dfb13a315..cac29156f 100644 --- a/src/adapters/AddExpressionAdapter.h +++ b/src/adapters/AddExpressionAdapter.h @@ -22,16 +22,16 @@ namespace storm { storm::dd::Add translateExpression(storm::expressions::Expression const& expression); storm::dd::Bdd translateBooleanExpression(storm::expressions::Expression const& expression); - virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override; - virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression) override; - virtual boost::any visit(storm::expressions::VariableExpression const& expression) override; - virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override; - virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override; - virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) override; private: // The manager responsible for the DDs built by this adapter. diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 77b39cc68..8fad6a8af 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -57,7 +57,7 @@ namespace storm { * @return An equivalent term for MathSAT. */ msat_term translateExpression(storm::expressions::Expression const& expression) { - msat_term result = boost::any_cast(expression.getBaseExpression().accept(*this)); + msat_term result = boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); STORM_LOG_THROW(!MSAT_ERROR_TERM(result), storm::exceptions::ExpressionEvaluationException, "Could not translate expression to MathSAT's format."); return result; } @@ -90,9 +90,9 @@ namespace storm { return declarationVariablePair->second; } - virtual boost::any visit(expressions::BinaryBooleanFunctionExpression const& expression) override { - msat_term leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); - msat_term rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override { + msat_term leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + msat_term rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: @@ -108,9 +108,9 @@ namespace storm { } } - virtual boost::any visit(expressions::BinaryNumericalFunctionExpression const& expression) override { - msat_term leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); - msat_term rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override { + msat_term leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + msat_term rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: @@ -130,9 +130,9 @@ namespace storm { } } - virtual boost::any visit(expressions::BinaryRelationExpression const& expression) override { - msat_term leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); - msat_term rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) override { + msat_term leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + msat_term rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); switch (expression.getRelationType()) { case storm::expressions::BinaryRelationExpression::RelationType::Equal: @@ -160,27 +160,27 @@ namespace storm { } } - virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override { - msat_term conditionResult = boost::any_cast(expression.getCondition()->accept(*this)); - msat_term thenResult = boost::any_cast(expression.getThenExpression()->accept(*this)); - msat_term elseResult = boost::any_cast(expression.getElseExpression()->accept(*this)); + virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override { + msat_term conditionResult = boost::any_cast(expression.getCondition()->accept(*this, data)); + msat_term thenResult = boost::any_cast(expression.getThenExpression()->accept(*this, data)); + msat_term elseResult = boost::any_cast(expression.getElseExpression()->accept(*this, data)); return msat_make_term_ite(env, conditionResult, thenResult, elseResult); } - virtual boost::any visit(expressions::BooleanLiteralExpression const& expression) override { + virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) override { return expression.getValue() ? msat_make_true(env) : msat_make_false(env); } - virtual boost::any visit(expressions::RationalLiteralExpression const& expression) override { + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) override { return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str()); } - virtual boost::any visit(expressions::IntegerLiteralExpression const& expression) override { + virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) override { return msat_make_number(env, std::to_string(static_cast(expression.getValue())).c_str()); } - virtual boost::any visit(expressions::UnaryBooleanFunctionExpression const& expression) override { - msat_term childResult = boost::any_cast(expression.getOperand()->accept(*this)); + virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) override { + msat_term childResult = boost::any_cast(expression.getOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: @@ -191,8 +191,8 @@ namespace storm { } } - virtual boost::any visit(expressions::UnaryNumericalFunctionExpression const& expression) override { - msat_term childResult = boost::any_cast(expression.getOperand()->accept(*this)); + virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) override { + msat_term childResult = boost::any_cast(expression.getOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: @@ -209,7 +209,7 @@ namespace storm { } } - virtual boost::any visit(expressions::VariableExpression const& expression) override { + virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data) override { return translateExpression(expression.getVariable()); } diff --git a/src/adapters/Z3ExpressionAdapter.cpp b/src/adapters/Z3ExpressionAdapter.cpp index a80355422..8258f42f5 100644 --- a/src/adapters/Z3ExpressionAdapter.cpp +++ b/src/adapters/Z3ExpressionAdapter.cpp @@ -16,7 +16,7 @@ namespace storm { z3::expr Z3ExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { STORM_LOG_ASSERT(expression.getManager() == this->manager, "Invalid expression for solver."); - z3::expr result = boost::any_cast(expression.getBaseExpression().accept(*this)); + z3::expr result = boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); for (z3::expr const& assertion : additionalAssertions) { result = result && assertion; @@ -139,9 +139,9 @@ namespace storm { } } - boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { - z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); - z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); switch(expression.getOperatorType()) { case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: @@ -160,9 +160,9 @@ namespace storm { } - boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { - z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); - z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); switch(expression.getOperatorType()) { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: @@ -184,9 +184,9 @@ namespace storm { } } - boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { - z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); - z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) { + z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); switch(expression.getRelationType()) { case storm::expressions::BinaryRelationExpression::RelationType::Equal: @@ -206,22 +206,22 @@ namespace storm { } } - boost::any Z3ExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) { return context.bool_val(expression.getValue()); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) { std::stringstream fractionStream; fractionStream << expression.getValue(); return context.real_val(fractionStream.str().c_str()); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) { return context.int_val(static_cast(expression.getValue())); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { - z3::expr childResult = boost::any_cast(expression.getOperand()->accept(*this)); + boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + z3::expr childResult = boost::any_cast(expression.getOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: @@ -231,8 +231,8 @@ namespace storm { } } - boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { - z3::expr childResult = boost::any_cast(expression.getOperand()->accept(*this)); + boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + z3::expr childResult = boost::any_cast(expression.getOperand()->accept(*this, data)); switch(expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: @@ -253,14 +253,14 @@ namespace storm { } } - boost::any Z3ExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { - z3::expr conditionResult = boost::any_cast(expression.getCondition()->accept(*this)); - z3::expr thenResult = boost::any_cast(expression.getThenExpression()->accept(*this)); - z3::expr elseResult = boost::any_cast(expression.getElseExpression()->accept(*this)); + boost::any Z3ExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { + z3::expr conditionResult = boost::any_cast(expression.getCondition()->accept(*this, data)); + z3::expr thenResult = boost::any_cast(expression.getThenExpression()->accept(*this, data)); + z3::expr elseResult = boost::any_cast(expression.getElseExpression()->accept(*this, data)); return z3::expr(context, Z3_mk_ite(context, conditionResult, thenResult, elseResult)); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) { return this->translateExpression(expression.getVariable()); } diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 2735f5713..70cfac18b 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -55,25 +55,25 @@ namespace storm { */ storm::expressions::Variable const& getVariable(z3::func_decl z3Declaration); - virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) override; + virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) override; + virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression) override; + virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) override; + virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) override; + virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override; + virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override; - virtual boost::any visit(storm::expressions::VariableExpression const& expression) override; + virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data) override; private: /*! diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index 9d44215d0..d37b61e50 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -4,6 +4,8 @@ #include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/InvalidAccessException.h" +#include "src/storage/expressions/Expressions.h" + namespace storm { namespace expressions { BaseExpression::BaseExpression(ExpressionManager const& manager, Type const& type) : manager(manager), type(type) { @@ -94,6 +96,86 @@ namespace storm { return this->shared_from_this(); } + bool BaseExpression::isIfThenElseExpression() const { + return false; + } + + IfThenElseExpression const& BaseExpression::asIfThenElseExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isBinaryBooleanFunctionExpression() const { + return false; + } + + BinaryBooleanFunctionExpression const& BaseExpression::asBinaryBooleanFunctionExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isBinaryNumericalFunctionExpression() const { + return false; + } + + BinaryNumericalFunctionExpression const& BaseExpression::asBinaryNumericalFunctionExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isBinaryRelationExpression() const { + return false; + } + + BinaryRelationExpression const& BaseExpression::asBinaryRelationExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isBooleanLiteralExpression() const { + return false; + } + + BooleanLiteralExpression const& BaseExpression::asBooleanLiteralExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isIntegerLiteralExpression() const { + return false; + } + + IntegerLiteralExpression const& BaseExpression::asIntegerLiteralExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isRationalLiteralExpression() const { + return false; + } + + RationalLiteralExpression const& BaseExpression::asRationalLiteralExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isUnaryBooleanFunctionExpression() const { + return false; + } + + UnaryBooleanFunctionExpression const& BaseExpression::asUnaryBooleanFunctionExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isUnaryNumericalFunctionExpression() const { + return false; + } + + UnaryNumericalFunctionExpression const& BaseExpression::asUnaryNumericalFunctionExpression() const { + return static_cast(*this); + } + + bool BaseExpression::isVariableExpression() const { + return false; + } + + VariableExpression const& BaseExpression::asVariableExpression() const { + return static_cast(*this); + } + std::ostream& operator<<(std::ostream& stream, BaseExpression const& expression) { expression.printToStream(stream); return stream; diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index f9b2792f4..7b5b2d973 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/src/storage/expressions/BaseExpression.h @@ -13,12 +13,24 @@ namespace storm { namespace expressions { - // Forward-declare expression manager. + // Forward-declare expression classes. class ExpressionManager; class Variable; class Valuation; class ExpressionVisitor; enum struct OperatorType; + + class IfThenElseExpression; + class BinaryBooleanFunctionExpression; + class BinaryNumericalFunctionExpression; + class BinaryRelationExpression; + class BooleanLiteralExpression; + class IntegerLiteralExpression; + class RationalLiteralExpression; + class UnaryBooleanFunctionExpression; + class UnaryNumericalFunctionExpression; + class VariableExpression; + /*! * The base class of all expression classes. */ @@ -164,7 +176,7 @@ namespace storm { * * @param visitor The visitor that is to be accepted. */ - virtual boost::any accept(ExpressionVisitor& visitor) const = 0; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const = 0; /*! * Retrieves whether the expression has a numerical type, i.e., integer or double. @@ -224,6 +236,36 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, BaseExpression const& expression); + virtual bool isIfThenElseExpression() const; + IfThenElseExpression const& asIfThenElseExpression() const; + + virtual bool isBinaryBooleanFunctionExpression() const; + BinaryBooleanFunctionExpression const& asBinaryBooleanFunctionExpression() const; + + virtual bool isBinaryNumericalFunctionExpression() const; + BinaryNumericalFunctionExpression const& asBinaryNumericalFunctionExpression() const; + + virtual bool isBinaryRelationExpression() const; + BinaryRelationExpression const& asBinaryRelationExpression() const; + + virtual bool isBooleanLiteralExpression() const; + BooleanLiteralExpression const& asBooleanLiteralExpression() const; + + virtual bool isIntegerLiteralExpression() const; + IntegerLiteralExpression const& asIntegerLiteralExpression() const; + + virtual bool isRationalLiteralExpression() const; + RationalLiteralExpression const& asRationalLiteralExpression() const; + + virtual bool isUnaryBooleanFunctionExpression() const; + UnaryBooleanFunctionExpression const& asUnaryBooleanFunctionExpression() const; + + virtual bool isUnaryNumericalFunctionExpression() const; + UnaryNumericalFunctionExpression const& asUnaryNumericalFunctionExpression() const; + + virtual bool isVariableExpression() const; + VariableExpression const& asVariableExpression() const; + protected: /*! * Prints the expression to the given stream. diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 6cb550609..0b832db09 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -119,8 +119,8 @@ namespace storm { } } - boost::any BinaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any BinaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } void BinaryBooleanFunctionExpression::printToStream(std::ostream& stream) const { diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h index d49658c7e..27a035cca 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h @@ -37,7 +37,7 @@ namespace storm { virtual storm::expressions::OperatorType getOperator() const override; virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the operator associated with the expression. diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp index 7c4367952..eda2d0377 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -113,8 +113,8 @@ namespace storm { } } - boost::any BinaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any BinaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } void BinaryNumericalFunctionExpression::printToStream(std::ostream& stream) const { diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storage/expressions/BinaryNumericalFunctionExpression.h index e3c7d227a..1320ab56b 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.h +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.h @@ -38,7 +38,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::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the operator associated with the expression. diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp index 858536d0c..04a8f7895 100644 --- a/src/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storage/expressions/BinaryRelationExpression.cpp @@ -81,8 +81,8 @@ namespace storm { } } - boost::any BinaryRelationExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any BinaryRelationExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } BinaryRelationExpression::RelationType BinaryRelationExpression::getRelationType() const { diff --git a/src/storage/expressions/BinaryRelationExpression.h b/src/storage/expressions/BinaryRelationExpression.h index 079a935a6..6dd73179c 100644 --- a/src/storage/expressions/BinaryRelationExpression.h +++ b/src/storage/expressions/BinaryRelationExpression.h @@ -37,7 +37,7 @@ namespace storm { virtual storm::expressions::OperatorType getOperator() const override; virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the relation associated with the expression. diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp index 9e4986b04..086d22abd 100644 --- a/src/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storage/expressions/BooleanLiteralExpression.cpp @@ -32,8 +32,8 @@ namespace storm { return this->shared_from_this(); } - boost::any BooleanLiteralExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any BooleanLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } bool BooleanLiteralExpression::getValue() const { diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h index f5dcb78a1..cea09a295 100644 --- a/src/storage/expressions/BooleanLiteralExpression.h +++ b/src/storage/expressions/BooleanLiteralExpression.h @@ -32,7 +32,7 @@ namespace storm { virtual bool isFalse() const override; virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the value of the boolean literal. diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 3d6094d8b..97df87d28 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -5,6 +5,7 @@ #include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/SubstitutionVisitor.h" #include "src/storage/expressions/LinearityCheckVisitor.h" +#include "src/storage/expressions/SyntacticalEqualityCheckVisitor.h" #include "src/storage/expressions/Expressions.h" #include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/InvalidArgumentException.h" @@ -158,8 +159,8 @@ namespace storm { return this->getBaseExpression().hasBitVectorType(); } - boost::any Expression::accept(ExpressionVisitor& visitor) const { - return this->getBaseExpression().accept(visitor); + boost::any Expression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return this->getBaseExpression().accept(visitor, data); } bool Expression::isInitialized() const { @@ -168,6 +169,14 @@ namespace storm { } return false; } + + bool Expression::isSyntacticallyEqual(storm::expressions::Expression const& other) const { + if (this->getBaseExpressionPointer() == other.getBaseExpressionPointer()) { + return true; + } + SyntacticalEqualityCheckVisitor checker; + return checker.isSyntaticallyEqual(*this, other); + } std::string Expression::toString() const { std::stringstream stream; diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 40fcaa572..e6b3cdf8d 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -298,7 +298,7 @@ namespace storm { * * @param visitor The visitor to accept. */ - boost::any accept(ExpressionVisitor& visitor) const; + boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const; /*! * Converts the expression into a string. @@ -307,11 +307,16 @@ namespace storm { */ std::string toString() const; - /** + /*! * Checks whether the object encapsulates a base-expression. */ bool isInitialized() const; + /*! + * Checks whether the two expressions are syntatically the same. + */ + bool isSyntacticallyEqual(storm::expressions::Expression const& other) const; + friend std::ostream& operator<<(std::ostream& stream, Expression const& expression); private: diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index 1abafc2a6..cfe2ce9b6 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -19,16 +19,16 @@ namespace storm { class ExpressionVisitor { public: - virtual boost::any visit(IfThenElseExpression const& expression) = 0; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) = 0; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) = 0; - virtual boost::any visit(BinaryRelationExpression const& expression) = 0; - virtual boost::any visit(VariableExpression const& expression) = 0; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) = 0; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) = 0; - virtual boost::any visit(BooleanLiteralExpression const& expression) = 0; - virtual boost::any visit(IntegerLiteralExpression const& expression) = 0; - virtual boost::any visit(RationalLiteralExpression const& expression) = 0; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) = 0; }; } } diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp index adde41a2d..8441fbeb0 100644 --- a/src/storage/expressions/IfThenElseExpression.cpp +++ b/src/storage/expressions/IfThenElseExpression.cpp @@ -88,8 +88,8 @@ namespace storm { } } - boost::any IfThenElseExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any IfThenElseExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::shared_ptr IfThenElseExpression::getCondition() const { diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h index d2503116b..347feba12 100644 --- a/src/storage/expressions/IfThenElseExpression.h +++ b/src/storage/expressions/IfThenElseExpression.h @@ -38,7 +38,7 @@ namespace storm { virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the condition expression of the if-then-else expression. diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp index 35ae07ee7..d8b7077b5 100644 --- a/src/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storage/expressions/IntegerLiteralExpression.cpp @@ -29,8 +29,8 @@ namespace storm { return this->shared_from_this(); } - boost::any IntegerLiteralExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any IntegerLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } int_fast64_t IntegerLiteralExpression::getValue() const { diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h index b4f732b83..3dc06e4ef 100644 --- a/src/storage/expressions/IntegerLiteralExpression.h +++ b/src/storage/expressions/IntegerLiteralExpression.h @@ -31,7 +31,7 @@ namespace storm { virtual bool isLiteral() const override; virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the value of the integer literal. diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp index dc9a909f9..6a8701610 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storage/expressions/LinearCoefficientVisitor.cpp @@ -85,20 +85,20 @@ namespace storm { } LinearCoefficientVisitor::VariableCoefficients LinearCoefficientVisitor::getLinearCoefficients(Expression const& expression) { - return boost::any_cast(expression.getBaseExpression().accept(*this)); + return boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); } - boost::any LinearCoefficientVisitor::visit(IfThenElseExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(BinaryBooleanFunctionExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - VariableCoefficients leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); - VariableCoefficients rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + boost::any LinearCoefficientVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + VariableCoefficients leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + VariableCoefficients rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); if (expression.getOperatorType() == BinaryNumericalFunctionExpression::OperatorType::Plus) { leftResult += std::move(rightResult); @@ -114,11 +114,11 @@ namespace storm { return leftResult; } - boost::any LinearCoefficientVisitor::visit(BinaryRelationExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(VariableExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(VariableExpression const& expression, boost::any const& data) { VariableCoefficients coefficients; if (expression.getType().isNumericalType()) { coefficients.setCoefficient(expression.getVariable(), 1); @@ -128,12 +128,12 @@ namespace storm { return coefficients; } - boost::any LinearCoefficientVisitor::visit(UnaryBooleanFunctionExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(UnaryNumericalFunctionExpression const& expression) { - VariableCoefficients childResult = boost::any_cast(expression.getOperand()->accept(*this)); + boost::any LinearCoefficientVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + VariableCoefficients childResult = boost::any_cast(expression.getOperand()->accept(*this, data)); if (expression.getOperatorType() == UnaryNumericalFunctionExpression::OperatorType::Minus) { childResult.negate(); @@ -143,15 +143,15 @@ namespace storm { } } - boost::any LinearCoefficientVisitor::visit(BooleanLiteralExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(IntegerLiteralExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { return VariableCoefficients(static_cast(expression.getValue())); } - boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { return VariableCoefficients(expression.getValueAsDouble()); } } diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index dea1bfc2e..b0c85a800 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -66,16 +66,16 @@ namespace storm { */ VariableCoefficients getLinearCoefficients(Expression const& expression); - virtual boost::any visit(IfThenElseExpression const& expression) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BinaryRelationExpression const& expression) override; - virtual boost::any visit(VariableExpression const& expression) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BooleanLiteralExpression const& expression) override; - virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(RationalLiteralExpression const& expression) override; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; }; } } diff --git a/src/storage/expressions/LinearityCheckVisitor.cpp b/src/storage/expressions/LinearityCheckVisitor.cpp index 7a33a501a..b762f9cf1 100644 --- a/src/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storage/expressions/LinearityCheckVisitor.cpp @@ -12,27 +12,27 @@ namespace storm { } bool LinearityCheckVisitor::check(Expression const& expression) { - LinearityStatus result = boost::any_cast(expression.getBaseExpression().accept(*this)); + LinearityStatus result = boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); return result == LinearityStatus::LinearWithoutVariables || result == LinearityStatus::LinearContainsVariables; } - boost::any LinearityCheckVisitor::visit(IfThenElseExpression const& expression) { + boost::any LinearityCheckVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { // An if-then-else expression is never linear. return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const& expression) { + boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { // Boolean function applications are not allowed in linear expressions. return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - LinearityStatus leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this)); + boost::any LinearityCheckVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + LinearityStatus leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); if (leftResult == LinearityStatus::NonLinear) { return LinearityStatus::NonLinear; } - LinearityStatus rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this)); + LinearityStatus rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); if (rightResult == LinearityStatus::NonLinear) { return LinearityStatus::NonLinear; } @@ -55,37 +55,37 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal binary numerical expression operator."); } - boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const& expression) { + boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(VariableExpression const& expression) { + boost::any LinearityCheckVisitor::visit(VariableExpression const& expression, boost::any const& data) { return LinearityStatus::LinearContainsVariables; } - boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression) { + boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { // Boolean function applications are not allowed in linear expressions. return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(UnaryNumericalFunctionExpression const& expression) { + boost::any LinearityCheckVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { switch (expression.getOperatorType()) { - case UnaryNumericalFunctionExpression::OperatorType::Minus: return expression.getOperand()->accept(*this); + case UnaryNumericalFunctionExpression::OperatorType::Minus: return expression.getOperand()->accept(*this, data); case UnaryNumericalFunctionExpression::OperatorType::Floor: case UnaryNumericalFunctionExpression::OperatorType::Ceil: return LinearityStatus::NonLinear; } STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator."); } - boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression) { + boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(IntegerLiteralExpression const& expression) { + boost::any LinearityCheckVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { return LinearityStatus::LinearWithoutVariables; } - boost::any LinearityCheckVisitor::visit(RationalLiteralExpression const& expression) { + boost::any LinearityCheckVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { return LinearityStatus::LinearWithoutVariables; } } diff --git a/src/storage/expressions/LinearityCheckVisitor.h b/src/storage/expressions/LinearityCheckVisitor.h index 6bb35b7e8..b2a465871 100644 --- a/src/storage/expressions/LinearityCheckVisitor.h +++ b/src/storage/expressions/LinearityCheckVisitor.h @@ -20,16 +20,16 @@ namespace storm { */ bool check(Expression const& expression); - virtual boost::any visit(IfThenElseExpression const& expression) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BinaryRelationExpression const& expression) override; - virtual boost::any visit(VariableExpression const& expression) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BooleanLiteralExpression const& expression) override; - virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(RationalLiteralExpression const& expression) override; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; private: enum class LinearityStatus { NonLinear, LinearContainsVariables, LinearWithoutVariables }; diff --git a/src/storage/expressions/RationalLiteralExpression.cpp b/src/storage/expressions/RationalLiteralExpression.cpp index 3fa226a8a..6c6ee88ff 100644 --- a/src/storage/expressions/RationalLiteralExpression.cpp +++ b/src/storage/expressions/RationalLiteralExpression.cpp @@ -34,8 +34,8 @@ namespace storm { return this->shared_from_this(); } - boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } double RationalLiteralExpression::getValueAsDouble() const { diff --git a/src/storage/expressions/RationalLiteralExpression.h b/src/storage/expressions/RationalLiteralExpression.h index 4eff900b2..e18cf8c43 100644 --- a/src/storage/expressions/RationalLiteralExpression.h +++ b/src/storage/expressions/RationalLiteralExpression.h @@ -48,7 +48,7 @@ namespace storm { virtual bool isLiteral() const override; virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the value of the double literal. diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index 1490e6f59..c2b4ff419 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -14,14 +14,14 @@ namespace storm { template Expression SubstitutionVisitor::substitute(Expression const& expression) { - return Expression(boost::any_cast>(expression.getBaseExpression().accept(*this))); + return Expression(boost::any_cast>(expression.getBaseExpression().accept(*this, boost::none))); } template - boost::any SubstitutionVisitor::visit(IfThenElseExpression const& expression) { - std::shared_ptr conditionExpression = boost::any_cast>(expression.getCondition()->accept(*this)); - std::shared_ptr thenExpression = boost::any_cast>(expression.getThenExpression()->accept(*this)); - std::shared_ptr elseExpression = boost::any_cast>(expression.getElseExpression()->accept(*this)); + boost::any SubstitutionVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + std::shared_ptr conditionExpression = boost::any_cast>(expression.getCondition()->accept(*this, data)); + std::shared_ptr thenExpression = boost::any_cast>(expression.getThenExpression()->accept(*this, data)); + std::shared_ptr elseExpression = boost::any_cast>(expression.getElseExpression()->accept(*this, data)); // If the arguments did not change, we simply push the expression itself. if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) { @@ -32,9 +32,9 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(BinaryBooleanFunctionExpression const& expression) { - std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any SubstitutionVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); // If the arguments did not change, we simply push the expression itself. if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { @@ -45,9 +45,9 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any SubstitutionVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); // If the arguments did not change, we simply push the expression itself. if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { @@ -58,9 +58,9 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(BinaryRelationExpression const& expression) { - std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any SubstitutionVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); // If the arguments did not change, we simply push the expression itself. if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { @@ -71,7 +71,7 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(VariableExpression const& expression) { + boost::any SubstitutionVisitor::visit(VariableExpression const& expression, boost::any const& data) { // If the variable is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->variableToExpressionMapping.find(expression.getVariable()); if (nameExpressionPair != this->variableToExpressionMapping.end()) { @@ -82,8 +82,8 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(UnaryBooleanFunctionExpression const& expression) { - std::shared_ptr operandExpression = boost::any_cast>(expression.getOperand()->accept(*this)); + boost::any SubstitutionVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + std::shared_ptr operandExpression = boost::any_cast>(expression.getOperand()->accept(*this, data)); // If the argument did not change, we simply push the expression itself. if (operandExpression.get() == expression.getOperand().get()) { @@ -94,8 +94,8 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(UnaryNumericalFunctionExpression const& expression) { - std::shared_ptr operandExpression = boost::any_cast>(expression.getOperand()->accept(*this)); + boost::any SubstitutionVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + std::shared_ptr operandExpression = boost::any_cast>(expression.getOperand()->accept(*this, data)); // If the argument did not change, we simply push the expression itself. if (operandExpression.get() == expression.getOperand().get()) { @@ -106,17 +106,17 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(BooleanLiteralExpression const& expression) { + boost::any SubstitutionVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { return expression.getSharedPointer(); } template - boost::any SubstitutionVisitor::visit(IntegerLiteralExpression const& expression) { + boost::any SubstitutionVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { return expression.getSharedPointer(); } template - boost::any SubstitutionVisitor::visit(RationalLiteralExpression const& expression) { + boost::any SubstitutionVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { return expression.getSharedPointer(); } diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index 5f1a93cb2..2131696c4 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -28,16 +28,16 @@ namespace storm { */ Expression substitute(Expression const& expression); - virtual boost::any visit(IfThenElseExpression const& expression) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BinaryRelationExpression const& expression) override; - virtual boost::any visit(VariableExpression const& expression) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BooleanLiteralExpression const& expression) override; - virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(RationalLiteralExpression const& expression) override; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; private: // A mapping of variables to expressions with which they shall be replaced. diff --git a/src/storage/expressions/SyntacticalEqualityCheckVisitor.cpp b/src/storage/expressions/SyntacticalEqualityCheckVisitor.cpp new file mode 100644 index 000000000..4277a7dbb --- /dev/null +++ b/src/storage/expressions/SyntacticalEqualityCheckVisitor.cpp @@ -0,0 +1,155 @@ +#include "src/storage/expressions/SyntacticalEqualityCheckVisitor.h" + +#include "src/storage/expressions/Expressions.h" + +namespace storm { + namespace expressions { + + bool SyntacticalEqualityCheckVisitor::isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) { + return boost::any_cast(expression1.accept(*this, std::ref(expression2.getBaseExpression()))); + } + + boost::any SyntacticalEqualityCheckVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isIfThenElseExpression()) { + IfThenElseExpression const& otherExpression = otherBaseExpression.asIfThenElseExpression(); + + bool result = boost::any_cast(expression.getCondition()->accept(*this, std::ref(*otherExpression.getCondition()))); + if (result) { + result = boost::any_cast(expression.getThenExpression()->accept(*this, std::ref(*otherExpression.getThenExpression()))); + } + if (result) { + result = boost::any_cast(expression.getElseExpression()->accept(*this, std::ref(*otherExpression.getElseExpression()))); + } + return result; + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isBinaryBooleanFunctionExpression()) { + BinaryBooleanFunctionExpression const& otherExpression = otherBaseExpression.asBinaryBooleanFunctionExpression(); + + bool result = expression.getOperatorType() == otherExpression.getOperatorType(); + if (result) { + result = boost::any_cast(expression.getFirstOperand()->accept(*this, std::ref(*otherExpression.getFirstOperand()))); + } + if (result) { + result = boost::any_cast(expression.getSecondOperand()->accept(*this, std::ref(*otherExpression.getSecondOperand()))); + } + return result; + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isBinaryNumericalFunctionExpression()) { + BinaryNumericalFunctionExpression const& otherExpression = otherBaseExpression.asBinaryNumericalFunctionExpression(); + + bool result = expression.getOperatorType() == otherExpression.getOperatorType(); + if (result) { + result = boost::any_cast(expression.getFirstOperand()->accept(*this, std::ref(*otherExpression.getFirstOperand()))); + } + if (result) { + result = boost::any_cast(expression.getSecondOperand()->accept(*this, std::ref(*otherExpression.getSecondOperand()))); + } + return result; + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isBinaryRelationExpression()) { + BinaryRelationExpression const& otherExpression = otherBaseExpression.asBinaryRelationExpression(); + + bool result = expression.getRelationType() == otherExpression.getRelationType(); + if (result) { + result = boost::any_cast(expression.getFirstOperand()->accept(*this, std::ref(*otherExpression.getFirstOperand()))); + } + if (result) { + result = boost::any_cast(expression.getSecondOperand()->accept(*this, std::ref(*otherExpression.getSecondOperand()))); + } + return result; + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(VariableExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isVariableExpression()) { + VariableExpression const& otherExpression = otherBaseExpression.asVariableExpression(); + return expression.getVariable() == otherExpression.getVariable(); + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isBinaryBooleanFunctionExpression()) { + UnaryBooleanFunctionExpression const& otherExpression = otherBaseExpression.asUnaryBooleanFunctionExpression(); + + bool result = expression.getOperatorType() == otherExpression.getOperatorType(); + if (result) { + result = boost::any_cast(expression.getOperand()->accept(*this, std::ref(*otherExpression.getOperand()))); + } + return result; + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isBinaryBooleanFunctionExpression()) { + UnaryNumericalFunctionExpression const& otherExpression = otherBaseExpression.asUnaryNumericalFunctionExpression(); + + bool result = expression.getOperatorType() == otherExpression.getOperatorType(); + if (result) { + result = boost::any_cast(expression.getOperand()->accept(*this, std::ref(*otherExpression.getOperand()))); + } + return result; + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isBooleanLiteralExpression()) { + BooleanLiteralExpression const& otherExpression = otherBaseExpression.asBooleanLiteralExpression(); + return expression.getValue() == otherExpression.getValue(); + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isIntegerLiteralExpression()) { + IntegerLiteralExpression const& otherExpression = otherBaseExpression.asIntegerLiteralExpression(); + return expression.getValue() == otherExpression.getValue(); + } else { + return false; + } + } + + boost::any SyntacticalEqualityCheckVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); + if (otherBaseExpression.isRationalLiteralExpression()) { + RationalLiteralExpression const& otherExpression = otherBaseExpression.asRationalLiteralExpression(); + return expression.getValue() == otherExpression.getValue(); + } else { + return false; + } + } + + } +} \ No newline at end of file diff --git a/src/storage/expressions/SyntacticalEqualityCheckVisitor.h b/src/storage/expressions/SyntacticalEqualityCheckVisitor.h new file mode 100644 index 000000000..82366e507 --- /dev/null +++ b/src/storage/expressions/SyntacticalEqualityCheckVisitor.h @@ -0,0 +1,27 @@ +#pragma once + +#include "src/storage/expressions/ExpressionVisitor.h" + +namespace storm { + namespace expressions { + + class Expression; + + class SyntacticalEqualityCheckVisitor : public ExpressionVisitor { + public: + bool isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2); + + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; + }; + + } +} \ No newline at end of file diff --git a/src/storage/expressions/ToExprtkStringVisitor.cpp b/src/storage/expressions/ToExprtkStringVisitor.cpp index 1492aeae5..88ab1132a 100644 --- a/src/storage/expressions/ToExprtkStringVisitor.cpp +++ b/src/storage/expressions/ToExprtkStringVisitor.cpp @@ -9,210 +9,210 @@ namespace storm { std::string ToExprtkStringVisitor::toString(BaseExpression const* expression) { stream.str(""); stream.clear(); - expression->accept(*this); + expression->accept(*this, boost::none); return stream.str(); } - boost::any ToExprtkStringVisitor::visit(IfThenElseExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { stream << "if("; - expression.getCondition()->accept(*this); + expression.getCondition()->accept(*this, data); stream << ","; - expression.getThenExpression()->accept(*this); + expression.getThenExpression()->accept(*this, data); stream << ","; - expression.getElseExpression()->accept(*this); + expression.getElseExpression()->accept(*this, data); stream << ")"; return boost::any(); } - boost::any ToExprtkStringVisitor::visit(BinaryBooleanFunctionExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { switch (expression.getOperatorType()) { case BinaryBooleanFunctionExpression::OperatorType::And: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << " and "; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Or: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << " or "; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Xor: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << " xor "; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Implies: stream << "(not("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << ") or "; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Iff: - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "=="; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); break; } return boost::any(); } - boost::any ToExprtkStringVisitor::visit(BinaryNumericalFunctionExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { switch (expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "+"; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Minus: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "-"; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Times: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "*"; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Divide: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "/"; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Power: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "^"; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Max: stream << "max("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << ","; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Min: stream << "min("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << ","; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; } return boost::any(); } - boost::any ToExprtkStringVisitor::visit(BinaryRelationExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { switch (expression.getRelationType()) { case BinaryRelationExpression::RelationType::Equal: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "=="; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryRelationExpression::RelationType::NotEqual: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "!="; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryRelationExpression::RelationType::Less: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "<"; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryRelationExpression::RelationType::LessOrEqual: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << "<="; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryRelationExpression::RelationType::Greater: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << ">"; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; case BinaryRelationExpression::RelationType::GreaterOrEqual: stream << "("; - expression.getFirstOperand()->accept(*this); + expression.getFirstOperand()->accept(*this, data); stream << ">="; - expression.getSecondOperand()->accept(*this); + expression.getSecondOperand()->accept(*this, data); stream << ")"; break; } return boost::any(); } - boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression, boost::any const& data) { stream << expression.getVariableName(); return boost::any(); } - boost::any ToExprtkStringVisitor::visit(UnaryBooleanFunctionExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { switch (expression.getOperatorType()) { case UnaryBooleanFunctionExpression::OperatorType::Not: stream << "not("; - expression.getOperand()->accept(*this); + expression.getOperand()->accept(*this, data); stream << ")"; } return boost::any(); } - boost::any ToExprtkStringVisitor::visit(UnaryNumericalFunctionExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { switch (expression.getOperatorType()) { case UnaryNumericalFunctionExpression::OperatorType::Minus: stream << "-("; - expression.getOperand()->accept(*this); + expression.getOperand()->accept(*this, data); stream << ")"; break; case UnaryNumericalFunctionExpression::OperatorType::Floor: stream << "floor("; - expression.getOperand()->accept(*this); + expression.getOperand()->accept(*this, data); stream << ")"; break; case UnaryNumericalFunctionExpression::OperatorType::Ceil: stream << "ceil("; - expression.getOperand()->accept(*this); + expression.getOperand()->accept(*this, data); stream << ")"; break; } return boost::any(); } - boost::any ToExprtkStringVisitor::visit(BooleanLiteralExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { stream << expression.getValue(); return boost::any(); } - boost::any ToExprtkStringVisitor::visit(IntegerLiteralExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { stream << expression.getValue(); return boost::any(); } - boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { stream << expression.getValue(); return boost::any(); } diff --git a/src/storage/expressions/ToExprtkStringVisitor.h b/src/storage/expressions/ToExprtkStringVisitor.h index d68da589d..efab0a176 100644 --- a/src/storage/expressions/ToExprtkStringVisitor.h +++ b/src/storage/expressions/ToExprtkStringVisitor.h @@ -16,16 +16,16 @@ namespace storm { std::string toString(Expression const& expression); std::string toString(BaseExpression const* expression); - virtual boost::any visit(IfThenElseExpression const& expression) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BinaryRelationExpression const& expression) override; - virtual boost::any visit(VariableExpression const& expression) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BooleanLiteralExpression const& expression) override; - virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(RationalLiteralExpression const& expression) override; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; private: std::stringstream stream; diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp index a219066e4..91a3cdc94 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -17,23 +17,23 @@ namespace storm { template RationalFunctionType ToRationalFunctionVisitor::toRationalFunction(Expression const& expression) { - return boost::any_cast(expression.accept(*this)); + return boost::any_cast(expression.accept(*this, boost::none)); } template - boost::any ToRationalFunctionVisitor::visit(IfThenElseExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(BinaryBooleanFunctionExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - RationalFunctionType firstOperandAsRationalFunction = boost::any_cast(expression.getFirstOperand()->accept(*this)); - RationalFunctionType secondOperandAsRationalFunction = boost::any_cast(expression.getSecondOperand()->accept(*this)); + boost::any ToRationalFunctionVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + RationalFunctionType firstOperandAsRationalFunction = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + RationalFunctionType secondOperandAsRationalFunction = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); uint_fast64_t exponentAsInteger = 0; switch(expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: @@ -62,12 +62,12 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(BinaryRelationExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(VariableExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(VariableExpression const& expression, boost::any const& data) { auto variablePair = variableToVariableMap.find(expression.getVariable()); if (variablePair != variableToVariableMap.end()) { return convertVariableToPolynomial(variablePair->second); @@ -79,27 +79,27 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(UnaryBooleanFunctionExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(BooleanLiteralExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(IntegerLiteralExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { return RationalFunctionType(carl::rationalize(static_cast(expression.getValue()))); } template - boost::any ToRationalFunctionVisitor::visit(RationalLiteralExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { return storm::utility::convertNumber(expression.getValue()); } diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h index 1cda5028f..0a30d7793 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storage/expressions/ToRationalFunctionVisitor.h @@ -18,16 +18,16 @@ namespace storm { RationalFunctionType toRationalFunction(Expression const& expression); - virtual boost::any visit(IfThenElseExpression const& expression) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BinaryRelationExpression const& expression) override; - virtual boost::any visit(VariableExpression const& expression) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BooleanLiteralExpression const& expression) override; - virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(RationalLiteralExpression const& expression) override; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; private: template> = carl::dummy> diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp index 1b7319927..cfe2cbb35 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storage/expressions/ToRationalNumberVisitor.cpp @@ -14,23 +14,23 @@ namespace storm { template RationalNumberType ToRationalNumberVisitor::toRationalNumber(Expression const& expression) { - return boost::any_cast(expression.accept(*this)); + return boost::any_cast(expression.accept(*this, boost::none)); } template - boost::any ToRationalNumberVisitor::visit(IfThenElseExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(BinaryBooleanFunctionExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - RationalNumberType firstOperandAsRationalNumber = boost::any_cast(expression.getFirstOperand()->accept(*this)); - RationalNumberType secondOperandAsRationalNumber = boost::any_cast(expression.getSecondOperand()->accept(*this)); + boost::any ToRationalNumberVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + RationalNumberType firstOperandAsRationalNumber = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); + RationalNumberType secondOperandAsRationalNumber = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); switch(expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: return firstOperandAsRationalNumber + secondOperandAsRationalNumber; @@ -63,32 +63,32 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(BinaryRelationExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(VariableExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(VariableExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot transform expressions containing variables to a rational number."); } template - boost::any ToRationalNumberVisitor::visit(UnaryBooleanFunctionExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(BooleanLiteralExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { #ifdef STORM_HAVE_CARL return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); #else @@ -97,7 +97,7 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { #ifdef STORM_HAVE_CARL return expression.getValue(); #else diff --git a/src/storage/expressions/ToRationalNumberVisitor.h b/src/storage/expressions/ToRationalNumberVisitor.h index 3d53b8a87..da803cf23 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storage/expressions/ToRationalNumberVisitor.h @@ -16,16 +16,16 @@ namespace storm { RationalNumberType toRationalNumber(Expression const& expression); - virtual boost::any visit(IfThenElseExpression const& expression) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BinaryRelationExpression const& expression) override; - virtual boost::any visit(VariableExpression const& expression) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; - virtual boost::any visit(BooleanLiteralExpression const& expression) override; - virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(RationalLiteralExpression const& expression) override; + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; }; } } diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp index 7c45e081d..825d3debc 100644 --- a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp @@ -49,8 +49,8 @@ namespace storm { } } - boost::any UnaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any UnaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } void UnaryBooleanFunctionExpression::printToStream(std::ostream& stream) const { diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storage/expressions/UnaryBooleanFunctionExpression.h index d13761c26..1f1974fa1 100644 --- a/src/storage/expressions/UnaryBooleanFunctionExpression.h +++ b/src/storage/expressions/UnaryBooleanFunctionExpression.h @@ -36,7 +36,7 @@ namespace storm { virtual storm::expressions::OperatorType getOperator() const override; virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the operator associated with this expression. diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp index f5178fb6f..988b17a12 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -98,8 +98,8 @@ namespace storm { } } - boost::any UnaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any UnaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } void UnaryNumericalFunctionExpression::printToStream(std::ostream& stream) const { diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storage/expressions/UnaryNumericalFunctionExpression.h index f9e2ab148..38d29d142 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.h +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.h @@ -37,7 +37,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::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the operator associated with this expression. diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp index 8ac6cb8b2..a3fe0ae38 100644 --- a/src/storage/expressions/VariableExpression.cpp +++ b/src/storage/expressions/VariableExpression.cpp @@ -63,8 +63,8 @@ namespace storm { return this->shared_from_this(); } - boost::any VariableExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); + boost::any VariableExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } void VariableExpression::printToStream(std::ostream& stream) const { diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h index cfc65fd31..f1f5bca16 100644 --- a/src/storage/expressions/VariableExpression.h +++ b/src/storage/expressions/VariableExpression.h @@ -35,7 +35,7 @@ namespace storm { virtual bool isVariable() const override; virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; /*! * Retrieves the name of the variable associated with this expression. diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp index 469446729..7c97d367c 100644 --- a/src/storage/jani/Assignment.cpp +++ b/src/storage/jani/Assignment.cpp @@ -7,6 +7,10 @@ namespace storm { // Intentionally left empty. } + bool Assignment::operator==(Assignment const& other) const { + return this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()); + } + storm::jani::Variable const& Assignment::getVariable() const { return variable.get(); } diff --git a/src/storage/jani/Assignment.h b/src/storage/jani/Assignment.h index e4b562863..dbdfb7edd 100644 --- a/src/storage/jani/Assignment.h +++ b/src/storage/jani/Assignment.h @@ -15,6 +15,8 @@ namespace storm { */ Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression); + bool operator==(Assignment const& other) const; + /*! * Retrieves the expression variable that is written in this assignment. */ diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp index 347140b1b..40f64e537 100644 --- a/src/storage/jani/Edge.cpp +++ b/src/storage/jani/Edge.cpp @@ -59,6 +59,14 @@ namespace storm { } } + void Edge::addTransientAssignment(Assignment const& assignment) { + transientAssignments.push_back(assignment); + } + + void Edge::liftTransientDestinationAssignments() { + + } + boost::container::flat_set const& Edge::getWrittenGlobalVariables() const { return writtenGlobalVariables; } diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h index cb872ebbe..f56685984 100644 --- a/src/storage/jani/Edge.h +++ b/src/storage/jani/Edge.h @@ -76,6 +76,19 @@ namespace storm { */ boost::container::flat_set const& getWrittenGlobalVariables() const; + /*! + * Adds a transient assignment to this edge. + * + * @param assignment The transient assignment to add. + */ + void addTransientAssignment(Assignment const& assignment); + + /*! + * Finds the transient assignments common to all destinations and lifts them to the edge. Afterwards, these + * assignments are no longer contained in the destination. + */ + void liftTransientDestinationAssignments(); + private: /// The index of the source location. uint64_t sourceLocationIndex; @@ -93,6 +106,9 @@ namespace storm { /// The destinations of this edge. std::vector destinations; + /// The transient assignments made when taking this edge. + std::vector transientAssignments; + /// A set of global variables that is written by at least one of the edge's destinations. This set is /// initialized by the call to finalize. boost::container::flat_set writtenGlobalVariables;