Browse Source
Initial MathSat integration.
Initial MathSat integration.
Expression adapter, solving, unsat assumptions implemented
cmake and tests missing
allsat and interpolation not yet implemented
Former-commit-id: 5177775fbe
main
David_Korzeniewski
11 years ago
3 changed files with 775 additions and 0 deletions
-
370src/adapters/MathSatExpressionAdapter.h
-
321src/solver/MathSatSmtSolver.cpp
-
84src/solver/MathSatSmtSolver.h
@ -0,0 +1,370 @@ |
|||
/* |
|||
* MathSatExpressionAdapter.h |
|||
* |
|||
* Author: David Korzeniewski |
|||
*/ |
|||
|
|||
#ifndef STORM_ADAPTERS_MATHSATEXPRESSIONADAPTER_H_ |
|||
#define STORM_ADAPTERS_MATHSATEXPRESSIONADAPTER_H_ |
|||
|
|||
#include "storm-config.h" |
|||
|
|||
#include <stack> |
|||
|
|||
#include "mathsat.h" |
|||
|
|||
#include "storage/expressions/Expressions.h" |
|||
#include "storage/expressions/ExpressionVisitor.h" |
|||
#include "src/exceptions/ExceptionMacros.h" |
|||
#include "src/exceptions/ExpressionEvaluationException.h" |
|||
#include "src/exceptions/InvalidTypeException.h" |
|||
#include "src/exceptions/NotImplementedException.h" |
|||
|
|||
namespace storm { |
|||
namespace adapters { |
|||
|
|||
class MathSatExpressionAdapter : public storm::expressions::ExpressionVisitor { |
|||
public: |
|||
/*! |
|||
* 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<std::string, msat_decl> const& variableToDeclMap) : env(env), stack(), variableToDeclMap(variableToDeclMap) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Translates the given expression to an equivalent term for MathSAT. |
|||
* |
|||
* @param expression The expression to translate. |
|||
* @param createMathSatVariables If set to true a solver variable is created for each variable in expression that is not |
|||
* yet known to the adapter. (i.e. values from the variableToExpressionMap passed to the constructor |
|||
* are not overwritten) |
|||
* @return An equivalent term for MathSAT. |
|||
*/ |
|||
msat_term translateExpression(storm::expressions::Expression const& expression, bool createMathSatVariables = false) { |
|||
//LOG4CPLUS_TRACE(logger, "Translating expression:\n" << expression->toString()); |
|||
expression.accept(this); |
|||
msat_term result = stack.top(); |
|||
stack.pop(); |
|||
if (MSAT_ERROR_TERM(result)) { |
|||
//LOG4CPLUS_WARN(logger, "Translating term to MathSAT returned an error!"); |
|||
} |
|||
|
|||
char* repr = msat_term_repr(result); |
|||
//LOG4CPLUS_TRACE(logger, "Result is:\n" << repr); |
|||
msat_free(repr); |
|||
return result; |
|||
} |
|||
|
|||
virtual void visit(expressions::BinaryBooleanFunctionExpression const* expression) override { |
|||
expression->getFirstOperand()->accept(this); |
|||
expression->getSecondOperand()->accept(this); |
|||
|
|||
msat_term rightResult = stack.top(); |
|||
stack.pop(); |
|||
msat_term leftResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
//char* repr = msat_term_repr(leftResult); |
|||
//LOG4CPLUS_TRACE(logger, "LHS: "<<repr); |
|||
//msat_free(repr); |
|||
//repr = msat_term_repr(rightResult); |
|||
//LOG4CPLUS_TRACE(logger, "RHS: "<<repr); |
|||
//msat_free(repr); |
|||
|
|||
switch (expression->getOperatorType()) { |
|||
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: |
|||
stack.push(msat_make_and(env, leftResult, rightResult)); |
|||
break; |
|||
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: |
|||
stack.push(msat_make_or(env, leftResult, rightResult)); |
|||
break; |
|||
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: |
|||
stack.push(msat_make_iff(env, leftResult, rightResult)); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; |
|||
} |
|||
|
|||
} |
|||
|
|||
virtual void visit(expressions::BinaryNumericalFunctionExpression const* expression) override { |
|||
expression->getFirstOperand()->accept(this); |
|||
expression->getSecondOperand()->accept(this); |
|||
|
|||
msat_term rightResult = stack.top(); |
|||
stack.pop(); |
|||
msat_term leftResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch (expression->getOperatorType()) { |
|||
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: |
|||
stack.push(msat_make_plus(env, leftResult, rightResult)); |
|||
break; |
|||
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus: |
|||
stack.push(msat_make_plus(env, leftResult, msat_make_times(env, msat_make_number(env, "-1"), rightResult))); |
|||
break; |
|||
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times: |
|||
stack.push(msat_make_times(env, leftResult, rightResult)); |
|||
break; |
|||
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide: |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unsupported numerical binary operator: '/' (division) in expression " << expression << "."; |
|||
break; |
|||
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min: |
|||
stack.push(msat_make_term_ite(env, msat_make_leq(env, leftResult, rightResult), leftResult, rightResult)); |
|||
break; |
|||
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max: |
|||
stack.push(msat_make_term_ite(env, msat_make_leq(env, leftResult, rightResult), rightResult, leftResult)); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numerical binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; |
|||
} |
|||
} |
|||
|
|||
virtual void visit(expressions::BinaryRelationExpression const* expression) override { |
|||
expression->getFirstOperand()->accept(this); |
|||
expression->getSecondOperand()->accept(this); |
|||
|
|||
msat_term rightResult = stack.top(); |
|||
stack.pop(); |
|||
msat_term leftResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch (expression->getRelationType()) { |
|||
case storm::expressions::BinaryRelationExpression::RelationType::Equal: |
|||
if (expression->getFirstOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool && expression->getSecondOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool) { |
|||
stack.push(msat_make_iff(env, leftResult, rightResult)); |
|||
} else { |
|||
stack.push(msat_make_equal(env, leftResult, rightResult)); |
|||
} |
|||
break; |
|||
case storm::expressions::BinaryRelationExpression::RelationType::NotEqual: |
|||
if (expression->getFirstOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool && expression->getSecondOperand()->getReturnType() == storm::expressions::ExpressionReturnType::Bool) { |
|||
stack.push(msat_make_not(env, msat_make_iff(env, leftResult, rightResult))); |
|||
} else { |
|||
stack.push(msat_make_not(env, msat_make_equal(env, leftResult, rightResult))); |
|||
} |
|||
break; |
|||
case storm::expressions::BinaryRelationExpression::RelationType::Less: |
|||
stack.push(msat_make_and(env, msat_make_not(env, msat_make_equal(env, leftResult, rightResult)), msat_make_leq(env, leftResult, rightResult))); |
|||
break; |
|||
case storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual: |
|||
stack.push(msat_make_leq(env, leftResult, rightResult)); |
|||
break; |
|||
case storm::expressions::BinaryRelationExpression::RelationType::Greater: |
|||
stack.push(msat_make_not(env, msat_make_leq(env, leftResult, rightResult))); |
|||
break; |
|||
case storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual: |
|||
stack.push(msat_make_or(env, msat_make_equal(env, leftResult, rightResult), msat_make_not(env, msat_make_leq(env, leftResult, rightResult)))); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary operator: '" << expression->getRelationType() << "' in expression " << expression << "."; |
|||
} |
|||
} |
|||
|
|||
virtual void visit(storm::expressions::IfThenElseExpression const* expression) override { |
|||
expression->getCondition()->accept(this); |
|||
expression->getThenExpression()->accept(this); |
|||
expression->getElseExpression()->accept(this); |
|||
|
|||
msat_term conditionResult = stack.top(); |
|||
stack.pop(); |
|||
msat_term thenResult = stack.top(); |
|||
stack.pop(); |
|||
msat_term elseResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
stack.push(msat_make_term_ite(env, conditionResult, thenResult, elseResult)); |
|||
} |
|||
|
|||
virtual void visit(expressions::BooleanLiteralExpression const* expression) override { |
|||
stack.push(expression->evaluateAsBool(nullptr) ? msat_make_true(env) : msat_make_false(env)); |
|||
} |
|||
|
|||
virtual void visit(expressions::DoubleLiteralExpression const* expression) override { |
|||
stack.push(msat_make_number(env, std::to_string(expression->evaluateAsDouble(nullptr)).c_str())); |
|||
} |
|||
|
|||
virtual void visit(expressions::IntegerLiteralExpression const* expression) override { |
|||
stack.push(msat_make_number(env, std::to_string(static_cast<int>(expression->evaluateAsInt(nullptr))).c_str())); |
|||
} |
|||
|
|||
virtual void visit(expressions::UnaryBooleanFunctionExpression const* expression) override { |
|||
expression->getOperand()->accept(this); |
|||
|
|||
msat_term childResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch (expression->getOperatorType()) { |
|||
case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: |
|||
stack.push(msat_make_not(env, childResult)); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary operator: '" << expression->getOperatorType() << "' in expression " << expression << "."; |
|||
} |
|||
} |
|||
|
|||
virtual void visit(expressions::UnaryNumericalFunctionExpression const* expression) override { |
|||
expression->getOperand()->accept(this); |
|||
|
|||
msat_term childResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch (expression->getOperatorType()) { |
|||
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: |
|||
stack.push(msat_make_times(env, msat_make_number(env, "-1"), childResult)); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numerical unary operator: '" << expression->getOperatorType() << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual void visit(expressions::VariableExpression const* expression) override { |
|||
if (variableToDeclMap.count(expression->getVariableName()) == 0) { |
|||
LOG4CPLUS_ERROR(logger, "Variable " << expression->getVariableName() << " is unknown!"); |
|||
} |
|||
//LOG4CPLUS_TRACE(logger, "Variable "<<expression->getVariableName()); |
|||
//char* repr = msat_decl_repr(variableToDeclMap.at(expression->getVariableName())); |
|||
//LOG4CPLUS_TRACE(logger, "Decl: "<<repr); |
|||
//msat_free(repr); |
|||
if (MSAT_ERROR_DECL(variableToDeclMap.at(expression->getVariableName()))) { |
|||
LOG4CPLUS_WARN(logger, "Encountered an invalid MathSAT declaration"); |
|||
} |
|||
stack.push(msat_make_constant(env, variableToDeclMap.at(expression->getVariableName()))); |
|||
} |
|||
|
|||
storm::expressions::Expression translateTerm(msat_term term) { |
|||
this->processTerm(term); |
|||
|
|||
storm::expressions::Expression result = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
return result; |
|||
} |
|||
|
|||
void processTerm(msat_term term) { |
|||
if (msat_term_is_and(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
this->processTerm(msat_term_get_arg(term, 1)); |
|||
|
|||
storm::expressions::Expression rightResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
storm::expressions::Expression leftResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(leftResult &&rightResult); |
|||
} else if (msat_term_is_or(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
this->processTerm(msat_term_get_arg(term, 1)); |
|||
|
|||
storm::expressions::Expression rightResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
storm::expressions::Expression leftResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(leftResult && rightResult); |
|||
} else if (msat_term_is_iff(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
this->processTerm(msat_term_get_arg(term, 1)); |
|||
|
|||
storm::expressions::Expression rightResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
storm::expressions::Expression leftResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(leftResult.iff(rightResult)); |
|||
} else if (msat_term_is_not(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
|
|||
storm::expressions::Expression childResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(!childResult); |
|||
} else if (msat_term_is_plus(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
this->processTerm(msat_term_get_arg(term, 1)); |
|||
|
|||
storm::expressions::Expression rightResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
storm::expressions::Expression leftResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(leftResult+rightResult); |
|||
} else if (msat_term_is_times(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
this->processTerm(msat_term_get_arg(term, 1)); |
|||
|
|||
storm::expressions::Expression rightResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
storm::expressions::Expression leftResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(leftResult * rightResult); |
|||
} else if (msat_term_is_equal(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
this->processTerm(msat_term_get_arg(term, 1)); |
|||
|
|||
storm::expressions::Expression rightResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
storm::expressions::Expression leftResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(leftResult == rightResult); |
|||
} else if (msat_term_is_leq(env, term)) { |
|||
this->processTerm(msat_term_get_arg(term, 0)); |
|||
this->processTerm(msat_term_get_arg(term, 1)); |
|||
|
|||
storm::expressions::Expression rightResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
storm::expressions::Expression leftResult = std::move(expression_stack.top()); |
|||
expression_stack.pop(); |
|||
|
|||
expression_stack.push(leftResult <= rightResult); |
|||
} else if (msat_term_is_true(env, term)) { |
|||
expression_stack.push(expressions::Expression::createTrue()); |
|||
} else if (msat_term_is_false(env, term)) { |
|||
expression_stack.push(expressions::Expression::createFalse()); |
|||
} else if (msat_term_is_boolean_constant(env, term)) { |
|||
char* name = msat_decl_get_name(msat_term_get_decl(term)); |
|||
std::string name_str(name); |
|||
expression_stack.push(expressions::Expression::createBooleanVariable(name_str.substr(0, name_str.find('/')))); |
|||
msat_free(name); |
|||
} else if (msat_term_is_constant(env, term)) { |
|||
char* name = msat_decl_get_name(msat_term_get_decl(term)); |
|||
std::string name_str(name); |
|||
if (msat_is_integer_type(env, msat_term_get_type(term))) { |
|||
expression_stack.push(expressions::Expression::createIntegerVariable(name_str.substr(0, name_str.find('/')))); |
|||
} else if (msat_is_rational_type(env, msat_term_get_type(term))) { |
|||
expression_stack.push(expressions::Expression::createDoubleVariable(name_str.substr(0, name_str.find('/')))); |
|||
} |
|||
msat_free(name); |
|||
} else if (msat_term_is_number(env, term)) { |
|||
if (msat_is_integer_type(env, msat_term_get_type(term))) { |
|||
expression_stack.push(expressions::Expression::createIntegerLiteral(std::stoll(msat_term_repr(term)))); |
|||
} else if (msat_is_rational_type(env, msat_term_get_type(term))) { |
|||
expression_stack.push(expressions::Expression::createDoubleLiteral(std::stod(msat_term_repr(term)))); |
|||
} |
|||
} else { |
|||
char* term_cstr = msat_term_repr(term); |
|||
std::string term_str(term_cstr); |
|||
msat_free(term_cstr); |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown term: '" << term_str << "'."; |
|||
} |
|||
} |
|||
|
|||
private: |
|||
msat_env& env; |
|||
std::stack<msat_term> stack; |
|||
std::stack<expressions::Expression> expression_stack; |
|||
std::map<std::string, msat_decl> variableToDeclMap; |
|||
}; |
|||
|
|||
} // namespace adapters |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_ADAPTERS_MATHSATEXPRESSIONADAPTER_H_ */ |
|||
@ -0,0 +1,321 @@ |
|||
#include "src/solver/MathSatSmtSolver.h"
|
|||
|
|||
#include <vector>
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
#ifdef STORM_HAVE_MSAT
|
|||
MathSatSmtSolver::MathSatModelReference::Z3ModelReference(z3::model &m, storm::adapters::Z3ExpressionAdapter &adapter) : m_model(m), m_adapter(adapter) { |
|||
|
|||
} |
|||
#endif
|
|||
|
|||
bool MathSatSmtSolver::Z3ModelReference::getBooleanValue(std::string const& name) const { |
|||
#ifdef STORM_HAVE_MSAT
|
|||
z3::expr z3Expr = this->m_adapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name)); |
|||
z3::expr z3ExprValuation = m_model.eval(z3Expr, true); |
|||
return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsBool(); |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
int_fast64_t MathSatSmtSolver::Z3ModelReference::getIntegerValue(std::string const& name) const { |
|||
#ifdef STORM_HAVE_MSAT
|
|||
z3::expr z3Expr = this->m_adapter.translateExpression(storm::expressions::Expression::createIntegerVariable(name)); |
|||
z3::expr z3ExprValuation = m_model.eval(z3Expr, true); |
|||
return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsInt(); |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
MathSatSmtSolver::MathSatSmtSolver(Options options) |
|||
#ifdef STORM_HAVE_MSAT
|
|||
: lastCheckAssumptions(false) |
|||
, lastResult(CheckResult::UNKNOWN) |
|||
#endif
|
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
m_cfg = msat_create_config(); |
|||
|
|||
if (static_cast<int>(options)& static_cast<int>(Options::InterpolantComputation)) { |
|||
msat_res = msat_set_option(m_cfg, "interpolation", "true"); |
|||
if (msat_res != 0) { |
|||
LOG4CPLUS_WARN(logger, "MathSAT returned an error!"); |
|||
} |
|||
} |
|||
m_env = msat_create_env(m_cfg); |
|||
#endif
|
|||
} |
|||
MathSatSmtSolver::~MathSatSmtSolver() { |
|||
msat_destroy_env(m_env); |
|||
msat_destroy_config(m_cfg); |
|||
}; |
|||
|
|||
void MathSatSmtSolver::push() |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
msat_push_backtrack_point(m_env); |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
void MathSatSmtSolver::pop() |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
msat_pop_backtrack_point(m_env); |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
void MathSatSmtSolver::pop(uint_fast64_t n) |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
for (uint_fast64_t i = 0; i < n; ++i) { |
|||
this->pop(); |
|||
} |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
void MathSatSmtSolver::reset() |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
msat_reset_env(m_env); |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
void MathSatSmtSolver::assertExpression(storm::expressions::Expression const& e) |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
msat_assert_formula(m_env, m_adapter.translateExpression(e, true)); |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
SmtSolver::CheckResult MathSatSmtSolver::check() |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
lastCheckAssumptions = false; |
|||
switch (msat_solve(m_env)) { |
|||
case MSAT_SAT: |
|||
this->lastResult = SmtSolver::CheckResult::SAT; |
|||
break; |
|||
case MSAT_UNSAT: |
|||
this->lastResult = SmtSolver::CheckResult::UNSAT; |
|||
break; |
|||
default: |
|||
this->lastResult = SmtSolver::CheckResult::UNKNOWN; |
|||
break; |
|||
} |
|||
return this->lastResult; |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
SmtSolver::CheckResult MathSatSmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
lastCheckAssumptions = true; |
|||
std::vector<msat_term> mathSatAssumptions; |
|||
mathSatAssumptions.reserve(assumptions.size()); |
|||
|
|||
for (storm::expressions::Expression assumption : assumptions) { |
|||
mathSatAssumptions.push_back(this->m_adapter.translateExpression(assumption)); |
|||
} |
|||
|
|||
switch (msat_solve_with_assumptions(m_env, mathSatAssumptions.data(), mathSatAssumptions.size())) { |
|||
case MSAT_SAT: |
|||
this->lastResult = SmtSolver::CheckResult::SAT; |
|||
break; |
|||
case MSAT_UNSAT: |
|||
this->lastResult = SmtSolver::CheckResult::UNSAT; |
|||
break; |
|||
default: |
|||
this->lastResult = SmtSolver::CheckResult::UNKNOWN; |
|||
break; |
|||
} |
|||
return this->lastResult; |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
SmtSolver::CheckResult MathSatSmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
lastCheckAssumptions = true; |
|||
std::vector<msat_term> mathSatAssumptions; |
|||
mathSatAssumptions.reserve(assumptions.size()); |
|||
|
|||
for (storm::expressions::Expression assumption : assumptions) { |
|||
mathSatAssumptions.push_back(this->m_adapter.translateExpression(assumption)); |
|||
} |
|||
|
|||
switch (msat_solve_with_assumptions(m_env, mathSatAssumptions.data(), mathSatAssumptions.size())) { |
|||
case MSAT_SAT: |
|||
this->lastResult = SmtSolver::CheckResult::SAT; |
|||
break; |
|||
case MSAT_UNSAT: |
|||
this->lastResult = SmtSolver::CheckResult::UNSAT; |
|||
break; |
|||
default: |
|||
this->lastResult = SmtSolver::CheckResult::UNKNOWN; |
|||
break; |
|||
} |
|||
return this->lastResult; |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
storm::expressions::SimpleValuation MathSatSmtSolver::getModel() |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
|
|||
LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT."); |
|||
|
|||
return this->MathSatModelToStorm(); |
|||
#else
|
|||
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 stormModel; |
|||
|
|||
msat_model_iterator model = msat_create_model_iterator(m_env); |
|||
|
|||
while (msat_model_iterator_has_next(model)) { |
|||
msat_term t, v; |
|||
msat_model_iterator_next(model, &t, &v); |
|||
|
|||
storm::expressions::Expression var_i_interp = this->m_adapter.translateTerm(v); |
|||
char* name = msat_decl_get_name(msat_term_get_decl(t)); |
|||
|
|||
switch (var_i_interp.getReturnType()) { |
|||
case storm::expressions::ExpressionReturnType::Bool: |
|||
|
|||
stormModel.addBooleanIdentifier(std::string(name), var_i_interp.evaluateAsBool()); |
|||
break; |
|||
case storm::expressions::ExpressionReturnType::Int: |
|||
stormModel.addIntegerIdentifier(std::string(name), var_i_interp.evaluateAsInt()); |
|||
break; |
|||
case storm::expressions::ExpressionReturnType::Double: |
|||
stormModel.addDoubleIdentifier(std::string(name), var_i_interp.evaluateAsDouble()); |
|||
break; |
|||
default: |
|||
LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") |
|||
break; |
|||
} |
|||
|
|||
msat_free(name); |
|||
|
|||
} |
|||
|
|||
return stormModel; |
|||
} |
|||
#endif
|
|||
|
|||
std::vector<storm::expressions::SimpleValuation> MathSatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important) |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
|
|||
std::vector<storm::expressions::SimpleValuation> valuations; |
|||
|
|||
this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool {valuations.push_back(valuation); return true; }); |
|||
|
|||
return valuations; |
|||
|
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
|
|||
#ifdef STORM_HAVE_MSAT
|
|||
struct AllsatValuationsCallbackUserData { |
|||
msat_env env; |
|||
storm::adapters::MathSatExpressionAdapter &adapter; |
|||
storm::expressions::SimpleValuation& valuation; |
|||
uint_fast64_t n; |
|||
}; |
|||
|
|||
int allsatValuationsCallback(msat_term *model, int size, void *user_data) { |
|||
AllsatValuationsCallbackUserData* user = reinterpret_cast<AllsatValuationsCallbackUserData*>(user_data); |
|||
++n; |
|||
|
|||
for (int i = 0; i < size; ++i) { |
|||
///
|
|||
} |
|||
} |
|||
#endif
|
|||
|
|||
|
|||
uint_fast64_t MathSatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
for (storm::expressions::Expression e : important) { |
|||
if (!e.isVariable()) { |
|||
throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions."; |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
return numModels; |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
uint_fast64_t MathSatSmtSolver::allSat(std::function<bool(SmtSolver::ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important) |
|||
{ |
|||
#ifdef STORM_HAVE_MSAT
|
|||
for (storm::expressions::Expression e : important) { |
|||
if (!e.isVariable()) { |
|||
throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions."; |
|||
} |
|||
} |
|||
|
|||
return numModels; |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
|
|||
std::vector<storm::expressions::Expression> MathSatSmtSolver::getUnsatAssumptions() { |
|||
#ifdef STORM_HAVE_MSAT
|
|||
if (lastResult != SmtSolver::CheckResult::UNSAT) { |
|||
throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last state is not unsat."; |
|||
} |
|||
if (!lastCheckAssumptions) { |
|||
throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last check had no assumptions."; |
|||
} |
|||
|
|||
size_t numUnsatAssumpations; |
|||
msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(m_env, &numUnsatAssumpations); |
|||
|
|||
std::vector<storm::expressions::Expression> unsatAssumptions; |
|||
unsatAssumptions.reserve(numUnsatAssumpations); |
|||
|
|||
for (unsigned int i = 0; i < numUnsatAssumpations; ++i) { |
|||
unsatAssumptions.push_back(this->m_adapter.translateTerm(msatUnsatAssumptions[i])); |
|||
} |
|||
|
|||
return unsatAssumptions; |
|||
#else
|
|||
LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); |
|||
#endif
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,84 @@ |
|||
#ifndef STORM_SOLVER_MATHSATSMTSOLVER |
|||
#define STORM_SOLVER_MATHSATSMTSOLVER |
|||
|
|||
#include "storm-config.h" |
|||
#include "src/solver/SmtSolver.h" |
|||
#include "src/adapters/MathSatExpressionAdapter.h" |
|||
|
|||
#ifndef STORM_HAVE_MSAT |
|||
#define STORM_HAVE_MSAT |
|||
#endif |
|||
|
|||
#ifdef STORM_HAVE_MSAT |
|||
#include "mathsat.h" |
|||
#endif |
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
class MathSatSmtSolver : public SmtSolver { |
|||
public: |
|||
class MathSatModelReference : public SmtSolver::ModelReference { |
|||
public: |
|||
#ifdef STORM_HAVE_MSAT |
|||
MathSatModelReference(msat_env& 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; |
|||
private: |
|||
#ifdef STORM_HAVE_MSAT |
|||
msat_env& env; |
|||
storm::adapters::MathSatExpressionAdapter &m_adapter; |
|||
#endif |
|||
}; |
|||
public: |
|||
MathSatSmtSolver(Options options = Options::ModelGeneration); |
|||
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 CheckResult check() override; |
|||
|
|||
virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override; |
|||
|
|||
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) override; |
|||
|
|||
virtual storm::expressions::SimpleValuation getModel() 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::function<bool(ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important) override; |
|||
|
|||
virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override; |
|||
|
|||
virtual void setInterpolationGroup(uint_fast64_t group) override; |
|||
|
|||
virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> groupsA) override; |
|||
|
|||
protected: |
|||
#ifdef STORM_HAVE_MSAT |
|||
virtual storm::expressions::SimpleValuation MathSatModelToStorm(); |
|||
#endif |
|||
private: |
|||
|
|||
#ifdef STORM_HAVE_MSAT |
|||
msat_config m_cfg; |
|||
msat_env m_env; |
|||
storm::adapters::MathSatExpressionAdapter m_adapter; |
|||
|
|||
bool lastCheckAssumptions; |
|||
CheckResult lastResult; |
|||
#endif |
|||
}; |
|||
} |
|||
} |
|||
#endif // STORM_SOLVER_MATHSATSMTSOLVER |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue