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