diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 8590e22c3..64881cfd1 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -30,68 +30,33 @@ namespace storm { class Z3ExpressionAdapter : public storm::expressions::ExpressionVisitor { public: /*! - * Creates a Z3ExpressionAdapter over the given Z3 context. + * Creates an expression adapter that can translate expressions to the format of Z3. * - * @remark The adapter internally creates helper variables prefixed with `__z3adapter_`. Avoid having variables with - * this prefix in the variableToExpressionMap, as this might lead to unexpected results. + * @warning The adapter internally creates helper variables prefixed with `__z3adapter_`. As a consequence, + * having variables with this prefix in the variableToExpressionMap might lead to unexpected results and is + * strictly to be avoided. * - * @param context A reference to the Z3 context over which to build the expressions. Be careful to guarantee - * the lifetime of the context as long as the instance of this adapter is used. - * @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions. + * @param context A reference to the Z3 context over which to build the expressions. The lifetime of the + * context needs to be guaranteed as long as the instance of this adapter is used. + * @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions (if already existing). + * @param createVariables If set to true, additional variables will be created for variables that appear in + * expressions and are not yet known to the adapter. */ - Z3ExpressionAdapter(z3::context& context, std::map const& variableToExpressionMap = std::map()) - : context(context) - , stack() - , additionalAssertions() - , additionalVariableCounter(0) - , variableToExpressionMap(variableToExpressionMap) { + Z3ExpressionAdapter(z3::context& context, std::map const& variableToExpressionMap = std::map(), bool createVariables = false) : context(context) , stack() , additionalAssertions() , additionalVariableCounter(0), variableToExpressionMap(variableToExpressionMap), createVariables(createVariables) { // Intentionally left empty. } /*! * Translates the given expression to an equivalent expression for Z3. * - * @remark The adapter internally creates helper variables prefixed with `__z3adapter_`. Avoid having variables with - * this prefix in the expression, as this might lead to unexpected results. + * @warning The adapter internally creates helper variables prefixed with `__z3adapter_`. As a consequence, + * having variables with this prefix in the variableToExpressionMap might lead to unexpected results and is + * strictly to be avoided. * * @param expression The expression to translate. - * @param createZ3Variables If set to true a solver variable is created for each variable in expression that is not - * yet known to the adapter. (i.e. values from the variableToExpressionMap passed to the constructor - * are not overwritten) * @return An equivalent expression for Z3. */ - z3::expr translateExpression(storm::expressions::Expression const& expression, bool createZ3Variables = false) { - if (createZ3Variables) { - std::map variables; - - try { - variables = expression.getVariablesAndTypes(); - } - catch (storm::exceptions::InvalidTypeException* e) { - STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e); - } - - for (auto variableAndType : variables) { - if (this->variableToExpressionMap.find(variableAndType.first) == this->variableToExpressionMap.end()) { - switch (variableAndType.second) - { - case storm::expressions::ExpressionReturnType::Bool: - this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.bool_const(variableAndType.first.c_str()))); - break; - case storm::expressions::ExpressionReturnType::Int: - this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.int_const(variableAndType.first.c_str()))); - break; - case storm::expressions::ExpressionReturnType::Double: - this->variableToExpressionMap.insert(std::make_pair(variableAndType.first, context.real_const(variableAndType.first.c_str()))); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first); - break; - } - } - } - } - + z3::expr translateExpression(storm::expressions::Expression const& expression) { expression.getBaseExpression().accept(this); z3::expr result = stack.top(); stack.pop(); @@ -105,38 +70,6 @@ namespace storm { } storm::expressions::Expression translateExpression(z3::expr const& expr) { - //std::cout << std::boolalpha << expr.is_var() << std::endl; - //std::cout << std::boolalpha << expr.is_app() << std::endl; - //std::cout << expr.decl().decl_kind() << std::endl; - - /* - if (expr.is_bool() && expr.is_const()) { - switch (Z3_get_bool_value(expr.ctx(), expr)) { - case Z3_L_FALSE: - return storm::expressions::Expression::createFalse(); - case Z3_L_TRUE: - return storm::expressions::Expression::createTrue(); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant boolean, but value is undefined."); - break; - } - } else if (expr.is_int() && expr.is_const()) { - int_fast64_t value; - if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) { - return storm::expressions::Expression::createIntegerLiteral(value); - } else { - STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer."); - } - } else if (expr.is_real() && expr.is_const()) { - int_fast64_t num; - int_fast64_t den; - if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { - return storm::expressions::Expression::createDoubleLiteral(static_cast(num) / static_cast(den)); - } else { - STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator."); - } - } else */ if (expr.is_app()) { switch (expr.decl().decl_kind()) { case Z3_OP_TRUE: @@ -202,7 +135,7 @@ namespace storm { case Z3_OP_IDIV: return this->translateExpression(expr.arg(0)) / this->translateExpression(expr.arg(1)); case Z3_OP_ANUM: - //Arithmetic numeral + // Arithmetic numeral. if (expr.is_int() && expr.is_const()) { long long value; if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) { @@ -220,8 +153,8 @@ namespace storm { } } case Z3_OP_UNINTERPRETED: - //storm only supports uninterpreted constant functions - STORM_LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non constant uninterpreted function."); + // Currently, we only support uninterpreted constant functions. + STORM_LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non-constant uninterpreted function."); if (expr.is_bool()) { return storm::expressions::Expression::createBooleanVariable(expr.decl().name().str()); } else if (expr.is_int()) { @@ -266,8 +199,8 @@ namespace storm { case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: stack.push(z3::expr(context, Z3_mk_iff(context, leftResult, rightResult))); break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."; + default: + STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown boolean binary operator '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."); } } @@ -300,8 +233,7 @@ namespace storm { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max: stack.push(ite(leftResult >= rightResult, leftResult, rightResult)); break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical binary operator: '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."; + default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."); } } @@ -333,8 +265,8 @@ namespace storm { case storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual: stack.push(leftResult >= rightResult); break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << static_cast(expression->getRelationType()) << "' in expression " << expression << "."; + default: + STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown boolean binary operator '" << static_cast(expression->getRelationType()) << "' in expression " << expression << "."); } } @@ -362,8 +294,8 @@ namespace storm { case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: stack.push(!childResult); break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."; + default: + STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown boolean binary operator '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."); } } @@ -381,18 +313,15 @@ namespace storm { z3::expr floorVariable = context.int_const(("__z3adapter_floor_" + std::to_string(additionalVariableCounter++)).c_str()); additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, floorVariable)) <= childResult && childResult < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1)); stack.push(floorVariable); - //throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter."; break; } case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{ z3::expr ceilVariable = context.int_const(("__z3adapter_ceil_" + std::to_string(additionalVariableCounter++)).c_str()); additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= childResult && childResult < z3::expr(context, Z3_mk_int2real(context, ceilVariable))); stack.push(ceilVariable); - //throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter."; break; } - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical unary operator: '" << static_cast(expression->getOperatorType()) << "'."; + default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical unary operator '" << static_cast(expression->getOperatorType()) << "'."); } } @@ -412,16 +341,53 @@ namespace storm { } virtual void visit(storm::expressions::VariableExpression const* expression) override { - stack.push(variableToExpressionMap.at(expression->getVariableName())); + std::map::iterator stringVariablePair = variableToExpressionMap.find(expression->getVariableName()); + z3::expr result(context); + + if (stringVariablePair == variableToExpressionMap.end() && createVariables) { + std::pair::iterator, bool> iteratorAndFlag; + switch (expression->getReturnType()) { + case storm::expressions::ExpressionReturnType::Bool: + iteratorAndFlag = this->variableToExpressionMap.insert(std::make_pair(expression->getVariableName(), context.bool_const(expression->getVariableName().c_str()))); + result = iteratorAndFlag.first->second; + break; + case storm::expressions::ExpressionReturnType::Int: + iteratorAndFlag = this->variableToExpressionMap.insert(std::make_pair(expression->getVariableName(), context.int_const(expression->getVariableName().c_str()))); + result = iteratorAndFlag.first->second; + break; + case storm::expressions::ExpressionReturnType::Double: + iteratorAndFlag = this->variableToExpressionMap.insert(std::make_pair(expression->getVariableName(), context.real_const(expression->getVariableName().c_str()))); + result = iteratorAndFlag.first->second; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable '" << expression->getVariableName() << "' with unknown type while trying to create solver variables."); + } + } else { + STORM_LOG_THROW(stringVariablePair != variableToExpressionMap.end(), storm::exceptions::InvalidArgumentException, "Expression refers to unknown variable '" << expression->getVariableName() << "'."); + result = stringVariablePair->second; + } + + stack.push(result); } private: + // The context that is used to translate the expressions. z3::context& context; + + // A stack that is used to communicate the translation results between method calls. std::stack stack; + + // A stack of assertions that need to be kept separate, because they were only impliclty part of an assertion that was added. std::stack additionalAssertions; + + // A counter for the variables that were created to identify the additional assertions. uint_fast64_t additionalVariableCounter; + // A mapping from variable names to their Z3 equivalent. std::map variableToExpressionMap; + + // A flag that indicates whether new variables are to be created when an unkown variable is encountered. + bool createVariables; }; #endif } // namespace adapters diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index ff7d5a344..1de65eb74 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -50,7 +50,7 @@ namespace storm { config.set("model", true); context = std::unique_ptr(new z3::context(config)); solver = std::unique_ptr(new z3::solver(*context)); - expressionAdapter = std::unique_ptr(new storm::adapters::Z3ExpressionAdapter(*context)); + expressionAdapter = std::unique_ptr(new storm::adapters::Z3ExpressionAdapter(*context, std::map(), true)); } Z3SmtSolver::~Z3SmtSolver() { @@ -96,7 +96,7 @@ namespace storm { void Z3SmtSolver::add(storm::expressions::Expression const& assertion) { #ifdef STORM_HAVE_Z3 - this->solver->add(expressionAdapter->translateExpression(assertion, true)); + this->solver->add(expressionAdapter->translateExpression(assertion)); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp index 68aee3adb..f63245a92 100644 --- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -11,7 +11,8 @@ TEST(Z3ExpressionAdapter, StormToZ3Basic) { z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map()); + storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map(), true); + storm::adapters::Z3ExpressionAdapter adapter2(ctx, std::map(), false); storm::expressions::Expression exprTrue = storm::expressions::Expression::createTrue(); z3::expr z3True = ctx.bool_val(true); @@ -29,16 +30,17 @@ TEST(Z3ExpressionAdapter, StormToZ3Basic) { storm::expressions::Expression exprConjunction = (storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")); z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y")); - ASSERT_THROW( adapter.translateExpression(exprConjunction, false), std::out_of_range ); //variables not yet created in adapter - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprConjunction, true), z3Conjunction))); + // Variables not yet created in adapter. + ASSERT_THROW( adapter2.translateExpression(exprConjunction), storm::exceptions::InvalidArgumentException ); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprConjunction), z3Conjunction))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); storm::expressions::Expression exprNor = !(storm::expressions::Expression::createBooleanVariable("x") || storm::expressions::Expression::createBooleanVariable("y")); z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y")); - ASSERT_NO_THROW(adapter.translateExpression(exprNor, false)); //variables already created in adapter - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprNor, true), z3Nor))); + ASSERT_NO_THROW(adapter.translateExpression(exprNor)); // Variables already created in adapter. + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprNor), z3Nor))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); @@ -49,18 +51,18 @@ TEST(Z3ExpressionAdapter, StormToZ3Integer) { z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map()); + storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map(), true); storm::expressions::Expression exprAdd = (storm::expressions::Expression::createIntegerVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createIntegerVariable("y")); z3::expr z3Add = (ctx.int_const("x") + ctx.int_const("y") < -ctx.int_const("y")); - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd, true), z3Add))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd), z3Add))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); storm::expressions::Expression exprMult = !(storm::expressions::Expression::createIntegerVariable("x") * storm::expressions::Expression::createIntegerVariable("y") == storm::expressions::Expression::createIntegerVariable("y")); z3::expr z3Mult = !(ctx.int_const("x") * ctx.int_const("y") == ctx.int_const("y")); - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult, true), z3Mult))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult), z3Mult))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); @@ -71,76 +73,64 @@ TEST(Z3ExpressionAdapter, StormToZ3Real) { z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map()); + storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map(), true); storm::expressions::Expression exprAdd = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") < -storm::expressions::Expression::createDoubleVariable("y")); z3::expr z3Add = (ctx.real_const("x") + ctx.real_const("y") < -ctx.real_const("y")); - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd, true), z3Add))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd), z3Add))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); storm::expressions::Expression exprMult = !(storm::expressions::Expression::createDoubleVariable("x") * storm::expressions::Expression::createDoubleVariable("y") == storm::expressions::Expression::createDoubleVariable("y")); z3::expr z3Mult = !(ctx.real_const("x") * ctx.real_const("y") == ctx.real_const("y")); - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult, true), z3Mult))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult), z3Mult))); s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); } -TEST(Z3ExpressionAdapter, StormToZ3TypeErrors) { - z3::context ctx; - z3::solver s(ctx); - z3::expr conjecture = ctx.bool_val(false); - - storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map()); - - storm::expressions::Expression exprFail1 = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createDoubleVariable("y")); - ASSERT_THROW(conjecture = adapter.translateExpression(exprFail1, true), storm::exceptions::InvalidTypeException); -} - TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) { z3::context ctx; z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); - storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map()); + storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map(), true); storm::expressions::Expression exprFloor = ((storm::expressions::Expression::createDoubleVariable("d").floor()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); z3::expr z3Floor = ctx.int_val(4) == ctx.int_const("i"); - //try { adapter.translateExpression(exprFloor, true); } - //catch (std::exception &e) { std::cout << e.what() << std::endl; } - - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFloor, true), z3Floor))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFloor), z3Floor))); s.add(conjecture); - ASSERT_TRUE(s.check() == z3::sat); //it is NOT logical equivalent + + // It is not logically equivalent, so this should be satisfiable. + ASSERT_TRUE(s.check() == z3::sat); s.reset(); - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprFloor, true), z3Floor))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprFloor), z3Floor))); s.add(conjecture); - ASSERT_TRUE(s.check() == z3::unsat); //it is NOT logical equivalent + + // However, the left part implies the right one, which is why this should be unsatisfiable. + ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - storm::expressions::Expression exprCeil = ((storm::expressions::Expression::createDoubleVariable("d").ceil()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); z3::expr z3Ceil = ctx.int_val(5) == ctx.int_const("i"); - //try { adapter.translateExpression(exprFloor, true); } - //catch (std::exception &e) { std::cout << e.what() << std::endl; } - - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprCeil, true), z3Ceil))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprCeil), z3Ceil))); s.add(conjecture); - ASSERT_TRUE(s.check() == z3::sat); //it is NOT logical equivalent + // It is not logically equivalent, so this should be satisfiable. + ASSERT_TRUE(s.check() == z3::sat); s.reset(); - ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprCeil, true), z3Ceil))); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprCeil), z3Ceil))); s.add(conjecture); - ASSERT_TRUE(s.check() == z3::unsat); //it is NOT logical equivalent + + // However, the left part implies the right one, which is why this should be unsatisfiable. + ASSERT_TRUE(s.check() == z3::unsat); s.reset(); } TEST(Z3ExpressionAdapter, Z3ToStormBasic) { z3::context ctx; - unsigned args = 2; storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map());