From b5d55335a6c3e4d1926a59d6691ab024e44aee9f Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 19 Dec 2014 13:15:28 +0100 Subject: [PATCH] All tests passing again. Former-commit-id: ffa8bef2d223fd063915828781bc8dbb66ea569b --- src/solver/MathsatSmtSolver.cpp | 81 +++++++++++-- src/solver/MathsatSmtSolver.h | 30 +++-- src/solver/SmtSolver.cpp | 6 +- src/solver/SmtSolver.h | 15 ++- src/solver/Z3SmtSolver.cpp | 89 ++++++++------ src/solver/Z3SmtSolver.h | 15 ++- src/storage/expressions/Expression.cpp | 4 + src/storage/expressions/Expression.h | 7 ++ .../solver/MathSatSmtSolverTest.cpp | 35 +++--- test/functional/solver/Z3SmtSolverTest.cpp | 114 +++++++++--------- 10 files changed, 257 insertions(+), 139 deletions(-) diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 6be855dae..8f7ea7b9c 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -7,9 +7,63 @@ namespace storm { namespace solver { +#ifdef STORM_HAVE_MSAT + MathsatSmtSolver::MathsatAllsatModelReference::MathsatAllsatModelReference(msat_env const& env, msat_term* model, std::unordered_map const& atomNameToSlotMapping) : env(env), model(model), atomNameToSlotMapping(atomNameToSlotMapping) { + // Intentionally left empty. + } +#endif + bool MathsatSmtSolver::MathsatAllsatModelReference::getBooleanValue(std::string const& name) const { + std::unordered_map::const_iterator nameSlotPair = atomNameToSlotMapping.find(name); + STORM_LOG_THROW(nameSlotPair != atomNameToSlotMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve value of unknown variable '" << name << "' from model."); + msat_term selectedTerm = model[nameSlotPair->second]; + + if (msat_term_is_not(env, selectedTerm)) { + return false; + } else { + return true; + } + } + + int_fast64_t MathsatSmtSolver::MathsatAllsatModelReference::getIntegerValue(std::string const& name) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve integer value from model that only contains boolean values."); + } + + double MathsatSmtSolver::MathsatAllsatModelReference::getDoubleValue(std::string const& name) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve double value from model that only contains boolean values."); + } + +#ifdef STORM_HAVE_MSAT + MathsatSmtSolver::MathsatModelReference::MathsatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter) : env(env), expressionAdapter(expressionAdapter) { + // Intentionally left empty. + } +#endif + bool MathsatSmtSolver::MathsatModelReference::getBooleanValue(std::string const& name) const { + msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name), false); + msat_term msatValue = msat_get_model_value(env, msatVariable); + storm::expressions::Expression value = expressionAdapter.translateTerm(msatValue); + STORM_LOG_THROW(value.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "Unable to retrieve boolean value of non-boolean variable '" << name << "'."); + return value.evaluateAsBool(); + } + + int_fast64_t MathsatSmtSolver::MathsatModelReference::getIntegerValue(std::string const& name) const { + msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name), false); + msat_term msatValue = msat_get_model_value(env, msatVariable); + storm::expressions::Expression value = expressionAdapter.translateTerm(msatValue); + STORM_LOG_THROW(value.hasIntegralReturnType(), storm::exceptions::InvalidArgumentException, "Unable to retrieve integer value of non-integer variable '" << name << "'."); + return value.evaluateAsInt(); + } + + double MathsatSmtSolver::MathsatModelReference::getDoubleValue(std::string const& name) const { + msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name), false); + msat_term msatValue = msat_get_model_value(env, msatVariable); + storm::expressions::Expression value = expressionAdapter.translateTerm(msatValue); + STORM_LOG_THROW(value.hasIntegralReturnType(), storm::exceptions::InvalidArgumentException, "Unable to retrieve double value of non-double variable '" << name << "'."); + return value.evaluateAsDouble(); + } + MathsatSmtSolver::MathsatSmtSolver(Options const& options) #ifdef STORM_HAVE_MSAT - : lastCheckAssumptions(false), lastResult(CheckResult::Unknown) + : expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif { #ifdef STORM_HAVE_MSAT @@ -35,7 +89,7 @@ namespace storm { } MathsatSmtSolver::~MathsatSmtSolver() { - STORM_LOG_THROW(MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Illegal MathSAT environment."); + STORM_LOG_THROW(!MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Illegal MathSAT environment."); msat_destroy_env(env); } @@ -154,7 +208,7 @@ namespace storm { #endif } - storm::expressions::SimpleValuation MathsatSmtSolver::getModel() + storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() { #ifdef STORM_HAVE_MSAT STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); @@ -163,6 +217,15 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } + + std::shared_ptr MathsatSmtSolver::getModel() { +#ifdef STORM_HAVE_MSAT + STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); + return std::shared_ptr(new MathsatModelReference(env, *expressionAdapter)); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); +#endif + } #ifdef STORM_HAVE_MSAT storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() { @@ -175,18 +238,18 @@ namespace storm { msat_term t, v; msat_model_iterator_next(modelIterator, &t, &v); - storm::expressions::Expression variableIInterpretation = this->expressionAdapter->translateTerm(v); + storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateTerm(v); char* name = msat_decl_get_name(msat_term_get_decl(t)); - switch (variableIInterpretation.getReturnType()) { + switch (variableInterpretation.getReturnType()) { case storm::expressions::ExpressionReturnType::Bool: - stormModel.addBooleanIdentifier(std::string(name), variableIInterpretation.evaluateAsBool()); + stormModel.addBooleanIdentifier(std::string(name), variableInterpretation.evaluateAsBool()); break; case storm::expressions::ExpressionReturnType::Int: - stormModel.addIntegerIdentifier(std::string(name), variableIInterpretation.evaluateAsInt()); + stormModel.addIntegerIdentifier(std::string(name), variableInterpretation.evaluateAsInt()); break; case storm::expressions::ExpressionReturnType::Double: - stormModel.addDoubleIdentifier(std::string(name), variableIInterpretation.evaluateAsDouble()); + stormModel.addDoubleIdentifier(std::string(name), variableInterpretation.evaluateAsDouble()); break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") @@ -260,7 +323,7 @@ namespace storm { static int allsatModelReferenceCallback(msat_term* model, int size, void* user_data) { AllsatModelReferenceCallbackUserData* user = reinterpret_cast(user_data); - MathsatSmtSolver::MathSatModelReference modelReference(user->env, model, user->atomNameToSlotMapping); + MathsatSmtSolver::MathsatAllsatModelReference modelReference(user->env, model, user->atomNameToSlotMapping); if (user->callback(modelReference)) { return 1; } else { diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index efd488450..011f0547a 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -25,11 +25,7 @@ namespace storm { */ class Options { public: - Options() : enableModelGeneration(false), enableUnsatCoreGeneration(false), enableInterpolantGeneration(false) { - // Intentionally left empty. - } - - Options(bool enableModelGeneration, bool enableUnsatCoreGeneration, bool enableInterpolantGeneration) : enableModelGeneration(enableModelGeneration), enableUnsatCoreGeneration(enableUnsatCoreGeneration), enableInterpolantGeneration(enableInterpolantGeneration) { + Options(bool enableModelGeneration = true, bool enableUnsatCoreGeneration = false, bool enableInterpolantGeneration = false) : enableModelGeneration(enableModelGeneration), enableUnsatCoreGeneration(enableUnsatCoreGeneration), enableInterpolantGeneration(enableInterpolantGeneration) { // Intentionally left empty. } @@ -38,10 +34,10 @@ namespace storm { bool enableInterpolantGeneration = false; }; - class MathSatModelReference : public SmtSolver::ModelReference { + class MathsatAllsatModelReference : public SmtSolver::ModelReference { public: #ifdef STORM_HAVE_MSAT - MathSatModelReference(msat_env const& env, msat_term* model, std::unordered_map const& atomNameToSlotMapping); + MathsatAllsatModelReference(msat_env const& env, msat_term* model, std::unordered_map const& atomNameToSlotMapping); #endif virtual bool getBooleanValue(std::string const& name) const override; virtual int_fast64_t getIntegerValue(std::string const& name) const override; @@ -55,6 +51,22 @@ namespace storm { #endif }; + class MathsatModelReference : public SmtSolver::ModelReference { + public: +#ifdef STORM_HAVE_MSAT + MathsatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter); +#endif + virtual bool getBooleanValue(std::string const& name) const override; + virtual int_fast64_t getIntegerValue(std::string const& name) const override; + virtual double getDoubleValue(std::string const& name) const override; + + private: +#ifdef STORM_HAVE_MSAT + msat_env const& env; + storm::adapters::MathsatExpressionAdapter& expressionAdapter; +#endif + }; + MathsatSmtSolver(Options const& options = Options()); virtual ~MathsatSmtSolver(); @@ -75,8 +87,10 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; - virtual storm::expressions::SimpleValuation getModel() override; + virtual storm::expressions::SimpleValuation getModelAsValuation() override; + virtual std::shared_ptr getModel() override; + virtual std::vector allSat(std::vector const& important) override; virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; diff --git a/src/solver/SmtSolver.cpp b/src/solver/SmtSolver.cpp index bfd699be4..46ffac841 100644 --- a/src/solver/SmtSolver.cpp +++ b/src/solver/SmtSolver.cpp @@ -32,7 +32,11 @@ namespace storm { } } - storm::expressions::SimpleValuation SmtSolver::getModel() { + storm::expressions::SimpleValuation SmtSolver::getModelAsValuation() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); + } + + std::shared_ptr SmtSolver::getModel() { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 83c3cff71..8eec37b11 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -133,8 +133,21 @@ namespace storm { * solver was instantiated with support for model generation. Note that this function may throw an exception * if it is not called immediately after a call to check() or checkWithAssumptions() that returned Sat * depending on the implementation. + * + * @return A valuation that holds the values of the variables in the current model. + */ + virtual storm::expressions::SimpleValuation getModelAsValuation(); + + /*! + * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that + * satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the + * solver was instantiated with support for model generation. Note that this function may throw an exception + * if it is not called immediately after a call to check() or checkWithAssumptions() that returned Sat + * depending on the implementation. + * + * @return A reference to a model that can be queried for the values of specific variables. */ - virtual storm::expressions::SimpleValuation getModel(); + virtual std::shared_ptr getModel(); /*! * Performs AllSat over the (provided) important atoms. That is, this function returns all models of the diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 638972027..ff7d5a344 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -1,4 +1,4 @@ -#include "src/solver/Z3SmtSolver.h" +#include "src/solver/Z3Smtsolver.h" #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidStateException.h" @@ -6,7 +6,7 @@ namespace storm { namespace solver { #ifdef STORM_HAVE_Z3 - Z3SmtSolver::Z3ModelReference::Z3ModelReference(z3::model const& model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : model(model), expressionAdapter(expressionAdapter) { + Z3SmtSolver::Z3ModelReference::Z3ModelReference(z3::model model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : model(model), expressionAdapter(expressionAdapter) { // Intentionally left empty. } #endif @@ -43,11 +43,15 @@ namespace storm { Z3SmtSolver::Z3SmtSolver() #ifdef STORM_HAVE_Z3 - : context(), solver(context), expressionAdapter(context), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) + : context(nullptr), solver(nullptr), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif { - // Intentionally left empty. - } + z3::config config; + config.set("model", true); + context = std::unique_ptr(new z3::context(config)); + solver = std::unique_ptr(new z3::solver(*context)); + expressionAdapter = std::unique_ptr(new storm::adapters::Z3ExpressionAdapter(*context)); + } Z3SmtSolver::~Z3SmtSolver() { // Intentionally left empty. @@ -56,7 +60,7 @@ namespace storm { void Z3SmtSolver::push() { #ifdef STORM_HAVE_Z3 - this->solver.push(); + this->solver->push(); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif @@ -65,7 +69,7 @@ namespace storm { void Z3SmtSolver::pop() { #ifdef STORM_HAVE_Z3 - this->solver.pop(); + this->solver->pop(); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif @@ -74,7 +78,7 @@ namespace storm { void Z3SmtSolver::pop(uint_fast64_t n) { #ifdef STORM_HAVE_Z3 - this->solver.pop(static_cast(n)); + this->solver->pop(static_cast(n)); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif @@ -83,7 +87,7 @@ namespace storm { void Z3SmtSolver::reset() { #ifdef STORM_HAVE_Z3 - this->solver.reset(); + this->solver->reset(); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif @@ -92,7 +96,7 @@ namespace storm { void Z3SmtSolver::add(storm::expressions::Expression const& assertion) { #ifdef STORM_HAVE_Z3 - this->solver.add(expressionAdapter.translateExpression(assertion, true)); + this->solver->add(expressionAdapter->translateExpression(assertion, true)); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif @@ -102,7 +106,7 @@ namespace storm { { #ifdef STORM_HAVE_Z3 lastCheckAssumptions = false; - switch (this->solver.check()) { + switch (this->solver->check()) { case z3::sat: this->lastResult = SmtSolver::CheckResult::Sat; break; @@ -123,13 +127,13 @@ namespace storm { { #ifdef STORM_HAVE_Z3 lastCheckAssumptions = true; - z3::expr_vector z3Assumptions(this->context); + z3::expr_vector z3Assumptions(*this->context); for (storm::expressions::Expression assumption : assumptions) { - z3Assumptions.push_back(this->expressionAdapter.translateExpression(assumption)); + z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption)); } - switch (this->solver.check(z3Assumptions)) { + switch (this->solver->check(z3Assumptions)) { case z3::sat: this->lastResult = SmtSolver::CheckResult::Sat; break; @@ -150,13 +154,13 @@ namespace storm { { #ifdef STORM_HAVE_Z3 lastCheckAssumptions = true; - z3::expr_vector z3Assumptions(this->context); + z3::expr_vector z3Assumptions(*this->context); for (storm::expressions::Expression assumption : assumptions) { - z3Assumptions.push_back(this->expressionAdapter.translateExpression(assumption)); + z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption)); } - switch (this->solver.check(z3Assumptions)) { + switch (this->solver->check(z3Assumptions)) { case z3::sat: this->lastResult = SmtSolver::CheckResult::Sat; break; @@ -173,15 +177,24 @@ namespace storm { #endif } - storm::expressions::SimpleValuation Z3SmtSolver::getModel() + storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation() { #ifdef STORM_HAVE_Z3 STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); - return this->convertZ3ModelToValuation(this->solver.get_model()); + return this->convertZ3ModelToValuation(this->solver->get_model()); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } + + std::shared_ptr Z3SmtSolver::getModel() { +#ifdef STORM_HAVE_Z3 + STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); + return std::shared_ptr(new Z3ModelReference(this->solver->get_model(), *this->expressionAdapter)); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); +#endif + } #ifdef STORM_HAVE_Z3 storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) { @@ -189,17 +202,17 @@ namespace storm { for (unsigned i = 0; i < model.num_consts(); ++i) { z3::func_decl variableI = model.get_const_decl(i); - storm::expressions::Expression variableIInterpretation = this->expressionAdapter.translateExpression(model.get_const_interp(variableI)); + storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateExpression(model.get_const_interp(variableI)); - switch (variableIInterpretation.getReturnType()) { + switch (variableInterpretation.getReturnType()) { case storm::expressions::ExpressionReturnType::Bool: - stormModel.addBooleanIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsBool()); + stormModel.addBooleanIdentifier(variableI.name().str(), variableInterpretation.evaluateAsBool()); break; case storm::expressions::ExpressionReturnType::Int: - stormModel.addIntegerIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsInt()); + stormModel.addIntegerIdentifier(variableI.name().str(), variableInterpretation.evaluateAsInt()); break; case storm::expressions::ExpressionReturnType::Double: - stormModel.addDoubleIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsDouble()); + stormModel.addDoubleIdentifier(variableI.name().str(), variableInterpretation.evaluateAsDouble()); break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") @@ -239,21 +252,21 @@ namespace storm { // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration. while (proceed && this->check() == CheckResult::Sat) { ++numberOfModels; - z3::model model = this->solver.get_model(); + z3::model model = this->solver->get_model(); - z3::expr modelExpr = this->context.bool_val(true); + z3::expr modelExpr = this->context->bool_val(true); storm::expressions::SimpleValuation valuation; for (storm::expressions::Expression const& importantAtom : important) { - z3::expr z3ImportantAtom = this->expressionAdapter.translateExpression(importantAtom); + z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom); z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true); modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation); if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Bool) { - valuation.addBooleanIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsBool()); + valuation.addBooleanIdentifier(importantAtom.getIdentifier(), this->expressionAdapter->translateExpression(z3ImportantAtomValuation).evaluateAsBool()); } else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Int) { - valuation.addIntegerIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsInt()); + valuation.addIntegerIdentifier(importantAtom.getIdentifier(), this->expressionAdapter->translateExpression(z3ImportantAtomValuation).evaluateAsInt()); } else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Double) { - valuation.addDoubleIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsDouble()); + valuation.addDoubleIdentifier(importantAtom.getIdentifier(), this->expressionAdapter->translateExpression(z3ImportantAtomValuation).evaluateAsDouble()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Important atom has invalid type."); } @@ -262,7 +275,7 @@ namespace storm { // Check if we are required to proceed, and if so rule out the current model. proceed = callback(valuation); if (proceed) { - this->solver.add(!modelExpr); + this->solver->add(!modelExpr); } } @@ -290,22 +303,22 @@ namespace storm { // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration. while (proceed && this->check() == CheckResult::Sat) { ++numberOfModels; - z3::model model = this->solver.get_model(); + z3::model model = this->solver->get_model(); - z3::expr modelExpr = this->context.bool_val(true); + z3::expr modelExpr = this->context->bool_val(true); storm::expressions::SimpleValuation valuation; for (storm::expressions::Expression const& importantAtom : important) { - z3::expr z3ImportantAtom = this->expressionAdapter.translateExpression(importantAtom); + z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom); z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true); modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation); } - Z3ModelReference modelRef(model, expressionAdapter); + Z3ModelReference modelRef(model, *expressionAdapter); // Check if we are required to proceed, and if so rule out the current model. proceed = callback(modelRef); if (proceed) { - this->solver.add(!modelExpr); + this->solver->add(!modelExpr); } } @@ -321,11 +334,11 @@ namespace storm { STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.") STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions."); - z3::expr_vector z3UnsatAssumptions = this->solver.unsat_core(); + z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core(); std::vector unsatAssumptions; for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) { - unsatAssumptions.push_back(this->expressionAdapter.translateExpression(z3UnsatAssumptions[i])); + unsatAssumptions.push_back(this->expressionAdapter->translateExpression(z3UnsatAssumptions[i])); } return unsatAssumptions; diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 0984aa2df..b5f222574 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -17,15 +17,16 @@ namespace storm { class Z3ModelReference : public SmtSolver::ModelReference { public: #ifdef STORM_HAVE_Z3 - Z3ModelReference(z3::model const& m, storm::adapters::Z3ExpressionAdapter& expressionAdapter); + Z3ModelReference(z3::model m, storm::adapters::Z3ExpressionAdapter& expressionAdapter); #endif virtual bool getBooleanValue(std::string const& name) const override; virtual int_fast64_t getIntegerValue(std::string const& name) const override; virtual double getDoubleValue(std::string const& name) const override; + private: #ifdef STORM_HAVE_Z3 // The Z3 model out of which the information can be extracted. - z3::model const& model; + z3::model model; // The expression adapter that is used to translate the variable names. storm::adapters::Z3ExpressionAdapter& expressionAdapter; @@ -52,7 +53,9 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; - virtual storm::expressions::SimpleValuation getModel() override; + virtual storm::expressions::SimpleValuation getModelAsValuation() override; + + virtual std::shared_ptr getModel() override; virtual std::vector allSat(std::vector const& important) override; @@ -73,13 +76,13 @@ namespace storm { storm::expressions::SimpleValuation convertZ3ModelToValuation(z3::model const& model); // The context used by the solver. - z3::context context; + std::unique_ptr context; // The actual solver object. - z3::solver solver; + std::unique_ptr solver; // An expression adapter that is used for translating the expression into Z3's format. - storm::adapters::Z3ExpressionAdapter expressionAdapter; + std::unique_ptr expressionAdapter; // A flag storing whether the last call to a check method provided aussumptions. bool lastCheckAssumptions; diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index ad74066b3..c0785bade 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -145,6 +145,10 @@ namespace storm { return this->getReturnType() == ExpressionReturnType::Bool; } + bool Expression::hasIntegralReturnType() const { + return this->getReturnType() == ExpressionReturnType::Int; + } + Expression Expression::createBooleanLiteral(bool value) { return Expression(std::shared_ptr(new BooleanLiteralExpression(value))); } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 504e3d96e..750641ddf 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -302,6 +302,13 @@ namespace storm { */ bool hasBooleanReturnType() const; + /*! + * Retrieves whether the expression has an integral return type. + * + * @return True iff the expression has a integral return type. + */ + bool hasIntegralReturnType() const; + /*! * Accepts the given visitor. * diff --git a/test/functional/solver/MathSatSmtSolverTest.cpp b/test/functional/solver/MathSatSmtSolverTest.cpp index 2ca48d935..2efdbc4fc 100644 --- a/test/functional/solver/MathSatSmtSolverTest.cpp +++ b/test/functional/solver/MathSatSmtSolverTest.cpp @@ -150,15 +150,14 @@ TEST(MathsatSmtSolver, GenerateModel) { && c == (a + b - storm::expressions::Expression::createIntegerLiteral(1)) && b + a > c; - (s.add(exprFormula)); - (result = s.check()); + s.add(exprFormula); + result = s.check(); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - storm::expressions::SimpleValuation model; - (model = s.getModel()); - int_fast64_t a_eval = model.getIntegerValue("a"); - int_fast64_t b_eval = model.getIntegerValue("b"); - int_fast64_t c_eval = model.getIntegerValue("c"); - ASSERT_TRUE(c_eval == a_eval + b_eval - 1); + std::shared_ptr model = s.getModel(); + int_fast64_t aEval = model->getIntegerValue("a"); + int_fast64_t bEval = model->getIntegerValue("b"); + int_fast64_t cEval = model->getIntegerValue("c"); + ASSERT_TRUE(cEval == aEval + bEval - 1); } TEST(MathsatSmtSolver, AllSat) { @@ -174,9 +173,9 @@ TEST(MathsatSmtSolver, AllSat) { 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.add(exprFormula1)); - (s.add(exprFormula2)); - (s.add(exprFormula3)); + s.add(exprFormula1); + s.add(exprFormula2); + s.add(exprFormula3); std::vector valuations = s.allSat({x,y}); @@ -196,7 +195,7 @@ TEST(MathsatSmtSolver, AllSat) { } TEST(MathsatSmtSolver, UnsatAssumptions) { - storm::solver::MathsatSmtSolver s; + storm::solver::MathsatSmtSolver s(storm::solver::MathsatSmtSolver::Options(false, true, false)); storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); @@ -210,9 +209,9 @@ TEST(MathsatSmtSolver, UnsatAssumptions) { storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1)); - (s.add(exprFormula)); - (s.add(exprFormula2)); - (result = s.checkWithAssumptions({ f2 })); + s.add(exprFormula); + s.add(exprFormula2); + result = s.checkWithAssumptions({ f2 }); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); std::vector unsatCore = s.getUnsatAssumptions(); ASSERT_EQ(unsatCore.size(), 1); @@ -237,7 +236,7 @@ TEST(MathsatSmtSolver, InterpolationTest) { s.add(exprFormula2); s.setInterpolationGroup(2); s.add(exprFormula3); - + ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); @@ -245,11 +244,11 @@ TEST(MathsatSmtSolver, InterpolationTest) { ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1})); storm::solver::MathsatSmtSolver s2; - + ASSERT_NO_THROW(s2.add(!(exprFormula && exprFormula2).implies(interpol))); ASSERT_NO_THROW(result = s2.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); - + ASSERT_NO_THROW(s2.reset()); ASSERT_NO_THROW(s2.add(interpol && exprFormula3)); ASSERT_NO_THROW(result = s2.check()); diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index 93f2876bb..7b05af248 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -8,23 +8,23 @@ TEST(Z3SmtSolver, CheckSat) { storm::solver::Z3SmtSolver s; storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - + storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); - + ASSERT_NO_THROW(s.add(exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); - + 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) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; - + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); @@ -34,24 +34,24 @@ TEST(Z3SmtSolver, CheckSat) { TEST(Z3SmtSolver, CheckUnsat) { storm::solver::Z3SmtSolver s; storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - + storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); - + ASSERT_NO_THROW(s.add(!exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.reset()); - - + + 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(2) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; - + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); @@ -61,11 +61,11 @@ TEST(Z3SmtSolver, CheckUnsat) { TEST(Z3SmtSolver, Backtracking) { storm::solver::Z3SmtSolver s; storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - + storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue(); storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse(); - + ASSERT_NO_THROW(s.add(expr1)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); @@ -88,18 +88,18 @@ TEST(Z3SmtSolver, Backtracking) { ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); - - + + 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) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; storm::expressions::Expression exprFormula2 = a >= storm::expressions::Expression::createIntegerLiteral(2); - + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); @@ -115,18 +115,18 @@ TEST(Z3SmtSolver, Backtracking) { TEST(Z3SmtSolver, Assumptions) { storm::solver::Z3SmtSolver s; storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; - + 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) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); - + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); @@ -144,31 +144,29 @@ TEST(Z3SmtSolver, Assumptions) { TEST(Z3SmtSolver, GenerateModel) { storm::solver::Z3SmtSolver s; storm::solver::SmtSolver::CheckResult result; - + 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) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; - - (s.add(exprFormula)); - (result = s.check()); + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; + + s.add(exprFormula); + result = s.check(); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); - storm::expressions::SimpleValuation model; - (model = s.getModel()); - int_fast64_t a_eval; - (a_eval = model.getIntegerValue("a")); - ASSERT_EQ(1, a_eval); + std::shared_ptr model = s.getModel(); + int_fast64_t aEval = model->getIntegerValue("a"); + ASSERT_EQ(1, aEval); } TEST(Z3SmtSolver, AllSat) { storm::solver::Z3SmtSolver s; storm::solver::SmtSolver::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"); @@ -177,13 +175,13 @@ TEST(Z3SmtSolver, AllSat) { 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.add(exprFormula1)); - (s.add(exprFormula2)); - (s.add(exprFormula3)); - + + s.add(exprFormula1); + s.add(exprFormula2); + s.add(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); @@ -192,7 +190,7 @@ TEST(Z3SmtSolver, AllSat) { } 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"))); } @@ -202,15 +200,15 @@ TEST(Z3SmtSolver, AllSat) { TEST(Z3SmtSolver, UnsatAssumptions) { storm::solver::Z3SmtSolver s; storm::solver::SmtSolver::CheckResult result; - + 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) - && a < storm::expressions::Expression::createIntegerLiteral(5) - && b > storm::expressions::Expression::createIntegerLiteral(7) - && c == (a * b) - && b + a > c; + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2));