Browse Source

added visitor that checks for syntatical equality of expressions

Former-commit-id: b6753a4891 [formerly 2b36b42bfa]
Former-commit-id: f693de5f30
main
dehnert 9 years ago
parent
commit
3d426798b3
  1. 54
      src/adapters/AddExpressionAdapter.cpp
  2. 20
      src/adapters/AddExpressionAdapter.h
  3. 44
      src/adapters/MathsatExpressionAdapter.h
  4. 44
      src/adapters/Z3ExpressionAdapter.cpp
  5. 20
      src/adapters/Z3ExpressionAdapter.h
  6. 82
      src/storage/expressions/BaseExpression.cpp
  7. 46
      src/storage/expressions/BaseExpression.h
  8. 4
      src/storage/expressions/BinaryBooleanFunctionExpression.cpp
  9. 2
      src/storage/expressions/BinaryBooleanFunctionExpression.h
  10. 4
      src/storage/expressions/BinaryNumericalFunctionExpression.cpp
  11. 2
      src/storage/expressions/BinaryNumericalFunctionExpression.h
  12. 4
      src/storage/expressions/BinaryRelationExpression.cpp
  13. 2
      src/storage/expressions/BinaryRelationExpression.h
  14. 4
      src/storage/expressions/BooleanLiteralExpression.cpp
  15. 2
      src/storage/expressions/BooleanLiteralExpression.h
  16. 13
      src/storage/expressions/Expression.cpp
  17. 9
      src/storage/expressions/Expression.h
  18. 20
      src/storage/expressions/ExpressionVisitor.h
  19. 4
      src/storage/expressions/IfThenElseExpression.cpp
  20. 2
      src/storage/expressions/IfThenElseExpression.h
  21. 4
      src/storage/expressions/IntegerLiteralExpression.cpp
  22. 2
      src/storage/expressions/IntegerLiteralExpression.h
  23. 28
      src/storage/expressions/LinearCoefficientVisitor.cpp
  24. 20
      src/storage/expressions/LinearCoefficientVisitor.h
  25. 28
      src/storage/expressions/LinearityCheckVisitor.cpp
  26. 20
      src/storage/expressions/LinearityCheckVisitor.h
  27. 4
      src/storage/expressions/RationalLiteralExpression.cpp
  28. 2
      src/storage/expressions/RationalLiteralExpression.h
  29. 44
      src/storage/expressions/SubstitutionVisitor.cpp
  30. 20
      src/storage/expressions/SubstitutionVisitor.h
  31. 155
      src/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
  32. 27
      src/storage/expressions/SyntacticalEqualityCheckVisitor.h
  33. 108
      src/storage/expressions/ToExprtkStringVisitor.cpp
  34. 20
      src/storage/expressions/ToExprtkStringVisitor.h
  35. 26
      src/storage/expressions/ToRationalFunctionVisitor.cpp
  36. 20
      src/storage/expressions/ToRationalFunctionVisitor.h
  37. 26
      src/storage/expressions/ToRationalNumberVisitor.cpp
  38. 20
      src/storage/expressions/ToRationalNumberVisitor.h
  39. 4
      src/storage/expressions/UnaryBooleanFunctionExpression.cpp
  40. 2
      src/storage/expressions/UnaryBooleanFunctionExpression.h
  41. 4
      src/storage/expressions/UnaryNumericalFunctionExpression.cpp
  42. 2
      src/storage/expressions/UnaryNumericalFunctionExpression.h
  43. 4
      src/storage/expressions/VariableExpression.cpp
  44. 2
      src/storage/expressions/VariableExpression.h
  45. 4
      src/storage/jani/Assignment.cpp
  46. 2
      src/storage/jani/Assignment.h
  47. 8
      src/storage/jani/Edge.cpp
  48. 16
      src/storage/jani/Edge.h

54
src/adapters/AddExpressionAdapter.cpp

