Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LpSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm/exceptions/InvalidAccessException.h"
5#include "storm/solver/GlpkLpSolver.h"
6#include "storm/solver/GurobiLpSolver.h"
7#include "storm/solver/LpSolver.h"
8#include "storm/solver/OptimizationDirection.h"
9#include "storm/storage/expressions/Expression.h"
10#include "storm/storage/expressions/Variable.h"
11#include "storm/utility/solver.h"
12#include "storm/utility/vector.h"
13namespace {
14
15class DefaultEnvironment {
16 public:
17 typedef double ValueType;
18 static const bool isExact = false;
19 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::FROMSETTINGS;
20 static const bool IntegerSupport = true;
21 static const bool IncrementalSupport = true;
22 static const bool strictRelationSupport = true;
23
24 static bool skip() {
25#ifdef STORM_HAVE_LP_SOLVER
26 return false;
27#else
28 return true;
29#endif
30 }
31};
32
33class GlpkEnvironment {
34 public:
35 typedef double ValueType;
36 static const bool isExact = false;
37 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Glpk;
38 static const bool IntegerSupport = true;
39 static const bool IncrementalSupport = true;
40 static const bool strictRelationSupport = true;
41
42 static bool skip() {
43 return false;
44 }
45};
46
47#ifdef STORM_HAVE_GUROBI
48class GurobiEnvironment {
49 public:
50 typedef double ValueType;
51 static const bool isExact = false;
52 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Gurobi;
53 static const bool IntegerSupport = true;
54 static const bool IncrementalSupport = true;
55 static const bool strictRelationSupport = true;
56
57 static bool skip() {
58 return storm::test::noGurobi;
59 }
60};
61#endif
62
63class Z3Environment {
64 public:
65 typedef storm::RationalNumber ValueType;
66 static const bool isExact = true;
67 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Z3;
68 static const bool IntegerSupport = true;
69 static const bool IncrementalSupport = true;
70 static const bool strictRelationSupport = true;
71
72 static bool skip() {
73 return false;
74 }
75};
76
77#ifdef STORM_HAVE_SOPLEX
78class SoplexEnvironment {
79 public:
80 typedef double ValueType;
81 static const bool isExact = false;
82 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Soplex;
83 static const bool IntegerSupport = false;
84 static const bool IncrementalSupport = false;
85 static const bool strictRelationSupport = false;
86
87 static bool skip() {
88 return false;
89 }
90};
91
92class SoplexExactEnvironment {
93 public:
94 typedef storm::RationalNumber ValueType;
95 static const bool isExact = true;
96 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Soplex;
97 static const bool IntegerSupport = false;
98 static const bool IncrementalSupport = false;
99 static const bool strictRelationSupport = false;
100
101 static bool skip() {
102 return false;
103 }
104};
105#endif
106
107template<typename TestType>
108class LpSolverTest : public ::testing::Test {
109 public:
110 typedef typename TestType::ValueType ValueType;
111
112 void SetUp() override {
113 if (skipped()) {
114 GTEST_SKIP();
115 }
116 }
117
118 storm::solver::LpSolverTypeSelection solverSelection() const {
119 return TestType::solverSelection;
120 }
121
122 std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> factory() const {
123 return storm::utility::solver::getLpSolverFactory<ValueType>(solverSelection());
124 }
125
126 ValueType parseNumber(std::string const& input) const {
127 return storm::utility::convertNumber<ValueType>(input);
128 }
129
130 ValueType precision() const {
131 return TestType::isExact ? parseNumber("0") : parseNumber("1e-15");
132 }
133
134 bool supportsInteger() const {
135 return TestType::IntegerSupport;
136 }
137
138 bool supportsIncremental() const {
139 return TestType::IncrementalSupport;
140 }
141
142 bool supportsStrictRelation() const {
143 return TestType::strictRelationSupport;
144 }
145
146 bool skipped() const {
147 return TestType::skip();
148 }
149};
150
151typedef ::testing::Types<DefaultEnvironment
152#ifdef STORM_HAVE_GLPK
153 ,
154 GlpkEnvironment
155#endif
156#ifdef STORM_HAVE_GUROBI
157 ,
158 GurobiEnvironment
159#endif
160#ifdef STORM_HAVE_Z3_OPTIMIZE
161 ,
162 Z3Environment
163#endif
164#ifdef STORM_HAVE_SOPLEX
165 ,
166 SoplexEnvironment, SoplexExactEnvironment
167#endif
168 >
169 TestingTypes;
170
171TYPED_TEST_SUITE(LpSolverTest, TestingTypes, );
172
173TYPED_TEST(LpSolverTest, LPOptimizeMax) {
174 typedef typename TestFixture::ValueType ValueType;
175 auto solver = this->factory()->create("");
176 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
177 storm::expressions::Variable x;
178 storm::expressions::Variable y;
179 storm::expressions::Variable z;
180 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
181 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
182 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
183 ASSERT_NO_THROW(solver->update());
184
185 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
186 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
187 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
188 ASSERT_NO_THROW(solver->update());
189
190 ASSERT_NO_THROW(solver->optimize());
191 ASSERT_TRUE(solver->isOptimal());
192 ASSERT_FALSE(solver->isUnbounded());
193 ASSERT_FALSE(solver->isInfeasible());
194 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
195 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(y), this->precision());
196 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(z), this->precision());
197 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
198}
199
200TYPED_TEST(LpSolverTest, LPOptimizeMaxRaw) {
201 typedef typename TestFixture::ValueType ValueType;
202 auto solver = this->factory()->createRaw("");
203 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
204 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
205 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
206 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 1));
207 ASSERT_NO_THROW(solver->update());
208
209 // x + y + z <= 12
210 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
211 constraint1.addToLhs(0, this->parseNumber("1"));
212 constraint1.addToLhs(1, this->parseNumber("1"));
213 constraint1.addToLhs(2, this->parseNumber("1"));
214 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
215 // -x + 1/2 * y + z == 5
216 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::Equal, this->parseNumber("5"), 3);
217 constraint2.addToLhs(0, -this->parseNumber("1"));
218 constraint2.addToLhs(1, this->parseNumber("1/2"));
219 constraint2.addToLhs(2, this->parseNumber("1"));
220 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
221 // -x + y <= 11/2
222 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
223 constraint3.addToLhs(0, -this->parseNumber("1"));
224 constraint3.addToLhs(1, this->parseNumber("1"));
225 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
226 ASSERT_NO_THROW(solver->update());
227
228 ASSERT_NO_THROW(solver->optimize());
229 ASSERT_TRUE(solver->isOptimal());
230 ASSERT_FALSE(solver->isUnbounded());
231 ASSERT_FALSE(solver->isInfeasible());
232 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
233 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(1), this->precision());
234 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(2), this->precision());
235 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
236}
237
238TYPED_TEST(LpSolverTest, LPOptimizeMin) {
239 typedef typename TestFixture::ValueType ValueType;
240 auto solver = this->factory()->create("");
241 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
242 storm::expressions::Variable x;
243 storm::expressions::Variable y;
244 storm::expressions::Variable z;
245 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
246 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
247 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
248 ASSERT_NO_THROW(solver->update());
249
250 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
251 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
252 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
253 ASSERT_NO_THROW(solver->update());
254
255 ASSERT_NO_THROW(solver->optimize());
256 ASSERT_TRUE(solver->isOptimal());
257 ASSERT_FALSE(solver->isUnbounded());
258 ASSERT_FALSE(solver->isInfeasible());
259
260 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
261 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(y), this->precision());
262 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(z), this->precision());
263 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
264}
265
266TYPED_TEST(LpSolverTest, LPOptimizeMinRaw) {
267 typedef typename TestFixture::ValueType ValueType;
268 auto solver = this->factory()->createRaw("");
269 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
270
271 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
272 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
273 ASSERT_EQ(2u, solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
274 ASSERT_NO_THROW(solver->update());
275
276 // x + y + z <= 12
277 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
278 constraint1.addToLhs(0, this->parseNumber("1"));
279 constraint1.addToLhs(1, this->parseNumber("1"));
280 constraint1.addToLhs(2, this->parseNumber("1"));
281 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
282 // -x + 1/2 * y + z <= 5
283 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::LessOrEqual, this->parseNumber("5"), 3);
284 constraint2.addToLhs(0, -this->parseNumber("1"));
285 constraint2.addToLhs(1, this->parseNumber("1/2"));
286 constraint2.addToLhs(2, this->parseNumber("1"));
287 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
288 // -x + y <= 11/2
289 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
290 constraint3.addToLhs(0, -this->parseNumber("1"));
291 constraint3.addToLhs(1, this->parseNumber("1"));
292 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
293 ASSERT_NO_THROW(solver->update());
294
295 ASSERT_NO_THROW(solver->optimize());
296 ASSERT_TRUE(solver->isOptimal());
297 ASSERT_FALSE(solver->isUnbounded());
298 ASSERT_FALSE(solver->isInfeasible());
299
300 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
301 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(1), this->precision());
302 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(2), this->precision());
303 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
304}
305
306TYPED_TEST(LpSolverTest, MILPOptimizeMax) {
307 if (!this->supportsInteger()) {
308 GTEST_SKIP();
309 }
310 typedef typename TestFixture::ValueType ValueType;
311 auto solver = this->factory()->create("");
312 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
313 storm::expressions::Variable x;
314 storm::expressions::Variable y;
315 storm::expressions::Variable z;
316 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
317 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
318 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
319 ASSERT_NO_THROW(solver->update());
320
321 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
322 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
323 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
324 ASSERT_NO_THROW(solver->update());
325 ASSERT_NO_THROW(solver->optimize());
326 ASSERT_TRUE(solver->isOptimal());
327 ASSERT_FALSE(solver->isUnbounded());
328 ASSERT_FALSE(solver->isInfeasible());
329
330 EXPECT_TRUE(solver->getBinaryValue(x));
331 EXPECT_EQ(6, solver->getIntegerValue(y));
332 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(z), this->precision());
333 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
334}
335
336TYPED_TEST(LpSolverTest, MILPOptimizeMaxRaw) {
337 if (!this->supportsInteger()) {
338 GTEST_SKIP();
339 }
340 typedef typename TestFixture::ValueType ValueType;
341 auto solver = this->factory()->createRaw("");
342 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
343 storm::expressions::Variable x;
344 storm::expressions::Variable y;
345 storm::expressions::Variable z;
346 ASSERT_EQ(0u, solver->addBinaryVariable("x", -1));
347 ASSERT_EQ(1u, solver->addLowerBoundedIntegerVariable("y", 0, 2));
348 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 1));
349 ASSERT_NO_THROW(solver->update());
350
351 // x + y + z <= 12
352 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
353 constraint1.addToLhs(0, this->parseNumber("1"));
354 constraint1.addToLhs(1, this->parseNumber("1"));
355 constraint1.addToLhs(2, this->parseNumber("1"));
356 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
357 // -x + 1/2 * y + z == 5
358 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::Equal, this->parseNumber("5"), 3);
359 constraint2.addToLhs(0, -this->parseNumber("1"));
360 constraint2.addToLhs(1, this->parseNumber("1/2"));
361 constraint2.addToLhs(2, this->parseNumber("1"));
362 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
363 // -x + y <= 11/2
364 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
365 constraint3.addToLhs(0, -this->parseNumber("1"));
366 constraint3.addToLhs(1, this->parseNumber("1"));
367 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
368 ASSERT_NO_THROW(solver->update());
369
370 ASSERT_NO_THROW(solver->optimize());
371 ASSERT_TRUE(solver->isOptimal());
372 ASSERT_FALSE(solver->isUnbounded());
373 ASSERT_FALSE(solver->isInfeasible());
374 EXPECT_TRUE(solver->getBinaryValue(0));
375 EXPECT_EQ(6, solver->getIntegerValue(1));
376 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(2), this->precision());
377 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
378}
379
380TYPED_TEST(LpSolverTest, MILPOptimizeMin) {
381 if (!this->supportsInteger()) {
382 GTEST_SKIP();
383 }
384 typedef typename TestFixture::ValueType ValueType;
385 auto solver = this->factory()->create("");
386 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
387 storm::expressions::Variable x;
388 storm::expressions::Variable y;
389 storm::expressions::Variable z;
390 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
391 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
392 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 0, 5, -1));
393 ASSERT_NO_THROW(solver->update());
394
395 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
396 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
397 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
398 ASSERT_NO_THROW(solver->update());
399
400#ifdef STORM_HAVE_Z3_OPTIMIZE
401 if (this->solverSelection() == storm::solver::LpSolverTypeSelection::Z3 && storm::test::z3AtLeastVersion(4, 8, 8)) {
402 // TODO: z3 v4.8.8 is known to be broken here. Check if this is fixed in future versions >4.8.8
403 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
404 }
405#endif
406
407 ASSERT_NO_THROW(solver->optimize());
408 ASSERT_TRUE(solver->isOptimal());
409 ASSERT_FALSE(solver->isUnbounded());
410 ASSERT_FALSE(solver->isInfeasible());
411
412 EXPECT_TRUE(solver->getBinaryValue(x));
413 EXPECT_EQ(0, solver->getIntegerValue(y));
414 EXPECT_NEAR(this->parseNumber("5"), solver->getContinuousValue(z), this->precision());
415 EXPECT_NEAR(this->parseNumber("-6"), solver->getObjectiveValue(), this->precision());
416}
417
418TYPED_TEST(LpSolverTest, LPInfeasible) {
419 typedef typename TestFixture::ValueType ValueType;
420 auto solver = this->factory()->create("");
421 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
422 storm::expressions::Variable x;
423 storm::expressions::Variable y;
424 storm::expressions::Variable z;
425 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
426 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
427 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
428 ASSERT_NO_THROW(solver->update());
429
430 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
431 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
432 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
433 if (this->supportsStrictRelation()) {
434 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
435 } else {
436 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
437 }
438 ASSERT_NO_THROW(solver->update());
439
440 ASSERT_NO_THROW(solver->optimize());
441 ASSERT_FALSE(solver->isOptimal());
442 ASSERT_FALSE(solver->isUnbounded());
443 ASSERT_TRUE(solver->isInfeasible());
444 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
445 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
446 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
447 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
448}
449
450TYPED_TEST(LpSolverTest, MILPInfeasible) {
451 if (!this->supportsInteger()) {
452 GTEST_SKIP();
453 }
454 typedef typename TestFixture::ValueType ValueType;
455 auto solver = this->factory()->create("");
456 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
457 storm::expressions::Variable x;
458 storm::expressions::Variable y;
459 storm::expressions::Variable z;
460 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
461 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
462 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
463 ASSERT_NO_THROW(solver->update());
464
465 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
466 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
467 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
468 if (this->supportsStrictRelation()) {
469 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
470 } else {
471 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
472 }
473 ASSERT_NO_THROW(solver->update());
474
475 ASSERT_NO_THROW(solver->optimize());
476 ASSERT_FALSE(solver->isOptimal());
477 ASSERT_FALSE(solver->isUnbounded());
478 ASSERT_TRUE(solver->isInfeasible());
479 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
480 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
481 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
482 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
483}
484
485TYPED_TEST(LpSolverTest, LPUnbounded) {
486 typedef typename TestFixture::ValueType ValueType;
487 auto solver = this->factory()->create("");
488 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
489 storm::expressions::Variable x;
490 storm::expressions::Variable y;
491 storm::expressions::Variable z;
492 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
493 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
494 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
495 ASSERT_NO_THROW(solver->update());
496
497 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
498 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
499 ASSERT_NO_THROW(solver->update());
500
501 ASSERT_NO_THROW(solver->optimize());
502 ASSERT_FALSE(solver->isOptimal());
503 ASSERT_TRUE(solver->isUnbounded());
504 ASSERT_FALSE(solver->isInfeasible());
505 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
506 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
507 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
508 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
509}
510
511TYPED_TEST(LpSolverTest, MILPUnbounded) {
512 if (!this->supportsInteger()) {
513 GTEST_SKIP();
514 }
515 typedef typename TestFixture::ValueType ValueType;
516 auto solver = this->factory()->create("");
517 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
518 storm::expressions::Variable x;
519 storm::expressions::Variable y;
520 storm::expressions::Variable z;
521 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
522 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
523 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
524 ASSERT_NO_THROW(solver->update());
525
526 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
527 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
528 ASSERT_NO_THROW(solver->update());
529
530 ASSERT_NO_THROW(solver->optimize());
531 ASSERT_FALSE(solver->isOptimal());
532 ASSERT_TRUE(solver->isUnbounded());
533 ASSERT_FALSE(solver->isInfeasible());
534 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
535 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
536 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
537 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
538}
539
540TYPED_TEST(LpSolverTest, Incremental) {
541 if (!this->supportsIncremental()) {
542 GTEST_SKIP();
543 }
544 typedef typename TestFixture::ValueType ValueType;
545 auto solver = this->factory()->create("");
546 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
547 storm::expressions::Variable x, y, z;
548 ASSERT_NO_THROW(x = solver->addUnboundedContinuousVariable("x", 1));
549
550 solver->push();
551 ASSERT_NO_THROW(solver->addConstraint("", x <= solver->getConstant(12)));
552 ASSERT_NO_THROW(solver->optimize());
553 // max x s.t. x<=12
554 ASSERT_TRUE(solver->isOptimal());
555 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
556
557 solver->push();
558 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y"));
559 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(6)));
560 ASSERT_NO_THROW(solver->addConstraint("", x <= y));
561 // max x s.t. x<=12 and y <= 6 and x <= y
562 ASSERT_NO_THROW(solver->optimize());
563 ASSERT_TRUE(solver->isOptimal());
564 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
565 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(y), this->precision());
566 solver->pop();
567 ASSERT_NO_THROW(solver->optimize());
568 // max x s.t. x<=12
569 ASSERT_TRUE(solver->isOptimal());
570 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
571
572#ifdef STORM_HAVE_Z3_OPTIMIZE
573 if (this->solverSelection() == storm::solver::LpSolverTypeSelection::Z3 && !storm::test::z3AtLeastVersion(4, 8, 5)) {
574 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
575 }
576#endif
577
578 solver->push();
579 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y", 10));
580 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(20)));
581 ASSERT_NO_THROW(solver->addConstraint("", y <= -x));
582 // max x+10y s.t. x<=12 and y<=20 and y<=-x
583 ASSERT_NO_THROW(solver->optimize());
584 ASSERT_TRUE(solver->isOptimal());
585 EXPECT_NEAR(this->parseNumber("-20"), solver->getContinuousValue(x), this->precision());
586 EXPECT_NEAR(this->parseNumber("20"), solver->getContinuousValue(y), this->precision());
587
588 solver->pop();
589 ASSERT_NO_THROW(solver->optimize());
590 // max x s.t. x<=12
591 ASSERT_TRUE(solver->isOptimal());
592 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
593
594 solver->push();
595 ASSERT_NO_THROW(z = solver->addUnboundedIntegerVariable("z"));
596 ASSERT_NO_THROW(solver->addConstraint("", z <= solver->getConstant(6)));
597 ASSERT_NO_THROW(solver->addConstraint("", x <= z));
598 ASSERT_NO_THROW(solver->optimize());
599 // max x s.t. x<=12 and z <= 6 and x <= z
600 ASSERT_TRUE(solver->isOptimal());
601 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
602 EXPECT_EQ(6, solver->getIntegerValue(z));
603
604 solver->pop();
605 ASSERT_NO_THROW(solver->optimize());
606 // max x s.t. x<=12
607 ASSERT_TRUE(solver->isOptimal());
608 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
609
610 solver->pop();
611 // max x s.t. true
612 ASSERT_NO_THROW(solver->optimize());
613 ASSERT_FALSE(solver->isOptimal());
614 ASSERT_TRUE(solver->isUnbounded());
615 ASSERT_FALSE(solver->isInfeasible());
616}
617
618} // namespace
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:53
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:99