diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 2f357cc11..914860bbc 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -157,6 +157,32 @@ namespace storm { virtual uint_fast64_t allSat(std::vector important, std::function callback) { throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); } + + /*! + * Retrieves the unsat core of the last call to check() + * + * @returns a subset of the asserted formulas s.t. this subset is unsat + * + * @throws InvalidStateException if no unsat core is available, i.e. the asserted formulas are consistent + * @throws IllegalFunctionCallException if unsat core generation is not configured for this solver + * @throws NotImplementedException if unsat core generation is not implemented with this solver class + */ + virtual std::vector getUnsatCore() { + throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation."); + } + + /*! + * Retrieves a subset of the assumptions from the last call to checkWithAssumptions(), s.t. the result is still unsatisfiable + * + * @returns a subset of the assumptions s.t. this subset of the assumptions results in unsat + * + * @throws InvalidStateException if no unsat assumptions is available, i.e. the asserted formulas are consistent + * @throws IllegalFunctionCallException if unsat assumptions generation is not configured for this solver + * @throws NotImplementedException if unsat assumptions generation is not implemented with this solver class + */ + virtual std::vector getUnsatAssumptions() { + throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation."); + } }; } } diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 038d9bcc3..6c13941e0 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -9,6 +9,7 @@ namespace storm { , m_solver(m_context) , m_adapter(m_context, {}) , lastResult(CheckResult::UNKNOWN) + , lastCheckAssumptions(false) #endif { //intentionally left empty @@ -63,6 +64,7 @@ namespace storm { SmtSolver::CheckResult Z3SmtSolver::check() { #ifdef STORM_HAVE_Z3 + lastCheckAssumptions = false; switch (this->m_solver.check()) { case z3::sat: this->lastResult = SmtSolver::CheckResult::SAT; @@ -83,6 +85,7 @@ namespace storm { SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set &assumptions) { #ifdef STORM_HAVE_Z3 + lastCheckAssumptions = true; z3::expr_vector z3Assumptions(this->m_context); for (storm::expressions::Expression assumption : assumptions) { @@ -109,6 +112,7 @@ namespace storm { SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list assumptions) { #ifdef STORM_HAVE_Z3 + lastCheckAssumptions = true; z3::expr_vector z3Assumptions(this->m_context); for (storm::expressions::Expression assumption : assumptions) { @@ -238,6 +242,27 @@ namespace storm { LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); #endif } + std::vector Z3SmtSolver::getUnsatAssumptions() { +#ifdef STORM_HAVE_Z3 + if (lastResult != SmtSolver::CheckResult::UNSAT) { + throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last state is not unsat."; + } + if (!lastCheckAssumptions) { + throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last check had no assumptions."; + } + z3::expr_vector z3UnsatAssumptions = this->m_solver.unsat_core(); + + std::vector unsatAssumptions; + + for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) { + unsatAssumptions.push_back(this->m_adapter.translateExpression(z3UnsatAssumptions[i])); + } + + return unsatAssumptions; +#else + LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); +#endif + } } } \ No newline at end of file diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index e2b4f2f87..a34c5d412 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -37,6 +37,8 @@ namespace storm { virtual uint_fast64_t allSat(std::vector important, std::function callback) override; + virtual std::vector getUnsatAssumptions() override; + protected: virtual storm::expressions::SimpleValuation z3ModelToStorm(z3::model m); private: @@ -46,6 +48,7 @@ namespace storm { z3::solver m_solver; storm::adapters::Z3ExpressionAdapter m_adapter; + bool lastCheckAssumptions; CheckResult lastResult; #endif }; diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index ee5a058c7..79d0cd0d0 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -223,6 +223,36 @@ TEST(Z3SmtSolver, AllSat) { } } +#else + ASSERT_TRUE(false) << "StoRM built without Z3 support."; +#endif +} + +TEST(Z3SmtSolver, UnsatAssumptions) { +#ifdef STORM_HAVE_Z3 + storm::solver::Z3SmtSolver s; + storm::solver::Z3SmtSolver::CheckResult result; + + 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 f2 = storm::expressions::Expression::createBooleanVariable("f2"); + storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); + + (s.assertExpression(exprFormula)); + (s.assertExpression(exprFormula2)); + (result = s.checkWithAssumptions({ f2 })); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + std::vector unsatCore = s.getUnsatAssumptions(); + ASSERT_EQ(unsatCore.size(), 1); + ASSERT_TRUE(unsatCore[0].isVariable()); + ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); + #else ASSERT_TRUE(false) << "StoRM built without Z3 support."; #endif