@ -19,37 +19,37 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> AddExpressionAdapter<Type, ValueType>::translateExpression(storm::expressions::Expression const& expression) {
if (expression.hasBooleanType()) {
return boost::any_cast<storm::dd::Bdd<Type>>(expression.accept(*this)).template toAdd<ValueType>();
return boost::any_cast<storm::dd::Bdd<Type>>(expression.accept(*this, boost::none)).template toAdd<ValueType>();
} else {
return boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.accept(*this));
return boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.accept(*this, boost::none));
}
}
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> AddExpressionAdapter<Type, ValueType>::translateBooleanExpression(storm::expressions::Expression const& expression) {
STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected expression of boolean type.");
return boost::any_cast<storm::dd::Bdd<Type>>(expression.accept(*this));
return boost::any_cast<storm::dd::Bdd<Type>>(expression.accept(*this, boost::none));
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IfThenElseExpression const& expression) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) {
if (expression.hasBooleanType()) {
storm::dd::Bdd<Type> elseDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getElseExpression()->accept(*this));
storm::dd::Bdd<Type> thenDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getThenExpression()->accept(*this));
storm::dd::Bdd<Type> conditionDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getCondition()->accept(*this));
storm::dd::Bdd<Type> elseDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getElseExpression()->accept(*this, data));
storm::dd::Bdd<Type> thenDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getThenExpression()->accept(*this, data));
storm::dd::Bdd<Type> conditionDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getCondition()->accept(*this, data));
return conditionDd.ite(thenDd, elseDd);
} else {
storm::dd::Add<Type, ValueType> elseDd = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getElseExpression()->accept(*this));
storm::dd::Add<Type, ValueType> thenDd = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getThenExpression()->accept(*this));
storm::dd::Bdd<Type> conditionDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getCondition()->accept(*this));
storm::dd::Add<Type, ValueType> elseDd = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getElseExpression()->accept(*this, data));
storm::dd::Add<Type, ValueType> thenDd = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getThenExpression()->accept(*this, data));
storm::dd::Bdd<Type> conditionDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getCondition()->accept(*this, data));
return conditionDd.ite(thenDd, elseDd);
}
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) {
storm::dd::Bdd<Type> leftResult = boost::any_cast<storm::dd::Bdd<Type>>(expression.getFirstOperand()->accept(*this));
storm::dd::Bdd<Type> rightResult = boost::any_cast<storm::dd::Bdd<Type>>(expression.getSecondOperand()->accept(*this));
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
storm::dd::Bdd<Type> leftResult = boost::any_cast<storm::dd::Bdd<Type>>(expression.getFirstOperand()->accept(*this, data));
storm::dd::Bdd<Type> rightResult = boost::any_cast<storm::dd::Bdd<Type>>(expression.getSecondOperand()->accept(*this, data));
storm::dd::Bdd<Type> result;
switch (expression.getOperatorType()) {
@ -74,9 +74,9 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) {
storm::dd::Add<Type, ValueType> leftResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getFirstOperand()->accept(*this));
storm::dd::Add<Type, ValueType> rightResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getSecondOperand()->accept(*this));
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
storm::dd::Add<Type, ValueType> leftResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getFirstOperand()->accept(*this, data));
storm::dd::Add<Type, ValueType> rightResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getSecondOperand()->accept(*this, data));
storm::dd::Add<Type, ValueType> result;
switch (expression.getOperatorType()) {
@ -109,9 +109,9 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryRelationExpression const& expression) {
storm::dd::Add<Type, ValueType> leftResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getFirstOperand()->accept(*this));
storm::dd::Add<Type, ValueType> rightResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getSecondOperand()->accept(*this));
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
storm::dd::Add<Type, ValueType> leftResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getFirstOperand()->accept(*this, data));
storm::dd::Add<Type, ValueType> rightResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getSecondOperand()->accept(*this, data));
storm::dd::Bdd<Type> result;
switch (expression.getRelationType()) {
@ -139,7 +139,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::VariableExpression const& expression) {
boost::any AddExpressionAdapter<Type, ValueType>::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<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) {
storm::dd::Bdd<Type> result = boost::any_cast<storm::dd::Bdd<Type>>(expression.getOperand()->accept(*this));
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
storm::dd::Bdd<Type> result = boost::any_cast<storm::dd::Bdd<Type>>(expression.getOperand()->accept(*this, data));
switch (expression.getOperatorType()) {
case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not:
@ -163,8 +163,8 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) {
storm::dd::Add<Type, ValueType> result = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getOperand()->accept(*this));
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
storm::dd::Add<Type, ValueType> result = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getOperand()->accept(*this, data));
switch (expression.getOperatorType()) {
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus:
@ -184,17 +184,17 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BooleanLiteralExpression const& expression) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) {
return expression.getValue() ? ddManager->getBddOne() : ddManager->getBddZero();
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IntegerLiteralExpression const& expression) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) {
return ddManager->getConstant(static_cast<ValueType>(expression.getValue()));
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::RationalLiteralExpression const& expression) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) {
return ddManager->getConstant(static_cast<ValueType>(expression.getValueAsDouble()));
}

