Implemented allSat with z3 and test

Former-commit-id: 3795fc00c2

src/solver/SmtSolver.h

@@ -126,28 +126,35 @@ namespace storm {
 			}
 
 			/*!
-			* Get get a maximal number of models for the assertion stack such that each model has a distinct valuation of the diversifyers.
+			* Performs all AllSat over the important atoms. All valuations of the important atoms such that the currently asserted formulas are satisfiable
+			* are returned from the function.
 			*
-			* @param diversifyers A set of expressions over which to diversify. For each returned model the valuation these terms is distinct.
+			* @warning If infinitely many valuations exist, such that the currently asserted formulas are satisfiable, this function will never return!
+			*
+			* @param important A set of expressions over which to perform all sat.
+			*
+			* @returns the set of all valuations of the important atoms, such that the currently asserted formulas are satisfiable
 			*
 			* @throws IllegalFunctionCallException if model generation is not configured for this solver
 			* @throws NotImplementedException if model generation is not implemented with this solver class
 			*/
-			virtual std::set<storm::expressions::SimpleValuation> solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers) {
+			virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> important) {
 				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
 			}
 
 			/*!
-			* Get get a maximal number of models for the assertion stack such that each model has a distinct valuation of the diversifyers.
-			* For each model that is found the provided callback function is called once with the model as parameter.
+			* 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 that valuation.
+			*
+			* @param important A set of expressions over which to perform all sat.
+			* @param callback A function to call for each found valuation.
 			*
-			* @param diversifyers A set of expressions over which to diversify. For each returned model the valuation these terms is distinct.
-			* @param callback A function to call for each found model.
+			* @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 solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&)> callback) {
+			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback) {
 				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
 			}
 		};

src/solver/Z3SmtSolver.cpp

@@ -138,13 +138,20 @@ namespace storm {
 			
 			LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT.");
 
-			z3::model m = this->m_solver.get_model();
+			return this->z3ModelToStorm(this->m_solver.get_model());
+#else
+			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
+		}
+
+		storm::expressions::SimpleValuation Z3SmtSolver::z3ModelToStorm(z3::model m) {
+#ifdef STORM_HAVE_Z3
 			storm::expressions::SimpleValuation stormModel;
 
 			for (unsigned i = 0; i < m.num_consts(); ++i) {
 				z3::func_decl var_i = m.get_const_decl(i);
 				storm::expressions::Expression var_i_interp = this->m_adapter.translateExpression(m.get_const_interp(var_i));
-				
+
 				switch (var_i_interp.getReturnType()) {
 					case storm::expressions::ExpressionReturnType::Bool:
 						stormModel.addBooleanIdentifier(var_i.name().str(), var_i_interp.evaluateAsBool());
@@ -157,29 +164,76 @@ namespace storm {
 						break;
 					default:
 						LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.")
-						break;
+							break;
 				}
 
 			}
 
+			return stormModel;
 #else
 			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
 #endif
 		}
 
-		std::set<storm::expressions::SimpleValuation> Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers)
+		std::vector<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> important)
 		{
 #ifdef STORM_HAVE_Z3
-			LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+			
+			std::vector<storm::expressions::SimpleValuation> valuations;
+
+			this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool {valuations.push_back(valuation); return true; });
+
+			return valuations;
+
 #else
 			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
 #endif
 		}
 
-		uint_fast64_t Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&) > callback)
+		uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback)
 		{
 #ifdef STORM_HAVE_Z3
-			LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+			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);
+					if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Bool) {
+						valuation.addBooleanIdentifier(importantAtom.getIdentifier(), this->m_adapter.translateExpression(z3ImportantAtomValuation).evaluateAsBool());
+					} else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Int) {
+						valuation.addIntegerIdentifier(importantAtom.getIdentifier(), this->m_adapter.translateExpression(z3ImportantAtomValuation).evaluateAsInt());
+					} else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Double) {
+						valuation.addDoubleIdentifier(importantAtom.getIdentifier(), this->m_adapter.translateExpression(z3ImportantAtomValuation).evaluateAsDouble());
+					} else {
+						throw storm::exceptions::InvalidTypeException() << "Important atom has invalid type";
+					}
+				}
+
+				proceed = callback(valuation);
+
+				this->m_solver.add(!modelExpr);
+			}
+
+			this->pop();
+
+			return numModels;
 #else
 			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
 #endif

src/solver/Z3SmtSolver.h

@@ -15,28 +15,30 @@ namespace storm {
 			Z3SmtSolver(Options options = Options::ModelGeneration);
 			virtual ~Z3SmtSolver();
 
-			virtual void push();
+			virtual void push() override;
 
-			virtual void pop();
+			virtual void pop() override;
 
-			virtual void pop(uint_fast64_t n);
+			virtual void pop(uint_fast64_t n) override;
 
-			virtual void reset();
+			virtual void reset() override;
 
-			virtual void assertExpression(storm::expressions::Expression &e);
+			virtual void assertExpression(storm::expressions::Expression &e) override;
 
-			virtual CheckResult check();
+			virtual CheckResult check() override;
 
-			virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions);
+			virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions) override;
 
-			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions);
+			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) override;
 
-			virtual storm::expressions::SimpleValuation getModel();
+			virtual storm::expressions::SimpleValuation getModel() override;
 
-			virtual std::set<storm::expressions::SimpleValuation> solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers);
+			virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> important) override;
 
-			virtual uint_fast64_t solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&) > callback);
+			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
 
+		protected:
+			virtual storm::expressions::SimpleValuation z3ModelToStorm(z3::model m);
 		private:
 
 #ifdef STORM_HAVE_Z3

src/storage/expressions/SimpleValuation.cpp

@@ -15,17 +15,17 @@ namespace storm {
         
         void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) {
             LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
-            this->identifierToValueMap.emplace(name, initialValue);
+			this->identifierToValueMap.emplace(name, initialValue);
         }
         
         void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) {
             LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
-            this->identifierToValueMap.emplace(name, initialValue);
+			this->identifierToValueMap.emplace(name, initialValue);
         }
         
         void SimpleValuation::addDoubleIdentifier(std::string const& name, double initialValue) {
             LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
-            this->identifierToValueMap.emplace(name, initialValue);
+			this->identifierToValueMap.emplace(name, initialValue);
         }
         
         void SimpleValuation::setBooleanValue(std::string const& name, bool value) {

test/functional/solver/Z3SmtSolverTest.cpp

@@ -168,7 +168,7 @@ TEST(Z3SmtSolver, GenerateModel) {
 	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)
+	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)
@@ -183,6 +183,46 @@ TEST(Z3SmtSolver, GenerateModel) {
 	(a_eval = model.getIntegerValue("a"));
 	ASSERT_EQ(1, a_eval);
 
+#else
+	ASSERT_TRUE(false) << "StoRM built without Z3 support.";
+#endif
+}
+
+
+TEST(Z3SmtSolver, AllSat) {
+#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 x = storm::expressions::Expression::createBooleanVariable("x");
+	storm::expressions::Expression y = storm::expressions::Expression::createBooleanVariable("y");
+	storm::expressions::Expression z = storm::expressions::Expression::createBooleanVariable("z");
+	storm::expressions::Expression exprFormula1 = x.implies(a > storm::expressions::Expression::createIntegerLiteral(5));
+	storm::expressions::Expression exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5));
+	storm::expressions::Expression exprFormula3 = z.implies(b < storm::expressions::Expression::createIntegerLiteral(5));
+
+	(s.assertExpression(exprFormula1));
+	(s.assertExpression(exprFormula2));
+	(s.assertExpression(exprFormula3));
+
+	std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x,y});
+
+	ASSERT_TRUE(valuations.size() == 3);
+	for (int i = 0; i < valuations.size(); ++i) {
+		ASSERT_EQ(valuations[i].getNumberOfIdentifiers(), 2);
+		ASSERT_TRUE(valuations[i].containsBooleanIdentifier("x"));
+		ASSERT_TRUE(valuations[i].containsBooleanIdentifier("y"));
+	}
+	for (int i = 0; i < valuations.size(); ++i) {
+		ASSERT_FALSE(valuations[i].getBooleanValue("x") && valuations[i].getBooleanValue("y"));
+
+		for (int j = i+1; j < valuations.size(); ++j) {
+			ASSERT_TRUE((valuations[i].getBooleanValue("x") != valuations[j].getBooleanValue("x")) || (valuations[i].getBooleanValue("y") != valuations[j].getBooleanValue("y")));
+		}
+	}
+
 #else
 	ASSERT_TRUE(false) << "StoRM built without Z3 support.";
 #endif