From f6963f5bd170b5ab3defb987dea6bb15420612b2 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 5 May 2017 15:59:26 +0200
Subject: [PATCH] Fixed translation of z3 expressions using the distinct
operator (n-ary !=) to storm expressions
---
src/storm/adapters/Z3ExpressionAdapter.cpp | 20 +++++++++++++++++++-
1 file changed, 19 insertions(+), 1 deletion(-)
diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp
index c4fbff3cd..d715f4599 100644
--- a/src/storm/adapters/Z3ExpressionAdapter.cpp
+++ b/src/storm/adapters/Z3ExpressionAdapter.cpp
@@ -54,6 +54,24 @@ namespace storm {
return manager.boolean(false);
case Z3_OP_EQ:
return this->translateExpression(expr.arg(0)) == this->translateExpression(expr.arg(1));
+ case Z3_OP_DISTINCT: {
+ unsigned args = expr.num_args();
+ STORM_LOG_THROW(args != 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. DISTINCT (mutual != ) operator with 0-arity is assumed to be an error.");
+ if (args == 1) {
+ return manager.boolean(true);
+ } else {
+ storm::expressions::Expression retVal = this->translateExpression(expr.arg(0)) != this->translateExpression(expr.arg(1));
+ for (unsigned arg2 = 2; arg2 < args; ++arg2) {
+ retVal = retVal && (this->translateExpression(expr.arg(0)) != this->translateExpression(expr.arg(arg2)));
+ }
+ for (unsigned arg1 = 1; arg1 < args; ++arg1) {
+ for (unsigned arg2 = arg1 + 1; arg2 < args; ++arg2) {
+ retVal = retVal && (this->translateExpression(expr.arg(arg1)) != this->translateExpression(expr.arg(arg2)));
+ }
+ }
+ return retVal;
+ }
+ }
case Z3_OP_ITE:
return storm::expressions::ite(this->translateExpression(expr.arg(0)), this->translateExpression(expr.arg(1)), this->translateExpression(expr.arg(2)));
case Z3_OP_AND: {
@@ -133,7 +151,7 @@ namespace storm {
STORM_LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non-constant uninterpreted function.");
return manager.getVariable(expr.decl().name().str()).getExpression();
default:
- STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unhandled Z3_decl_kind " << expr.decl().kind() <<".");
+ STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unhandled Z3_decl_kind " << expr.decl().decl_kind() <<".");
break;
}
} else {