20
src/adapters/AddExpressionAdapter.h

@ -22,16 +22,16 @@ namespace storm {
storm::dd::Add<Type, ValueType> translateExpression(storm::expressions::Expression const& expression);
storm::dd::Bdd<Type> 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.

44
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<msat_term>(expression.getBaseExpression().accept(*this));
msat_term result = boost::any_cast<msat_term>(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<msat_term>(expression.getFirstOperand()->accept(*this));
msat_term rightResult = boost::any_cast<msat_term>(expression.getSecondOperand()->accept(*this));
virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override {
msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));
msat_term rightResult = boost::any_cast<msat_term>(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<msat_term>(expression.getFirstOperand()->accept(*this));
msat_term rightResult = boost::any_cast<msat_term>(expression.getSecondOperand()->accept(*this));
virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override {
msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));
msat_term rightResult = boost::any_cast<msat_term>(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<msat_term>(expression.getFirstOperand()->accept(*this));
msat_term rightResult = boost::any_cast<msat_term>(expression.getSecondOperand()->accept(*this));
virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) override {
msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));
msat_term rightResult = boost::any_cast<msat_term>(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<msat_term>(expression.getCondition()->accept(*this));
msat_term thenResult = boost::any_cast<msat_term>(expression.getThenExpression()->accept(*this));
msat_term elseResult = boost::any_cast<msat_term>(expression.getElseExpression()->accept(*this));
virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override {
msat_term conditionResult = boost::any_cast<msat_term>(expression.getCondition()->accept(*this, data));
msat_term thenResult = boost::any_cast<msat_term>(expression.getThenExpression()->accept(*this, data));
msat_term elseResult = boost::any_cast<msat_term>(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<int>(expression.getValue())).c_str());
}
virtual boost::any visit(expressions::UnaryBooleanFunctionExpression const& expression) override {
msat_term childResult = boost::any_cast<msat_term>(expression.getOperand()->accept(*this));
virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) override {
msat_term childResult = boost::any_cast<msat_term>(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<msat_term>(expression.getOperand()->accept(*this));
virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) override {
msat_term childResult = boost::any_cast<msat_term>(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());
}

44
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<z3::expr>(expression.getBaseExpression().accept(*this));
z3::expr result = boost::any_cast<z3::expr>(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<z3::expr>(expression.getFirstOperand()->accept(*this));
z3::expr rightResult = boost::any_cast<z3::expr>(expression.getSecondOperand()->accept(*this));
boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
z3::expr leftResult = boost::any_cast<z3::expr>(expression.getFirstOperand()->accept(*this, data));
z3::expr rightResult = boost::any_cast<z3::expr>(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<z3::expr>(expression.getFirstOperand()->accept(*this));
z3::expr rightResult = boost::any_cast<z3::expr>(expression.getSecondOperand()->accept(*this));
boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
z3::expr leftResult = boost::any_cast<z3::expr>(expression.getFirstOperand()->accept(*this, data));
z3::expr rightResult = boost::any_cast<z3::expr>(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<z3::expr>(expression.getFirstOperand()->accept(*this));
z3::expr rightResult = boost::any_cast<z3::expr>(expression.getSecondOperand()->accept(*this));
boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
z3::expr leftResult = boost::any_cast<z3::expr>(expression.getFirstOperand()->accept(*this, data));
z3::expr rightResult = boost::any_cast<z3::expr>(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<int>(expression.getValue()));
}
boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) {
z3::expr childResult = boost::any_cast<z3::expr>(expression.getOperand()->accept(*this));
boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
z3::expr childResult = boost::any_cast<z3::expr>(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<z3::expr>(expression.getOperand()->accept(*this));
boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
z3::expr childResult = boost::any_cast<z3::expr>(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<z3::expr>(expression.getCondition()->accept(*this));
z3::expr thenResult = boost::any_cast<z3::expr>(expression.getThenExpression()->accept(*this));
z3::expr elseResult = boost::any_cast<z3::expr>(expression.getElseExpression()->accept(*this));
boost::any Z3ExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) {
z3::expr conditionResult = boost::any_cast<z3::expr>(expression.getCondition()->accept(*this, data));
z3::expr thenResult = boost::any_cast<z3::expr>(expression.getThenExpression()->accept(*this, data));
z3::expr elseResult = boost::any_cast<z3::expr>(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());
}

20
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:
/*!

82
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<IfThenElseExpression const&>(*this);
}
bool BaseExpression::isBinaryBooleanFunctionExpression() const {
return false;
}
BinaryBooleanFunctionExpression const& BaseExpression::asBinaryBooleanFunctionExpression() const {
return static_cast<BinaryBooleanFunctionExpression const&>(*this);
}
bool BaseExpression::isBinaryNumericalFunctionExpression() const {
return false;
}
BinaryNumericalFunctionExpression const& BaseExpression::asBinaryNumericalFunctionExpression() const {
return static_cast<BinaryNumericalFunctionExpression const&>(*this);
}
bool BaseExpression::isBinaryRelationExpression() const {
return false;
}
BinaryRelationExpression const& BaseExpression::asBinaryRelationExpression() const {
return static_cast<BinaryRelationExpression const&>(*this);
}
bool BaseExpression::isBooleanLiteralExpression() const {
return false;
}
BooleanLiteralExpression const& BaseExpression::asBooleanLiteralExpression() const {
return static_cast<BooleanLiteralExpression const&>(*this);
}
bool BaseExpression::isIntegerLiteralExpression() const {
return false;
}
IntegerLiteralExpression const& BaseExpression::asIntegerLiteralExpression() const {
return static_cast<IntegerLiteralExpression const&>(*this);
}
bool BaseExpression::isRationalLiteralExpression() const {
return false;
}
RationalLiteralExpression const& BaseExpression::asRationalLiteralExpression() const {
return static_cast<RationalLiteralExpression const&>(*this);
}
bool BaseExpression::isUnaryBooleanFunctionExpression() const {
return false;
}
UnaryBooleanFunctionExpression const& BaseExpression::asUnaryBooleanFunctionExpression() const {
return static_cast<UnaryBooleanFunctionExpression const&>(*this);
}
bool BaseExpression::isUnaryNumericalFunctionExpression() const {
return false;
}
UnaryNumericalFunctionExpression const& BaseExpression::asUnaryNumericalFunctionExpression() const {
return static_cast<UnaryNumericalFunctionExpression const&>(*this);
}
bool BaseExpression::isVariableExpression() const {
return false;
}
VariableExpression const& BaseExpression::asVariableExpression() const {
return static_cast<VariableExpression const&>(*this);
}
std::ostream& operator<<(std::ostream& stream, BaseExpression const& expression) {
expression.printToStream(stream);
return stream;

46
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.

4
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 {

2
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<BaseExpression const> 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.

4
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 {

2
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<BaseExpression const> 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.

4
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 {

2
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<BaseExpression const> 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.

4
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 {

2
src/storage/expressions/BooleanLiteralExpression.h

@ -32,7 +32,7 @@ namespace storm {
virtual bool isFalse() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> 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.

13
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;

9
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:

20
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;
};
}
}

4
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<BaseExpression const> IfThenElseExpression::getCondition() const {

2
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<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> 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.

4
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 {

2
src/storage/expressions/IntegerLiteralExpression.h

@ -31,7 +31,7 @@ namespace storm {
virtual bool isLiteral() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> 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.

28
src/storage/expressions/LinearCoefficientVisitor.cpp

@ -85,20 +85,20 @@ namespace storm {
}
LinearCoefficientVisitor::VariableCoefficients LinearCoefficientVisitor::getLinearCoefficients(Expression const& expression) {
return boost::any_cast<VariableCoefficients>(expression.getBaseExpression().accept(*this));
return boost::any_cast<VariableCoefficients>(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<VariableCoefficients>(expression.getFirstOperand()->accept(*this));
VariableCoefficients rightResult = boost::any_cast<VariableCoefficients>(expression.getSecondOperand()->accept(*this));
boost::any LinearCoefficientVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
VariableCoefficients leftResult = boost::any_cast<VariableCoefficients>(expression.getFirstOperand()->accept(*this, data));
VariableCoefficients rightResult = boost::any_cast<VariableCoefficients>(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<VariableCoefficients>(expression.getOperand()->accept(*this));
boost::any LinearCoefficientVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
VariableCoefficients childResult = boost::any_cast<VariableCoefficients>(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<double>(expression.getValue()));
}
boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression) {
boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) {
return VariableCoefficients(expression.getValueAsDouble());
}
}

20
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;
};
}
}

28
src/storage/expressions/LinearityCheckVisitor.cpp

@ -12,27 +12,27 @@ namespace storm {
}
bool LinearityCheckVisitor::check(Expression const& expression) {
LinearityStatus result = boost::any_cast<LinearityStatus>(expression.getBaseExpression().accept(*this));
LinearityStatus result = boost::any_cast<LinearityStatus>(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<LinearityStatus>(expression.getFirstOperand()->accept(*this));
boost::any LinearityCheckVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
LinearityStatus leftResult = boost::any_cast<LinearityStatus>(expression.getFirstOperand()->accept(*this, data));
if (leftResult == LinearityStatus::NonLinear) {
return LinearityStatus::NonLinear;
}
LinearityStatus rightResult = boost::any_cast<LinearityStatus>(expression.getSecondOperand()->accept(*this));
LinearityStatus rightResult = boost::any_cast<LinearityStatus>(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;
}
}

20
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 };

4
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 {

2
src/storage/expressions/RationalLiteralExpression.h

@ -48,7 +48,7 @@ namespace storm {
virtual bool isLiteral() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> 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.

44
src/storage/expressions/SubstitutionVisitor.cpp

@ -14,14 +14,14 @@ namespace storm {
template<typename MapType>
Expression SubstitutionVisitor<MapType>::substitute(Expression const& expression) {
return Expression(boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getBaseExpression().accept(*this)));
return Expression(boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getBaseExpression().accept(*this, boost::none)));
}
template<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(IfThenElseExpression const& expression) {
std::shared_ptr<BaseExpression const> conditionExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getCondition()->accept(*this));
std::shared_ptr<BaseExpression const> thenExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getThenExpression()->accept(*this));
std::shared_ptr<BaseExpression const> elseExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getElseExpression()->accept(*this));
boost::any SubstitutionVisitor<MapType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
std::shared_ptr<BaseExpression const> conditionExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getCondition()->accept(*this, data));
std::shared_ptr<BaseExpression const> thenExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getThenExpression()->accept(*this, data));
std::shared_ptr<BaseExpression const> elseExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(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<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const& expression) {
std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this));
std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSecondOperand()->accept(*this));
boost::any SubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this, data));
std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(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<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const& expression) {
std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this));
std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSecondOperand()->accept(*this));
boost::any SubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this, data));
std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(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<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(BinaryRelationExpression const& expression) {
std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this));
std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSecondOperand()->accept(*this));
boost::any SubstitutionVisitor<MapType>::visit(BinaryRelationExpression const& expression, boost::any const& data) {
std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getFirstOperand()->accept(*this, data));
std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(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<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(VariableExpression const& expression) {
boost::any SubstitutionVisitor<MapType>::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<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const& expression) {
std::shared_ptr<BaseExpression const> operandExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getOperand()->accept(*this));
boost::any SubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
std::shared_ptr<BaseExpression const> operandExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(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<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const& expression) {
std::shared_ptr<BaseExpression const> operandExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getOperand()->accept(*this));
boost::any SubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
std::shared_ptr<BaseExpression const> operandExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(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<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const& expression) {
boost::any SubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
return expression.getSharedPointer();
}
template<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const& expression) {
boost::any SubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
return expression.getSharedPointer();
}
template<typename MapType>
boost::any SubstitutionVisitor<MapType>::visit(RationalLiteralExpression const& expression) {
boost::any SubstitutionVisitor<MapType>::visit(RationalLiteralExpression const& expression, boost::any const& data) {
return expression.getSharedPointer();
}

20
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.

155
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<bool>(expression1.accept(*this, std::ref(expression2.getBaseExpression())));
}
boost::any SyntacticalEqualityCheckVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
if (otherBaseExpression.isIfThenElseExpression()) {
IfThenElseExpression const& otherExpression = otherBaseExpression.asIfThenElseExpression();
bool result = boost::any_cast<bool>(expression.getCondition()->accept(*this, std::ref(*otherExpression.getCondition())));
if (result) {
result = boost::any_cast<bool>(expression.getThenExpression()->accept(*this, std::ref(*otherExpression.getThenExpression())));
}
if (result) {
result = boost::any_cast<bool>(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<std::reference_wrapper<BaseExpression const>>(data).get();
if (otherBaseExpression.isBinaryBooleanFunctionExpression()) {
BinaryBooleanFunctionExpression const& otherExpression = otherBaseExpression.asBinaryBooleanFunctionExpression();
bool result = expression.getOperatorType() == otherExpression.getOperatorType();
if (result) {
result = boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, std::ref(*otherExpression.getFirstOperand())));
}
if (result) {
result = boost::any_cast<bool>(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<std::reference_wrapper<BaseExpression const>>(data).get();
if (otherBaseExpression.isBinaryNumericalFunctionExpression()) {
BinaryNumericalFunctionExpression const& otherExpression = otherBaseExpression.asBinaryNumericalFunctionExpression();
bool result = expression.getOperatorType() == otherExpression.getOperatorType();
if (result) {
result = boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, std::ref(*otherExpression.getFirstOperand())));
}
if (result) {
result = boost::any_cast<bool>(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<std::reference_wrapper<BaseExpression const>>(data).get();
if (otherBaseExpression.isBinaryRelationExpression()) {
BinaryRelationExpression const& otherExpression = otherBaseExpression.asBinaryRelationExpression();
bool result = expression.getRelationType() == otherExpression.getRelationType();
if (result) {
result = boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, std::ref(*otherExpression.getFirstOperand())));
}
if (result) {
result = boost::any_cast<bool>(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<std::reference_wrapper<BaseExpression const>>(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<std::reference_wrapper<BaseExpression const>>(data).get();
if (otherBaseExpression.isBinaryBooleanFunctionExpression()) {
UnaryBooleanFunctionExpression const& otherExpression = otherBaseExpression.asUnaryBooleanFunctionExpression();
bool result = expression.getOperatorType() == otherExpression.getOperatorType();
if (result) {
result = boost::any_cast<bool>(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<std::reference_wrapper<BaseExpression const>>(data).get();
if (otherBaseExpression.isBinaryBooleanFunctionExpression()) {
UnaryNumericalFunctionExpression const& otherExpression = otherBaseExpression.asUnaryNumericalFunctionExpression();
bool result = expression.getOperatorType() == otherExpression.getOperatorType();
if (result) {
result = boost::any_cast<bool>(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<std::reference_wrapper<BaseExpression const>>(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<std::reference_wrapper<BaseExpression const>>(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<std::reference_wrapper<BaseExpression const>>(data).get();
if (otherBaseExpression.isRationalLiteralExpression()) {
RationalLiteralExpression const& otherExpression = otherBaseExpression.asRationalLiteralExpression();
return expression.getValue() == otherExpression.getValue();
} else {
return false;
}
}
}
}

27
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;
};
}
}

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

20
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;

26
src/storage/expressions/ToRationalFunctionVisitor.cpp

@ -17,23 +17,23 @@ namespace storm {
template<typename RationalFunctionType>
RationalFunctionType ToRationalFunctionVisitor<RationalFunctionType>::toRationalFunction(Expression const& expression) {
return boost::any_cast<RationalFunctionType>(expression.accept(*this));
return boost::any_cast<RationalFunctionType>(expression.accept(*this, boost::none));
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryBooleanFunctionExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryNumericalFunctionExpression const& expression) {
RationalFunctionType firstOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getFirstOperand()->accept(*this));
RationalFunctionType secondOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getSecondOperand()->accept(*this));
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
RationalFunctionType firstOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getFirstOperand()->accept(*this, data));
RationalFunctionType secondOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getSecondOperand()->accept(*this, data));
uint_fast64_t exponentAsInteger = 0;
switch(expression.getOperatorType()) {
case BinaryNumericalFunctionExpression::OperatorType::Plus:
@ -62,12 +62,12 @@ namespace storm {
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryRelationExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryRelationExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(VariableExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::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<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryBooleanFunctionExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryNumericalFunctionExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BooleanLiteralExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IntegerLiteralExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
return RationalFunctionType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue())));
}
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(RationalLiteralExpression const& expression) {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(RationalLiteralExpression const& expression, boost::any const& data) {
return storm::utility::convertNumber<storm::RationalFunction>(expression.getValue());
}

20
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<typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>

26
src/storage/expressions/ToRationalNumberVisitor.cpp

@ -14,23 +14,23 @@ namespace storm {
template<typename RationalNumberType>
RationalNumberType ToRationalNumberVisitor<RationalNumberType>::toRationalNumber(Expression const& expression) {
return boost::any_cast<RationalNumberType>(expression.accept(*this));
return boost::any_cast<RationalNumberType>(expression.accept(*this, boost::none));
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryBooleanFunctionExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryNumericalFunctionExpression const& expression) {
RationalNumberType firstOperandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getFirstOperand()->accept(*this));
RationalNumberType secondOperandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getSecondOperand()->accept(*this));
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
RationalNumberType firstOperandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getFirstOperand()->accept(*this, data));
RationalNumberType secondOperandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getSecondOperand()->accept(*this, data));
switch(expression.getOperatorType()) {
case BinaryNumericalFunctionExpression::OperatorType::Plus:
return firstOperandAsRationalNumber + secondOperandAsRationalNumber;
@ -63,32 +63,32 @@ namespace storm {
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryRelationExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryRelationExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(VariableExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::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<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryBooleanFunctionExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryNumericalFunctionExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BooleanLiteralExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IntegerLiteralExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
#ifdef STORM_HAVE_CARL
return RationalNumberType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue())));
#else
@ -97,7 +97,7 @@ namespace storm {
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(RationalLiteralExpression const& expression) {
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(RationalLiteralExpression const& expression, boost::any const& data) {
#ifdef STORM_HAVE_CARL
return expression.getValue();
#else

20
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;
};
}
}

4
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 {

2
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<BaseExpression const> 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.

4
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 {

2
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<BaseExpression const> 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.

4
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 {

2
src/storage/expressions/VariableExpression.h

@ -35,7 +35,7 @@ namespace storm {
virtual bool isVariable() const override;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual std::shared_ptr<BaseExpression const> 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.

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

2
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.
*/

8
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<storm::expressions::Variable> const& Edge::getWrittenGlobalVariables() const {
return writtenGlobalVariables;
}

16
src/storage/jani/Edge.h

@ -76,6 +76,19 @@ namespace storm {
*/
boost::container::flat_set<storm::expressions::Variable> 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<EdgeDestination> destinations;
/// The transient assignments made when taking this edge.
std::vector<Assignment> 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 <code>finalize</code>.
boost::container::flat_set<storm::expressions::Variable> writtenGlobalVariables;

Loading…
Cancel
Save