Merge branch 'SmtSolvers'

Former-commit-id: 51451a63ba

src/solver/SmtSolver.h

@@ -32,6 +32,12 @@ namespace storm {
 			};
 			//! possible check results
 			enum class CheckResult { SAT, UNSAT, UNKNOWN };
+
+			class ModelReference {
+			public:
+				virtual bool getBooleanValue(std::string const& name) const =0;
+				virtual int_fast64_t getIntegerValue(std::string const& name) const =0;
+			};
 		public:
 			/*!
 			* Constructs a new smt solver with the given options.
@@ -158,6 +164,23 @@ namespace storm {
 				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
 			}
 
+			/*!
+			* Performs all AllSat over the important atoms. Once a valuation of the important atoms such that the currently asserted formulas are satisfiable
+			* is found the callback is called with a reference to the model. The lifetime of that model is controlled by the solver implementation. It will most
+			* certainly be invalid after the callback returned.
+			*
+			* @param important A set of expressions over which to perform all sat.
+			* @param callback A function to call for each found valuation.
+			*
+			* @returns the number of valuations of the important atoms, such that the currently asserted formulas are satisfiable that where found
+			*
+			* @throws IllegalFunctionCallException if model generation is not configured for this solver
+			* @throws NotImplementedException if model generation is not implemented with this solver class
+			*/
+			virtual uint_fast64_t allSat(std::function<bool(ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important) {
+				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
+			} //hack: switching the parameters is the only way to have overloading work with lambdas
+
 			/*!
 			* Retrieves the unsat core of the last call to check()
 			*
@@ -183,6 +206,36 @@ namespace storm {
 			virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() {
 				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation.");
 			}
+
+			/*!
+			* Sets the current interpolation group. All terms added to the assertion stack after this call will belong to
+			* the set group until the next call to this function.
+			*
+			* @param group the interpolation group all expressions asserted after this call are assigned
+			*
+			* @throws IllegalFunctionCallException if interpolation is not configured for this solver
+			* @throws NotImplementedException if interpolation is not implemented with this solver class
+			*/
+			virtual void setInterpolationGroup(uint_fast64_t group) {
+				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support interpolation.");
+			}
+
+			/*!
+			* Retrieves an interpolant for a pair (A, B) of formulas. The formula A is the conjunction of all
+			* formulas in the groups listet in the parameter groupsA, the formula B ist the conjunction of all
+			* other asserted formulas. The solver has to be in an UNSAT state.
+			*
+			* @param groupsA the interpolation groups whose conjunctions make up the formula A
+			*
+			* @returns the interpolant for (A, B), i.e. an expression I that is implied by A but the conjunction of I and B is inconsistent.
+			*
+			* @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 storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> groupsA) {
+				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support interpolation.");
+			}
 		};
 	}
 }

src/solver/Z3SmtSolver.cpp

@@ -3,6 +3,32 @@
 
 namespace storm {
 	namespace solver {
+#ifdef STORM_HAVE_Z3
+		Z3SmtSolver::Z3ModelReference::Z3ModelReference(z3::model &m, storm::adapters::Z3ExpressionAdapter &adapter) : m_model(m), m_adapter(adapter) {
+
+		}
+#endif
+
+		bool Z3SmtSolver::Z3ModelReference::getBooleanValue(std::string const& name) const {
+#ifdef STORM_HAVE_Z3
+			z3::expr z3Expr = this->m_adapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name));
+			z3::expr z3ExprValuation = m_model.eval(z3Expr, true);
+			return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsBool();
+#else
+			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
+		}
+
+		int_fast64_t Z3SmtSolver::Z3ModelReference::getIntegerValue(std::string const& name) const {
+#ifdef STORM_HAVE_Z3
+			z3::expr z3Expr = this->m_adapter.translateExpression(storm::expressions::Expression::createIntegerVariable(name));
+			z3::expr z3ExprValuation = m_model.eval(z3Expr, true);
+			return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsInt();
+#else
+			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
+		}
+
 		Z3SmtSolver::Z3SmtSolver(Options options)
 #ifdef STORM_HAVE_Z3
 			: m_context()
@@ -240,6 +266,47 @@ namespace storm {
 			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
 #endif
 		}
+
+		uint_fast64_t Z3SmtSolver::allSat(std::function<bool(SmtSolver::ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important)
+		{
+#ifdef STORM_HAVE_Z3
+			for (storm::expressions::Expression e : important) {
+				if (!e.isVariable()) {
+					throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions.";
+				}
+			}
+
+			uint_fast64_t numModels = 0;
+			bool proceed = true;
+
+			this->push();
+
+			while (proceed && this->check() == CheckResult::SAT) {
+				++numModels;
+				z3::model m = this->m_solver.get_model();
+
+				z3::expr modelExpr = this->m_context.bool_val(true);
+				storm::expressions::SimpleValuation valuation;
+
+				for (storm::expressions::Expression importantAtom : important) {
+					z3::expr z3ImportantAtom = this->m_adapter.translateExpression(importantAtom);
+					z3::expr z3ImportantAtomValuation = m.eval(z3ImportantAtom, true);
+					modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
+				}
+
+				proceed = callback(Z3ModelReference(m, m_adapter));
+
+				this->m_solver.add(!modelExpr);
+			}
+
+			this->pop();
+
+			return numModels;
+#else
+			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
+		}
+
 		std::vector<storm::expressions::Expression> Z3SmtSolver::getUnsatAssumptions() {
 #ifdef STORM_HAVE_Z3
 			if (lastResult != SmtSolver::CheckResult::UNSAT) {

src/solver/Z3SmtSolver.h

@@ -13,6 +13,20 @@
 namespace storm {
 	namespace solver {
 		class Z3SmtSolver : public SmtSolver {
+		public:
+			class Z3ModelReference : public SmtSolver::ModelReference {
+			public:
+#ifdef STORM_HAVE_Z3
+				Z3ModelReference(z3::model& m, storm::adapters::Z3ExpressionAdapter &adapter);
+#endif
+				virtual bool getBooleanValue(std::string const& name) const override;
+				virtual int_fast64_t getIntegerValue(std::string const& name) const override;
+			private:
+#ifdef STORM_HAVE_Z3
+				z3::model &m_model;
+				storm::adapters::Z3ExpressionAdapter &m_adapter;
+#endif
+			};
 		public:
 			Z3SmtSolver(Options options = Options::ModelGeneration);
 			virtual ~Z3SmtSolver();
@@ -39,6 +53,8 @@ namespace storm {
 
 			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
 
+			virtual uint_fast64_t allSat(std::function<bool(ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important) override;
+
 			virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;
 
 		protected: