From 29083cc89cce8e88e732a9b19556873663141dbe Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Tue, 6 May 2014 17:17:39 +0200 Subject: [PATCH] Implemented asserting expressions and checking satisfiability with z3 Former-commit-id: bb49a49226b392a99081b8bb66c82d4f2f88f4e0 --- src/solver/SmtSolver.h | 14 ++--- src/solver/Z3SmtSolver.cpp | 125 +++++++++++++++++++++++++++++++++++++ src/solver/Z3SmtSolver.h | 48 ++++++++++++++ 3 files changed, 180 insertions(+), 7 deletions(-) create mode 100644 src/solver/Z3SmtSolver.cpp create mode 100644 src/solver/Z3SmtSolver.h diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index d71fece46..296a984b0 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -59,29 +59,29 @@ namespace storm { //! assert an expression in the solver //! @param e the asserted expression, the return type has to be bool //! @throws IllegalArgumentTypeException if the return type of the expression is not bool - virtual void assert(storm::expressions::Expression &e) = 0; + virtual void assertExpression(storm::expressions::Expression &e) = 0; //! assert a set of expressions in the solver //! @param es the asserted expressions //! @see assert(storm::expressions::Expression &e) - virtual void assert(std::set &es) { + virtual void assertExpression(std::set &es) { for (storm::expressions::Expression e : es) { - this->assert(e); + this->assertExpression(e); } } //! assert a set of expressions in the solver //! @param es the asserted expressions //! @see assert(storm::expressions::Expression &e) - virtual void assert(std::unordered_set &es) { + virtual void assertExpression(std::unordered_set &es) { for (storm::expressions::Expression e : es) { - this->assert(e); + this->assertExpression(e); } } //! assert a set of expressions in the solver //! @param es the asserted expressions //! @see assert(storm::expressions::Expression &e) - virtual void assert(std::initializer_list &es) { + virtual void assertExpression(std::initializer_list &es) { for (storm::expressions::Expression e : es) { - this->assert(e); + this->assertExpression(e); } } diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp new file mode 100644 index 000000000..33495a9fa --- /dev/null +++ b/src/solver/Z3SmtSolver.cpp @@ -0,0 +1,125 @@ +#include "src/solver/Z3SmtSolver.h" + + +namespace storm { + namespace solver { + Z3SmtSolver::Z3SmtSolver(Options options) + : m_context() + , m_solver(m_context) + , m_adapter(m_context, {}) { + //intentionally left empty + } + Z3SmtSolver::~Z3SmtSolver() {}; + + void Z3SmtSolver::push() + { + this->m_solver.push(); + } + + void Z3SmtSolver::pop() + { + this->m_solver.pop(); + } + + void Z3SmtSolver::pop(uint_fast64_t n) + { + this->m_solver.pop(n); + } + + void Z3SmtSolver::reset() + { + this->m_solver.reset(); + } + + void Z3SmtSolver::assertExpression(storm::expressions::Expression &e) + { + this->m_solver.add(m_adapter.translateExpression(e, true)); + } + + SmtSolver::CheckResult Z3SmtSolver::check() + { + switch (this->m_solver.check()) + { + case z3::sat: + return SmtSolver::CheckResult::SAT; + case z3::unsat: + return SmtSolver::CheckResult::UNSAT; + default: + break; + } + } + + SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set &assumptions) + { + z3::expr_vector z3Assumptions(this->m_context); + + for (storm::expressions::Expression assumption : assumptions) { + z3Assumptions.push_back(this->m_adapter.translateExpression(assumption)); + } + + switch (this->m_solver.check(z3Assumptions)) + { + case z3::sat: + return SmtSolver::CheckResult::SAT; + case z3::unsat: + return SmtSolver::CheckResult::UNSAT; + default: + break; + } + } + + SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::unordered_set &assumptions) + { + z3::expr_vector z3Assumptions(this->m_context); + + for (storm::expressions::Expression assumption : assumptions) { + z3Assumptions.push_back(this->m_adapter.translateExpression(assumption)); + } + + switch (this->m_solver.check(z3Assumptions)) + { + case z3::sat: + return SmtSolver::CheckResult::SAT; + case z3::unsat: + return SmtSolver::CheckResult::UNSAT; + default: + break; + } + } + + SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list &assumptions) + { + z3::expr_vector z3Assumptions(this->m_context); + + for (storm::expressions::Expression assumption : assumptions) { + z3Assumptions.push_back(this->m_adapter.translateExpression(assumption)); + } + + switch (this->m_solver.check(z3Assumptions)) + { + case z3::sat: + return SmtSolver::CheckResult::SAT; + case z3::unsat: + return SmtSolver::CheckResult::UNSAT; + default: + break; + } + } + + storm::expressions::SimpleValuation Z3SmtSolver::getModel() + { + throw std::logic_error("The method or operation is not implemented."); + } + + std::set Z3SmtSolver::solveAndDiversify(std::set diversifyers) + { + throw std::logic_error("The method or operation is not implemented."); + } + + uint_fast64_t Z3SmtSolver::solveAndDiversify(std::set diversifyers, std::function callback) + { + throw std::logic_error("The method or operation is not implemented."); + } + + } +} \ No newline at end of file diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h new file mode 100644 index 000000000..c9f81447d --- /dev/null +++ b/src/solver/Z3SmtSolver.h @@ -0,0 +1,48 @@ +#ifndef STORM_SOLVER_Z3SMTSOLVER +#define STORM_SOLVER_Z3SMTSOLVER + +#include "src/solver/SmtSolver.h" +#include "src/adapters/Z3ExpressionAdapter.h" + +#include "z3++.h" +#include "z3.h" + +namespace storm { + namespace solver { + class Z3SmtSolver : public SmtSolver { + public: + Z3SmtSolver(Options options = Options::ModelGeneration); + virtual ~Z3SmtSolver(); + + virtual void push(); + + virtual void pop(); + + virtual void pop(uint_fast64_t n); + + virtual void reset(); + + virtual void assertExpression(storm::expressions::Expression &e); + + virtual CheckResult check(); + + virtual CheckResult checkWithAssumptions(std::set &assumptions); + + virtual CheckResult checkWithAssumptions(std::unordered_set &assumptions); + + virtual CheckResult checkWithAssumptions(std::initializer_list &assumptions); + + virtual storm::expressions::SimpleValuation getModel(); + + virtual std::set solveAndDiversify(std::set diversifyers); + + virtual uint_fast64_t solveAndDiversify(std::set diversifyers, std::function callback); + + private: + z3::context m_context; + z3::solver m_solver; + storm::adapters::Z3ExpressionAdapter m_adapter; + }; + } +} +#endif // STORM_SOLVER_Z3SMTSOLVER \ No newline at end of file