From 9a7b4f69ef9f0b5bd092acd5a51b9a6ba74aa197 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Wed, 21 May 2014 16:59:24 +0200 Subject: [PATCH] More tests and some small bugfixes for Z3SmtSolver Former-commit-id: 71def90649e4638ada0596d8a15f7043338ad715 --- src/adapters/Z3ExpressionAdapter.h | 10 +- src/solver/SmtSolver.h | 2 +- src/solver/Z3SmtSolver.cpp | 2 +- src/solver/Z3SmtSolver.h | 2 +- .../adapter/Z3ExpressionAdapterTest.cpp | 116 +++++++++++++++++- test/functional/solver/Z3SmtSolverTest.cpp | 110 ++++++++++++++++- 6 files changed, 232 insertions(+), 10 deletions(-) diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 4dddc466a..bd722a553 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -352,14 +352,16 @@ namespace storm { break; case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: { 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 < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1)); - throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter."; + 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 < z3::expr(context, Z3_mk_int2real(context, ceilVariable))); - throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter."; + 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: " diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 4337217c1..b859899ca 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -110,7 +110,7 @@ namespace storm { //! @param es the asserted expressions //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool //! @see check() - virtual CheckResult checkWithAssumptions(std::initializer_list &assumptions) = 0; + virtual CheckResult checkWithAssumptions(std::initializer_list assumptions) = 0; /*! * Gets a model for the assertion stack (and possibly assumtions) for the last call to ::check or ::checkWithAssumptions if that call diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index f889807fe..ffa627ca1 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -101,7 +101,7 @@ namespace storm { #endif } - SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list &assumptions) + SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list assumptions) { #ifdef STORM_HAVE_Z3 z3::expr_vector z3Assumptions(this->m_context); diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 07da7d921..916b69b91 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -29,7 +29,7 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set &assumptions); - virtual CheckResult checkWithAssumptions(std::initializer_list &assumptions); + virtual CheckResult checkWithAssumptions(std::initializer_list assumptions); virtual storm::expressions::SimpleValuation getModel(); diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp index fc7f69079..b31dd0f7b 100644 --- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -5,7 +5,7 @@ #include "src/adapters/Z3ExpressionAdapter.h" #include "src/settings/Settings.h" -TEST(Z3ExpressionAdapter, StormToZ3) { +TEST(Z3ExpressionAdapter, StormToZ3Basic) { #ifdef STORM_HAVE_Z3 z3::context ctx; z3::solver s(ctx); @@ -42,6 +42,120 @@ TEST(Z3ExpressionAdapter, StormToZ3) { s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); + +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +} + +TEST(Z3ExpressionAdapter, StormToZ3Integer) { +#ifdef STORM_HAVE_Z3 + z3::context ctx; + z3::solver s(ctx); + z3::expr conjecture = ctx.bool_val(false); + + storm::adapters::Z3ExpressionAdapter adapter(ctx, {}); + + 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))); + 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))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::unsat); + s.reset(); + +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +} + +TEST(Z3ExpressionAdapter, StormToZ3Real) { +#ifdef STORM_HAVE_Z3 + z3::context ctx; + z3::solver s(ctx); + z3::expr conjecture = ctx.bool_val(false); + + storm::adapters::Z3ExpressionAdapter adapter(ctx, {}); + + 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))); + 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))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::unsat); + s.reset(); + +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +} + +TEST(Z3ExpressionAdapter, StormToZ3TypeErrors) { +#ifdef STORM_HAVE_Z3 + z3::context ctx; + z3::solver s(ctx); + z3::expr conjecture = ctx.bool_val(false); + + storm::adapters::Z3ExpressionAdapter adapter(ctx, {}); + + 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); + +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +} + +TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) { +#ifdef STORM_HAVE_Z3 + z3::context ctx; + z3::solver s(ctx); + z3::expr conjecture = ctx.bool_val(false); + + storm::adapters::Z3ExpressionAdapter adapter(ctx, {}); + + 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))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::sat); //it is NOT logical equivalent + s.reset(); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprFloor, true), z3Floor))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::unsat); //it is NOT logical equivalent + 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))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::sat); //it is NOT logical equivalent + s.reset(); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprCeil, true), z3Ceil))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::unsat); //it is NOT logical equivalent + s.reset(); #else ASSERT_TRUE(false) << "StoRM built without Z3 support."; #endif diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index 3be4c57fe..9334e8ae5 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -4,14 +4,60 @@ #include "src/solver/Z3SmtSolver.h" #include "src/settings/Settings.h" -TEST(Z3SmtSolver, CheckSatisfiability) { +TEST(Z3SmtSolver, CheckSat) { #ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; + storm::solver::Z3SmtSolver::CheckResult result; + + storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); + + ASSERT_NO_THROW(s.assertExpression(exprDeMorgan)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.reset()); + + storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); + storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); + storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; + + ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.reset()); + +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +} + +TEST(Z3SmtSolver, CheckUnsat) { +#ifdef STORM_HAVE_Z3 + storm::solver::Z3SmtSolver s; + storm::solver::Z3SmtSolver::CheckResult result; storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); ASSERT_NO_THROW(s.assertExpression(!exprDeMorgan)); - storm::solver::Z3SmtSolver::CheckResult result; + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_NO_THROW(s.reset()); + + + storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); + storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); + storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(2) + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; + + ASSERT_NO_THROW(s.assertExpression(exprFormula)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); @@ -19,3 +65,63 @@ TEST(Z3SmtSolver, CheckSatisfiability) { ASSERT_TRUE(false) << "StoRM built without Z3 support."; #endif } + + +TEST(Z3SmtSolver, Backtracking) { +#ifdef STORM_HAVE_Z3 + storm::solver::Z3SmtSolver s; + storm::solver::Z3SmtSolver::CheckResult result; + + storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue(); + storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); + storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse(); + + ASSERT_NO_THROW(s.assertExpression(expr1)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.assertExpression(expr2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_NO_THROW(s.pop()); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.assertExpression(expr2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.assertExpression(expr3)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_NO_THROW(s.pop(2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.reset()); + + + storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); + storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); + storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; + storm::expressions::Expression exprFormula2 = a >= storm::expressions::Expression::createIntegerLiteral(2); + + ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.push()); + ASSERT_NO_THROW(s.assertExpression(exprFormula2)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_NO_THROW(s.pop()); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +}