Browse Source

convenience functions for operatiosn on expressions

Former-commit-id: 65db15d5d0
tempestpy_adaptions
sjunges 9 years ago
parent
commit
a6aa909a12
  1. 22
      src/storage/expressions/Expression.cpp
  2. 8
      src/storage/expressions/Expression.h

22
src/storage/expressions/Expression.cpp

@ -283,6 +283,11 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Iff))); return Expression(std::shared_ptr<BaseExpression>(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<BaseExpression>(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor)));
}
Expression floor(Expression const& first) { Expression floor(Expression const& first) {
STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand."); STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand.");
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor))); return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor)));
@ -293,6 +298,23 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil))); return Expression(std::shared_ptr<BaseExpression>(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<storm::expressions::Expression> const& expressions) { Expression disjunction(std::vector<storm::expressions::Expression> const& expressions) {
return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; }); return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; });
} }

8
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 ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression);
friend Expression implies(Expression const& first, Expression const& second); friend Expression implies(Expression const& first, Expression const& second);
friend Expression iff(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 floor(Expression const& first);
friend Expression ceil(Expression const& first); friend Expression ceil(Expression const& first);
friend Expression minimum(Expression const& first, Expression const& second); 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 ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression);
Expression implies(Expression const& first, Expression const& second); Expression implies(Expression const& first, Expression const& second);
Expression iff(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 floor(Expression const& first);
Expression ceil(Expression const& first); Expression ceil(Expression const& first);
Expression minimum(Expression const& first, Expression const& second); Expression minimum(Expression const& first, Expression const& second);

Loading…
Cancel
Save