Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Z3ExpressionAdapterTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include <memory>
5#include "storm/storage/expressions/ExpressionManager.h"
6
7#ifdef STORM_HAVE_Z3
8#include "storm/adapters/Z3ExpressionAdapter.h"
9#include "storm/settings/SettingsManager.h"
10#include "storm/storage/expressions/OperatorType.h"
11#include "z3++.h"
12
13TEST(Z3ExpressionAdapter, StormToZ3Basic) {
14 z3::context ctx;
15 z3::solver s(ctx);
16 z3::expr conjecture = ctx.bool_val(false);
17
18 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
19 storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx);
20
21 storm::expressions::Expression exprTrue = manager->boolean(true);
22 z3::expr z3True = ctx.bool_val(true);
23 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprTrue), z3True)));
24 s.add(conjecture);
25 ASSERT_TRUE(s.check() == z3::unsat);
26 s.reset();
27
28 storm::expressions::Expression exprFalse = manager->boolean(false);
29 z3::expr z3False = ctx.bool_val(false);
30 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFalse), z3False)));
31 s.add(conjecture);
32 ASSERT_TRUE(s.check() == z3::unsat);
33 s.reset();
34
35 storm::expressions::Variable x = manager->declareBooleanVariable("x");
36 storm::expressions::Variable y = manager->declareBooleanVariable("y");
37 storm::expressions::Expression exprConjunction = x && y;
38 z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y"));
39
40 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprConjunction), z3Conjunction)));
41 s.add(conjecture);
42 ASSERT_TRUE(s.check() == z3::unsat);
43 s.reset();
44
45 storm::expressions::Expression exprNor = !(x || y);
46 z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y"));
47 ASSERT_NO_THROW(adapter.translateExpression(exprNor)); // Variables already created in adapter.
48 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprNor), z3Nor)));
49 s.add(conjecture);
50 ASSERT_TRUE(s.check() == z3::unsat);
51 s.reset();
52}
53
54TEST(Z3ExpressionAdapter, StormToZ3Integer) {
55 z3::context ctx;
56 z3::solver s(ctx);
57 z3::expr conjecture = ctx.bool_val(false);
58
59 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
60 storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx);
61
62 storm::expressions::Variable x = manager->declareIntegerVariable("x");
63 storm::expressions::Variable y = manager->declareIntegerVariable("y");
64
65 storm::expressions::Expression exprAdd = x + y < -y;
66 z3::expr z3Add = (ctx.int_const("x") + ctx.int_const("y") < -ctx.int_const("y"));
67 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd), z3Add)));
68 s.add(conjecture);
69 ASSERT_TRUE(s.check() == z3::unsat);
70 s.reset();
71
72 storm::expressions::Expression exprMult = !(x * y == y);
73 z3::expr z3Mult = !(ctx.int_const("x") * ctx.int_const("y") == ctx.int_const("y"));
74 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult), z3Mult)));
75 s.add(conjecture);
76 ASSERT_TRUE(s.check() == z3::unsat);
77 s.reset();
78}
79
80TEST(Z3ExpressionAdapter, StormToZ3Real) {
81 z3::context ctx;
82 z3::solver s(ctx);
83 z3::expr conjecture = ctx.bool_val(false);
84
85 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
86 storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx);
87
88 storm::expressions::Variable x = manager->declareRationalVariable("x");
89 storm::expressions::Variable y = manager->declareRationalVariable("y");
90
91 storm::expressions::Expression exprAdd = x + y < -y;
92 z3::expr z3Add = (ctx.real_const("x") + ctx.real_const("y") < -ctx.real_const("y"));
93 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprAdd), z3Add)));
94 s.add(conjecture);
95 ASSERT_TRUE(s.check() == z3::unsat);
96 s.reset();
97
98 storm::expressions::Expression exprMult = !(x * y == y);
99 z3::expr z3Mult = !(ctx.real_const("x") * ctx.real_const("y") == ctx.real_const("y"));
100 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprMult), z3Mult)));
101 s.add(conjecture);
102 ASSERT_TRUE(s.check() == z3::unsat);
103 s.reset();
104}
105
106TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) {
107 z3::context ctx;
108 z3::solver s(ctx);
109 z3::expr conjecture = ctx.bool_val(false);
110
111 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
112 storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx);
113
114 storm::expressions::Variable d = manager->declareRationalVariable("d");
115 storm::expressions::Variable i = manager->declareIntegerVariable("i");
116
117 storm::expressions::Expression exprFloor = storm::expressions::floor(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991);
118 z3::expr z3Floor = ctx.int_val(4) == ctx.int_const("i");
119
120 conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFloor), z3Floor));
121 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFloor), z3Floor)));
122 s.add(conjecture);
123
124 // It is not logically equivalent, so this should be satisfiable.
125 ASSERT_TRUE(s.check() == z3::sat);
126 s.reset();
127 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprFloor), z3Floor)));
128 s.add(conjecture);
129
130 // However, the left part implies the right one, which is why this should be unsatisfiable.
131 ASSERT_TRUE(s.check() == z3::unsat);
132 s.reset();
133
134 storm::expressions::Expression exprCeil = storm::expressions::ceil(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991);
135 z3::expr z3Ceil = ctx.int_val(5) == ctx.int_const("i");
136
137 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprCeil), z3Ceil)));
138 s.add(conjecture);
139 // It is not logically equivalent, so this should be satisfiable.
140 ASSERT_TRUE(s.check() == z3::sat);
141 s.reset();
142 ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_implies(ctx, adapter.translateExpression(exprCeil), z3Ceil)));
143 s.add(conjecture);
144
145 // However, the left part implies the right one, which is why this should be unsatisfiable.
146 ASSERT_TRUE(s.check() == z3::unsat);
147 s.reset();
148}
149
150TEST(Z3ExpressionAdapter, Z3ToStormBasic) {
151 z3::context ctx;
152
153 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
154 manager->declareBooleanVariable("x");
155 manager->declareBooleanVariable("y");
156 storm::adapters::Z3ExpressionAdapter adapter(*manager, ctx);
157
158 z3::expr z3True = ctx.bool_val(true);
159 storm::expressions::Expression exprTrue;
160 exprTrue = adapter.translateExpression(z3True);
161 ASSERT_TRUE(exprTrue.isTrue());
162
163 z3::expr z3False = ctx.bool_val(false);
164 storm::expressions::Expression exprFalse;
165 exprFalse = adapter.translateExpression(z3False);
166 ASSERT_TRUE(exprFalse.isFalse());
167
168 z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y"));
169 storm::expressions::Expression exprConjunction;
170 (exprConjunction = adapter.translateExpression(z3Conjunction));
171 ASSERT_EQ(storm::expressions::OperatorType::And, exprConjunction.getOperator());
172 ASSERT_TRUE(exprConjunction.getOperand(0).isVariable());
173 ASSERT_EQ("x", exprConjunction.getOperand(0).getIdentifier());
174 ASSERT_TRUE(exprConjunction.getOperand(1).isVariable());
175 ASSERT_EQ("y", exprConjunction.getOperand(1).getIdentifier());
176
177 z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y"));
178 storm::expressions::Expression exprNor;
179 (exprNor = adapter.translateExpression(z3Nor));
180 ASSERT_EQ(storm::expressions::OperatorType::Not, exprNor.getOperator());
181 ASSERT_EQ(storm::expressions::OperatorType::Or, exprNor.getOperand(0).getOperator());
182 ASSERT_TRUE(exprNor.getOperand(0).getOperand(0).isVariable());
183 ASSERT_EQ("x", exprNor.getOperand(0).getOperand(0).getIdentifier());
184 ASSERT_TRUE(exprNor.getOperand(0).getOperand(1).isVariable());
185 ASSERT_EQ("y", exprNor.getOperand(0).getOperand(1).getIdentifier());
186}
187#endif
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
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:72
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:662
storm_gtest.h