Storm
A Modern Probabilistic Model Checker
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Z3SmtSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#ifdef STORM_HAVE_Z3
5#include "storm/solver/Z3SmtSolver.h"
6
7TEST(Z3SmtSolver, 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::Z3SmtSolver 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 = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a * b) && b + a > c;
28
29 ASSERT_NO_THROW(s.add(exprFormula));
30 ASSERT_NO_THROW(result = s.check());
31 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
32 ASSERT_NO_THROW(s.reset());
33}
34
35TEST(Z3SmtSolver, CheckUnsat) {
36 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
37
38 storm::expressions::Variable x = manager->declareBooleanVariable("x");
39 storm::expressions::Variable y = manager->declareBooleanVariable("y");
40
41 storm::solver::Z3SmtSolver s(*manager);
42 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
43
44 storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y);
45
46 ASSERT_NO_THROW(s.add(!exprDeMorgan));
47 ASSERT_NO_THROW(result = s.check());
48 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
49 ASSERT_NO_THROW(s.reset());
50
51 storm::expressions::Variable a = manager->declareIntegerVariable("a");
52 storm::expressions::Variable b = manager->declareIntegerVariable("b");
53 storm::expressions::Variable c = manager->declareIntegerVariable("c");
54
55 storm::expressions::Expression exprFormula =
56 a >= manager->rational(2) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b + manager->integer(1)) && b + a > c;
57
58 ASSERT_NO_THROW(s.add(exprFormula));
59 ASSERT_NO_THROW(result = s.check());
60 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
61}
62
63TEST(Z3SmtSolver, Backtracking) {
64 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
65
66 storm::solver::Z3SmtSolver s(*manager);
67 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
68
69 storm::expressions::Expression expr1 = manager->boolean(true);
70 storm::expressions::Expression expr2 = manager->boolean(false);
71 storm::expressions::Expression expr3 = manager->boolean(false);
72
73 ASSERT_NO_THROW(s.add(expr1));
74 ASSERT_NO_THROW(result = s.check());
75 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
76 ASSERT_NO_THROW(s.push());
77 ASSERT_NO_THROW(s.add(expr2));
78 ASSERT_NO_THROW(result = s.check());
79 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
80 ASSERT_NO_THROW(s.pop());
81 ASSERT_NO_THROW(result = s.check());
82 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
83 ASSERT_NO_THROW(s.push());
84 ASSERT_NO_THROW(s.add(expr2));
85 ASSERT_NO_THROW(result = s.check());
86 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
87 ASSERT_NO_THROW(s.push());
88 ASSERT_NO_THROW(s.add(expr3));
89 ASSERT_NO_THROW(result = s.check());
90 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
91 ASSERT_NO_THROW(s.pop(2));
92 ASSERT_NO_THROW(result = s.check());
93 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
94 ASSERT_NO_THROW(s.reset());
95
96 storm::expressions::Variable a = manager->declareIntegerVariable("a");
97 storm::expressions::Variable b = manager->declareIntegerVariable("b");
98 storm::expressions::Variable c = manager->declareIntegerVariable("c");
99 storm::expressions::Expression exprFormula =
100 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b - manager->integer(1)) && b + a > c;
101 storm::expressions::Expression exprFormula2 = c > a + b + manager->integer(1);
102
103 ASSERT_NO_THROW(s.add(exprFormula));
104 ASSERT_NO_THROW(result = s.check());
105 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
106 ASSERT_NO_THROW(s.push());
107 ASSERT_NO_THROW(s.add(exprFormula2));
108 ASSERT_NO_THROW(result = s.check());
109 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
110 ASSERT_NO_THROW(s.pop());
111 ASSERT_NO_THROW(result = s.check());
112 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
113}
114
115TEST(Z3SmtSolver, Assumptions) {
116 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
117
118 storm::solver::Z3SmtSolver s(*manager);
119 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
120
121 storm::expressions::Variable a = manager->declareIntegerVariable("a");
122 storm::expressions::Variable b = manager->declareIntegerVariable("b");
123 storm::expressions::Variable c = manager->declareIntegerVariable("c");
124 storm::expressions::Expression exprFormula =
125 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
126 storm::expressions::Variable f2 = manager->declareBooleanVariable("f2");
127 storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1));
128
129 ASSERT_NO_THROW(s.add(exprFormula));
130 ASSERT_NO_THROW(result = s.check());
131 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
132 ASSERT_NO_THROW(s.add(exprFormula2));
133 ASSERT_NO_THROW(result = s.check());
134 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
135 ASSERT_NO_THROW(result = s.checkWithAssumptions({f2}));
136 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
137 ASSERT_NO_THROW(result = s.check());
138 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
139 ASSERT_NO_THROW(result = s.checkWithAssumptions({!f2}));
140 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
141}
142
143TEST(Z3SmtSolver, GenerateModel) {
144 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
145
146 storm::solver::Z3SmtSolver s(*manager);
147 storm::solver::SmtSolver::CheckResult result;
148
149 storm::expressions::Variable a = manager->declareIntegerVariable("a");
150 storm::expressions::Variable b = manager->declareIntegerVariable("b");
151 storm::expressions::Variable c = manager->declareIntegerVariable("c");
152 storm::expressions::Expression exprFormula =
153 a > manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
154
155 s.add(exprFormula);
156 result = s.check();
157 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
158 std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
159 int_fast64_t aEval = model->getIntegerValue(a);
160 int_fast64_t bEval = model->getIntegerValue(b);
161 int_fast64_t cEval = model->getIntegerValue(c);
162 ASSERT_TRUE(cEval == aEval + bEval - 1);
163}
164
165TEST(Z3SmtSolver, AllSat) {
166 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
167
168 storm::solver::Z3SmtSolver s(*manager);
169
170 storm::expressions::Variable a = manager->declareIntegerVariable("a");
171 storm::expressions::Variable b = manager->declareIntegerVariable("b");
172 storm::expressions::Variable x = manager->declareBooleanVariable("x");
173 storm::expressions::Variable y = manager->declareBooleanVariable("y");
174 storm::expressions::Variable z = manager->declareBooleanVariable("z");
175 storm::expressions::Expression exprFormula1 = storm::expressions::implies(x, a > manager->integer(5));
176 storm::expressions::Expression exprFormula2 = storm::expressions::implies(y, a < manager->integer(5));
177 storm::expressions::Expression exprFormula3 = storm::expressions::implies(z, b < manager->integer(5));
178
179 s.add(exprFormula1);
180 s.add(exprFormula2);
181 s.add(exprFormula3);
182
183 std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x, y});
184
185 ASSERT_TRUE(valuations.size() == 3);
186 for (uint64_t i = 0; i < valuations.size(); ++i) {
187 ASSERT_FALSE(valuations[i].getBooleanValue(x) && valuations[i].getBooleanValue(y));
188
189 for (uint64_t j = i + 1; j < valuations.size(); ++j) {
190 ASSERT_TRUE((valuations[i].getBooleanValue(x) != valuations[j].getBooleanValue(x)) ||
191 (valuations[i].getBooleanValue(y) != valuations[j].getBooleanValue(y)));
192 }
193 }
194}
195
196TEST(Z3SmtSolver, UnsatAssumptions) {
197 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
198
199 storm::solver::Z3SmtSolver s(*manager);
200 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
201
202 storm::expressions::Variable a = manager->declareIntegerVariable("a");
203 storm::expressions::Variable b = manager->declareIntegerVariable("b");
204 storm::expressions::Variable c = manager->declareIntegerVariable("c");
205 storm::expressions::Expression exprFormula =
206 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
207 storm::expressions::Variable f2 = manager->declareBooleanVariable("f2");
208 storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1));
209
210 s.add(exprFormula);
211 s.add(exprFormula2);
212 result = s.checkWithAssumptions({f2});
213 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
214 std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
215 ASSERT_EQ(1ull, unsatCore.size());
216 ASSERT_TRUE(unsatCore[0].isVariable());
217 ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
218}
219
220#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::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