diff --git a/src/adapters/MathSatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h similarity index 92% rename from src/adapters/MathSatExpressionAdapter.h rename to src/adapters/MathsatExpressionAdapter.h index 7b12967fd..3b6005847 100644 --- a/src/adapters/MathSatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -24,16 +24,16 @@ namespace storm { namespace adapters { - class MathSatExpressionAdapter : public storm::expressions::ExpressionVisitor { + class MathsatExpressionAdapter : public storm::expressions::ExpressionVisitor { public: /*! - * Creates a MathSatExpressionAdapter over the given MathSAT enviroment. + * Creates a MathsatExpressionAdapter over the given MathSAT enviroment. * * @param context A reference to the MathSAT enviroment over which to build the expressions. Be careful to guarantee * the lifetime of the context as long as the instance of this adapter is used. * @param variableToDeclMap A mapping from variable names to their corresponding MathSAT Declarations. */ - MathSatExpressionAdapter(msat_env& env, std::map const& variableToDeclMap) : env(env), stack(), variableToDeclMap(variableToDeclMap) { + MathsatExpressionAdapter(msat_env& env, std::map const& variableToDeclarationMap = std::map()) : env(env), stack(), variableToDeclarationMap(variableToDeclarationMap) { // Intentionally left empty. } @@ -58,17 +58,17 @@ namespace storm { } for (auto variableAndType : variables) { - if (this->variableToDeclMap.find(variableAndType.first) == this->variableToDeclMap.end()) { + if (this->variableToDeclarationMap.find(variableAndType.first) == this->variableToDeclarationMap.end()) { switch (variableAndType.second) { case storm::expressions::ExpressionReturnType::Bool: - this->variableToDeclMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_bool_type(env)))); + this->variableToDeclarationMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_bool_type(env)))); break; case storm::expressions::ExpressionReturnType::Int: - this->variableToDeclMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_integer_type(env)))); + this->variableToDeclarationMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_integer_type(env)))); break; case storm::expressions::ExpressionReturnType::Double: - this->variableToDeclMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_rational_type(env)))); + this->variableToDeclarationMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_rational_type(env)))); break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first); @@ -260,15 +260,15 @@ namespace storm { } virtual void visit(expressions::VariableExpression const* expression) override { - STORM_LOG_THROW(variableToDeclMap.count(expression->getVariableName()) != 0, storm::exceptions::InvalidArgumentException, "Variable '" << expression->getVariableName() << "' is unknown."); + STORM_LOG_THROW(variableToDeclarationMap.count(expression->getVariableName()) != 0, storm::exceptions::InvalidArgumentException, "Variable '" << expression->getVariableName() << "' is unknown."); //LOG4CPLUS_TRACE(logger, "Variable "<getVariableName()); //char* repr = msat_decl_repr(variableToDeclMap.at(expression->getVariableName())); //LOG4CPLUS_TRACE(logger, "Decl: "<getVariableName()))) { + if (MSAT_ERROR_DECL(variableToDeclarationMap.at(expression->getVariableName()))) { STORM_LOG_WARN("Encountered an invalid MathSAT declaration."); } - stack.push(msat_make_constant(env, variableToDeclMap.at(expression->getVariableName()))); + stack.push(msat_make_constant(env, variableToDeclarationMap.at(expression->getVariableName()))); } storm::expressions::Expression translateTerm(msat_term term) { @@ -394,7 +394,7 @@ namespace storm { msat_env& env; std::stack stack; std::stack expression_stack; - std::map variableToDeclMap; + std::map variableToDeclarationMap; }; } // namespace adapters diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 4c162378f..8590e22c3 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -39,7 +39,7 @@ namespace storm { * the lifetime of the context as long as the instance of this adapter is used. * @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions. */ - Z3ExpressionAdapter(z3::context& context, std::map const& variableToExpressionMap) + Z3ExpressionAdapter(z3::context& context, std::map const& variableToExpressionMap = std::map()) : context(context) , stack() , additionalAssertions() diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 278ed2b3b..2fc22103a 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -1,99 +1,92 @@ -#include "src/solver/MathSatSmtSolver.h" +#include "src/solver/MathsatSmtSolver.h" #include #include "src/exceptions/UnexpectedException.h" +#include "src/exceptions/InvalidStateException.h" namespace storm { namespace solver { - MathSatSmtSolver::MathSatSmtSolver(Options options) + MathsatSmtSolver::MathsatSmtSolver(Options const& options) #ifdef STORM_HAVE_MSAT - : lastCheckAssumptions(false) - , lastResult(CheckResult::UNKNOWN) + : lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif { #ifdef STORM_HAVE_MSAT - msat_config m_cfg = msat_create_config(); - - if (static_cast(options)& static_cast(Options::InterpolantComputation)) { - msat_set_option(m_cfg, "interpolation", "true"); + msat_config config = msat_create_config(); + if (options.enableInterpolantGeneration) { + msat_set_option(config, "interpolation", "true"); } + if (options.enableModelGeneration) { + msat_set_option(config, "model_generation", "true"); + } + if (options.enableUnsatCoreGeneration) { + msat_set_option(config, "unsat_core_generation", "true"); + } + STORM_LOG_THROW(!MSAT_ERROR_CONFIG(config), storm::exceptions::UnexpectedException, "Unable to create Mathsat configuration."); - msat_set_option(m_cfg, "model_generation", "true"); - - m_env = msat_create_env(m_cfg); - STORM_LOG_THROW(!MSAT_ERROR_ENV(m_env), storm::exceptions::UnexpectedException, "Unable to create Mathsat environment."); - - msat_destroy_config(m_cfg); + // Based on the configuration, build the environment, check for errors and destroy the configuration. + env = msat_create_env(config); + STORM_LOG_THROW(!MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Unable to create Mathsat environment."); + msat_destroy_config(config); - m_adapter = new storm::adapters::MathSatExpressionAdapter(m_env, variableToDeclMap); + expressionAdapter = std::unique_ptr(new storm::adapters::MathsatExpressionAdapter(env)); #endif } - MathSatSmtSolver::~MathSatSmtSolver() { - msat_destroy_env(m_env); - }; - - void MathSatSmtSolver::push() - { -#ifdef STORM_HAVE_MSAT - msat_push_backtrack_point(m_env); -#else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); -#endif + + MathsatSmtSolver::~MathsatSmtSolver() { + STORM_LOG_THROW(MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Illegal MathSAT environment."); + msat_destroy_env(env); } - void MathSatSmtSolver::pop() - { + void MathsatSmtSolver::push() { #ifdef STORM_HAVE_MSAT - msat_pop_backtrack_point(m_env); + msat_push_backtrack_point(env); #else STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } - void MathSatSmtSolver::pop(uint_fast64_t n) - { + void MathsatSmtSolver::pop() { #ifdef STORM_HAVE_MSAT - for (uint_fast64_t i = 0; i < n; ++i) { - this->pop(); - } + msat_pop_backtrack_point(env); #else STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } - void MathSatSmtSolver::reset() + void MathsatSmtSolver::reset() { #ifdef STORM_HAVE_MSAT - msat_reset_env(m_env); + msat_reset_env(env); #else STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } - void MathSatSmtSolver::assertExpression(storm::expressions::Expression const& e) + void MathsatSmtSolver::add(storm::expressions::Expression const& e) { #ifdef STORM_HAVE_MSAT - msat_assert_formula(m_env, m_adapter->translateExpression(e, true)); + msat_assert_formula(env, expressionAdapter->translateExpression(e, true)); #else STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } - SmtSolver::CheckResult MathSatSmtSolver::check() + SmtSolver::CheckResult MathsatSmtSolver::check() { #ifdef STORM_HAVE_MSAT lastCheckAssumptions = false; - switch (msat_solve(m_env)) { + switch (msat_solve(env)) { case MSAT_SAT: - this->lastResult = SmtSolver::CheckResult::SAT; + this->lastResult = SmtSolver::CheckResult::Sat; break; case MSAT_UNSAT: - this->lastResult = SmtSolver::CheckResult::UNSAT; + this->lastResult = SmtSolver::CheckResult::Unsat; break; default: - this->lastResult = SmtSolver::CheckResult::UNKNOWN; + this->lastResult = SmtSolver::CheckResult::Unknown; break; } return this->lastResult; @@ -102,7 +95,7 @@ namespace storm { #endif } - SmtSolver::CheckResult MathSatSmtSolver::checkWithAssumptions(std::set const& assumptions) + SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::set const& assumptions) { #ifdef STORM_HAVE_MSAT lastCheckAssumptions = true; @@ -110,18 +103,18 @@ namespace storm { mathSatAssumptions.reserve(assumptions.size()); for (storm::expressions::Expression assumption : assumptions) { - mathSatAssumptions.push_back(this->m_adapter->translateExpression(assumption)); + mathSatAssumptions.push_back(this->expressionAdapter->translateExpression(assumption)); } - switch (msat_solve_with_assumptions(m_env, mathSatAssumptions.data(), mathSatAssumptions.size())) { + switch (msat_solve_with_assumptions(env, mathSatAssumptions.data(), mathSatAssumptions.size())) { case MSAT_SAT: - this->lastResult = SmtSolver::CheckResult::SAT; + this->lastResult = SmtSolver::CheckResult::Sat; break; case MSAT_UNSAT: - this->lastResult = SmtSolver::CheckResult::UNSAT; + this->lastResult = SmtSolver::CheckResult::Unsat; break; default: - this->lastResult = SmtSolver::CheckResult::UNKNOWN; + this->lastResult = SmtSolver::CheckResult::Unknown; break; } return this->lastResult; @@ -130,7 +123,7 @@ namespace storm { #endif } - SmtSolver::CheckResult MathSatSmtSolver::checkWithAssumptions(std::initializer_list assumptions) + SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_MSAT lastCheckAssumptions = true; @@ -138,18 +131,18 @@ namespace storm { mathSatAssumptions.reserve(assumptions.size()); for (storm::expressions::Expression assumption : assumptions) { - mathSatAssumptions.push_back(this->m_adapter->translateExpression(assumption)); + mathSatAssumptions.push_back(this->expressionAdapter->translateExpression(assumption)); } - switch (msat_solve_with_assumptions(m_env, mathSatAssumptions.data(), mathSatAssumptions.size())) { + switch (msat_solve_with_assumptions(env, mathSatAssumptions.data(), mathSatAssumptions.size())) { case MSAT_SAT: - this->lastResult = SmtSolver::CheckResult::SAT; + this->lastResult = SmtSolver::CheckResult::Sat; break; case MSAT_UNSAT: - this->lastResult = SmtSolver::CheckResult::UNSAT; + this->lastResult = SmtSolver::CheckResult::Unsat; break; default: - this->lastResult = SmtSolver::CheckResult::UNKNOWN; + this->lastResult = SmtSolver::CheckResult::Unknown; break; } return this->lastResult; @@ -158,23 +151,22 @@ namespace storm { #endif } - storm::expressions::SimpleValuation MathSatSmtSolver::getModel() + storm::expressions::SimpleValuation MathsatSmtSolver::getModel() { #ifdef STORM_HAVE_MSAT - STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT."); - - return this->MathSatModelToStorm(); + STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT."); + return this->convertMathsatModelToValuation(); #else STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } #ifdef STORM_HAVE_MSAT - storm::expressions::SimpleValuation MathSatSmtSolver::MathSatModelToStorm() { + storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() { storm::expressions::SimpleValuation stormModel; - msat_model_iterator model = msat_create_model_iterator(m_env); + msat_model_iterator model = msat_create_model_iterator(env); STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(model), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator."); @@ -182,7 +174,7 @@ namespace storm { msat_term t, v; msat_model_iterator_next(model, &t, &v); - storm::expressions::Expression var_i_interp = this->m_adapter->translateTerm(v); + storm::expressions::Expression var_i_interp = this->expressionAdapter->translateTerm(v); char* name = msat_decl_get_name(msat_term_get_decl(t)); switch (var_i_interp.getReturnType()) { @@ -209,7 +201,7 @@ namespace storm { } #endif - std::vector MathSatSmtSolver::allSat(std::vector const& important) + std::vector MathsatSmtSolver::allSat(std::vector const& important) { #ifdef STORM_HAVE_MSAT @@ -229,13 +221,13 @@ namespace storm { class AllsatValuationsCallbackUserData { public: AllsatValuationsCallbackUserData(msat_env &env, - storm::adapters::MathSatExpressionAdapter &adapter, - std::function &callback) + storm::adapters::MathsatExpressionAdapter &adapter, + std::function const& callback) : env(env), adapter(adapter), callback(callback) { } msat_env &env; - storm::adapters::MathSatExpressionAdapter &adapter; - std::function &callback; + storm::adapters::MathsatExpressionAdapter &adapter; + std::function const& callback; }; int allsatValuationsCallback(msat_term *model, int size, void *user_data) { @@ -265,7 +257,7 @@ namespace storm { #endif - uint_fast64_t MathSatSmtSolver::allSat(std::vector const& important, std::function callback) + uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT std::vector msatImportant; @@ -275,11 +267,11 @@ namespace storm { if (!e.isVariable()) { throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions."; } - msatImportant.push_back(m_adapter->translateExpression(e)); + msatImportant.push_back(expressionAdapter->translateExpression(e)); } - AllsatValuationsCallbackUserData allSatUserData(m_env, *m_adapter, callback); - int numModels = msat_all_sat(m_env, msatImportant.data(), msatImportant.size(), &allsatValuationsCallback, &allSatUserData); + AllsatValuationsCallbackUserData allSatUserData(env, *expressionAdapter, callback); + int numModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &allsatValuationsCallback, &allSatUserData); return numModels; #else @@ -287,7 +279,7 @@ namespace storm { #endif } - uint_fast64_t MathSatSmtSolver::allSat(std::function callback, std::vector const& important) + uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented."); @@ -296,9 +288,9 @@ namespace storm { #endif } - std::vector MathSatSmtSolver::getUnsatAssumptions() { + std::vector MathsatSmtSolver::getUnsatAssumptions() { #ifdef STORM_HAVE_MSAT - if (lastResult != SmtSolver::CheckResult::UNSAT) { + if (lastResult != SmtSolver::CheckResult::Unsat) { throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last state is not unsat."; } if (!lastCheckAssumptions) { @@ -306,13 +298,13 @@ namespace storm { } size_t numUnsatAssumpations; - msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(m_env, &numUnsatAssumpations); + msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(env, &numUnsatAssumpations); std::vector unsatAssumptions; unsatAssumptions.reserve(numUnsatAssumpations); for (unsigned int i = 0; i < numUnsatAssumpations; ++i) { - unsatAssumptions.push_back(this->m_adapter->translateTerm(msatUnsatAssumptions[i])); + unsatAssumptions.push_back(this->expressionAdapter->translateTerm(msatUnsatAssumptions[i])); } return unsatAssumptions; @@ -321,26 +313,26 @@ namespace storm { #endif } - void MathSatSmtSolver::setInterpolationGroup(uint_fast64_t group) { + void MathsatSmtSolver::setInterpolationGroup(uint_fast64_t group) { #ifdef STORM_HAVE_MSAT auto groupIter = this->interpolationGroups.find(group); if( groupIter == this->interpolationGroups.end() ) { - int newGroup = msat_create_itp_group(m_env); + int newGroup = msat_create_itp_group(env); auto insertResult = this->interpolationGroups.insert(std::make_pair(group, newGroup)); if (!insertResult.second) { throw storm::exceptions::InvalidStateException() << "Internal error in MathSAT wrapper: Unable to insert newly created interpolation group."; } groupIter = insertResult.first; } - msat_set_itp_group(m_env, groupIter->second); + msat_set_itp_group(env, groupIter->second); #else STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } - storm::expressions::Expression MathSatSmtSolver::getInterpolant(std::vector groupsA) { + storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector const& groupsA) { #ifdef STORM_HAVE_MSAT - if (lastResult != SmtSolver::CheckResult::UNSAT) { + if (lastResult != SmtSolver::CheckResult::Unsat) { throw storm::exceptions::InvalidStateException() << "getInterpolant was called but last state is not unsat."; } if (lastCheckAssumptions) { @@ -356,11 +348,11 @@ namespace storm { } msatInterpolationGroupsA.push_back(groupIter->second); } - msat_term interpolant = msat_get_interpolant(m_env, msatInterpolationGroupsA.data(), msatInterpolationGroupsA.size()); + msat_term interpolant = msat_get_interpolant(env, msatInterpolationGroupsA.data(), msatInterpolationGroupsA.size()); STORM_LOG_THROW(!MSAT_ERROR_TERM(interpolant), storm::exceptions::UnexpectedException, "Unable to retrieve an interpolant."); - return this->m_adapter->translateTerm(interpolant); + return this->expressionAdapter->translateTerm(interpolant); #else STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index 4cea5f5ee..4cff5f4f1 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -3,7 +3,7 @@ #include "storm-config.h" #include "src/solver/SmtSolver.h" -#include "src/adapters/MathSatExpressionAdapter.h" +#include "src/adapters/MathsatExpressionAdapter.h" #include #ifndef STORM_HAVE_MSAT @@ -16,12 +16,23 @@ namespace storm { namespace solver { - class MathSatSmtSolver : public SmtSolver { + class MathsatSmtSolver : public SmtSolver { public: /*! - * A class that captures options that may be passed to Mathsat solver. + * A class that captures options that may be passed to the Mathsat solver. Settings these options has some + * implications due to the implementation of MathSAT. For example, enabling interpolation means that the + * solver must not be used for checking satisfiable formulas. */ 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) { + // Intentionally left empty. + } + bool enableModelGeneration = false; bool enableUnsatCoreGeneration = false; bool enableInterpolantGeneration = false; @@ -30,65 +41,72 @@ namespace storm { class MathSatModelReference : public SmtSolver::ModelReference { public: #ifdef STORM_HAVE_MSAT - MathSatModelReference(msat_env& env, storm::adapters::MathSatExpressionAdapter &adapter); + MathSatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& adapter); #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& env; - storm::adapters::MathSatExpressionAdapter &m_adapter; + msat_env const& env; + storm::adapters::MathsatExpressionAdapter& expressionAdapter; #endif }; + public: - MathSatSmtSolver(Options options = Options::ModelGeneration); - virtual ~MathSatSmtSolver(); + MathsatSmtSolver(Options const& options = Options()); + + virtual ~MathsatSmtSolver(); virtual void push() override; virtual void pop() override; - virtual void pop(uint_fast64_t n) override; - virtual void reset() override; - virtual void assertExpression(storm::expressions::Expression const& e) override; + virtual void add(storm::expressions::Expression const& assertion) override; virtual CheckResult check() override; virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; - virtual CheckResult checkWithAssumptions(std::initializer_list assumptions) override; + virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; virtual storm::expressions::SimpleValuation getModel() override; virtual std::vector allSat(std::vector const& important) override; - virtual uint_fast64_t allSat(std::vector const& important, std::function callback) override; + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; - virtual uint_fast64_t allSat(std::function callback, std::vector const& important) override; + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; virtual std::vector getUnsatAssumptions() override; virtual void setInterpolationGroup(uint_fast64_t group) override; - virtual storm::expressions::Expression getInterpolant(std::vector groupsA) override; + virtual storm::expressions::Expression getInterpolant(std::vector const& groupsA) override; - protected: -#ifdef STORM_HAVE_MSAT - virtual storm::expressions::SimpleValuation MathSatModelToStorm(); -#endif private: - #ifdef STORM_HAVE_MSAT - msat_env m_env; - storm::adapters::MathSatExpressionAdapter *m_adapter; + storm::expressions::SimpleValuation convertMathsatModelToValuation(); + + // The MathSAT environment. + msat_env env; + + // The expression adapter used to translate expressions to MathSAT's format. This has to be a pointer, since + // it must be initialized after creating the environment, but the adapter class has no default constructor. + std::unique_ptr expressionAdapter; + // A flag storing whether the last call was a check involving assumptions. bool lastCheckAssumptions; + + // The result of the last call to any of the check methods. CheckResult lastResult; - typedef boost::container::flat_map InterpolationGroupMap; - InterpolationGroupMap interpolationGroups; - std::map variableToDeclMap; + + // A mapping of interpolation group indices to their MathSAT identifier. + typedef boost::container::flat_map InterpolationGroupMapType; + InterpolationGroupMapType interpolationGroups; #endif }; } diff --git a/src/solver/SmtSolver.cpp b/src/solver/SmtSolver.cpp index caaeae5d6..bfd699be4 100644 --- a/src/solver/SmtSolver.cpp +++ b/src/solver/SmtSolver.cpp @@ -26,6 +26,12 @@ namespace storm { } } + void SmtSolver::pop(uint_fast64_t n) { + for (uint_fast64_t i = 0; i < n; ++i) { + this->pop(); + } + } + storm::expressions::SimpleValuation SmtSolver::getModel() { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } @@ -34,11 +40,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } - uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function callback) { + uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function const& callback) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } - uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function callback) { + uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function const& callback) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } @@ -54,7 +60,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); } - storm::expressions::Expression SmtSolver::getInterpolant(std::vector groupsA) { + storm::expressions::Expression SmtSolver::getInterpolant(std::vector const& groupsA) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); } diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index ae556f278..83c3cff71 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -69,7 +69,7 @@ namespace storm { * * @param n The number of backtracking points to pop. */ - virtual void pop(uint_fast64_t n) = 0; + virtual void pop(uint_fast64_t n); /*! * Removes all assertions from the solver's stack. @@ -125,7 +125,7 @@ namespace storm { * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability. */ - virtual CheckResult checkWithAssumptions(std::initializer_list assumptions) = 0; + virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) = 0; /*! * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that @@ -159,7 +159,7 @@ namespace storm { * * @return The number of models of the important atoms that where found. */ - virtual uint_fast64_t allSat(std::vector const& important, std::function callback); + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback); /*! * Performs AllSat over the (provided) important atoms. That is, this function determines all models of the @@ -172,7 +172,7 @@ namespace storm { * * @return The number of models of the important atoms that where found. */ - virtual uint_fast64_t allSat(std::vector const& important, std::function callback); + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback); /*! * If the last call to check() returned Unsat, this function can be used to retrieve the unsatisfiable core @@ -217,7 +217,7 @@ namespace storm { * @return The interpolant for the formulas (A, B), i.e. an expression I that is implied by A but the * conjunction of I and B is inconsistent. */ - virtual storm::expressions::Expression getInterpolant(std::vector groupsA); + virtual storm::expressions::Expression getInterpolant(std::vector const& groupsA); }; } } diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 28ad16c86..17360d2a5 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -43,11 +43,7 @@ namespace storm { Z3SmtSolver::Z3SmtSolver() #ifdef STORM_HAVE_Z3 - : context() - , solver(context) - , expressionAdapter(context, std::map()) - , lastCheckAssumptions(false) - , lastResult(CheckResult::Unknown) + : context(), solver(context), expressionAdapter(context), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif { // Intentionally left empty. @@ -227,7 +223,7 @@ namespace storm { #endif } - uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function callback) + uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_Z3 for (storm::expressions::Expression const& atom : important) { @@ -278,7 +274,7 @@ namespace storm { #endif } - uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function callback) + uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_Z3 for (storm::expressions::Expression const& atom : important) { diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index b389f7dfc..0984aa2df 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -50,15 +50,15 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; - virtual CheckResult checkWithAssumptions(std::initializer_list assumptions) override; + virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; virtual storm::expressions::SimpleValuation getModel() override; virtual std::vector allSat(std::vector const& important) override; - virtual uint_fast64_t allSat(std::vector const& important, std::function callback) override; + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; - virtual uint_fast64_t allSat(std::vector const& important, std::function callback) override; + virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; virtual std::vector getUnsatAssumptions() override;