Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Cvc5ExpressionAdapterTest.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/adapters/Cvc5ExpressionAdapter.h"
6#include "storm/storage/expressions/ExpressionManager.h"
7#include "storm/storage/expressions/IntegerLiteralExpression.h"
8#include "storm/storage/expressions/OperatorType.h"
9#include "storm/storage/expressions/RationalLiteralExpression.h"
10#include "storm/storage/expressions/VariableExpression.h"
11
12namespace {
17void assertEquivalent(storm::expressions::Expression const& expression, cvc5::Term const& term, cvc5::TermManager& termManager, cvc5::Solver& solver,
18 storm::adapters::Cvc5ExpressionAdapter& adapter) {
19 // Note that the variables occurring in the term have to be the ones that the adapter uses. Two constants with the
20 // same name are distinct variables for cvc5.
21 cvc5::Term equivalence = termManager.mkTerm(cvc5::Kind::EQUAL, {adapter.translateExpression(expression), term});
22 solver.assertFormula(termManager.mkTerm(cvc5::Kind::NOT, {equivalence}));
23 ASSERT_TRUE(solver.checkSat().isUnsat()) << "Not equivalent: " << expression << " (" << adapter.translateExpression(expression) << ") vs " << term;
24 solver.resetAssertions();
25}
26} // namespace
27
28TEST(Cvc5ExpressionAdapter, StormToCvc5Boolean) {
29 cvc5::TermManager termManager;
30 cvc5::Solver solver(termManager);
31
32 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
33 storm::adapters::Cvc5ExpressionAdapter adapter(*manager, solver);
34
35 storm::expressions::Variable x = manager->declareBooleanVariable("x");
36 storm::expressions::Variable y = manager->declareBooleanVariable("y");
37
38 cvc5::Term cvc5X = adapter.translateExpression(x);
39 cvc5::Term cvc5Y = adapter.translateExpression(y);
40
41 assertEquivalent(manager->boolean(true), termManager.mkBoolean(true), termManager, solver, adapter);
42 assertEquivalent(manager->boolean(false), termManager.mkBoolean(false), termManager, solver, adapter);
43 assertEquivalent(x && y, termManager.mkTerm(cvc5::Kind::AND, {cvc5X, cvc5Y}), termManager, solver, adapter);
44 assertEquivalent(x || y, termManager.mkTerm(cvc5::Kind::OR, {cvc5X, cvc5Y}), termManager, solver, adapter);
45 assertEquivalent(!(x && y), termManager.mkTerm(cvc5::Kind::NOT, {termManager.mkTerm(cvc5::Kind::AND, {cvc5X, cvc5Y})}), termManager, solver, adapter);
46 assertEquivalent(storm::expressions::iff(x, y), termManager.mkTerm(cvc5::Kind::EQUAL, {cvc5X, cvc5Y}), termManager, solver, adapter);
47 assertEquivalent(storm::expressions::implies(x, y), termManager.mkTerm(cvc5::Kind::IMPLIES, {cvc5X, cvc5Y}), termManager, solver, adapter);
48}
49
50TEST(Cvc5ExpressionAdapter, StormToCvc5Integer) {
51 cvc5::TermManager termManager;
52 cvc5::Solver solver(termManager);
53
54 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
55 storm::adapters::Cvc5ExpressionAdapter adapter(*manager, solver);
56
57 storm::expressions::Variable x = manager->declareIntegerVariable("x");
58 storm::expressions::Variable y = manager->declareIntegerVariable("y");
59
60 cvc5::Term cvc5X = adapter.translateExpression(x);
61 cvc5::Term cvc5Y = adapter.translateExpression(y);
62
63 assertEquivalent(manager->integer(0), termManager.mkInteger(0), termManager, solver, adapter);
64 assertEquivalent(manager->integer(-13), termManager.mkInteger(-13), termManager, solver, adapter);
65 assertEquivalent(x + y, termManager.mkTerm(cvc5::Kind::ADD, {cvc5X, cvc5Y}), termManager, solver, adapter);
66 assertEquivalent(x - y, termManager.mkTerm(cvc5::Kind::SUB, {cvc5X, cvc5Y}), termManager, solver, adapter);
67 assertEquivalent(-x, termManager.mkTerm(cvc5::Kind::NEG, {cvc5X}), termManager, solver, adapter);
68 assertEquivalent(x * y, termManager.mkTerm(cvc5::Kind::MULT, {cvc5X, cvc5Y}), termManager, solver, adapter);
69 assertEquivalent(x + y < -y,
70 termManager.mkTerm(cvc5::Kind::LT, {termManager.mkTerm(cvc5::Kind::ADD, {cvc5X, cvc5Y}), termManager.mkTerm(cvc5::Kind::NEG, {cvc5Y})}),
71 termManager, solver, adapter);
72 assertEquivalent(storm::expressions::pow(x, manager->integer(2), true), termManager.mkTerm(cvc5::Kind::POW, {cvc5X, termManager.mkInteger(2)}), termManager,
73 solver, adapter);
74}
75
76TEST(Cvc5ExpressionAdapter, StormToCvc5Real) {
77 cvc5::TermManager termManager;
78 cvc5::Solver solver(termManager);
79
80 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
81 storm::adapters::Cvc5ExpressionAdapter adapter(*manager, solver);
82
83 storm::expressions::Variable x = manager->declareRationalVariable("x");
84 storm::expressions::Variable y = manager->declareRationalVariable("y");
85
86 cvc5::Term cvc5X = adapter.translateExpression(x);
87 cvc5::Term cvc5Y = adapter.translateExpression(y);
88
89 assertEquivalent(manager->rational(storm::RationalNumber(1, 2)), termManager.mkReal(1, 2), termManager, solver, adapter);
90 assertEquivalent(manager->rational(storm::RationalNumber(-3, 4)), termManager.mkReal(-3, 4), termManager, solver, adapter);
91 assertEquivalent(x + y, termManager.mkTerm(cvc5::Kind::ADD, {cvc5X, cvc5Y}), termManager, solver, adapter);
92 assertEquivalent(x - y, termManager.mkTerm(cvc5::Kind::SUB, {cvc5X, cvc5Y}), termManager, solver, adapter);
93 assertEquivalent(-x, termManager.mkTerm(cvc5::Kind::NEG, {cvc5X}), termManager, solver, adapter);
94 assertEquivalent(x * y, termManager.mkTerm(cvc5::Kind::MULT, {cvc5X, cvc5Y}), termManager, solver, adapter);
95 assertEquivalent(x / y, termManager.mkTerm(cvc5::Kind::DIVISION, {cvc5X, cvc5Y}), termManager, solver, adapter);
96 assertEquivalent(storm::expressions::Expression(x) < storm::expressions::Expression(y), termManager.mkTerm(cvc5::Kind::LT, {cvc5X, cvc5Y}), termManager,
97 solver, adapter);
98}
99
100TEST(Cvc5ExpressionAdapter, StormToCvc5MixedNumericalTypes) {
101 cvc5::TermManager termManager;
102 cvc5::Solver solver(termManager);
103
104 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
105 storm::adapters::Cvc5ExpressionAdapter adapter(*manager, solver);
106
107 storm::expressions::Variable intVar = manager->declareIntegerVariable("intVar");
108 storm::expressions::Variable realVar = manager->declareRationalVariable("realVar");
109
110 cvc5::Term cvc5IntVar = adapter.translateExpression(intVar);
111 cvc5::Term cvc5RealVar = adapter.translateExpression(realVar);
112 cvc5::Term cvc5ToReal = termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar});
113
114 // Dividing an integer by a rational requires the integer to be converted into a rational.
115 assertEquivalent(intVar / realVar, termManager.mkTerm(cvc5::Kind::DIVISION, {cvc5ToReal, cvc5RealVar}), termManager, solver, adapter);
116
117 // Dividing two integers yields a rational number, so both operands have to be converted.
118 storm::expressions::Variable intVar2 = manager->declareIntegerVariable("intVar2");
119 cvc5::Term cvc5IntVar2 = adapter.translateExpression(intVar2);
120 assertEquivalent(intVar / intVar2, termManager.mkTerm(cvc5::Kind::DIVISION, {cvc5ToReal, termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar2})}),
121 termManager, solver, adapter);
122
123 // Storm types the quotient of two integers as an integer, whereas cvc5 divides over the rational numbers.
124 // Surrounding integer terms must therefore still be translated into a term cvc5 accepts.
125 storm::expressions::Variable intVar3 = manager->declareIntegerVariable("intVar3");
126 cvc5::Term cvc5IntVar3 = adapter.translateExpression(intVar3);
127 assertEquivalent(intVar / intVar2 + intVar3 == manager->integer(0),
128 termManager.mkTerm(cvc5::Kind::EQUAL,
129 {termManager.mkTerm(cvc5::Kind::ADD,
130 {termManager.mkTerm(cvc5::Kind::DIVISION, {termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar}),
131 termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar2})}),
132 termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar3})}),
133 termManager.mkReal(0)}),
134 termManager, solver, adapter);
135
136 // The same holds for the built-in min and max, which cvc5 expresses as an ITE.
137 assertEquivalent(
138 storm::expressions::minimum(intVar / intVar2, intVar3),
139 termManager.mkTerm(
140 cvc5::Kind::ITE,
141 {termManager.mkTerm(cvc5::Kind::LEQ, {termManager.mkTerm(cvc5::Kind::DIVISION, {termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar}),
142 termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar2})}),
143 termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar3})}),
144 termManager.mkTerm(cvc5::Kind::DIVISION,
145 {termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar}), termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar2})}),
146 termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5IntVar3})}),
147 termManager, solver, adapter);
148}
149
150TEST(Cvc5ExpressionAdapter, StormToCvc5FloorAndCeil) {
151 cvc5::TermManager termManager;
152 cvc5::Solver solver(termManager);
153
154 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
155 storm::adapters::Cvc5ExpressionAdapter adapter(*manager, solver);
156
157 storm::expressions::Variable x = manager->declareRationalVariable("x");
158 cvc5::Term cvc5X = adapter.translateExpression(x);
159
160 cvc5::Term cvc5Floor = adapter.translateExpression(storm::expressions::floor(x));
161 cvc5::Term cvc5Ceil = adapter.translateExpression(storm::expressions::ceil(x));
162
163 // The floor and the ceiling of a real number are integers, which we check by looking at the model.
164 solver.assertFormula(termManager.mkTerm(cvc5::Kind::EQUAL, {cvc5X, termManager.mkReal(7, 3)}));
165 solver.assertFormula(termManager.mkTerm(cvc5::Kind::EQUAL, {cvc5Floor, termManager.mkInteger(2)}));
166 solver.assertFormula(termManager.mkTerm(cvc5::Kind::EQUAL, {cvc5Ceil, termManager.mkInteger(3)}));
167 ASSERT_TRUE(solver.checkSat().isSat());
168
169 // Storm's floor is cvc5's to_int, whereas the ceiling is the negation of the floor of the negation.
170 assertEquivalent(storm::expressions::floor(x), termManager.mkTerm(cvc5::Kind::TO_INTEGER, {cvc5X}), termManager, solver, adapter);
171 assertEquivalent(storm::expressions::ceil(x),
172 termManager.mkTerm(cvc5::Kind::NEG, {termManager.mkTerm(cvc5::Kind::TO_INTEGER, {termManager.mkTerm(cvc5::Kind::NEG, {cvc5X})})}),
173 termManager, solver, adapter);
174
175 // The floor and the ceiling of an integer are the integer itself.
176 storm::expressions::Variable intVar = manager->declareIntegerVariable("intVar");
177 cvc5::Term cvc5IntVar = adapter.translateExpression(intVar);
178 assertEquivalent(storm::expressions::floor(intVar), cvc5IntVar, termManager, solver, adapter);
179 assertEquivalent(storm::expressions::ceil(intVar), cvc5IntVar, termManager, solver, adapter);
180}
181
182TEST(Cvc5ExpressionAdapter, StormToCvc5IfThenElse) {
183 cvc5::TermManager termManager;
184 cvc5::Solver solver(termManager);
185
186 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
187 storm::adapters::Cvc5ExpressionAdapter adapter(*manager, solver);
188
189 storm::expressions::Variable x = manager->declareBooleanVariable("x");
190 storm::expressions::Variable y = manager->declareIntegerVariable("y");
191 storm::expressions::Variable z = manager->declareIntegerVariable("z");
192
193 cvc5::Term cvc5X = adapter.translateExpression(x);
194 cvc5::Term cvc5Y = adapter.translateExpression(y);
195 cvc5::Term cvc5Z = adapter.translateExpression(z);
196
197 assertEquivalent(storm::expressions::ite(x, y, z), termManager.mkTerm(cvc5::Kind::ITE, {cvc5X, cvc5Y, cvc5Z}), termManager, solver, adapter);
198
199 // Storm admits an ITE that selects between an integer and a rational number, so the integer branch has to be
200 // converted before the term can be handed to cvc5.
201 storm::expressions::Variable r = manager->declareRationalVariable("r");
202 cvc5::Term cvc5R = adapter.translateExpression(r);
203 assertEquivalent(storm::expressions::ite(x, y, r), termManager.mkTerm(cvc5::Kind::ITE, {cvc5X, termManager.mkTerm(cvc5::Kind::TO_REAL, {cvc5Y}), cvc5R}),
204 termManager, solver, adapter);
205}
206
207TEST(Cvc5ExpressionAdapter, Cvc5ToStorm) {
208 cvc5::TermManager termManager;
209 cvc5::Solver solver(termManager);
210
211 std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
212 storm::adapters::Cvc5ExpressionAdapter adapter(*manager, solver);
213
214 // Boolean constants can be translated back to storm.
215 storm::expressions::Expression translatedTrue = adapter.translateExpression(termManager.mkBoolean(true));
216 ASSERT_TRUE(translatedTrue.isTrue());
217 ASSERT_TRUE(adapter.translateExpression(termManager.mkBoolean(false)).isFalse());
218
219 // cvc5 prints negative integers in the SMT-LIB notation, i.e., as "(- 42)".
220 auto const assertIntegerLiteral = [&adapter, &termManager](int64_t value) {
221 storm::expressions::Expression translated = adapter.translateExpression(termManager.mkInteger(value));
222 auto const* integerLiteral = dynamic_cast<storm::expressions::IntegerLiteralExpression const*>(&translated.getBaseExpression());
223 EXPECT_TRUE(integerLiteral != nullptr);
224 if (integerLiteral != nullptr) {
225 EXPECT_EQ(value, integerLiteral->getValue());
226 }
227 };
228 assertIntegerLiteral(-42);
229 assertIntegerLiteral(0);
230 assertIntegerLiteral(42);
231
232 // cvc5 prints non-integral rationals in the SMT-LIB notation, e.g., 1/2 is printed as "(/ 1 2)" and -3/4 as
233 // "(/ (- 3) 4)", whereas integral rationals are printed in decimal notation.
234 auto const assertRationalLiteral = [&adapter, &termManager](int numerator, int denominator) {
235 storm::expressions::Expression translated = adapter.translateExpression(termManager.mkReal(numerator, denominator));
236 auto const* rationalLiteral = dynamic_cast<storm::expressions::RationalLiteralExpression const*>(&translated.getBaseExpression());
237 EXPECT_TRUE(rationalLiteral != nullptr);
238 if (rationalLiteral != nullptr) {
239 EXPECT_EQ(storm::RationalNumber(numerator, denominator), rationalLiteral->getValue());
240 }
241 };
242 assertRationalLiteral(1, 2);
243 assertRationalLiteral(-3, 4);
244 assertRationalLiteral(7, 3);
245 assertRationalLiteral(2, 1);
246
247 // Free constants and the usual operators can be translated back to storm.
248 storm::expressions::Variable xVar = manager->declareIntegerVariable("x");
249 storm::expressions::Variable yVar = manager->declareIntegerVariable("y");
250 cvc5::Term cvc5X = adapter.translateExpression(xVar);
251 cvc5::Term cvc5Y = adapter.translateExpression(yVar);
252 cvc5::Term cvc5Sum = termManager.mkTerm(cvc5::Kind::ADD, {cvc5X, cvc5Y});
253 cvc5::Term cvc5Less = termManager.mkTerm(cvc5::Kind::LT, {cvc5Sum, termManager.mkInteger(0)});
254
255 storm::expressions::Expression translatedSum = adapter.translateExpression(cvc5Sum);
256 storm::expressions::Expression translatedLess = adapter.translateExpression(cvc5Less);
257
258 ASSERT_EQ(storm::expressions::OperatorType::Plus, translatedSum.getOperator());
259 ASSERT_TRUE(translatedSum.getOperand(0).isVariable());
260 ASSERT_EQ("x", translatedSum.getOperand(0).getIdentifier());
261 ASSERT_TRUE(translatedSum.getOperand(1).isVariable());
262 ASSERT_EQ("y", translatedSum.getOperand(1).getIdentifier());
263
264 ASSERT_EQ(storm::expressions::OperatorType::Less, translatedLess.getOperator());
265 ASSERT_EQ(storm::expressions::OperatorType::Plus, translatedLess.getOperand(0).getOperator());
266 auto const* zeroLiteral = dynamic_cast<storm::expressions::IntegerLiteralExpression const*>(&translatedLess.getOperand(1).getBaseExpression());
267 ASSERT_TRUE(zeroLiteral != nullptr);
268 ASSERT_EQ(0, zeroLiteral->getValue());
269
270 // cvc5 admits sums and products with more than two operands, so all of them have to be taken into account.
271 cvc5::Term cvc5ThreeWaySum = termManager.mkTerm(cvc5::Kind::ADD, {cvc5X, cvc5Y, adapter.translateExpression(manager->integer(3))});
272 storm::expressions::Expression translatedThreeWaySum = adapter.translateExpression(cvc5ThreeWaySum);
273 ASSERT_EQ(storm::expressions::OperatorType::Plus, translatedThreeWaySum.getOperator());
274 EXPECT_EQ((translatedSum + manager->integer(3)).toString(), translatedThreeWaySum.toString());
275
276 cvc5::Term cvc5ThreeWayProduct = termManager.mkTerm(cvc5::Kind::MULT, {cvc5X, cvc5Y, adapter.translateExpression(manager->integer(3))});
277 storm::expressions::Expression translatedThreeWayProduct = adapter.translateExpression(cvc5ThreeWayProduct);
278 ASSERT_EQ(storm::expressions::OperatorType::Times, translatedThreeWayProduct.getOperator());
279 EXPECT_EQ((translatedSum.getOperand(0) * translatedSum.getOperand(1) * manager->integer(3)).toString(), translatedThreeWayProduct.toString());
280
281 // cvc5 also uses EQUAL for boolean equivalence. Translating such a term back has to yield an iff, because storm's
282 // operator== only accepts numerical operands and throws otherwise. This matters for getUnsatAssumptions(), which
283 // translates every assumption of the returned core back.
284 storm::expressions::Variable aVar = manager->declareBooleanVariable("a");
285 storm::expressions::Variable bVar = manager->declareBooleanVariable("b");
286 cvc5::Term cvc5Equivalent = termManager.mkTerm(cvc5::Kind::EQUAL, {adapter.translateExpression(aVar), adapter.translateExpression(bVar)});
287 storm::expressions::Expression translatedEquivalent = adapter.translateExpression(cvc5Equivalent);
288 ASSERT_TRUE(translatedEquivalent.hasBooleanType());
289 EXPECT_EQ(storm::expressions::iff(aVar.getExpression(), bVar.getExpression()).toString(), translatedEquivalent.toString());
290}
291#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::hasBooleanType
bool hasBooleanType() const
Retrieves whether the expression has a boolean return type.
Definition Expression.cpp:193
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::getBaseExpression
BaseExpression const & getBaseExpression() const
Retrieves the base expression underlying this expression object.
Definition Expression.cpp:169
storm::expressions::Expression::toString
std::string toString() const
Converts the expression into a string.
Definition Expression.cpp:236
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::Variable::getExpression
storm::expressions::Expression getExpression() const
Retrieves an expression that represents the variable.
Definition Variable.cpp:34
storm::expressions::ceil
Expression ceil(Expression const &first)
Definition Expression.cpp:468
storm::expressions::ite
Expression ite(Expression const &condition, Expression const &thenExpression, Expression const &elseExpression)
Definition Expression.cpp:425
storm::expressions::iff
Expression iff(Expression const &first, Expression const &second)
Definition Expression.cpp:440
storm::expressions::pow
Expression pow(Expression const &base, Expression const &exponent, bool allowIntegerType)
The type of the resulting expression is.
Definition Expression.cpp:454
storm::expressions::minimum
Expression minimum(Expression const &first, Expression const &second)
Definition Expression.cpp:411
storm::expressions::floor
Expression floor(Expression const &first)
Definition Expression.cpp:461
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::utility::denominator
NumberTraits< RationalType >::IntegerType denominator(RationalType const &number)
storm::utility::numerator
NumberTraits< RationalType >::IntegerType numerator(RationalType const &number)
storm_gtest.h