From a6aa909a12612e49f3adcd8d0f69869f7aab9990 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 27 May 2016 00:25:12 +0200 Subject: [PATCH] convenience functions for operatiosn on expressions Former-commit-id: 65db15d5d05b3934598a3c313766a691e938ef35 --- src/storage/expressions/Expression.cpp | 26 ++++++++++++++++++++++++-- src/storage/expressions/Expression.h | 8 ++++++++ 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 755d3e5dc..d3121032c 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -236,7 +236,7 @@ namespace storm { return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor))); } } - + Expression operator>(Expression const& first, Expression const& second) { assertSameManager(first.getBaseExpression(), second.getBaseExpression()); return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::Greater))); @@ -282,6 +282,11 @@ namespace storm { assertSameManager(first.getBaseExpression(), second.getBaseExpression()); return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Iff))); } + + Expression xclusiveor(Expression const& first, Expression const& second) { + assertSameManager(first.getBaseExpression(), second.getBaseExpression()); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor))); + } Expression floor(Expression const& first) { STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand."); @@ -292,7 +297,24 @@ namespace storm { STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'ceil' requires numerical operand."); return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil))); } - + + Expression abs(Expression const& first) { + STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Abs is only defined for numerical operands"); + return ite(first < first.getManager().integer(0), -first, first); + } + + Expression sign(Expression const& first) { + STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Sign is only defined for numerical operands"); + // TODO implement (via Ite?) + STORM_LOG_ERROR("Not yet implemented"); + } + + Expression truncate(Expression const& first) { + STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Truncate is only defined for numerical operands"); + // TODO implement (via Ite?) + STORM_LOG_ERROR("Not yet implemented"); + } + Expression disjunction(std::vector const& expressions) { return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; }); } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 42ddd003e..11cfb2350 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -40,6 +40,10 @@ namespace storm { friend Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression); friend Expression implies(Expression const& first, Expression const& second); friend Expression iff(Expression const& first, Expression const& second); + friend Expression xclusiveor(Expression const& first, Expression const& second); + friend Expression abs(Expression const& first); + friend Expression truncate(Expression const& first); + friend Expression sign(Expression const& first); friend Expression floor(Expression const& first); friend Expression ceil(Expression const& first); friend Expression minimum(Expression const& first, Expression const& second); @@ -337,6 +341,10 @@ namespace storm { Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression); Expression implies(Expression const& first, Expression const& second); Expression iff(Expression const& first, Expression const& second); + Expression xclusiveor(Expression const& first, Expression const& second); + Expression abs(Expression const& first); + Expression truncate(Expression const& first); + Expression sign(Expression const& first); Expression floor(Expression const& first); Expression ceil(Expression const& first); Expression minimum(Expression const& first, Expression const& second);