Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Cvc5SmtSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#ifdef STORM_HAVE_CVC5
5#include "storm/exceptions/InvalidTypeException.h"
6#include "storm/solver/Cvc5SmtSolver.h"
7#include "storm/storage/expressions/OperatorType.h"
8
9TEST(Cvc5SmtSolver, CheckSat) {
10 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
11
12 storm::expressions::Variable x = manager->declareBooleanVariable("x");
13 storm::expressions::Variable y = manager->declareBooleanVariable("y");
14
15 storm::solver::Cvc5SmtSolver s(*manager);
16 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
17
18 storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y);
19
20 ASSERT_NO_THROW(s.add(exprDeMorgan));
21 ASSERT_NO_THROW(result = s.check());
22 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
23 ASSERT_NO_THROW(s.reset());
24
25 storm::expressions::Variable a = manager->declareIntegerVariable("a");
26 storm::expressions::Variable b = manager->declareIntegerVariable("b");
27 storm::expressions::Variable c = manager->declareIntegerVariable("c");
28
29 storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a * b) && b + a > c;
30
31 ASSERT_NO_THROW(s.add(exprFormula));
32 ASSERT_NO_THROW(result = s.check());
33 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
34 ASSERT_NO_THROW(s.reset());
35}
36
37TEST(Cvc5SmtSolver, CheckUnsat) {
38 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
39
40 storm::expressions::Variable x = manager->declareBooleanVariable("x");
41 storm::expressions::Variable y = manager->declareBooleanVariable("y");
42
43 storm::solver::Cvc5SmtSolver s(*manager);
44 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
45
46 storm::expressions::Expression exprDeMorgan = storm::expressions::iff(!(x && y), !x || !y);
47
48 ASSERT_NO_THROW(s.add(!exprDeMorgan));
49 ASSERT_NO_THROW(result = s.check());
50 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
51 ASSERT_NO_THROW(s.reset());
52
53 storm::expressions::Variable a = manager->declareIntegerVariable("a");
54 storm::expressions::Variable b = manager->declareIntegerVariable("b");
55 storm::expressions::Variable c = manager->declareIntegerVariable("c");
56
57 storm::expressions::Expression exprFormula =
58 a >= manager->rational(2) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b + manager->integer(1)) && b + a > c;
59
60 ASSERT_NO_THROW(s.add(exprFormula));
61 ASSERT_NO_THROW(result = s.check());
62 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
63 ASSERT_NO_THROW(s.reset());
64}
65
66TEST(Cvc5SmtSolver, Backtracking) {
67 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
68
69 storm::solver::Cvc5SmtSolver s(*manager);
70 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
71
72 storm::expressions::Expression expr1 = manager->boolean(true);
73 storm::expressions::Expression expr2 = manager->boolean(false);
74 storm::expressions::Expression expr3 = manager->boolean(false);
75
76 ASSERT_NO_THROW(s.add(expr1));
77 ASSERT_NO_THROW(result = s.check());
78 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
79 ASSERT_NO_THROW(s.push());
80 ASSERT_NO_THROW(s.add(expr2));
81 ASSERT_NO_THROW(result = s.check());
82 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
83 ASSERT_NO_THROW(s.pop());
84 ASSERT_NO_THROW(result = s.check());
85 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
86 ASSERT_NO_THROW(s.push());
87 ASSERT_NO_THROW(s.add(expr2));
88 ASSERT_NO_THROW(result = s.check());
89 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
90 ASSERT_NO_THROW(s.push());
91 ASSERT_NO_THROW(s.add(expr3));
92 ASSERT_NO_THROW(result = s.check());
93 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
94 ASSERT_NO_THROW(s.pop(2));
95 ASSERT_NO_THROW(result = s.check());
96 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
97 ASSERT_NO_THROW(s.reset());
98
99 storm::expressions::Variable a = manager->declareIntegerVariable("a");
100 storm::expressions::Variable b = manager->declareIntegerVariable("b");
101 storm::expressions::Variable c = manager->declareIntegerVariable("c");
102 storm::expressions::Expression exprFormula =
103 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == (a + b - manager->integer(1)) && b + a > c;
104 storm::expressions::Expression exprFormula2 = c > a + b + manager->integer(1);
105
106 ASSERT_NO_THROW(s.add(exprFormula));
107 ASSERT_NO_THROW(result = s.check());
108 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
109 ASSERT_NO_THROW(s.push());
110 ASSERT_NO_THROW(s.add(exprFormula2));
111 ASSERT_NO_THROW(result = s.check());
112 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
113 ASSERT_NO_THROW(s.pop());
114 ASSERT_NO_THROW(result = s.check());
115 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
116}
117
118TEST(Cvc5SmtSolver, Assumptions) {
119 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
120
121 storm::solver::Cvc5SmtSolver s(*manager);
122 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
123
124 storm::expressions::Variable a = manager->declareIntegerVariable("a");
125 storm::expressions::Variable b = manager->declareIntegerVariable("b");
126 storm::expressions::Variable c = manager->declareIntegerVariable("c");
127 storm::expressions::Expression exprFormula =
128 a >= manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
129 storm::expressions::Variable f2 = manager->declareBooleanVariable("f2");
130 storm::expressions::Expression exprFormula2 = storm::expressions::implies(f2, c > a + b + manager->integer(1));
131
132 ASSERT_NO_THROW(s.add(exprFormula));
133 ASSERT_NO_THROW(result = s.check());
134 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
135 ASSERT_NO_THROW(s.add(exprFormula2));
136 ASSERT_NO_THROW(result = s.check());
137 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
138 ASSERT_NO_THROW(result = s.checkWithAssumptions({f2}));
139 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
140 ASSERT_NO_THROW(result = s.check());
141 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
142 ASSERT_NO_THROW(result = s.checkWithAssumptions({!f2}));
143 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
144}
145
146TEST(Cvc5SmtSolver, GenerateModel) {
147 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
148
149 storm::solver::Cvc5SmtSolver s(*manager);
150 storm::solver::SmtSolver::CheckResult result;
151
152 storm::expressions::Variable a = manager->declareIntegerVariable("a");
153 storm::expressions::Variable b = manager->declareIntegerVariable("b");
154 storm::expressions::Variable c = manager->declareIntegerVariable("c");
155 storm::expressions::Expression exprFormula =
156 a > manager->integer(0) && a < manager->integer(5) && b > manager->integer(7) && c == a + b - manager->integer(1) && b + a > c;
157
158 s.add(exprFormula);
159 result = s.check();
160 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
161 std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
162 int64_t aEval = model->getIntegerValue(a);
163 int64_t bEval = model->getIntegerValue(b);
164 int64_t cEval = model->getIntegerValue(c);
165 ASSERT_TRUE(cEval == aEval + bEval - 1);
166}
167
168TEST(Cvc5SmtSolver, GenerateValuation) {
169 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
170
171 storm::solver::Cvc5SmtSolver s(*manager);
172 storm::solver::SmtSolver::CheckResult result;
173
174 storm::expressions::Variable a = manager->declareIntegerVariable("a");
175 storm::expressions::Variable b = manager->declareBooleanVariable("b");
176 storm::expressions::Expression exprFormula = a > manager->integer(0) && a < manager->integer(5) && b;
177
178 s.add(exprFormula);
179 result = s.check();
180 ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
181
182 storm::expressions::SimpleValuation valuation = s.getModelAsValuation();
183 ASSERT_NO_THROW(ASSERT_TRUE(valuation.getIntegerValue(a) > 0));
184 ASSERT_NO_THROW(ASSERT_TRUE(valuation.getIntegerValue(a) < 5));
185 ASSERT_NO_THROW(ASSERT_TRUE(valuation.getBooleanValue(b)));
186}
187
188TEST(Cvc5SmtSolver, AllSat) {
189 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
190
191 storm::solver::Cvc5SmtSolver s(*manager);
192
193 storm::expressions::Variable a = manager->declareIntegerVariable("a");
194 storm::expressions::Variable b = manager->declareIntegerVariable("b");
195 storm::expressions::Variable x = manager->declareBooleanVariable("x");
196 storm::expressions::Variable y = manager->declareBooleanVariable("y");
197 storm::expressions::Variable z = manager->declareBooleanVariable("z");
198 storm::expressions::Expression exprFormula1 = storm::expressions::implies(x, a > manager->integer(5));
199 storm::expressions::Expression exprFormula2 = storm::expressions::implies(y, a < manager->integer(5));
200 storm::expressions::Expression exprFormula3 = storm::expressions::implies(z, b < manager->integer(5));
201
202 s.add(exprFormula1);
203 s.add(exprFormula2);
204 s.add(exprFormula3);
205
206 std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x, y});
207
208 ASSERT_TRUE(valuations.size() == 3);
209 for (uint64_t i = 0; i < valuations.size(); ++i) {
210 ASSERT_FALSE(valuations[i].getBooleanValue(x) && valuations[i].getBooleanValue(y));
211
212 for (uint64_t j = i + 1; j < valuations.size(); ++j) {
213 ASSERT_TRUE((valuations[i].getBooleanValue(x) != valuations[j].getBooleanValue(x)) ||
214 (valuations[i].getBooleanValue(y) != valuations[j].getBooleanValue(y)));
215 }
216 }
217}
218
219TEST(Cvc5SmtSolver, AddNotCurrentModel) {
220 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
221
222 storm::solver::Cvc5SmtSolver s(*manager);
223
224 storm::expressions::Variable x = manager->declareBooleanVariable("x");
225
226 // The formula is a tautology, so that both values of x constitute a model.
227 s.add(x || !x);
228
229 std::vector<storm::expressions::SimpleValuation> valuations;
230 while (s.check() == storm::solver::SmtSolver::CheckResult::Sat) {
231 valuations.push_back(s.getModelAsValuation());
232 s.addNotCurrentModel();
233 }
234
235 ASSERT_EQ(2ull, valuations.size());
236 ASSERT_NE(valuations[0].getBooleanValue(x), valuations[1].getBooleanValue(x));
237 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Unsat, s.check());
238}
239
240TEST(Cvc5SmtSolver, ModelReferenceDescribesItsOwnModel) {
241 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
242
243 storm::solver::Cvc5SmtSolver s(*manager);
244
245 storm::expressions::Variable a = manager->declareIntegerVariable("a");
246 storm::expressions::Variable b = manager->declareBooleanVariable("b");
247 s.add(a == manager->integer(42) && b);
248
249 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Sat, s.check());
250 std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
251
252 // The string representation must describe the model that the reference holds.
253 std::string modelString = model->toString();
254 EXPECT_NE(modelString.find("a"), std::string::npos);
255 EXPECT_NE(modelString.find("b"), std::string::npos);
256 EXPECT_NE(modelString.find("42"), std::string::npos);
257
258 // The reference keeps describing that model, even after the solver has moved on.
259 s.addNotCurrentModel();
260 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Unsat, s.check());
261 EXPECT_EQ(modelString, model->toString());
262 EXPECT_EQ(42, model->getIntegerValue(a));
263 EXPECT_TRUE(model->getBooleanValue(b));
264}
265
266TEST(Cvc5SmtSolver, ModelReferenceRejectsValuesOfTheWrongType) {
267 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
268
269 storm::solver::Cvc5SmtSolver s(*manager);
270
271 storm::expressions::Variable a = manager->declareIntegerVariable("a");
272 storm::expressions::Variable b = manager->declareBooleanVariable("b");
273 storm::expressions::Variable c = manager->declareRationalVariable("c");
274 s.add(a == manager->integer(42) && b && c == manager->rational(0.5));
275 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Sat, s.check());
276 std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
277
278 // The values are stored per type, so reading a variable with the wrong getter would access an unrelated
279 // entry instead of reporting the mistake.
280 EXPECT_THROW(model->getBooleanValue(a), storm::exceptions::InvalidTypeException);
281 EXPECT_THROW(model->getBooleanValue(c), storm::exceptions::InvalidTypeException);
282 EXPECT_THROW(model->getIntegerValue(b), storm::exceptions::InvalidTypeException);
283 EXPECT_THROW(model->getIntegerValue(c), storm::exceptions::InvalidTypeException);
284 EXPECT_THROW(model->getRationalValue(a), storm::exceptions::InvalidTypeException);
285 EXPECT_THROW(model->getRationalValue(b), storm::exceptions::InvalidTypeException);
286
287 // The matching getters still work.
288 EXPECT_EQ(42, model->getIntegerValue(a));
289 EXPECT_TRUE(model->getBooleanValue(b));
290 EXPECT_DOUBLE_EQ(0.5, model->getRationalValue(c));
291}
292
293TEST(Cvc5SmtSolver, ModelReferenceReadsBitVectorVariableAsInteger) {
294 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
295
296 storm::solver::Cvc5SmtSolver s(*manager);
297
298 // A bitvector variable is modelled as an unbounded integer, so its value is read with the integer getter, as
299 // IterativePolicySearch does for its scheduler variables.
300 storm::expressions::Variable bv = manager->declareBitVectorVariable("bv", 8);
301 s.add(bv == manager->integer(3));
302 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Sat, s.check());
303 std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
304
305 EXPECT_EQ(3, model->getIntegerValue(bv));
306 EXPECT_THROW(model->getBooleanValue(bv), storm::exceptions::InvalidTypeException);
307}
308
309TEST(Cvc5SmtSolver, ModelReferenceOutlivesItsSolver) {
310 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
311
312 storm::expressions::Variable a = manager->declareIntegerVariable("a");
313 storm::expressions::Variable b = manager->declareBooleanVariable("b");
314 storm::expressions::Variable c = manager->declareRationalVariable("c");
315
316 std::shared_ptr<storm::solver::SmtSolver::ModelReference> model;
317 {
318 storm::solver::Cvc5SmtSolver s(*manager);
319 s.add(a == manager->integer(7) && b && c == manager->rational(0.5));
320 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Sat, s.check());
321 model = s.getModel();
322 }
323
324 // The solver (and its expression adapter) are gone, but the values are still readable.
325 EXPECT_EQ(7, model->getIntegerValue(a));
326 EXPECT_TRUE(model->getBooleanValue(b));
327 EXPECT_DOUBLE_EQ(0.5, model->getRationalValue(c));
328 EXPECT_NO_THROW(model->toString());
329}
330
331TEST(Cvc5SmtSolver, AddNotCurrentModelWithUnconstrainedVariable) {
332 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
333
334 storm::solver::Cvc5SmtSolver s(*manager);
335
336 storm::expressions::Variable x = manager->declareBooleanVariable("x");
337
338 // The tautology does not mention y, so the model does not constrain it. Ruling out the current
339 // model must not constrain y, otherwise models would be missed.
340 storm::expressions::Variable y = manager->declareBooleanVariable("y");
341 s.add(x || !x);
342
343 std::vector<bool> yValues;
344 while (s.check() == storm::solver::SmtSolver::CheckResult::Sat) {
345 yValues.push_back(s.getModelAsValuation().getBooleanValue(y));
346 s.addNotCurrentModel();
347 }
348
349 // x takes both values, and y is free to take both values in each case.
350 ASSERT_EQ(4ull, yValues.size());
351 EXPECT_NE(yValues[0], yValues[1]);
352 EXPECT_NE(yValues[2], yValues[3]);
353}
354
355TEST(Cvc5SmtSolver, AddNotCurrentModelEnumeratesModelsIncrementally) {
356 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
357
358 storm::solver::Cvc5SmtSolver s(*manager);
359
360 storm::expressions::Variable x = manager->declareIntegerVariable("x");
361 storm::expressions::Variable y = manager->declareIntegerVariable("y");
362 s.add(x >= manager->integer(0) && x <= manager->integer(3) && y >= manager->integer(0) && y <= manager->integer(2));
363
364 // Enumerate all models without resetting the solver.
365 uint64_t numberOfModels = 0;
366 while (s.check() == storm::solver::SmtSolver::CheckResult::Sat) {
367 ++numberOfModels;
368 ASSERT_LE(numberOfModels, 12ull);
369 s.addNotCurrentModel(false);
370 }
371 EXPECT_EQ(12ull, numberOfModels);
372}
373
374TEST(Cvc5SmtSolver, AddNotCurrentModelKeepsScopes) {
375 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
376
377 storm::solver::Cvc5SmtSolver s(*manager);
378
379 storm::expressions::Variable x = manager->declareIntegerVariable("x");
380 s.add(x >= manager->integer(0) && x <= manager->integer(1));
381
382 s.push();
383 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Sat, s.check());
384 s.addNotCurrentModel();
385 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Sat, s.check());
386 s.addNotCurrentModel();
387 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Unsat, s.check());
388
389 // The blocking clauses belong to the scope, so popping it makes both models available again.
390 ASSERT_NO_THROW(s.pop());
391 EXPECT_EQ(storm::solver::SmtSolver::CheckResult::Sat, s.check());
392}
393
394TEST(Cvc5SmtSolver, AddNotCurrentModelWithOnlyBitVectorVariables) {
395 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
396
397 storm::solver::Cvc5SmtSolver s(*manager);
398
399 // The bitvector is the only variable, so the blocking clause must not degenerate to "false".
400 storm::expressions::Variable bv = manager->declareBitVectorVariable("bv", 8);
401 s.add(bv == manager->integer(0) || bv == manager->integer(1));
402
403 std::vector<int64_t> values;
404 while (s.check() == storm::solver::SmtSolver::CheckResult::Sat) {
405 values.push_back(s.getModelAsValuation().getIntegerValue(bv));
406 s.addNotCurrentModel();
407 }
408
409 // Both values of the bitvector are models.
410 ASSERT_EQ(2ull, values.size());
411 EXPECT_NE(values[0], values[1]);
412}
413
414TEST(Cvc5SmtSolver, UnsatAssumptions) {
415 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
416
417 storm::solver::Cvc5SmtSolver s(*manager);
418 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
419
420 storm::expressions::Variable a = manager->declareIntegerVariable("a");
421 storm::expressions::Variable b = manager->declareBooleanVariable("b");
422 storm::expressions::Expression exprFormula = a >= manager->integer(0) && a < manager->integer(5);
423 storm::expressions::Expression exprB = b;
424 storm::expressions::Expression exprNotB = !b;
425
426 // The formula is satisfiable on its own, but the two assumptions are contradictory.
427 ASSERT_NO_THROW(s.add(exprFormula));
428 ASSERT_NO_THROW(result = s.checkWithAssumptions({exprB, exprNotB}));
429 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Unsat, result);
430
431 std::vector<storm::expressions::Expression> unsatAssumptions = s.getUnsatAssumptions();
432 ASSERT_EQ(2ull, unsatAssumptions.size());
433
434 auto const isAssumptionB = [](storm::expressions::Expression const& expression) { return expression.isVariable() && expression.getIdentifier() == "b"; };
435 auto const isAssumptionNotB = [&isAssumptionB](storm::expressions::Expression const& expression) {
436 return expression.getOperator() == storm::expressions::OperatorType::Not && isAssumptionB(expression.getOperand(0));
437 };
438 ASSERT_TRUE((isAssumptionB(unsatAssumptions[0]) && isAssumptionNotB(unsatAssumptions[1])) ||
439 (isAssumptionNotB(unsatAssumptions[0]) && isAssumptionB(unsatAssumptions[1])));
440
441 // A satisfiable check does not yield an unsatisfiable core.
442 ASSERT_NO_THROW(result = s.checkWithAssumptions({exprB}));
443 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Sat, result);
444 ASSERT_ANY_THROW(s.getUnsatAssumptions());
445}
446
447TEST(Cvc5SmtSolver, UnsatAssumptionsWithBooleanEquivalence) {
448 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
449
450 storm::solver::Cvc5SmtSolver s(*manager);
451 storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
452
453 storm::expressions::Variable a = manager->declareBooleanVariable("a");
454 storm::expressions::Variable b = manager->declareBooleanVariable("b");
455 storm::expressions::Expression equivalence = storm::expressions::iff(a.getExpression(), b.getExpression());
456 storm::expressions::Expression exprA = a;
457 storm::expressions::Expression exprNotB = !b;
458
459 // a <=> b together with a and !b is contradictory. cvc5 encodes the equivalence as EQUAL, so translating the core
460 // back has to produce iff; storm's == only accepts numerical operands and would throw on boolean operands.
461 ASSERT_NO_THROW(result = s.checkWithAssumptions({equivalence, exprA, exprNotB}));
462 ASSERT_EQ(storm::solver::SmtSolver::CheckResult::Unsat, result);
463
464 std::vector<storm::expressions::Expression> unsatAssumptions;
465 ASSERT_NO_THROW(unsatAssumptions = s.getUnsatAssumptions());
466 EXPECT_FALSE(unsatAssumptions.empty());
467}
468#endif
TEST
TEST(RegionConstraintCheckerTest, AffineConstraintHoldsThroughout)
Definition RegionConstraintCheckerTest.cpp:75
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::SimpleValuation
A simple implementation of the valuation interface.
Definition SimpleValuation.h:17
storm::expressions::SimpleValuation::getIntegerValue
virtual int_fast64_t getIntegerValue(Variable const &integerVariable) const override
Retrieves the value of the given integer variable.
Definition SimpleValuation.cpp:95
storm::expressions::SimpleValuation::getBooleanValue
virtual bool getBooleanValue(Variable const &booleanVariable) const override
Retrieves the value of the given boolean variable.
Definition SimpleValuation.cpp:90
storm::expressions::Variable::getExpression
storm::expressions::Expression getExpression() const
Retrieves an expression that represents the variable.
Definition Variable.cpp:34
storm::solver::SmtSolver::CheckResult
CheckResult
possible check results
Definition SmtSolver.h:24
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:681
storm_gtest.h