From 0e180469343579b4f5caed3d071ac5a1ef8c1eb6 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 10 May 2019 10:48:12 +0200 Subject: [PATCH] Fixed translating ceil(x) to mathsat expressions. --- src/storm/adapters/MathsatExpressionAdapter.h | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index e99c7d0c5..88ed84dcd 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -257,13 +257,11 @@ namespace storm { switch (expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: return msat_make_times(env, msat_make_number(env, "-1"), childResult); - break; case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: return msat_make_floor(env, childResult); - break; case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil: - return msat_make_plus(env, msat_make_floor(env, childResult), msat_make_number(env, "1")); - break; + // Mathsat does not support ceil... but ceil(x) = -floor(-x) wheeii \o/ + return msat_make_times(env, msat_make_number(env, "-1"), msat_make_floor(env, msat_make_times(env, msat_make_number(env, "-1"), childResult))); default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical unary operator: '" << static_cast(expression.getOperatorType()) << "' in expression " << expression << "."); }