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 typedef typename TestFixture::ValueType ValueType;
176 auto solver = this->factory()->create("");
177 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
178 storm::expressions::Variable x;
179 storm::expressions::Variable y;
180 storm::expressions::Variable z;
181 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
182 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
183 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
184 ASSERT_NO_THROW(solver->update());
185
186 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
187 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
188 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
189 ASSERT_NO_THROW(solver->update());
190
191 ASSERT_NO_THROW(solver->optimize());
192 ASSERT_TRUE(solver->isOptimal());
193 ASSERT_FALSE(solver->isUnbounded());
194 ASSERT_FALSE(solver->isInfeasible());
195 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
196 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(y), this->precision());
197 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(z), this->precision());
198 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
199}
200
201TYPED_TEST(LpSolverTest, LPOptimizeMaxRaw) {
202 typedef typename TestFixture::ValueType ValueType;
203 auto solver = this->factory()->createRaw("");
204 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
205 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
206 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
207 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 1));
208 ASSERT_NO_THROW(solver->update());
209
210 // x + y + z <= 12
211 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
212 constraint1.addToLhs(0, this->parseNumber("1"));
213 constraint1.addToLhs(1, this->parseNumber("1"));
214 constraint1.addToLhs(2, this->parseNumber("1"));
215 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
216 // -x + 1/2 * y + z == 5
217 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::Equal, this->parseNumber("5"), 3);
218 constraint2.addToLhs(0, -this->parseNumber("1"));
219 constraint2.addToLhs(1, this->parseNumber("1/2"));
220 constraint2.addToLhs(2, this->parseNumber("1"));
221 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
222 // -x + y <= 11/2
223 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
224 constraint3.addToLhs(0, -this->parseNumber("1"));
225 constraint3.addToLhs(1, this->parseNumber("1"));
226 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
227 ASSERT_NO_THROW(solver->update());
228
229 ASSERT_NO_THROW(solver->optimize());
230 ASSERT_TRUE(solver->isOptimal());
231 ASSERT_FALSE(solver->isUnbounded());
232 ASSERT_FALSE(solver->isInfeasible());
233 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
234 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(1), this->precision());
235 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(2), this->precision());
236 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
237}
238
239TYPED_TEST(LpSolverTest, LPOptimizeMin) {
240 typedef typename TestFixture::ValueType ValueType;
241 auto solver = this->factory()->create("");
242 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
243 storm::expressions::Variable x;
244 storm::expressions::Variable y;
245 storm::expressions::Variable z;
246 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
247 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
248 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
249 ASSERT_NO_THROW(solver->update());
250
251 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
252 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
253 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
254 ASSERT_NO_THROW(solver->update());
255
256 ASSERT_NO_THROW(solver->optimize());
257 ASSERT_TRUE(solver->isOptimal());
258 ASSERT_FALSE(solver->isUnbounded());
259 ASSERT_FALSE(solver->isInfeasible());
260
261 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
262 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(y), this->precision());
263 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(z), this->precision());
264 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
265}
266
267TYPED_TEST(LpSolverTest, LPOptimizeMinRaw) {
268 typedef typename TestFixture::ValueType ValueType;
269 auto solver = this->factory()->createRaw("");
270 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
271
272 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
273 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
274 ASSERT_EQ(2u, solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
275 ASSERT_NO_THROW(solver->update());
276
277 // x + y + z <= 12
278 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
279 constraint1.addToLhs(0, this->parseNumber("1"));
280 constraint1.addToLhs(1, this->parseNumber("1"));
281 constraint1.addToLhs(2, this->parseNumber("1"));
282 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
283 // -x + 1/2 * y + z <= 5
284 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::LessOrEqual, this->parseNumber("5"), 3);
285 constraint2.addToLhs(0, -this->parseNumber("1"));
286 constraint2.addToLhs(1, this->parseNumber("1/2"));
287 constraint2.addToLhs(2, this->parseNumber("1"));
288 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
289 // -x + y <= 11/2
290 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
291 constraint3.addToLhs(0, -this->parseNumber("1"));
292 constraint3.addToLhs(1, this->parseNumber("1"));
293 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
294 ASSERT_NO_THROW(solver->update());
295
296 ASSERT_NO_THROW(solver->optimize());
297 ASSERT_TRUE(solver->isOptimal());
298 ASSERT_FALSE(solver->isUnbounded());
299 ASSERT_FALSE(solver->isInfeasible());
300
301 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
302 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(1), this->precision());
303 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(2), this->precision());
304 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
305}
306
307TYPED_TEST(LpSolverTest, MILPOptimizeMax) {
308 if (!this->supportsInteger()) {
309 GTEST_SKIP();
310 }
311 typedef typename TestFixture::ValueType ValueType;
312 auto solver = this->factory()->create("");
313 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
314 storm::expressions::Variable x;
315 storm::expressions::Variable y;
316 storm::expressions::Variable z;
317 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
318 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
319 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
320 ASSERT_NO_THROW(solver->update());
321
322 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
323 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
324 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
325 ASSERT_NO_THROW(solver->update());
326 ASSERT_NO_THROW(solver->optimize());
327 ASSERT_TRUE(solver->isOptimal());
328 ASSERT_FALSE(solver->isUnbounded());
329 ASSERT_FALSE(solver->isInfeasible());
330
331 EXPECT_TRUE(solver->getBinaryValue(x));
332 EXPECT_EQ(6, solver->getIntegerValue(y));
333 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(z), this->precision());
334 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
335}
336
337TYPED_TEST(LpSolverTest, MILPOptimizeMaxRaw) {
338 if (!this->supportsInteger()) {
339 GTEST_SKIP();
340 }
341 typedef typename TestFixture::ValueType ValueType;
342 auto solver = this->factory()->createRaw("");
343 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
344 storm::expressions::Variable x;
345 storm::expressions::Variable y;
346 storm::expressions::Variable z;
347 ASSERT_EQ(0u, solver->addBinaryVariable("x", -1));
348 ASSERT_EQ(1u, solver->addLowerBoundedIntegerVariable("y", 0, 2));
349 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 1));
350 ASSERT_NO_THROW(solver->update());
351
352 // x + y + z <= 12
353 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
354 constraint1.addToLhs(0, this->parseNumber("1"));
355 constraint1.addToLhs(1, this->parseNumber("1"));
356 constraint1.addToLhs(2, this->parseNumber("1"));
357 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
358 // -x + 1/2 * y + z == 5
359 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::Equal, this->parseNumber("5"), 3);
360 constraint2.addToLhs(0, -this->parseNumber("1"));
361 constraint2.addToLhs(1, this->parseNumber("1/2"));
362 constraint2.addToLhs(2, this->parseNumber("1"));
363 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
364 // -x + y <= 11/2
365 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
366 constraint3.addToLhs(0, -this->parseNumber("1"));
367 constraint3.addToLhs(1, this->parseNumber("1"));
368 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
369 ASSERT_NO_THROW(solver->update());
370
371 ASSERT_NO_THROW(solver->optimize());
372 ASSERT_TRUE(solver->isOptimal());
373 ASSERT_FALSE(solver->isUnbounded());
374 ASSERT_FALSE(solver->isInfeasible());
375 EXPECT_TRUE(solver->getBinaryValue(0));
376 EXPECT_EQ(6, solver->getIntegerValue(1));
377 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(2), this->precision());
378 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
379}
380
381TYPED_TEST(LpSolverTest, MILPOptimizeMin) {
382 if (!this->supportsInteger()) {
383 GTEST_SKIP();
384 }
385 typedef typename TestFixture::ValueType ValueType;
386 auto solver = this->factory()->create("");
387 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
388 storm::expressions::Variable x;
389 storm::expressions::Variable y;
390 storm::expressions::Variable z;
391 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
392 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
393 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 0, 5, -1));
394 ASSERT_NO_THROW(solver->update());
395
396 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
397 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
398 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
399 ASSERT_NO_THROW(solver->update());
400
401#ifdef STORM_HAVE_Z3_OPTIMIZE
402 if (this->solverSelection() == storm::solver::LpSolverTypeSelection::Z3 && storm::test::z3AtLeastVersion(4, 8, 8)) {
403 // TODO: z3 v4.8.8 is known to be broken here. Check if this is fixed in future versions >4.8.8
404 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
405 }
406#endif
407
408 ASSERT_NO_THROW(solver->optimize());
409 ASSERT_TRUE(solver->isOptimal());
410 ASSERT_FALSE(solver->isUnbounded());
411 ASSERT_FALSE(solver->isInfeasible());
412
413 EXPECT_TRUE(solver->getBinaryValue(x));
414 EXPECT_EQ(0, solver->getIntegerValue(y));
415 EXPECT_NEAR(this->parseNumber("5"), solver->getContinuousValue(z), this->precision());
416 EXPECT_NEAR(this->parseNumber("-6"), solver->getObjectiveValue(), this->precision());
417}
418
419TYPED_TEST(LpSolverTest, LPInfeasible) {
420 typedef typename TestFixture::ValueType ValueType;
421 auto solver = this->factory()->create("");
422 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
423 storm::expressions::Variable x;
424 storm::expressions::Variable y;
425 storm::expressions::Variable z;
426 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
427 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
428 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
429 ASSERT_NO_THROW(solver->update());
430
431 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
432 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
433 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
434 if (this->supportsStrictRelation()) {
435 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
436 } else {
437 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
438 }
439 ASSERT_NO_THROW(solver->update());
440
441 ASSERT_NO_THROW(solver->optimize());
442 ASSERT_FALSE(solver->isOptimal());
443 ASSERT_FALSE(solver->isUnbounded());
444 ASSERT_TRUE(solver->isInfeasible());
445 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
446 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
447 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
448 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
449}
450
451TYPED_TEST(LpSolverTest, MILPInfeasible) {
452 if (!this->supportsInteger()) {
453 GTEST_SKIP();
454 }
455 typedef typename TestFixture::ValueType ValueType;
456 auto solver = this->factory()->create("");
457 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
458 storm::expressions::Variable x;
459 storm::expressions::Variable y;
460 storm::expressions::Variable z;
461 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
462 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
463 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
464 ASSERT_NO_THROW(solver->update());
465
466 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
467 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
468 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
469 if (this->supportsStrictRelation()) {
470 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
471 } else {
472 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
473 }
474 ASSERT_NO_THROW(solver->update());
475
476 ASSERT_NO_THROW(solver->optimize());
477 ASSERT_FALSE(solver->isOptimal());
478 ASSERT_FALSE(solver->isUnbounded());
479 ASSERT_TRUE(solver->isInfeasible());
480 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
481 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
482 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
483 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
484}
485
486TYPED_TEST(LpSolverTest, LPUnbounded) {
487 typedef typename TestFixture::ValueType ValueType;
488 auto solver = this->factory()->create("");
489 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
490 storm::expressions::Variable x;
491 storm::expressions::Variable y;
492 storm::expressions::Variable z;
493 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
494 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
495 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
496 ASSERT_NO_THROW(solver->update());
497
498 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
499 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
500 ASSERT_NO_THROW(solver->update());
501
502 ASSERT_NO_THROW(solver->optimize());
503 ASSERT_FALSE(solver->isOptimal());
504 ASSERT_TRUE(solver->isUnbounded());
505 ASSERT_FALSE(solver->isInfeasible());
506 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
507 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
508 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
509 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
510}
511
512TYPED_TEST(LpSolverTest, MILPUnbounded) {
513 if (!this->supportsInteger()) {
514 GTEST_SKIP();
515 }
516 typedef typename TestFixture::ValueType ValueType;
517 auto solver = this->factory()->create("");
518 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
519 storm::expressions::Variable x;
520 storm::expressions::Variable y;
521 storm::expressions::Variable z;
522 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
523 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
524 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
525 ASSERT_NO_THROW(solver->update());
526
527 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
528 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
529 ASSERT_NO_THROW(solver->update());
530
531 ASSERT_NO_THROW(solver->optimize());
532 ASSERT_FALSE(solver->isOptimal());
533 ASSERT_TRUE(solver->isUnbounded());
534 ASSERT_FALSE(solver->isInfeasible());
535 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
536 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
537 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
538 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
539}
540
541TYPED_TEST(LpSolverTest, Incremental) {
542 if (!this->supportsIncremental()) {
543 GTEST_SKIP();
544 }
545 typedef typename TestFixture::ValueType ValueType;
546 auto solver = this->factory()->create("");
547 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
548 storm::expressions::Variable x, y, z;
549 ASSERT_NO_THROW(x = solver->addUnboundedContinuousVariable("x", 1));
550
551 solver->push();
552 ASSERT_NO_THROW(solver->addConstraint("", x <= solver->getConstant(12)));
553 ASSERT_NO_THROW(solver->optimize());
554 // max x s.t. x<=12
555 ASSERT_TRUE(solver->isOptimal());
556 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
557
558 solver->push();
559 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y"));
560 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(6)));
561 ASSERT_NO_THROW(solver->addConstraint("", x <= y));
562 // max x s.t. x<=12 and y <= 6 and x <= y
563 ASSERT_NO_THROW(solver->optimize());
564 ASSERT_TRUE(solver->isOptimal());
565 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
566 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(y), this->precision());
567 solver->pop();
568 ASSERT_NO_THROW(solver->optimize());
569 // max x s.t. x<=12
570 ASSERT_TRUE(solver->isOptimal());
571 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
572
573#ifdef STORM_HAVE_Z3_OPTIMIZE
574 if (this->solverSelection() == storm::solver::LpSolverTypeSelection::Z3 && !storm::test::z3AtLeastVersion(4, 8, 5)) {
575 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
576 }
577#endif
578
579 solver->push();
580 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y", 10));
581 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(20)));
582 ASSERT_NO_THROW(solver->addConstraint("", y <= -x));
583 // max x+10y s.t. x<=12 and y<=20 and y<=-x
584 ASSERT_NO_THROW(solver->optimize());
585 ASSERT_TRUE(solver->isOptimal());
586 EXPECT_NEAR(this->parseNumber("-20"), solver->getContinuousValue(x), this->precision());
587 EXPECT_NEAR(this->parseNumber("20"), solver->getContinuousValue(y), this->precision());
588
589 solver->pop();
590 ASSERT_NO_THROW(solver->optimize());
591 // max x s.t. x<=12
592 ASSERT_TRUE(solver->isOptimal());
593 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
594
595 solver->push();
596 ASSERT_NO_THROW(z = solver->addUnboundedIntegerVariable("z"));
597 ASSERT_NO_THROW(solver->addConstraint("", z <= solver->getConstant(6)));
598 ASSERT_NO_THROW(solver->addConstraint("", x <= z));
599 ASSERT_NO_THROW(solver->optimize());
600 // max x s.t. x<=12 and z <= 6 and x <= z
601 ASSERT_TRUE(solver->isOptimal());
602 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
603 EXPECT_EQ(6, solver->getIntegerValue(z));
604
605 solver->pop();
606 ASSERT_NO_THROW(solver->optimize());
607 // max x s.t. x<=12
608 ASSERT_TRUE(solver->isOptimal());
609 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
610
611 solver->pop();
612 // max x s.t. true
613 ASSERT_NO_THROW(solver->optimize());
614 ASSERT_FALSE(solver->isOptimal());
615 ASSERT_TRUE(solver->isUnbounded());
616 ASSERT_FALSE(solver->isInfeasible());
617}
618
619} // 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: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