Browse Source

Further refactoring of MathSAT solver.

Former-commit-id: 317a9f9545
main
dehnert 11 years ago
parent
commit
81571878f7
  1. 22
      src/adapters/MathsatExpressionAdapter.h
  2. 2
      src/adapters/Z3ExpressionAdapter.h
  3. 158
      src/solver/MathsatSmtSolver.cpp
  4. 68
      src/solver/MathsatSmtSolver.h
  5. 12
      src/solver/SmtSolver.cpp
  6. 10
      src/solver/SmtSolver.h
  7. 10
      src/solver/Z3SmtSolver.cpp
  8. 6
      src/solver/Z3SmtSolver.h

22
src/adapters/MathSatExpressionAdapter.h → src/adapters/MathsatExpressionAdapter.h

@ -24,16 +24,16 @@
namespace storm { namespace storm {
namespace adapters { namespace adapters {
class MathSatExpressionAdapter : public storm::expressions::ExpressionVisitor {
class MathsatExpressionAdapter : public storm::expressions::ExpressionVisitor {
public: 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 * @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. * 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. * @param variableToDeclMap A mapping from variable names to their corresponding MathSAT Declarations.
*/ */
MathSatExpressionAdapter(msat_env& env, std::map<std::string, msat_decl> const& variableToDeclMap) : env(env), stack(), variableToDeclMap(variableToDeclMap) {
MathsatExpressionAdapter(msat_env& env, std::map<std::string, msat_decl> const& variableToDeclarationMap = std::map<std::string, msat_decl>()) : env(env), stack(), variableToDeclarationMap(variableToDeclarationMap) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -58,17 +58,17 @@ namespace storm {
} }
for (auto variableAndType : variables) { 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) switch (variableAndType.second)
{ {
case storm::expressions::ExpressionReturnType::Bool: 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; break;
case storm::expressions::ExpressionReturnType::Int: 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; break;
case storm::expressions::ExpressionReturnType::Double: 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; break;
default: default:
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first); 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 { 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 "<<expression->getVariableName()); //LOG4CPLUS_TRACE(logger, "Variable "<<expression->getVariableName());
//char* repr = msat_decl_repr(variableToDeclMap.at(expression->getVariableName())); //char* repr = msat_decl_repr(variableToDeclMap.at(expression->getVariableName()));
//LOG4CPLUS_TRACE(logger, "Decl: "<<repr); //LOG4CPLUS_TRACE(logger, "Decl: "<<repr);
//msat_free(repr); //msat_free(repr);
if (MSAT_ERROR_DECL(variableToDeclMap.at(expression->getVariableName()))) {
if (MSAT_ERROR_DECL(variableToDeclarationMap.at(expression->getVariableName()))) {
STORM_LOG_WARN("Encountered an invalid MathSAT declaration."); 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) { storm::expressions::Expression translateTerm(msat_term term) {
@ -394,7 +394,7 @@ namespace storm {
msat_env& env; msat_env& env;
std::stack<msat_term> stack; std::stack<msat_term> stack;
std::stack<expressions::Expression> expression_stack; std::stack<expressions::Expression> expression_stack;
std::map<std::string, msat_decl> variableToDeclMap;
std::map<std::string, msat_decl> variableToDeclarationMap;
}; };
} // namespace adapters } // namespace adapters

2
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. * 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. * @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions.
*/ */
Z3ExpressionAdapter(z3::context& context, std::map<std::string, z3::expr> const& variableToExpressionMap)
Z3ExpressionAdapter(z3::context& context, std::map<std::string, z3::expr> const& variableToExpressionMap = std::map<std::string, z3::expr>())
: context(context) : context(context)
, stack() , stack()
, additionalAssertions() , additionalAssertions()

158
src/solver/MathsatSmtSolver.cpp

@ -1,99 +1,92 @@
#include "src/solver/MathSatSmtSolver.h"
#include "src/solver/MathsatSmtSolver.h"
#include <vector> #include <vector>
#include "src/exceptions/UnexpectedException.h" #include "src/exceptions/UnexpectedException.h"
#include "src/exceptions/InvalidStateException.h"
namespace storm { namespace storm {
namespace solver { namespace solver {
MathSatSmtSolver::MathSatSmtSolver(Options options)
MathsatSmtSolver::MathsatSmtSolver(Options const& options)
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
: lastCheckAssumptions(false)
, lastResult(CheckResult::UNKNOWN)
: lastCheckAssumptions(false), lastResult(CheckResult::Unknown)
#endif #endif
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_config m_cfg = msat_create_config();
if (static_cast<int>(options)& static_cast<int>(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<storm::adapters::MathsatExpressionAdapter>(new storm::adapters::MathsatExpressionAdapter(env));
#endif #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 #ifdef STORM_HAVE_MSAT
msat_pop_backtrack_point(m_env);
msat_push_backtrack_point(env);
#else #else
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
#endif #endif
} }
void MathSatSmtSolver::pop(uint_fast64_t n)
{
void MathsatSmtSolver::pop() {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
for (uint_fast64_t i = 0; i < n; ++i) {
this->pop();
}
msat_pop_backtrack_point(env);
#else #else
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
#endif #endif
} }
void MathSatSmtSolver::reset()
void MathsatSmtSolver::reset()
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_reset_env(m_env);
msat_reset_env(env);
#else #else
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
#endif #endif
} }
void MathSatSmtSolver::assertExpression(storm::expressions::Expression const& e)
void MathsatSmtSolver::add(storm::expressions::Expression const& e)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_assert_formula(m_env, m_adapter->translateExpression(e, true));
msat_assert_formula(env, expressionAdapter->translateExpression(e, true));
#else #else
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
#endif #endif
} }
SmtSolver::CheckResult MathSatSmtSolver::check()
SmtSolver::CheckResult MathsatSmtSolver::check()
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
lastCheckAssumptions = false; lastCheckAssumptions = false;
switch (msat_solve(m_env)) {
switch (msat_solve(env)) {
case MSAT_SAT: case MSAT_SAT:
this->lastResult = SmtSolver::CheckResult::SAT;
this->lastResult = SmtSolver::CheckResult::Sat;
break; break;
case MSAT_UNSAT: case MSAT_UNSAT:
this->lastResult = SmtSolver::CheckResult::UNSAT;
this->lastResult = SmtSolver::CheckResult::Unsat;
break; break;
default: default:
this->lastResult = SmtSolver::CheckResult::UNKNOWN;
this->lastResult = SmtSolver::CheckResult::Unknown;
break; break;
} }
return this->lastResult; return this->lastResult;
@ -102,7 +95,7 @@ namespace storm {
#endif #endif
} }
SmtSolver::CheckResult MathSatSmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions)
SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
lastCheckAssumptions = true; lastCheckAssumptions = true;
@ -110,18 +103,18 @@ namespace storm {
mathSatAssumptions.reserve(assumptions.size()); mathSatAssumptions.reserve(assumptions.size());
for (storm::expressions::Expression assumption : assumptions) { 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: case MSAT_SAT:
this->lastResult = SmtSolver::CheckResult::SAT;
this->lastResult = SmtSolver::CheckResult::Sat;
break; break;
case MSAT_UNSAT: case MSAT_UNSAT:
this->lastResult = SmtSolver::CheckResult::UNSAT;
this->lastResult = SmtSolver::CheckResult::Unsat;
break; break;
default: default:
this->lastResult = SmtSolver::CheckResult::UNKNOWN;
this->lastResult = SmtSolver::CheckResult::Unknown;
break; break;
} }
return this->lastResult; return this->lastResult;
@ -130,7 +123,7 @@ namespace storm {
#endif #endif
} }
SmtSolver::CheckResult MathSatSmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions)
SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
lastCheckAssumptions = true; lastCheckAssumptions = true;
@ -138,18 +131,18 @@ namespace storm {
mathSatAssumptions.reserve(assumptions.size()); mathSatAssumptions.reserve(assumptions.size());
for (storm::expressions::Expression assumption : assumptions) { 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: case MSAT_SAT:
this->lastResult = SmtSolver::CheckResult::SAT;
this->lastResult = SmtSolver::CheckResult::Sat;
break; break;
case MSAT_UNSAT: case MSAT_UNSAT:
this->lastResult = SmtSolver::CheckResult::UNSAT;
this->lastResult = SmtSolver::CheckResult::Unsat;
break; break;
default: default:
this->lastResult = SmtSolver::CheckResult::UNKNOWN;
this->lastResult = SmtSolver::CheckResult::Unknown;
break; break;
} }
return this->lastResult; return this->lastResult;
@ -158,23 +151,22 @@ namespace storm {
#endif #endif
} }
storm::expressions::SimpleValuation MathSatSmtSolver::getModel()
storm::expressions::SimpleValuation MathsatSmtSolver::getModel()
{ {
#ifdef STORM_HAVE_MSAT #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 #else
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
#endif #endif
} }
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
storm::expressions::SimpleValuation MathSatSmtSolver::MathSatModelToStorm() {
storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() {
storm::expressions::SimpleValuation stormModel; 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."); 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_term t, v;
msat_model_iterator_next(model, &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)); char* name = msat_decl_get_name(msat_term_get_decl(t));
switch (var_i_interp.getReturnType()) { switch (var_i_interp.getReturnType()) {
@ -209,7 +201,7 @@ namespace storm {
} }
#endif #endif
std::vector<storm::expressions::SimpleValuation> MathSatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important)
std::vector<storm::expressions::SimpleValuation> MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
@ -229,13 +221,13 @@ namespace storm {
class AllsatValuationsCallbackUserData { class AllsatValuationsCallbackUserData {
public: public:
AllsatValuationsCallbackUserData(msat_env &env, AllsatValuationsCallbackUserData(msat_env &env,
storm::adapters::MathSatExpressionAdapter &adapter,
std::function<bool(storm::expressions::SimpleValuation&)> &callback)
storm::adapters::MathsatExpressionAdapter &adapter,
std::function<bool(storm::expressions::SimpleValuation&)> const& callback)
: env(env), adapter(adapter), callback(callback) { : env(env), adapter(adapter), callback(callback) {
} }
msat_env &env; msat_env &env;
storm::adapters::MathSatExpressionAdapter &adapter;
std::function<bool(storm::expressions::SimpleValuation&)> &callback;
storm::adapters::MathsatExpressionAdapter &adapter;
std::function<bool(storm::expressions::SimpleValuation&)> const& callback;
}; };
int allsatValuationsCallback(msat_term *model, int size, void *user_data) { int allsatValuationsCallback(msat_term *model, int size, void *user_data) {
@ -265,7 +257,7 @@ namespace storm {
#endif #endif
uint_fast64_t MathSatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback)
uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
std::vector<msat_term> msatImportant; std::vector<msat_term> msatImportant;
@ -275,11 +267,11 @@ namespace storm {
if (!e.isVariable()) { if (!e.isVariable()) {
throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions."; 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; return numModels;
#else #else
@ -287,7 +279,7 @@ namespace storm {
#endif #endif
} }
uint_fast64_t MathSatSmtSolver::allSat(std::function<bool(SmtSolver::ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important)
uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented.");
@ -296,9 +288,9 @@ namespace storm {
#endif #endif
} }
std::vector<storm::expressions::Expression> MathSatSmtSolver::getUnsatAssumptions() {
std::vector<storm::expressions::Expression> MathsatSmtSolver::getUnsatAssumptions() {
#ifdef STORM_HAVE_MSAT #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."; throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last state is not unsat.";
} }
if (!lastCheckAssumptions) { if (!lastCheckAssumptions) {
@ -306,13 +298,13 @@ namespace storm {
} }
size_t numUnsatAssumpations; size_t numUnsatAssumpations;
msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(m_env, &numUnsatAssumpations);
msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(env, &numUnsatAssumpations);
std::vector<storm::expressions::Expression> unsatAssumptions; std::vector<storm::expressions::Expression> unsatAssumptions;
unsatAssumptions.reserve(numUnsatAssumpations); unsatAssumptions.reserve(numUnsatAssumpations);
for (unsigned int i = 0; i < numUnsatAssumpations; ++i) { 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; return unsatAssumptions;
@ -321,26 +313,26 @@ namespace storm {
#endif #endif
} }
void MathSatSmtSolver::setInterpolationGroup(uint_fast64_t group) {
void MathsatSmtSolver::setInterpolationGroup(uint_fast64_t group) {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
auto groupIter = this->interpolationGroups.find(group); auto groupIter = this->interpolationGroups.find(group);
if( groupIter == this->interpolationGroups.end() ) { 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)); auto insertResult = this->interpolationGroups.insert(std::make_pair(group, newGroup));
if (!insertResult.second) { if (!insertResult.second) {
throw storm::exceptions::InvalidStateException() << "Internal error in MathSAT wrapper: Unable to insert newly created interpolation group."; throw storm::exceptions::InvalidStateException() << "Internal error in MathSAT wrapper: Unable to insert newly created interpolation group.";
} }
groupIter = insertResult.first; groupIter = insertResult.first;
} }
msat_set_itp_group(m_env, groupIter->second);
msat_set_itp_group(env, groupIter->second);
#else #else
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
#endif #endif
} }
storm::expressions::Expression MathSatSmtSolver::getInterpolant(std::vector<uint_fast64_t> groupsA) {
storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector<uint_fast64_t> const& groupsA) {
#ifdef STORM_HAVE_MSAT #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."; throw storm::exceptions::InvalidStateException() << "getInterpolant was called but last state is not unsat.";
} }
if (lastCheckAssumptions) { if (lastCheckAssumptions) {
@ -356,11 +348,11 @@ namespace storm {
} }
msatInterpolationGroupsA.push_back(groupIter->second); 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."); 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 #else
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
#endif #endif

68
src/solver/MathsatSmtSolver.h

@ -3,7 +3,7 @@
#include "storm-config.h" #include "storm-config.h"
#include "src/solver/SmtSolver.h" #include "src/solver/SmtSolver.h"
#include "src/adapters/MathSatExpressionAdapter.h"
#include "src/adapters/MathsatExpressionAdapter.h"
#include <boost/container/flat_map.hpp> #include <boost/container/flat_map.hpp>
#ifndef STORM_HAVE_MSAT #ifndef STORM_HAVE_MSAT
@ -16,12 +16,23 @@
namespace storm { namespace storm {
namespace solver { namespace solver {
class MathSatSmtSolver : public SmtSolver {
class MathsatSmtSolver : public SmtSolver {
public: 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 { 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 enableModelGeneration = false;
bool enableUnsatCoreGeneration = false; bool enableUnsatCoreGeneration = false;
bool enableInterpolantGeneration = false; bool enableInterpolantGeneration = false;
@ -30,65 +41,72 @@ namespace storm {
class MathSatModelReference : public SmtSolver::ModelReference { class MathSatModelReference : public SmtSolver::ModelReference {
public: public:
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
MathSatModelReference(msat_env& env, storm::adapters::MathSatExpressionAdapter &adapter);
MathSatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& adapter);
#endif #endif
virtual bool getBooleanValue(std::string const& name) const override; virtual bool getBooleanValue(std::string const& name) const override;
virtual int_fast64_t getIntegerValue(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: private:
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_env& env;
storm::adapters::MathSatExpressionAdapter &m_adapter;
msat_env const& env;
storm::adapters::MathsatExpressionAdapter& expressionAdapter;
#endif #endif
}; };
public: public:
MathSatSmtSolver(Options options = Options::ModelGeneration);
virtual ~MathSatSmtSolver();
MathsatSmtSolver(Options const& options = Options());
virtual ~MathsatSmtSolver();
virtual void push() override; virtual void push() override;
virtual void pop() override; virtual void pop() override;
virtual void pop(uint_fast64_t n) override;
virtual void reset() 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 check() override;
virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override; virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) override;
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
virtual storm::expressions::SimpleValuation getModel() override; virtual storm::expressions::SimpleValuation getModel() override;
virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) override; virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) override;
virtual uint_fast64_t allSat(std::function<bool(ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> const& callback) override;
virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override; virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;
virtual void setInterpolationGroup(uint_fast64_t group) override; virtual void setInterpolationGroup(uint_fast64_t group) override;
virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> groupsA) override;
virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> const& groupsA) override;
protected:
#ifdef STORM_HAVE_MSAT
virtual storm::expressions::SimpleValuation MathSatModelToStorm();
#endif
private: private:
#ifdef STORM_HAVE_MSAT #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<storm::adapters::MathsatExpressionAdapter> expressionAdapter;
// A flag storing whether the last call was a check involving assumptions.
bool lastCheckAssumptions; bool lastCheckAssumptions;
// The result of the last call to any of the check methods.
CheckResult lastResult; CheckResult lastResult;
typedef boost::container::flat_map<uint_fast64_t, int> InterpolationGroupMap;
InterpolationGroupMap interpolationGroups;
std::map<std::string, msat_decl> variableToDeclMap;
// A mapping of interpolation group indices to their MathSAT identifier.
typedef boost::container::flat_map<uint_fast64_t, int> InterpolationGroupMapType;
InterpolationGroupMapType interpolationGroups;
#endif #endif
}; };
} }

12
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::expressions::SimpleValuation SmtSolver::getModel() {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); 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."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation.");
} }
uint_fast64_t SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) {
uint_fast64_t SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation.");
} }
uint_fast64_t SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> callback) {
uint_fast64_t SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> const& callback) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); 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_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants.");
} }
storm::expressions::Expression SmtSolver::getInterpolant(std::vector<uint_fast64_t> groupsA) {
storm::expressions::Expression SmtSolver::getInterpolant(std::vector<uint_fast64_t> const& groupsA) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants.");
} }

