sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

More tests and some small bugfixes for Z3SmtSolver 

Former-commit-id: 71def90649
tempestpy_adaptions
David_Korzeniewski 11 years ago
parent
45bc8ea665
commit
9a7b4f69ef
6 changed files with 232 additions and 10 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/adapters/Z3ExpressionAdapter.h
  2. 2
      src/solver/SmtSolver.h
  3. 2
      src/solver/Z3SmtSolver.cpp
  4. 2
      src/solver/Z3SmtSolver.h
  5. 116
      test/functional/adapter/Z3ExpressionAdapterTest.cpp
  6. 110
      test/functional/solver/Z3SmtSolverTest.cpp

10
src/adapters/Z3ExpressionAdapter.h
View File

@ -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: "

2
src/solver/SmtSolver.h
View File

@ -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<storm::expressions::Expression> &assumptions) = 0;
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) = 0;
/*!
* Gets a model for the assertion stack (and possibly assumtions) for the last call to ::check or ::checkWithAssumptions if that call

2
src/solver/Z3SmtSolver.cpp
View File

@ -101,7 +101,7 @@ namespace storm {
#endif
}
SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> &assumptions)
SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions)
{
#ifdef STORM_HAVE_Z3
z3::expr_vector z3Assumptions(this->m_context);

2
src/solver/Z3SmtSolver.h
View File

@ -29,7 +29,7 @@ namespace storm {
virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions);
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> &assumptions);
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions);
virtual storm::expressions::SimpleValuation getModel();

116
test/functional/adapter/Z3ExpressionAdapterTest.cpp
View File

@ -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

110
test/functional/solver/Z3SmtSolverTest.cpp
View File

@ -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
}
Write Preview
Loading…
Cancel
Save