Implemented asserting expressions and checking satisfiability with z3

Former-commit-id: bb49a49226

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<storm::expressions::Expression> &es) {
+			virtual void assertExpression(std::set<storm::expressions::Expression> &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<storm::expressions::Expression> &es) {
+			virtual void assertExpression(std::unordered_set<storm::expressions::Expression> &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<storm::expressions::Expression> &es) {
+			virtual void assertExpression(std::initializer_list<storm::expressions::Expression> &es) {
 				for (storm::expressions::Expression e : es) {
-					this->assert(e);
+					this->assertExpression(e);
 				}
 			}
 

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<storm::expressions::Expression> &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<storm::expressions::Expression> &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<storm::expressions::Expression> &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<storm::expressions::SimpleValuation> Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers)
+		{
+			throw std::logic_error("The method or operation is not implemented.");
+		}
+
+		uint_fast64_t Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&) > callback)
+		{
+			throw std::logic_error("The method or operation is not implemented.");
+		}
+
+	}
+}

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<storm::expressions::Expression> &assumptions);
+
+			virtual CheckResult checkWithAssumptions(std::unordered_set<storm::expressions::Expression> &assumptions);
+
+			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> &assumptions);
+
+			virtual storm::expressions::SimpleValuation getModel();
+
+			virtual std::set<storm::expressions::SimpleValuation> solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers);
+
+			virtual uint_fast64_t solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&) > callback);
+
+		private:
+			z3::context m_context;
+			z3::solver m_solver;
+			storm::adapters::Z3ExpressionAdapter m_adapter;
+		};
+	}
+}
+#endif // STORM_SOLVER_Z3SMTSOLVER