10
src/solver/SmtSolver.h

@ -69,7 +69,7 @@ namespace storm {
* *
* @param n The number of backtracking points to pop. * @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. * 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 * @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. * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability.
*/ */
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) = 0;
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) = 0;
/*! /*!
* If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that * 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. * @return The number of models of the important atoms that where found.
*/ */
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback);
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback);
/*! /*!
* Performs AllSat over the (provided) important atoms. That is, this function determines all models of the * 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. * @return The number of models of the important atoms that where found.
*/ */
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> callback);
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> const& callback);
/*! /*!
* If the last call to check() returned Unsat, this function can be used to retrieve the unsatisfiable core * 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 * @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. * conjunction of I and B is inconsistent.
*/ */
virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> groupsA);
virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> const& groupsA);
}; };
} }
} }

10
src/solver/Z3SmtSolver.cpp

@ -43,11 +43,7 @@ namespace storm {
Z3SmtSolver::Z3SmtSolver() Z3SmtSolver::Z3SmtSolver()
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
: context()
, solver(context)
, expressionAdapter(context, std::map<std::string, z3::expr>())
, lastCheckAssumptions(false)
, lastResult(CheckResult::Unknown)
: context(), solver(context), expressionAdapter(context), lastCheckAssumptions(false), lastResult(CheckResult::Unknown)
#endif #endif
{ {
// Intentionally left empty. // Intentionally left empty.
@ -227,7 +223,7 @@ namespace storm {
#endif #endif
} }
uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback)
uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback)
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
for (storm::expressions::Expression const& atom : important) { for (storm::expressions::Expression const& atom : important) {
@ -278,7 +274,7 @@ namespace storm {
#endif #endif
} }
uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(SmtSolver::ModelReference&)> callback)
uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback)
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
for (storm::expressions::Expression const& atom : important) { for (storm::expressions::Expression const& atom : important) {

6
src/solver/Z3SmtSolver.h

@ -50,15 +50,15 @@ namespace storm {
virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override; virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) override;
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
virtual storm::expressions::SimpleValuation getModel() override; virtual storm::expressions::SimpleValuation getModel() override;
virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) override; virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> callback) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> const& callback) override;
virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override; virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;

Loading…
Cancel
Save