Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MathsatExpressionAdapterTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#ifdef STORM_HAVE_MATHSAT
5#include <mathsat.h>
6#include "storm/adapters/MathsatExpressionAdapter.h"
7#include "storm/settings/SettingsManager.h"
8#include "storm/storage/expressions/ExpressionManager.h"
9#include "storm/storage/expressions/Expressions.h"
10#include "storm/storage/expressions/OperatorType.h"
11
12TEST(MathsatExpressionAdapter, StormToMathsatBasic) {
13 msat_config config = msat_create_config();
14 msat_env env = msat_create_env(config);
15 ASSERT_FALSE(MSAT_ERROR_ENV(env));
16 msat_destroy_config(config);
17
18 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
19 storm::adapters::MathsatExpressionAdapter adapter(*manager, env);
20
21 storm::expressions::Expression exprTrue = manager->boolean(true);
22 msat_term msatTrue = msat_make_true(env);
23 msat_term conjecture;
24 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, msatTrue, adapter.translateExpression(exprTrue))));
25 msat_assert_formula(env, conjecture);
26 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
27 msat_reset_env(env);
28
29 storm::expressions::Expression exprFalse = manager->boolean(false);
30 msat_term msatFalse = msat_make_false(env);
31 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprFalse), msatFalse)));
32 msat_assert_formula(env, conjecture);
33 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
34 msat_reset_env(env);
35
36 storm::expressions::Variable x = manager->declareBooleanVariable("x");
37 storm::expressions::Variable y = manager->declareBooleanVariable("y");
38 storm::expressions::Expression exprConjunction = x && y;
39 msat_term msatConjunction = msat_make_and(env, msat_make_constant(env, msat_declare_function(env, "x", msat_get_bool_type(env))),
40 msat_make_constant(env, msat_declare_function(env, "y", msat_get_bool_type(env))));
41
42 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprConjunction), msatConjunction)));
43 msat_assert_formula(env, conjecture);
44 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
45 msat_reset_env(env);
46
47 storm::expressions::Expression exprNor = !(x || y);
48 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))),
49 msat_make_constant(env, msat_declare_function(env, "y", msat_get_bool_type(env)))));
50 ASSERT_NO_THROW(adapter.translateExpression(exprNor)); // Variables already created in adapter.
51 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprNor), msatNor)));
52 msat_assert_formula(env, conjecture);
53 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
54 msat_reset_env(env);
55}
56
57TEST(MathsatExpressionAdapter, StormToMathsatInteger) {
58 msat_config config = msat_create_config();
59 msat_env env = msat_create_env(config);
60 ASSERT_FALSE(MSAT_ERROR_ENV(env));
61 msat_destroy_config(config);
62
63 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
64 storm::adapters::MathsatExpressionAdapter adapter(*manager, env);
65
66 storm::expressions::Variable x = manager->declareIntegerVariable("x");
67 storm::expressions::Variable y = manager->declareIntegerVariable("y");
68
69 storm::expressions::Expression exprAdd = x + y < -y;
70 msat_decl xDecl = msat_declare_function(env, "x", msat_get_integer_type(env));
71 msat_term xVar = msat_make_constant(env, xDecl);
72 msat_decl yDecl = msat_declare_function(env, "y", msat_get_integer_type(env));
73 msat_term yVar = msat_make_constant(env, yDecl);
74 msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), yVar);
75 msat_term msatAdd = msat_make_plus(env, xVar, yVar);
76 msat_term msatLess = msat_make_and(env, msat_make_leq(env, msatAdd, minusY), msat_make_not(env, msat_make_equal(env, msatAdd, minusY)));
77 msat_term conjecture;
78 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprAdd), msatLess)));
79 msat_assert_formula(env, conjecture);
80 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
81 msat_reset_env(env);
82
83 storm::expressions::Expression exprMult = !(x * y == y);
84 msat_term msatTimes = msat_make_times(env, xVar, yVar);
85 msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, yVar));
86 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprMult), msatNotEqual)));
87 msat_assert_formula(env, conjecture);
88 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
89 msat_reset_env(env);
90}
91
92TEST(MathsatExpressionAdapter, StormToMathsatReal) {
93 msat_config config = msat_create_config();
94 msat_env env = msat_create_env(config);
95 ASSERT_FALSE(MSAT_ERROR_ENV(env));
96 msat_destroy_config(config);
97
98 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
99 storm::adapters::MathsatExpressionAdapter adapter(*manager, env);
100
101 storm::expressions::Variable x = manager->declareRationalVariable("x");
102 storm::expressions::Variable y = manager->declareRationalVariable("y");
103
104 storm::expressions::Expression exprAdd = x + y < -y;
105 msat_decl xDecl = msat_declare_function(env, "x", msat_get_rational_type(env));
106 msat_term xVar = msat_make_constant(env, xDecl);
107 msat_decl yDecl = msat_declare_function(env, "y", msat_get_rational_type(env));
108 msat_term yVar = msat_make_constant(env, yDecl);
109 msat_term minusY = msat_make_times(env, msat_make_number(env, "-1"), yVar);
110 msat_term msatAdd = msat_make_plus(env, xVar, yVar);
111 msat_term msatLess = msat_make_and(env, msat_make_leq(env, msatAdd, minusY), msat_make_not(env, msat_make_equal(env, msatAdd, minusY)));
112 msat_term conjecture;
113 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprAdd), msatLess)));
114 msat_assert_formula(env, conjecture);
115 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
116 msat_reset_env(env);
117
118 storm::expressions::Expression exprMult = !(x * y == y);
119 msat_term msatTimes = msat_make_times(env, xVar, yVar);
120 msat_term msatNotEqual = msat_make_not(env, msat_make_equal(env, msatTimes, yVar));
121 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprMult), msatNotEqual)));
122 msat_assert_formula(env, conjecture);
123 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
124 msat_reset_env(env);
125}
126
127TEST(MathsatExpressionAdapter, StormToMathsatFloorCeil) {
128 msat_config config = msat_create_config();
129 msat_env env = msat_create_env(config);
130 ASSERT_FALSE(MSAT_ERROR_ENV(env));
131 msat_destroy_config(config);
132
133 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
134 storm::adapters::MathsatExpressionAdapter adapter(*manager, env);
135
136 storm::expressions::Variable d = manager->declareRationalVariable("d");
137 storm::expressions::Variable i = manager->declareIntegerVariable("i");
138
139 storm::expressions::Expression exprFloor = storm::expressions::floor(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991);
140 msat_decl iDecl = msat_declare_function(env, "i", msat_get_integer_type(env));
141 msat_term iVar = msat_make_constant(env, iDecl);
142 msat_term msatEqualsFour = msat_make_equal(env, msat_make_number(env, "4"), iVar);
143 msat_term conjecture;
144 msat_term translatedExpr = adapter.translateExpression(exprFloor);
145 msat_term msatIff = msat_make_iff(env, translatedExpr, msatEqualsFour);
146 ASSERT_NO_THROW(conjecture = msat_make_not(env, msatIff));
147 msat_assert_formula(env, conjecture);
148
149 // It is not logically equivalent, so this should be satisfiable.
150 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_SAT);
151 msat_reset_env(env);
152 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_or(env, msat_make_not(env, adapter.translateExpression(exprFloor)), msatEqualsFour)));
153 msat_assert_formula(env, conjecture);
154
155 // However, the left part implies the right one, which is why this should be unsatisfiable.
156 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_UNSAT);
157 msat_reset_env(env);
158
159 storm::expressions::Expression exprCeil = storm::expressions::ceil(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991);
160 msat_term msatEqualsFive = msat_make_equal(env, msat_make_number(env, "5"), iVar);
161
162 ASSERT_NO_THROW(conjecture = msat_make_not(env, msat_make_iff(env, adapter.translateExpression(exprFloor), msatEqualsFive)));
163 msat_assert_formula(env, conjecture);
164
165 // It is not logically equivalent, so this should be satisfiable.
166 ASSERT_TRUE(msat_solve(env) == msat_result::MSAT_SAT);
167 msat_reset_env(env);
168 ASSERT_NO_THROW(conjecture = msat_make_or(env, msat_make_not(env, adapter.translateExpression(exprFloor)), msatEqualsFive));
169 msat_assert_formula(env, conjecture);
170 msat_reset_env(env);
171}
172
173TEST(MathsatExpressionAdapter, MathsatToStormBasic) {
174 msat_config config = msat_create_config();
175 msat_env env = msat_create_env(config);
176 ASSERT_FALSE(MSAT_ERROR_ENV(env));
177 msat_destroy_config(config);
178
179 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
180 manager->declareBooleanVariable("x");
181 manager->declareBooleanVariable("y");
182 storm::adapters::MathsatExpressionAdapter adapter(*manager, env);
183
184 msat_term msatTrue = msat_make_true(env);
185 storm::expressions::Expression exprTrue;
186 ASSERT_NO_THROW(exprTrue = adapter.translateExpression(msatTrue));
187 ASSERT_TRUE(exprTrue.isTrue());
188
189 msat_term msatFalse = msat_make_false(env);
190 storm::expressions::Expression exprFalse;
191 ASSERT_NO_THROW(exprTrue = adapter.translateExpression(msatFalse));
192 ASSERT_TRUE(exprTrue.isFalse());
193
194 msat_decl xDecl = msat_declare_function(env, "x", msat_get_bool_type(env));
195 msat_term x = msat_make_constant(env, xDecl);
196 msat_decl yDecl = msat_declare_function(env, "y", msat_get_bool_type(env));
197 msat_term y = msat_make_constant(env, yDecl);
198 msat_term msatConjunction = msat_make_and(env, x, y);
199 storm::expressions::Expression exprConjunction;
200 ASSERT_NO_THROW(exprConjunction = adapter.translateExpression(msatConjunction));
201 ASSERT_EQ(storm::expressions::OperatorType::And, exprConjunction.getOperator());
202 ASSERT_TRUE(exprConjunction.getOperand(0).isVariable());
203 ASSERT_EQ("x", exprConjunction.getOperand(0).getIdentifier());
204 ASSERT_TRUE(exprConjunction.getOperand(1).isVariable());
205 ASSERT_EQ("y", exprConjunction.getOperand(1).getIdentifier());
206
207 msat_term msatNor = msat_make_not(env, msat_make_or(env, x, y));
208 storm::expressions::Expression exprNor;
209 ASSERT_NO_THROW(exprNor = adapter.translateExpression(msatNor));
210 ASSERT_EQ(storm::expressions::OperatorType::Not, exprNor.getOperator());
211 ASSERT_EQ(storm::expressions::OperatorType::Or, exprNor.getOperand(0).getOperator());
212 ASSERT_TRUE(exprNor.getOperand(0).getOperand(0).isVariable());
213 ASSERT_EQ("x", exprNor.getOperand(0).getOperand(0).getIdentifier());
214 ASSERT_TRUE(exprNor.getOperand(0).getOperand(1).isVariable());
215 ASSERT_EQ("y", exprNor.getOperand(0).getOperand(1).getIdentifier());
216}
217#endif
TEST
TEST(RegionConstraintCheckerTest, AffineConstraintHoldsThroughout)
Definition RegionConstraintCheckerTest.cpp:75
storm::expressions::Expression::isVariable
bool isVariable() const
Retrieves whether the expression is a variable.
Definition Expression.cpp:114
storm::expressions::Expression::getOperator
OperatorType getOperator() const
Retrieves the operator of a function application.
Definition Expression.cpp:86
storm::expressions::Expression::getOperand
Expression getOperand(uint_fast64_t operandIndex) const
Retrieves the given operand from the expression.
Definition Expression.cpp:98
storm::expressions::Expression::getIdentifier
std::string const & getIdentifier() const
Retrieves the identifier associated with this expression.
Definition Expression.cpp:102
storm::expressions::Expression::isFalse
bool isFalse() const
Checks if the expression is equal to the boolean literal false.
Definition Expression.cpp:122
storm::expressions::Expression::isTrue
bool isTrue() const
Checks if the expression is equal to the boolean literal true.
Definition Expression.cpp:118
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:71
storm::expressions::ceil
Expression ceil(Expression const &first)
Definition Expression.cpp:468
storm::expressions::floor
Expression floor(Expression const &first)
Definition Expression.cpp:461
storm::settings::manager
SettingsManager const & manager()
Retrieves the settings manager.
Definition SettingsManager.cpp:681
storm_gtest.h