From d8be64f0d7a2e2db1b43b87e72b6b508524dd94d Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 17 Dec 2014 17:11:57 +0100 Subject: [PATCH] Started on making MathSatSmtSolver work properly. Former-commit-id: c370658b26ff9fe1dec577f16b4c4ad1fece7a75 --- src/adapters/MathSatExpressionAdapter.h | 31 ++++++++++ src/exceptions/UnexpectedException.h | 15 +++++ src/solver/MathSatSmtSolver.cpp | 7 +++ .../solver/MathSatSmtSolverTest.cpp | 58 +++++++++++++++++++ test/functional/solver/Z3SmtSolverTest.cpp | 14 ++--- 5 files changed, 118 insertions(+), 7 deletions(-) create mode 100644 src/exceptions/UnexpectedException.h create mode 100644 test/functional/solver/MathSatSmtSolverTest.cpp diff --git a/src/adapters/MathSatExpressionAdapter.h b/src/adapters/MathSatExpressionAdapter.h index 4436959e1..0bdaba346 100644 --- a/src/adapters/MathSatExpressionAdapter.h +++ b/src/adapters/MathSatExpressionAdapter.h @@ -47,6 +47,37 @@ namespace storm { * @return An equivalent term for MathSAT. */ msat_term translateExpression(storm::expressions::Expression const& expression, bool createMathSatVariables = false) { + if (createMathSatVariables) { + std::map variables; + + try { + variables = expression.getVariablesAndTypes(); + } + catch (storm::exceptions::InvalidTypeException* e) { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e); + } + + for (auto variableAndType : variables) { + if (this->variableToDeclMap.find(variableAndType.first) == this->variableToDeclMap.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)))); + 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)))); + 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)))); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first); + break; + } + } + } + } + //LOG4CPLUS_TRACE(logger, "Translating expression:\n" << expression->toString()); expression.getBaseExpression().accept(this); msat_term result = stack.top(); diff --git a/src/exceptions/UnexpectedException.h b/src/exceptions/UnexpectedException.h new file mode 100644 index 000000000..4e2f8f43b --- /dev/null +++ b/src/exceptions/UnexpectedException.h @@ -0,0 +1,15 @@ +#ifndef STORM_EXCEPTIONS_UNEXPECTEDEXCEPTION_H_ +#define STORM_EXCEPTIONS_UNEXPECTEDEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" +#include "src/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(UnexpectedException) + + } // namespace exceptions +} // namespace storm + +#endif /* STORM_EXCEPTIONS_UNEXPECTEDEXCEPTION_H_ */ diff --git a/src/solver/MathSatSmtSolver.cpp b/src/solver/MathSatSmtSolver.cpp index 285f8d422..2e14ba701 100644 --- a/src/solver/MathSatSmtSolver.cpp +++ b/src/solver/MathSatSmtSolver.cpp @@ -2,6 +2,8 @@ #include +#include "src/exceptions/UnexpectedException.h" + namespace storm { namespace solver { @@ -17,6 +19,9 @@ namespace storm { if (static_cast(options)& static_cast(Options::InterpolantComputation)) { msat_set_option(m_cfg, "interpolation", "true"); } + + msat_set_option(m_cfg, "model_generation", "true"); + m_env = msat_create_env(m_cfg); m_adapter = new storm::adapters::MathSatExpressionAdapter(m_env, variableToDeclMap); @@ -169,6 +174,8 @@ namespace storm { msat_model_iterator model = msat_create_model_iterator(m_env); + STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(model), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator."); + while (msat_model_iterator_has_next(model)) { msat_term t, v; msat_model_iterator_next(model, &t, &v); diff --git a/test/functional/solver/MathSatSmtSolverTest.cpp b/test/functional/solver/MathSatSmtSolverTest.cpp new file mode 100644 index 000000000..2b86bc510 --- /dev/null +++ b/test/functional/solver/MathSatSmtSolverTest.cpp @@ -0,0 +1,58 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_MSAT +#include "src/solver/MathSatSmtSolver.h" + +TEST(MathSatSmtSolver, CheckSat) { + storm::solver::MathSatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; + + storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); + + ASSERT_NO_THROW(s.assertExpression(exprDeMorgan)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.reset()); + + storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); + storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); + storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0) + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a * b) + && b + a > c; + + ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_NO_THROW(s.reset()); +} + +TEST(MathSatSmtSolver, CheckUnsat) { + storm::solver::MathSatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; + + storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); + + ASSERT_NO_THROW(s.assertExpression(!exprDeMorgan)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_NO_THROW(s.reset()); + + storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); + storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); + storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c"); + storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(2) + && a < storm::expressions::Expression::createIntegerLiteral(5) + && b > storm::expressions::Expression::createIntegerLiteral(7) + && c == (a + b + storm::expressions::Expression::createIntegerLiteral(1)) + && b + a > c; + + ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(result = s.check()); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); +} + +#endif \ No newline at end of file diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index 1f5a0cf86..171042e52 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -7,7 +7,7 @@ TEST(Z3SmtSolver, CheckSat) { storm::solver::Z3SmtSolver s; - storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); @@ -33,7 +33,7 @@ TEST(Z3SmtSolver, CheckSat) { TEST(Z3SmtSolver, CheckUnsat) { storm::solver::Z3SmtSolver s; - storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); @@ -60,7 +60,7 @@ TEST(Z3SmtSolver, CheckUnsat) { TEST(Z3SmtSolver, Backtracking) { storm::solver::Z3SmtSolver s; - storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue(); storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); @@ -114,7 +114,7 @@ TEST(Z3SmtSolver, Backtracking) { TEST(Z3SmtSolver, Assumptions) { storm::solver::Z3SmtSolver s; - storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -143,7 +143,7 @@ TEST(Z3SmtSolver, Assumptions) { TEST(Z3SmtSolver, GenerateModel) { storm::solver::Z3SmtSolver s; - storm::solver::Z3SmtSolver::CheckResult result; + storm::solver::SmtSolver::CheckResult result; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -167,7 +167,7 @@ TEST(Z3SmtSolver, GenerateModel) { TEST(Z3SmtSolver, AllSat) { storm::solver::Z3SmtSolver s; - storm::solver::Z3SmtSolver::CheckResult result; + storm::solver::SmtSolver::CheckResult result; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -201,7 +201,7 @@ TEST(Z3SmtSolver, AllSat) { TEST(Z3SmtSolver, UnsatAssumptions) { storm::solver::Z3SmtSolver s; - storm::solver::Z3SmtSolver::CheckResult result; + storm::solver::SmtSolver::CheckResult result; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");