diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index b7c1781fd..4dddc466a 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -13,6 +13,7 @@ #include "z3++.h" #include "z3.h" +#include "storm-config.h" #include "src/storage/expressions/Expressions.h" #include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/ExpressionEvaluationException.h" @@ -21,7 +22,8 @@ namespace storm { namespace adapters { - + +#ifdef STORM_HAVE_Z3 class Z3ExpressionAdapter : public storm::expressions::ExpressionVisitor { public: /*! @@ -392,7 +394,7 @@ namespace storm { std::map variableToExpressionMap; }; - +#endif } // namespace adapters } // namespace storm diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index f108e7e7d..f889807fe 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -4,40 +4,64 @@ namespace storm { namespace solver { Z3SmtSolver::Z3SmtSolver(Options options) +#ifdef STORM_HAVE_Z3 : m_context() , m_solver(m_context) - , m_adapter(m_context, {}) { + , m_adapter(m_context, {}) +#endif + { //intentionally left empty } Z3SmtSolver::~Z3SmtSolver() {}; void Z3SmtSolver::push() { +#ifdef STORM_HAVE_Z3 this->m_solver.push(); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } void Z3SmtSolver::pop() { +#ifdef STORM_HAVE_Z3 this->m_solver.pop(); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } void Z3SmtSolver::pop(uint_fast64_t n) { +#ifdef STORM_HAVE_Z3 this->m_solver.pop((unsigned int)n); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } void Z3SmtSolver::reset() { +#ifdef STORM_HAVE_Z3 this->m_solver.reset(); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } void Z3SmtSolver::assertExpression(storm::expressions::Expression &e) { +#ifdef STORM_HAVE_Z3 this->m_solver.add(m_adapter.translateExpression(e, true)); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } SmtSolver::CheckResult Z3SmtSolver::check() { +#ifdef STORM_HAVE_Z3 switch (this->m_solver.check()) { case z3::sat: @@ -47,10 +71,15 @@ namespace storm { default: break; } + return SmtSolver::CheckResult::UNKNOWN; +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set &assumptions) { +#ifdef STORM_HAVE_Z3 z3::expr_vector z3Assumptions(this->m_context); for (storm::expressions::Expression assumption : assumptions) { @@ -66,10 +95,15 @@ namespace storm { default: break; } + return SmtSolver::CheckResult::UNKNOWN; +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list &assumptions) { +#ifdef STORM_HAVE_Z3 z3::expr_vector z3Assumptions(this->m_context); for (storm::expressions::Expression assumption : assumptions) { @@ -85,21 +119,37 @@ namespace storm { default: break; } + return SmtSolver::CheckResult::UNKNOWN; +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } storm::expressions::SimpleValuation Z3SmtSolver::getModel() { - throw std::logic_error("The method or operation is not implemented."); +#ifdef STORM_HAVE_Z3 + LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface."); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } std::set Z3SmtSolver::solveAndDiversify(std::set diversifyers) { - throw std::logic_error("The method or operation is not implemented."); +#ifdef STORM_HAVE_Z3 + LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface."); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } uint_fast64_t Z3SmtSolver::solveAndDiversify(std::set diversifyers, std::function callback) { - throw std::logic_error("The method or operation is not implemented."); +#ifdef STORM_HAVE_Z3 + LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface."); +#else + LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif } } diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 7fdf21307..07da7d921 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -1,6 +1,7 @@ #ifndef STORM_SOLVER_Z3SMTSOLVER #define STORM_SOLVER_Z3SMTSOLVER +#include "storm-config.h" #include "src/solver/SmtSolver.h" #include "src/adapters/Z3ExpressionAdapter.h" @@ -37,9 +38,12 @@ namespace storm { virtual uint_fast64_t solveAndDiversify(std::set diversifyers, std::function callback); private: + +#ifdef STORM_HAVE_Z3 z3::context m_context; z3::solver m_solver; storm::adapters::Z3ExpressionAdapter m_adapter; +#endif }; } } diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp new file mode 100644 index 000000000..fc7f69079 --- /dev/null +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -0,0 +1,49 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "z3++.h" +#include "src/adapters/Z3ExpressionAdapter.h" +#include "src/settings/Settings.h" + +TEST(Z3ExpressionAdapter, StormToZ3) { +#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 exprTrue = storm::expressions::Expression::createTrue(); + z3::expr z3True = ctx.bool_val(true); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprTrue), z3True))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::unsat); + s.reset(); + + storm::expressions::Expression exprFalse = storm::expressions::Expression::createFalse(); + z3::expr z3False = ctx.bool_val(false); + ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFalse), z3False))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::unsat); + s.reset(); + + 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))); + 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))); + s.add(conjecture); + ASSERT_TRUE(s.check() == z3::unsat); + 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 new file mode 100644 index 000000000..3be4c57fe --- /dev/null +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -0,0 +1,21 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/solver/Z3SmtSolver.h" +#include "src/settings/Settings.h" + +TEST(Z3SmtSolver, CheckSatisfiability) { +#ifdef STORM_HAVE_Z3 + storm::solver::Z3SmtSolver s; + + 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); + +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +}