From a815a6f4252328813ea4358187dd9752038993fb Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Wed, 25 Jun 2014 15:59:53 +0200 Subject: [PATCH] Implemented allSat with z3 and test Former-commit-id: 3795fc00c21fc00802e5210a340a9902aeca9228 --- src/solver/SmtSolver.h | 23 ++++--- src/solver/Z3SmtSolver.cpp | 68 ++++++++++++++++++--- src/solver/Z3SmtSolver.h | 24 ++++---- src/storage/expressions/SimpleValuation.cpp | 6 +- test/functional/solver/Z3SmtSolverTest.cpp | 42 ++++++++++++- 5 files changed, 133 insertions(+), 30 deletions(-) diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index b859899ca..2f357cc11 100644 --- a/src/solver/SmtSolver.h +++ b/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 solveAndDiversify(std::set diversifyers) { + virtual std::vector allSat(std::vector 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 diversifyers, std::function callback) { + virtual uint_fast64_t allSat(std::vector important, std::function callback) { throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); } }; diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 9dbe3a9b7..038d9bcc3 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/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 Z3SmtSolver::solveAndDiversify(std::set diversifyers) + std::vector Z3SmtSolver::allSat(std::vector important) { #ifdef STORM_HAVE_Z3 - LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface."); + + std::vector 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 diversifyers, std::function callback) + uint_fast64_t Z3SmtSolver::allSat(std::vector important, std::function 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 diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 672eba271..e2b4f2f87 100644 --- a/src/solver/Z3SmtSolver.h +++ b/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 &assumptions); + virtual CheckResult checkWithAssumptions(std::set &assumptions) override; - virtual CheckResult checkWithAssumptions(std::initializer_list assumptions); + virtual CheckResult checkWithAssumptions(std::initializer_list assumptions) override; - virtual storm::expressions::SimpleValuation getModel(); + virtual storm::expressions::SimpleValuation getModel() override; - virtual std::set solveAndDiversify(std::set diversifyers); + virtual std::vector allSat(std::vector important) override; - virtual uint_fast64_t solveAndDiversify(std::set diversifyers, std::function callback); + virtual uint_fast64_t allSat(std::vector important, std::function callback) override; + protected: + virtual storm::expressions::SimpleValuation z3ModelToStorm(z3::model m); private: #ifdef STORM_HAVE_Z3 diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 923bbe84b..f50b1ef49 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/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) { diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index e33a2be4f..ee5a058c7 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/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 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