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