Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MathsatSmtSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#ifdef STORM_HAVE_MSAT
5#include "storm/solver/MathsatSmtSolver.h"
6
7TEST(MathsatSmtSolver, CheckSat) {
8 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
9
10 storm::expressions::Variable x = manager->declareBooleanVariable("x");
11 storm::expressions::Variable y = manager->declareBooleanVariable("y");
12
13 storm::solver::MathsatSmtSolver s(*manager);
14 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
15
16 storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y);
17
18 ASSERT_NO_THROW(s.add(exprDeMorgan));
19 ASSERT_NO_THROW(result = s.check());
20 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
21 ASSERT_NO_THROW(s.reset());
22
23 storm::expressions::Variable a = manager->declareIntegerVariable("a");
24 storm::expressions::Variable b = manager->declareIntegerVariable("b");
25 storm::expressions::Variable c = manager->declareIntegerVariable("c");
26
27 storm::expressions::Expression exprFormula =
28 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b - manager->integer(1)) && b + a > c;
29
30 ASSERT_NO_THROW(s.add(exprFormula));
31 ASSERT_NO_THROW(result = s.check());
32 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
33 ASSERT_NO_THROW(s.reset());
34}
35
36TEST(MathsatSmtSolver, CheckUnsat) {
37 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
38
39 storm::expressions::Variable x = manager->declareBooleanVariable("x");
40 storm::expressions::Variable y = manager->declareBooleanVariable("y");
41
42 storm::solver::MathsatSmtSolver s(*manager);
43 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
44
45 storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y);
46
47 ASSERT_NO_THROW(s.add(!exprDeMorgan));
48 ASSERT_NO_THROW(result = s.check());
49 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
50 ASSERT_NO_THROW(s.reset());
51
52 storm::expressions::Variable a = manager->declareIntegerVariable("a");
53 storm::expressions::Variable b = manager->declareIntegerVariable("b");
54 storm::expressions::Variable c = manager->declareIntegerVariable("c");
55
56 storm::expressions::Expression exprFormula =
57 a >= manager->rational(2) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b + manager->integer(1)) && b + a > c;
58
59 ASSERT_NO_THROW(s.add(exprFormula));
60 ASSERT_NO_THROW(result = s.check());
61 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
62}
63
64TEST(MathsatSmtSolver, Backtracking) {
65 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
66
67 storm::solver::MathsatSmtSolver s(*manager);
68 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
69
70 storm::expressions::Expression expr1 = manager->boolean(true);
71 storm::expressions::Expression expr2 = manager->boolean(false);
72 storm::expressions::Expression expr3 = manager->boolean(false);
73
74 ASSERT_NO_THROW(s.add(expr1));
75 ASSERT_NO_THROW(result = s.check());
76 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
77 ASSERT_NO_THROW(s.push());
78 ASSERT_NO_THROW(s.add(expr2));
79 ASSERT_NO_THROW(result = s.check());
80 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
81 ASSERT_NO_THROW(s.pop());
82 ASSERT_NO_THROW(result = s.check());
83 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
84 ASSERT_NO_THROW(s.push());
85 ASSERT_NO_THROW(s.add(expr2));
86 ASSERT_NO_THROW(result = s.check());
87 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
88 ASSERT_NO_THROW(s.push());
89 ASSERT_NO_THROW(s.add(expr3));
90 ASSERT_NO_THROW(result = s.check());
91 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
92 ASSERT_NO_THROW(s.pop(2));
93 ASSERT_NO_THROW(result = s.check());
94 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
95 ASSERT_NO_THROW(s.reset());
96
97 storm::expressions::Variable a = manager->declareIntegerVariable("a");
98 storm::expressions::Variable b = manager->declareIntegerVariable("b");
99 storm::expressions::Variable c = manager->declareIntegerVariable("c");
100 storm::expressions::Expression exprFormula =
101 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b - manager->integer(1)) && b + a > c;
102 storm::expressions::Expression exprFormula2 = c > a + b + manager->integer(1);
103
104 ASSERT_NO_THROW(s.add(exprFormula));
105 ASSERT_NO_THROW(result = s.check());
106 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
107 ASSERT_NO_THROW(s.push());
108 ASSERT_NO_THROW(s.add(exprFormula2));
109 ASSERT_NO_THROW(result = s.check());
110 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
111 ASSERT_NO_THROW(s.pop());
112 ASSERT_NO_THROW(result = s.check());
113 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
114}
115
116TEST(MathsatSmtSolver, Assumptions) {
117 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
118
119 storm::solver::MathsatSmtSolver s(*manager);
120 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
121
122 storm::expressions::Variable a = manager->declareIntegerVariable("a");
123 storm::expressions::Variable b = manager->declareIntegerVariable("b");
124 storm::expressions::Variable c = manager->declareIntegerVariable("c");
125 storm::expressions::Expression exprFormula =
126 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
127 storm::expressions::Variable f2 = manager->declareBooleanVariable("f2");
128 storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1));
129
130 ASSERT_NO_THROW(s.add(exprFormula));
131 ASSERT_NO_THROW(result = s.check());
132 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
133 ASSERT_NO_THROW(s.add(exprFormula2));
134 ASSERT_NO_THROW(result = s.check());
135 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
136 ASSERT_NO_THROW(result = s.checkWithAssumptions({f2}));
137 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
138 ASSERT_NO_THROW(result = s.check());
139 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
140 ASSERT_NO_THROW(result = s.checkWithAssumptions({!f2}));
141 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
142}
143
144TEST(MathsatSmtSolver, GenerateModel) {
145 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
146
147 storm::solver::MathsatSmtSolver s(*manager);
148 storm::solver::SmtSolver::CheckResult result;
149
150 storm::expressions::Variable a = manager->declareIntegerVariable("a");
151 storm::expressions::Variable b = manager->declareIntegerVariable("b");
152 storm::expressions::Variable c = manager->declareIntegerVariable("c");
153 storm::expressions::Expression exprFormula =
154 a > manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
155
156 s.add(exprFormula);
157 result = s.check();
158 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
159 std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
160 int_fast64_t aEval = model->getIntegerValue(a);
161 int_fast64_t bEval = model->getIntegerValue(b);
162 int_fast64_t cEval = model->getIntegerValue(c);
163 ASSERT_TRUE(cEval == aEval + bEval - 1);
164}
165
166TEST(MathsatSmtSolver, AllSat) {
167 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
168
169 storm::solver::MathsatSmtSolver s(*manager);
170
171 storm::expressions::Variable a = manager->declareIntegerVariable("a");
172 storm::expressions::Variable b = manager->declareIntegerVariable("b");
173 storm::expressions::Variable x = manager->declareBooleanVariable("x");
174 storm::expressions::Variable y = manager->declareBooleanVariable("y");
175 storm::expressions::Variable z = manager->declareBooleanVariable("z");
176 storm::expressions::Expression exprFormula1 = storm::expressions::implies(x, a > manager->integer(5));
177 storm::expressions::Expression exprFormula2 = storm::expressions::implies(y, a < manager->integer(5));
178 storm::expressions::Expression exprFormula3 = storm::expressions::implies(z, b < manager->integer(5));
179
180 s.add(exprFormula1);
181 s.add(exprFormula2);
182 s.add(exprFormula3);
183
184 std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x, y});
185
186 ASSERT_TRUE(valuations.size() == 3);
187 for (uint64_t i = 0; i < valuations.size(); ++i) {
188 ASSERT_FALSE(valuations[i].getBooleanValue(x) && valuations[i].getBooleanValue(y));
189
190 for (uint64_t j = i + 1; j < valuations.size(); ++j) {
191 ASSERT_TRUE((valuations[i].getBooleanValue(x) != valuations[j].getBooleanValue(x)) ||
192 (valuations[i].getBooleanValue(y) != valuations[j].getBooleanValue(y)));
193 }
194 }
195}
196
197TEST(MathsatSmtSolver, UnsatAssumptions) {
198 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
199
200 storm::solver::MathsatSmtSolver s(*manager, storm::solver::MathsatSmtSolver::Options(false, true, false));
201 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
202
203 storm::expressions::Variable a = manager->declareIntegerVariable("a");
204 storm::expressions::Variable b = manager->declareIntegerVariable("b");
205 storm::expressions::Variable c = manager->declareIntegerVariable("c");
206 storm::expressions::Expression exprFormula =
207 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
208 storm::expressions::Variable f2 = manager->declareBooleanVariable("f2");
209 storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1));
210
211 s.add(exprFormula);
212 s.add(exprFormula2);
213 result = s.checkWithAssumptions({f2});
214 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
215 std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
216 ASSERT_EQ(1ull, unsatCore.size());
217 ASSERT_TRUE(unsatCore[0].isVariable());
218 ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
219}
220
221TEST(MathsatSmtSolver, InterpolationTest) {
222 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
223
224 storm::solver::MathsatSmtSolver s(*manager, storm::solver::MathsatSmtSolver::Options(false, false, true));
225 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
226
227 storm::expressions::Variable a = manager->declareIntegerVariable("a");
228 storm::expressions::Variable b = manager->declareIntegerVariable("b");
229 storm::expressions::Variable c = manager->declareIntegerVariable("c");
230 storm::expressions::Expression exprFormula = a > b;
231 storm::expressions::Expression exprFormula2 = b > c;
232 storm::expressions::Expression exprFormula3 = c > a;
233
234 s.setInterpolationGroup(0);
235 s.add(exprFormula);
236 s.setInterpolationGroup(1);
237 s.add(exprFormula2);
238 s.setInterpolationGroup(2);
239 s.add(exprFormula3);
240
241 ASSERT_NO_THROW(result = s.check());
242 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
243
244 storm::expressions::Expression interpol;
245 ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1}));
246
247 storm::solver::MathsatSmtSolver s2(*manager);
248
249 ASSERT_NO_THROW(s2.add(!storm::expressions::implies(exprFormula && exprFormula2, interpol)));
250 ASSERT_NO_THROW(result = s2.check());
251 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
252
253 ASSERT_NO_THROW(s2.reset());
254 ASSERT_NO_THROW(s2.add(interpol && exprFormula3));
255 ASSERT_NO_THROW(result = s2.check());
256 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
257}
258
259#endif
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:72
storm::solver::MathsatSmtSolver::Options
A class that captures options that may be passed to the Mathsat solver.
Definition MathsatSmtSolver.h:22
storm::solver::SmtSolver::CheckResult
CheckResult
possible check results
Definition SmtSolver.h:25
storm::expressions::iff
Expression iff(Expression const &first, Expression const &second)
Definition Expression.cpp:440
storm::expressions::implies
Expression implies(Expression const &first, Expression const &second)
Definition Expression.cpp:433
storm::settings::manager
SettingsManager const & manager()
Retrieves the settings manager.
Definition SettingsManager.cpp:662
storm_gtest.h