From 7b8c382303cb317ef0bd4225080212e4410ec389 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 22 Dec 2014 23:41:10 +0100 Subject: [PATCH] Added tests for Mathsat expression adapter. Former-commit-id: 4f8ef4c3c322fa06308147f833a5b1593058ef52 --- src/adapters/MathsatExpressionAdapter.h | 29 ++- .../adapter/MathsatExpressionAdapterTest.cpp | 200 ++++++++++++++++++ .../adapter/Z3ExpressionAdapterTest.cpp | 1 + 3 files changed, 219 insertions(+), 11 deletions(-) create mode 100644 test/functional/adapter/MathsatExpressionAdapterTest.cpp diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index f07b2cac5..46189935f 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -207,6 +207,12 @@ namespace storm { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: stack.push(msat_make_times(env, msat_make_number(env, "-1"), childResult)); break; + case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: + stack.push(msat_make_floor(env, childResult)); + break; + case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil: + stack.push(msat_make_plus(env, msat_make_floor(env, childResult), msat_make_number(env, "1"))); + break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical unary operator: '" << static_cast(expression->getOperatorType()) << "' in expression " << expression << "."); } @@ -220,25 +226,26 @@ namespace storm { std::pair::iterator, bool> iteratorAndFlag; switch (expression->getReturnType()) { case storm::expressions::ExpressionReturnType::Bool: - iteratorAndFlag = this->variableToDeclarationMap.insert(std::make_pair(expression->getVariableName(), msat_declare_function(env, expression->getVariableName().c_str(), msat_get_bool_type(env)))); - result = iteratorAndFlag.first->second; - break; + iteratorAndFlag = this->variableToDeclarationMap.insert(std::make_pair(expression->getVariableName(), msat_declare_function(env, expression->getVariableName().c_str(), msat_get_bool_type(env)))); + result = iteratorAndFlag.first->second; + break; case storm::expressions::ExpressionReturnType::Int: - iteratorAndFlag = this->variableToDeclarationMap.insert(std::make_pair(expression->getVariableName(), msat_declare_function(env, expression->getVariableName().c_str(), msat_get_integer_type(env)))); - result = iteratorAndFlag.first->second; - break; + iteratorAndFlag = this->variableToDeclarationMap.insert(std::make_pair(expression->getVariableName(), msat_declare_function(env, expression->getVariableName().c_str(), msat_get_integer_type(env)))); + result = iteratorAndFlag.first->second; + break; case storm::expressions::ExpressionReturnType::Double: - iteratorAndFlag = this->variableToDeclarationMap.insert(std::make_pair(expression->getVariableName(), msat_declare_function(env, expression->getVariableName().c_str(), msat_get_rational_type(env)))); - result = iteratorAndFlag.first->second; - break; + iteratorAndFlag = this->variableToDeclarationMap.insert(std::make_pair(expression->getVariableName(), msat_declare_function(env, expression->getVariableName().c_str(), msat_get_rational_type(env)))); + result = iteratorAndFlag.first->second; + break; default: - STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable '" << expression->getVariableName() << "' with unknown type while trying to create solver variables."); + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable '" << expression->getVariableName() << "' with unknown type while trying to create solver variables."); } } else { STORM_LOG_THROW(stringVariablePair != variableToDeclarationMap.end(), storm::exceptions::InvalidArgumentException, "Expression refers to unknown variable '" << expression->getVariableName() << "'."); result = stringVariablePair->second; } - + + STORM_LOG_THROW(!MSAT_ERROR_DECL(result), storm::exceptions::ExpressionEvaluationException, "Unable to translate expression to MathSAT format, because a variable could not be translated."); stack.push(msat_make_constant(env, result)); } diff --git a/test/functional/adapter/MathsatExpressionAdapterTest.cpp b/test/functional/adapter/MathsatExpressionAdapterTest.cpp new file mode 100644 index 000000000..b59100a17 --- /dev/null +++ b/test/functional/adapter/MathsatExpressionAdapterTest.cpp @@ -0,0 +1,200 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_MSAT +#include "mathsat.h" +#include "src/adapters/MathsatExpressionAdapter.h" +#include "src/settings/SettingsManager.h" + +TEST(MathsatExpressionAdapter, StormToMathsatBasic) { + msat_config config = msat_create_config(); + msat_env env = msat_create_env(config); + ASSERT_FALSE(MSAT_ERROR_ENV(env)); + msat_destroy_config(config); + + storm::adapters::MathsatExpressionAdapter adapter(env); + storm::adapters::MathsatExpressionAdapter adapter2(env, false); + + storm::expressions::Expression exprTrue = storm::expressions::Expression::createTrue(); + msat_term msatTrue = msat_make_true(env); + msat_term conjecture; + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, msatTrue, adapter.translateExpression(exprTrue)))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); + + storm::expressions::Expression exprFalse = storm::expressions::Expression::createFalse(); + msat_term msatFalse = msat_make_false(env); + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprFalse), msatFalse))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); + + storm::expressions::Expression exprConjunction = (storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")); + msat_term msatConjunction = msat_make_and(env, msat_make_constant(env, msat_declare_function(env, "x", msat_get_bool_type(env))), msat_make_constant(env, msat_declare_function(env, "y", msat_get_bool_type(env)))); + + // Variables not yet created in adapter. + ASSERT_THROW(adapter2.translateExpression(exprConjunction), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprConjunction), msatConjunction))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); + + storm::expressions::Expression exprNor = !(storm::expressions::Expression::createBooleanVariable("x") || storm::expressions::Expression::createBooleanVariable("y")); + msat_term msatNor = msat_make_not(env, msat_make_or(env, msat_make_constant(env, msat_declare_function(env, "x", msat_get_bool_type(env))), msat_make_constant(env, msat_declare_function(env, "y", msat_get_bool_type(env))))); + ASSERT_NO_THROW(adapter.translateExpression(exprNor)); // Variables already created in adapter. + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprNor), msatNor))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); +} + +TEST(MathsatExpressionAdapter, StormToMathsatInteger) { + msat_config config = msat_create_config(); + msat_env env = msat_create_env(config); + ASSERT_FALSE(MSAT_ERROR_ENV(env)); + msat_destroy_config(config); + + storm::adapters::MathsatExpressionAdapter adapter(env); + + storm::expressions::Expression exprAdd = (storm::expressions::Expression::createIntegerVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createIntegerVariable("y")); + msat_decl xDecl = msat_declare_function(env, "x", msat_get_integer_type(env)); + msat_term x = msat_make_constant(env, xDecl); + msat_decl yDecl = msat_declare_function(env, "y", msat_get_integer_type(env)); + msat_term y = msat_make_constant(env, yDecl); + msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), y); + msat_term msatAdd = msat_make_plus(env, x, y); + msat_term msatLess = msat_make_and(env, msat_make_leq(env, msatAdd, minusY), msat_make_not(env, msat_make_equal(env, msatAdd, minusY))); + msat_term conjecture; + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprAdd), msatLess))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); + + storm::expressions::Expression exprMult = !(storm::expressions::Expression::createIntegerVariable("x") * storm::expressions::Expression::createIntegerVariable("y") == storm::expressions::Expression::createIntegerVariable("y")); + msat_term msatTimes = msat_make_times(env, x, y); + msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, y)); + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprMult), msatNotEqual))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); +} + +TEST(MathsatExpressionAdapter, StormToMathsatReal) { + msat_config config = msat_create_config(); + msat_env env = msat_create_env(config); + ASSERT_FALSE(MSAT_ERROR_ENV(env)); + msat_destroy_config(config); + + storm::adapters::MathsatExpressionAdapter adapter(env); + + storm::expressions::Expression exprAdd = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") < -storm::expressions::Expression::createDoubleVariable("y")); + msat_decl xDecl = msat_declare_function(env, "x", msat_get_rational_type(env)); + msat_term x = msat_make_constant(env, xDecl); + msat_decl yDecl = msat_declare_function(env, "y", msat_get_rational_type(env)); + msat_term y = msat_make_constant(env, yDecl); + msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), y); + msat_term msatAdd = msat_make_plus(env, x, y); + msat_term msatLess = msat_make_and(env, msat_make_leq(env, msatAdd, minusY), msat_make_not(env, msat_make_equal(env, msatAdd, minusY))); + msat_term conjecture; + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprAdd), msatLess))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); + + storm::expressions::Expression exprMult = !(storm::expressions::Expression::createDoubleVariable("x") * storm::expressions::Expression::createDoubleVariable("y") == storm::expressions::Expression::createDoubleVariable("y")); + msat_term msatTimes = msat_make_times(env, x, y); + msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, y)); + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprMult), msatNotEqual))); + msat_assert_formula(env, conjecture); + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); +} + +TEST(MathsatExpressionAdapter, StormToMathsatFloorCeil) { + msat_config config = msat_create_config(); + msat_env env = msat_create_env(config); + ASSERT_FALSE(MSAT_ERROR_ENV(env)); + msat_destroy_config(config); + + storm::adapters::MathsatExpressionAdapter adapter(env); + + storm::expressions::Expression exprFloor = ((storm::expressions::Expression::createDoubleVariable("d").floor()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); + + msat_decl iDecl = msat_declare_function(env, "i", msat_get_integer_type(env)); + msat_term i = msat_make_constant(env, iDecl); + msat_term msatEqualsFour = msat_make_equal(env, msat_make_number(env, "4"), i); + msat_term conjecture; + msat_term translatedExpr = adapter.translateExpression(exprFloor); + msat_term msatIff = msat_make_iff(env, translatedExpr, msatEqualsFour); + ASSERT_NO_THROW(conjecture = msat_make_not(env, msatIff)); + msat_assert_formula(env, conjecture); + + // It is not logically equivalent, so this should be satisfiable. + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_SAT); + msat_reset_env(env); + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_or(env, msat_make_not(env, adapter.translateExpression(exprFloor)), msatEqualsFour))); + msat_assert_formula(env, conjecture); + + // However, the left part implies the right one, which is why this should be unsatisfiable. + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT); + msat_reset_env(env); + + storm::expressions::Expression exprCeil = ((storm::expressions::Expression::createDoubleVariable("d").ceil()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991)); + msat_term msatEqualsFive = msat_make_equal(env, msat_make_number(env, "5"), i); + + ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprFloor), msatEqualsFive))); + msat_assert_formula(env, conjecture); + + // It is not logically equivalent, so this should be satisfiable. + ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_SAT); + msat_reset_env(env); + ASSERT_NO_THROW(conjecture = msat_make_or(env, msat_make_not(env, adapter.translateExpression(exprFloor)), msatEqualsFive)); + msat_assert_formula(env, conjecture); + msat_reset_env(env); +} + +TEST(MathsatExpressionAdapter, MathsatToStormBasic) { + msat_config config = msat_create_config(); + msat_env env = msat_create_env(config); + ASSERT_FALSE(MSAT_ERROR_ENV(env)); + msat_destroy_config(config); + + unsigned args = 2; + + storm::adapters::MathsatExpressionAdapter adapter(env); + + msat_term msatTrue = msat_make_true(env); + storm::expressions::Expression exprTrue; + ASSERT_NO_THROW(exprTrue = adapter.translateExpression(msatTrue)); + ASSERT_TRUE(exprTrue.isTrue()); + + msat_term msatFalse = msat_make_false(env); + storm::expressions::Expression exprFalse; + ASSERT_NO_THROW(exprTrue = adapter.translateExpression(msatFalse)); + ASSERT_TRUE(exprTrue.isFalse()); + + msat_decl xDecl = msat_declare_function(env, "x", msat_get_bool_type(env)); + msat_term x = msat_make_constant(env, xDecl); + msat_decl yDecl = msat_declare_function(env, "y", msat_get_bool_type(env)); + msat_term y = msat_make_constant(env, yDecl); + msat_term msatConjunction = msat_make_and(env, x, y); + storm::expressions::Expression exprConjunction; + ASSERT_NO_THROW(exprConjunction = adapter.translateExpression(msatConjunction)); + ASSERT_EQ(storm::expressions::OperatorType::And, exprConjunction.getOperator()); + ASSERT_TRUE(exprConjunction.getOperand(0).isVariable()); + ASSERT_EQ("x", exprConjunction.getOperand(0).getIdentifier()); + ASSERT_TRUE(exprConjunction.getOperand(1).isVariable()); + ASSERT_EQ("y", exprConjunction.getOperand(1).getIdentifier()); + + msat_term msatNor = msat_make_not(env, msat_make_or(env, x, y)); + storm::expressions::Expression exprNor; + ASSERT_NO_THROW(exprNor = adapter.translateExpression(msatNor)); + ASSERT_EQ(storm::expressions::OperatorType::Not, exprNor.getOperator()); + ASSERT_EQ(storm::expressions::OperatorType::Or, exprNor.getOperand(0).getOperator()); + ASSERT_TRUE(exprNor.getOperand(0).getOperand(0).isVariable()); + ASSERT_EQ("x", exprNor.getOperand(0).getOperand(0).getIdentifier()); + ASSERT_TRUE(exprNor.getOperand(0).getOperand(1).isVariable()); + ASSERT_EQ("y", exprNor.getOperand(0).getOperand(1).getIdentifier()); +} +#endif \ No newline at end of file diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp index 6ed24925b..49d1959ed 100644 --- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -30,6 +30,7 @@ TEST(Z3ExpressionAdapter, StormToZ3Basic) { storm::expressions::Expression exprConjunction = (storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")); z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y")); + // Variables not yet created in adapter. ASSERT_THROW( adapter2.translateExpression(exprConjunction), storm::exceptions::InvalidArgumentException ); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprConjunction), z3Conjunction)));