Storm 1.14.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 <optional>
5
6#include "storm/environment/Environment.h"
7#include "storm/exceptions/InvalidAccessException.h"
8#include "storm/solver/GlpkLpSolver.h"
9#include "storm/solver/GurobiLpSolver.h"
10#include "storm/solver/LpSolver.h"
11#include "storm/solver/OptimizationDirection.h"
12#include "storm/storage/expressions/Expression.h"
13#include "storm/storage/expressions/Variable.h"
14#include "storm/utility/solver.h"
15#include "storm/utility/vector.h"
16
17namespace {
18
19class DefaultEnvironment {
20 public:
21 typedef double ValueType;
22 static const bool isExact = false;
23 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::FROMSETTINGS;
24 static const bool IntegerSupport = true;
25 static const bool IncrementalSupport = true;
26 static const bool strictRelationSupport = true;
27 static const bool IndicatorSupport = false;
28
29 static bool skip() {
30#ifdef STORM_HAVE_LP_SOLVER
31 return false;
32#else
33 return true;
34#endif
35 }
36};
37
38class GlpkEnvironment {
39 public:
40 typedef double ValueType;
41 static const bool isExact = false;
42 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Glpk;
43 static const bool IntegerSupport = true;
44 static const bool IncrementalSupport = true;
45 static const bool strictRelationSupport = true;
46 static const bool IndicatorSupport = false;
47
48 static bool skip() {
49 return false;
50 }
51};
52
53#ifdef STORM_HAVE_GUROBI
54class GurobiEnvironment {
55 public:
56 typedef double ValueType;
57 static const bool isExact = false;
58 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Gurobi;
59 static const bool IntegerSupport = true;
60 static const bool IncrementalSupport = true;
61 static const bool strictRelationSupport = true;
62 static const bool IndicatorSupport = true;
63
64 static bool skip() {
65 return storm::test::noGurobi;
66 }
67};
68#endif
69
70class Z3Environment {
71 public:
72 typedef storm::RationalNumber ValueType;
73 static const bool isExact = true;
74 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Z3;
75 static const bool IntegerSupport = true;
76 static const bool IncrementalSupport = true;
77 static const bool strictRelationSupport = true;
78 static const bool IndicatorSupport = true;
79
80 static bool skip() {
81 return false;
82 }
83};
84
85#ifdef STORM_HAVE_SOPLEX
86class SoplexEnvironment {
87 public:
88 typedef double ValueType;
89 static const bool isExact = false;
90 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Soplex;
91 static const bool IntegerSupport = false;
92 static const bool IncrementalSupport = false;
93 static const bool strictRelationSupport = false;
94 static const bool IndicatorSupport = false;
95
96 static bool skip() {
97 return false;
98 }
99};
100
101class SoplexExactEnvironment {
102 public:
103 typedef storm::RationalNumber ValueType;
104 static const bool isExact = true;
105 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Soplex;
106 static const bool IntegerSupport = false;
107 static const bool IncrementalSupport = false;
108 static const bool strictRelationSupport = false;
109 static const bool IndicatorSupport = false;
110
111 static bool skip() {
112 return false;
113 }
114};
115#endif
116
117#ifdef STORM_HAVE_HIGHS
118class HighsEnvironment {
119 public:
120 typedef double ValueType;
121 static const bool isExact = false;
122 static const storm::solver::LpSolverTypeSelection solverSelection = storm::solver::LpSolverTypeSelection::Highs;
123 static const bool IntegerSupport = true;
124 static const bool IncrementalSupport = false;
125 static const bool strictRelationSupport = false;
126 static const bool IndicatorSupport = true;
127
128 static bool skip() {
129 return false;
130 }
131};
132#endif
133
134template<typename TestType>
135class LpSolverTest : public ::testing::Test {
136 public:
137 typedef typename TestType::ValueType ValueType;
138
139 void SetUp() override {
140 if (skipped()) {
141 GTEST_SKIP();
142 }
143 }
144
145 storm::solver::LpSolverTypeSelection solverSelection() const {
146 return TestType::solverSelection;
147 }
148
149 storm::Environment env() const {
150 return storm::Environment();
151 }
152
153 std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> factory() const {
154 return storm::utility::solver::getLpSolverFactory<ValueType>(env(), solverSelection());
155 }
156
157 ValueType parseNumber(std::string const& input) const {
158 return storm::utility::convertNumber<ValueType>(input);
159 }
160
161 ValueType precision() const {
162 return TestType::isExact ? parseNumber("0") : parseNumber("1e-15");
163 }
164
165 bool supportsInteger() const {
166 return TestType::IntegerSupport;
167 }
168
169 bool supportsIncremental() const {
170 return TestType::IncrementalSupport;
171 }
172
173 bool supportsStrictRelation() const {
174 return TestType::strictRelationSupport;
175 }
176
177 bool supportsIndicator() const {
178 return TestType::IndicatorSupport;
179 }
180
181 // Builds a solver with a bounded continuous variable x in [0, 5] (with objective coefficient 1) and a binary variable b.
182 // If fixedB has a value, b is fixed to that value via a regular constraint.
183 // Adds the indicator constraint (b == indicatorValue) => (x rel rhs), optimizes in the given direction and returns the solver.
184 std::unique_ptr<storm::solver::LpSolver<ValueType>> solveIndicatorScenario(storm::OptimizationDirection dir, bool indicatorValue,
185 std::optional<bool> fixedB, storm::expressions::RelationType rel,
186 std::string const& rhs, storm::expressions::Variable& x,
187 storm::expressions::Variable& b) {
188 auto solver = this->factory()->create(this->env(), "");
189 solver->setOptimizationDirection(dir);
190 x = solver->addBoundedContinuousVariable("x", 0, this->parseNumber("5"), 1);
191 b = solver->addBinaryVariable("b");
192 if (fixedB.has_value()) {
193 solver->addConstraint("", b == solver->getConstant(*fixedB ? 1 : 0));
194 }
195 storm::expressions::Expression rhsExpression = solver->getConstant(this->parseNumber(rhs));
196 storm::expressions::Expression constraint;
197 if (rel == storm::expressions::RelationType::LessOrEqual) {
198 constraint = x <= rhsExpression;
199 } else if (rel == storm::expressions::RelationType::GreaterOrEqual) {
200 constraint = x >= rhsExpression;
201 } else {
202 constraint = x == rhsExpression;
203 }
204 solver->addIndicatorConstraint("", b, indicatorValue, constraint);
205 solver->update();
206 solver->optimize();
207 return solver;
208 }
209
210 bool skipped() const {
211 return TestType::skip();
212 }
213};
214
215typedef ::testing::Types<DefaultEnvironment
216#ifdef STORM_HAVE_GLPK
217 ,
218 GlpkEnvironment
219#endif
220#ifdef STORM_HAVE_GUROBI
221 ,
222 GurobiEnvironment
223#endif
224#ifdef STORM_HAVE_HIGHS
225 ,
226 HighsEnvironment
227#endif
228#ifdef STORM_HAVE_SOPLEX
229 ,
230 SoplexEnvironment, SoplexExactEnvironment
231#endif
232#ifdef STORM_HAVE_Z3
233 ,
234 Z3Environment
235#endif
236 >
237 TestingTypes;
238
239TYPED_TEST_SUITE(LpSolverTest, TestingTypes, );
240
241TYPED_TEST(LpSolverTest, LPOptimizeMax) {
242 auto solver = this->factory()->create(this->env(), "");
243 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
244 storm::expressions::Variable x;
245 storm::expressions::Variable y;
246 storm::expressions::Variable z;
247 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
248 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
249 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
250 ASSERT_NO_THROW(solver->update());
251
252 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
253 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
254 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
255 ASSERT_NO_THROW(solver->update());
256
257 ASSERT_NO_THROW(solver->optimize());
258 ASSERT_TRUE(solver->isOptimal());
259 ASSERT_FALSE(solver->isUnbounded());
260 ASSERT_FALSE(solver->isInfeasible());
261 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
262 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(y), this->precision());
263 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(z), this->precision());
264 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
265}
266
267TYPED_TEST(LpSolverTest, LPOptimizeMaxRaw) {
268 typedef typename TestFixture::ValueType ValueType;
269 auto solver = this->factory()->createRaw(this->env(), "");
270 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
271 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
272 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
273 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 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::Equal, 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 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
300 EXPECT_NEAR(this->parseNumber("13/2"), solver->getContinuousValue(1), this->precision());
301 EXPECT_NEAR(this->parseNumber("11/4"), solver->getContinuousValue(2), this->precision());
302 EXPECT_NEAR(this->parseNumber("59/4"), solver->getObjectiveValue(), this->precision());
303}
304
305TYPED_TEST(LpSolverTest, LPOptimizeMin) {
306 auto solver = this->factory()->create(this->env(), "");
307 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
308 storm::expressions::Variable x;
309 storm::expressions::Variable y;
310 storm::expressions::Variable z;
311 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
312 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
313 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
314 ASSERT_NO_THROW(solver->update());
315
316 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
317 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
318 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
319 ASSERT_NO_THROW(solver->update());
320
321 ASSERT_NO_THROW(solver->optimize());
322 ASSERT_TRUE(solver->isOptimal());
323 ASSERT_FALSE(solver->isUnbounded());
324 ASSERT_FALSE(solver->isInfeasible());
325
326 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(x), this->precision());
327 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(y), this->precision());
328 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(z), this->precision());
329 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
330}
331
332TYPED_TEST(LpSolverTest, LPOptimizeMinRaw) {
333 typedef typename TestFixture::ValueType ValueType;
334 auto solver = this->factory()->createRaw(this->env(), "");
335 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
336
337 ASSERT_EQ(0u, solver->addBoundedContinuousVariable("x", 0, 1, -1));
338 ASSERT_EQ(1u, solver->addLowerBoundedContinuousVariable("y", 0, 2));
339 ASSERT_EQ(2u, solver->addBoundedContinuousVariable("z", 1, this->parseNumber("57/10"), -1));
340 ASSERT_NO_THROW(solver->update());
341
342 // x + y + z <= 12
343 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
344 constraint1.addToLhs(0, this->parseNumber("1"));
345 constraint1.addToLhs(1, this->parseNumber("1"));
346 constraint1.addToLhs(2, this->parseNumber("1"));
347 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
348 // -x + 1/2 * y + z <= 5
349 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::LessOrEqual, this->parseNumber("5"), 3);
350 constraint2.addToLhs(0, -this->parseNumber("1"));
351 constraint2.addToLhs(1, this->parseNumber("1/2"));
352 constraint2.addToLhs(2, this->parseNumber("1"));
353 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
354 // -x + y <= 11/2
355 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
356 constraint3.addToLhs(0, -this->parseNumber("1"));
357 constraint3.addToLhs(1, this->parseNumber("1"));
358 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
359 ASSERT_NO_THROW(solver->update());
360
361 ASSERT_NO_THROW(solver->optimize());
362 ASSERT_TRUE(solver->isOptimal());
363 ASSERT_FALSE(solver->isUnbounded());
364 ASSERT_FALSE(solver->isInfeasible());
365
366 EXPECT_NEAR(this->parseNumber("1"), solver->getContinuousValue(0), this->precision());
367 EXPECT_NEAR(this->parseNumber("0"), solver->getContinuousValue(1), this->precision());
368 EXPECT_NEAR(this->parseNumber("57/10"), solver->getContinuousValue(2), this->precision());
369 EXPECT_NEAR(this->parseNumber("-67/10"), solver->getObjectiveValue(), this->precision());
370}
371
372TYPED_TEST(LpSolverTest, MILPOptimizeMax) {
373 if (!this->supportsInteger()) {
374 GTEST_SKIP();
375 }
376 auto solver = this->factory()->create(this->env(), "");
377 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
378 storm::expressions::Variable x;
379 storm::expressions::Variable y;
380 storm::expressions::Variable z;
381 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
382 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
383 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
384 ASSERT_NO_THROW(solver->update());
385
386 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
387 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
388 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
389 ASSERT_NO_THROW(solver->update());
390 ASSERT_NO_THROW(solver->optimize());
391 ASSERT_TRUE(solver->isOptimal());
392 ASSERT_FALSE(solver->isUnbounded());
393 ASSERT_FALSE(solver->isInfeasible());
394
395 EXPECT_TRUE(solver->getBinaryValue(x));
396 EXPECT_EQ(6, solver->getIntegerValue(y));
397 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(z), this->precision());
398 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
399}
400
401TYPED_TEST(LpSolverTest, MILPOptimizeMaxRaw) {
402 if (!this->supportsInteger()) {
403 GTEST_SKIP();
404 }
405 typedef typename TestFixture::ValueType ValueType;
406 auto solver = this->factory()->createRaw(this->env(), "");
407 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
408 storm::expressions::Variable x;
409 storm::expressions::Variable y;
410 storm::expressions::Variable z;
411 ASSERT_EQ(0u, solver->addBinaryVariable("x", -1));
412 ASSERT_EQ(1u, solver->addLowerBoundedIntegerVariable("y", 0, 2));
413 ASSERT_EQ(2u, solver->addLowerBoundedContinuousVariable("z", 0, 1));
414 ASSERT_NO_THROW(solver->update());
415
416 // x + y + z <= 12
417 storm::solver::RawLpConstraint<ValueType> constraint1(storm::expressions::RelationType::LessOrEqual, this->parseNumber("12"), 3);
418 constraint1.addToLhs(0, this->parseNumber("1"));
419 constraint1.addToLhs(1, this->parseNumber("1"));
420 constraint1.addToLhs(2, this->parseNumber("1"));
421 ASSERT_NO_THROW(solver->addConstraint("", constraint1));
422 // -x + 1/2 * y + z == 5
423 storm::solver::RawLpConstraint<ValueType> constraint2(storm::expressions::RelationType::Equal, this->parseNumber("5"), 3);
424 constraint2.addToLhs(0, -this->parseNumber("1"));
425 constraint2.addToLhs(1, this->parseNumber("1/2"));
426 constraint2.addToLhs(2, this->parseNumber("1"));
427 ASSERT_NO_THROW(solver->addConstraint("", constraint2));
428 // -x + y <= 11/2
429 storm::solver::RawLpConstraint<ValueType> constraint3(storm::expressions::RelationType::LessOrEqual, this->parseNumber("11/2"), 2);
430 constraint3.addToLhs(0, -this->parseNumber("1"));
431 constraint3.addToLhs(1, this->parseNumber("1"));
432 ASSERT_NO_THROW(solver->addConstraint("", constraint3));
433 ASSERT_NO_THROW(solver->update());
434
435 ASSERT_NO_THROW(solver->optimize());
436 ASSERT_TRUE(solver->isOptimal());
437 ASSERT_FALSE(solver->isUnbounded());
438 ASSERT_FALSE(solver->isInfeasible());
439 EXPECT_TRUE(solver->getBinaryValue(0));
440 EXPECT_EQ(6, solver->getIntegerValue(1));
441 EXPECT_NEAR(this->parseNumber("3"), solver->getContinuousValue(2), this->precision());
442 EXPECT_NEAR(this->parseNumber("14"), solver->getObjectiveValue(), this->precision());
443}
444
445TYPED_TEST(LpSolverTest, MILPOptimizeMin) {
446 if (!this->supportsInteger()) {
447 GTEST_SKIP();
448 }
449 auto solver = this->factory()->create(this->env(), "");
450 solver->setOptimizationDirection(storm::OptimizationDirection::Minimize);
451 storm::expressions::Variable x;
452 storm::expressions::Variable y;
453 storm::expressions::Variable z;
454 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
455 ASSERT_NO_THROW(y = solver->addLowerBoundedIntegerVariable("y", 0, 2));
456 ASSERT_NO_THROW(z = solver->addBoundedContinuousVariable("z", 0, 5, -1));
457 ASSERT_NO_THROW(solver->update());
458
459 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
460 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x <= solver->getConstant(5)));
461 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
462 ASSERT_NO_THROW(solver->update());
463
464#ifdef STORM_HAVE_Z3
465 if (this->solverSelection() == storm::solver::LpSolverTypeSelection::Z3 && storm::test::z3AtLeastVersion(4, 8, 8) &&
466 !storm::test::z3AtLeastVersion(4, 13, 3)) {
467 // z3 v4.8.8 is known to be broken here. It is working for v4.13.3.
468 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
469 }
470#endif
471
472 ASSERT_NO_THROW(solver->optimize());
473 ASSERT_TRUE(solver->isOptimal());
474 ASSERT_FALSE(solver->isUnbounded());
475 ASSERT_FALSE(solver->isInfeasible());
476
477 EXPECT_TRUE(solver->getBinaryValue(x));
478 EXPECT_EQ(0, solver->getIntegerValue(y));
479 EXPECT_NEAR(this->parseNumber("5"), solver->getContinuousValue(z), this->precision());
480 EXPECT_NEAR(this->parseNumber("-6"), solver->getObjectiveValue(), this->precision());
481}
482
483TYPED_TEST(LpSolverTest, LPInfeasible) {
484 auto solver = this->factory()->create(this->env(), "");
485 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
486 storm::expressions::Variable x;
487 storm::expressions::Variable y;
488 storm::expressions::Variable z;
489 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
490 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
491 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
492 ASSERT_NO_THROW(solver->update());
493
494 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
495 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
496 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
497 if (this->supportsStrictRelation()) {
498 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
499 } else {
500 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
501 }
502 ASSERT_NO_THROW(solver->update());
503
504 ASSERT_NO_THROW(solver->optimize());
505 ASSERT_FALSE(solver->isOptimal());
506 ASSERT_FALSE(solver->isUnbounded());
507 ASSERT_TRUE(solver->isInfeasible());
508 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
509 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
510 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
511 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
512}
513
514TYPED_TEST(LpSolverTest, MILPInfeasible) {
515 if (!this->supportsInteger()) {
516 GTEST_SKIP();
517 }
518 auto solver = this->factory()->create(this->env(), "");
519 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
520 storm::expressions::Variable x;
521 storm::expressions::Variable y;
522 storm::expressions::Variable z;
523 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
524 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
525 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
526 ASSERT_NO_THROW(solver->update());
527
528 ASSERT_NO_THROW(solver->addConstraint("", x + y + z <= solver->getConstant(12)));
529 ASSERT_NO_THROW(solver->addConstraint("", solver->getConstant(this->parseNumber("1/2")) * y + z - x == solver->getConstant(5)));
530 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
531 if (this->supportsStrictRelation()) {
532 ASSERT_NO_THROW(solver->addConstraint("", y > solver->getConstant((this->parseNumber("7")))));
533 } else {
534 ASSERT_NO_THROW(solver->addConstraint("", y >= solver->getConstant(this->parseNumber("7") + this->precision())));
535 }
536 ASSERT_NO_THROW(solver->update());
537
538 ASSERT_NO_THROW(solver->optimize());
539 ASSERT_FALSE(solver->isOptimal());
540 ASSERT_FALSE(solver->isUnbounded());
541 ASSERT_TRUE(solver->isInfeasible());
542 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
543 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
544 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
545 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
546}
547
548TYPED_TEST(LpSolverTest, LPUnbounded) {
549 auto solver = this->factory()->create(this->env(), "");
550 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
551 storm::expressions::Variable x;
552 storm::expressions::Variable y;
553 storm::expressions::Variable z;
554 ASSERT_NO_THROW(x = solver->addBoundedContinuousVariable("x", 0, 1, -1));
555 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
556 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
557 ASSERT_NO_THROW(solver->update());
558
559 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
560 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
561 ASSERT_NO_THROW(solver->update());
562
563 ASSERT_NO_THROW(solver->optimize());
564 ASSERT_FALSE(solver->isOptimal());
565 ASSERT_TRUE(solver->isUnbounded());
566 ASSERT_FALSE(solver->isInfeasible());
567 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(x), storm::exceptions::InvalidAccessException);
568 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(y), storm::exceptions::InvalidAccessException);
569 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
570 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
571}
572
573TYPED_TEST(LpSolverTest, MILPUnbounded) {
574 if (!this->supportsInteger()) {
575 GTEST_SKIP();
576 }
577 auto solver = this->factory()->create(this->env(), "");
578 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
579 storm::expressions::Variable x;
580 storm::expressions::Variable y;
581 storm::expressions::Variable z;
582 ASSERT_NO_THROW(x = solver->addBinaryVariable("x", -1));
583 ASSERT_NO_THROW(y = solver->addLowerBoundedContinuousVariable("y", 0, 2));
584 ASSERT_NO_THROW(z = solver->addLowerBoundedContinuousVariable("z", 0, 1));
585 ASSERT_NO_THROW(solver->update());
586
587 ASSERT_NO_THROW(solver->addConstraint("", x + y - z <= solver->getConstant(12)));
588 ASSERT_NO_THROW(solver->addConstraint("", y - x <= solver->getConstant(this->parseNumber("11/2"))));
589 ASSERT_NO_THROW(solver->update());
590
591 ASSERT_NO_THROW(solver->optimize());
592 ASSERT_FALSE(solver->isOptimal());
593 ASSERT_TRUE(solver->isUnbounded());
594 ASSERT_FALSE(solver->isInfeasible());
595 STORM_SILENT_ASSERT_THROW(solver->getBinaryValue(x), storm::exceptions::InvalidAccessException);
596 STORM_SILENT_ASSERT_THROW(solver->getIntegerValue(y), storm::exceptions::InvalidAccessException);
597 STORM_SILENT_ASSERT_THROW(solver->getContinuousValue(z), storm::exceptions::InvalidAccessException);
598 STORM_SILENT_ASSERT_THROW(solver->getObjectiveValue(), storm::exceptions::InvalidAccessException);
599}
600
601TYPED_TEST(LpSolverTest, Incremental) {
602 if (!this->supportsIncremental()) {
603 GTEST_SKIP();
604 }
605 auto solver = this->factory()->create(this->env(), "");
606 solver->setOptimizationDirection(storm::OptimizationDirection::Maximize);
607 storm::expressions::Variable x, y, z;
608 ASSERT_NO_THROW(x = solver->addUnboundedContinuousVariable("x", 1));
609
610 solver->push();
611 ASSERT_NO_THROW(solver->addConstraint("", x <= solver->getConstant(12)));
612 ASSERT_NO_THROW(solver->optimize());
613 // max x s.t. x<=12
614 ASSERT_TRUE(solver->isOptimal());
615 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
616
617 solver->push();
618 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y"));
619 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(6)));
620 ASSERT_NO_THROW(solver->addConstraint("", x <= y));
621 // max x s.t. x<=12 and y <= 6 and x <= y
622 ASSERT_NO_THROW(solver->optimize());
623 ASSERT_TRUE(solver->isOptimal());
624 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
625 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(y), this->precision());
626 solver->pop();
627 ASSERT_NO_THROW(solver->optimize());
628 // max x s.t. x<=12
629 ASSERT_TRUE(solver->isOptimal());
630 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
631
632 solver->push();
633 ASSERT_NO_THROW(y = solver->addUnboundedContinuousVariable("y", 10));
634 ASSERT_NO_THROW(solver->addConstraint("", y <= solver->getConstant(20)));
635 ASSERT_NO_THROW(solver->addConstraint("", y <= -x));
636 // max x+10y s.t. x<=12 and y<=20 and y<=-x
637 ASSERT_NO_THROW(solver->optimize());
638 ASSERT_TRUE(solver->isOptimal());
639 EXPECT_NEAR(this->parseNumber("-20"), solver->getContinuousValue(x), this->precision());
640 EXPECT_NEAR(this->parseNumber("20"), solver->getContinuousValue(y), this->precision());
641
642 solver->pop();
643 ASSERT_NO_THROW(solver->optimize());
644 // max x s.t. x<=12
645 ASSERT_TRUE(solver->isOptimal());
646 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
647
648 solver->push();
649 ASSERT_NO_THROW(z = solver->addUnboundedIntegerVariable("z"));
650 ASSERT_NO_THROW(solver->addConstraint("", z <= solver->getConstant(6)));
651 ASSERT_NO_THROW(solver->addConstraint("", x <= z));
652 ASSERT_NO_THROW(solver->optimize());
653 // max x s.t. x<=12 and z <= 6 and x <= z
654 ASSERT_TRUE(solver->isOptimal());
655 EXPECT_NEAR(this->parseNumber("6"), solver->getContinuousValue(x), this->precision());
656 EXPECT_EQ(6, solver->getIntegerValue(z));
657
658 solver->pop();
659 ASSERT_NO_THROW(solver->optimize());
660 // max x s.t. x<=12
661 ASSERT_TRUE(solver->isOptimal());
662 EXPECT_NEAR(this->parseNumber("12"), solver->getContinuousValue(x), this->precision());
663
664 solver->pop();
665 // max x s.t. true
666 ASSERT_NO_THROW(solver->optimize());
667 ASSERT_FALSE(solver->isOptimal());
668 ASSERT_TRUE(solver->isUnbounded());
669 ASSERT_FALSE(solver->isInfeasible());
670}
671
672TYPED_TEST(LpSolverTest, IndicatorConstraintLeq) {
673 if (!this->supportsIndicator()) {
674 GTEST_SKIP();
675 }
676 storm::expressions::Variable x;
677 storm::expressions::Variable b;
678
679 // (b == 1) => x <= 2, with b fixed to 1: the constraint must be enforced.
680 auto enforced = this->solveIndicatorScenario(storm::OptimizationDirection::Maximize, true, std::optional<bool>(true),
681 storm::expressions::RelationType::LessOrEqual, "2", x, b);
682 ASSERT_TRUE(enforced->isOptimal());
683 EXPECT_TRUE(enforced->getBinaryValue(b));
684 EXPECT_NEAR(this->parseNumber("2"), enforced->getContinuousValue(x), this->precision());
685
686 // (b == 1) => x <= 2, with b fixed to 0: the constraint must be inactive.
687 auto relaxed = this->solveIndicatorScenario(storm::OptimizationDirection::Maximize, true, std::optional<bool>(false),
688 storm::expressions::RelationType::LessOrEqual, "2", x, b);
689 ASSERT_TRUE(relaxed->isOptimal());
690 EXPECT_FALSE(relaxed->getBinaryValue(b));
691 EXPECT_NEAR(this->parseNumber("5"), relaxed->getContinuousValue(x), this->precision());
692}
693
694TYPED_TEST(LpSolverTest, IndicatorConstraintLeqInactive) {
695 if (!this->supportsIndicator()) {
696 GTEST_SKIP();
697 }
698 storm::expressions::Variable x;
699 storm::expressions::Variable b;
700
701 // (b == 0) => x <= 2, with b fixed to 1: the constraint must be inactive.
702 auto relaxed = this->solveIndicatorScenario(storm::OptimizationDirection::Maximize, false, std::optional<bool>(true),
703 storm::expressions::RelationType::LessOrEqual, "2", x, b);
704 ASSERT_TRUE(relaxed->isOptimal());
705 EXPECT_TRUE(relaxed->getBinaryValue(b));
706 EXPECT_NEAR(this->parseNumber("5"), relaxed->getContinuousValue(x), this->precision());
707
708 // (b == 0) => x <= 2, with b fixed to 0: the constraint must be enforced.
709 auto enforced = this->solveIndicatorScenario(storm::OptimizationDirection::Maximize, false, std::optional<bool>(false),
710 storm::expressions::RelationType::LessOrEqual, "2", x, b);
711 ASSERT_TRUE(enforced->isOptimal());
712 EXPECT_FALSE(enforced->getBinaryValue(b));
713 EXPECT_NEAR(this->parseNumber("2"), enforced->getContinuousValue(x), this->precision());
714}
715
716TYPED_TEST(LpSolverTest, IndicatorConstraintGeq) {
717 if (!this->supportsIndicator()) {
718 GTEST_SKIP();
719 }
720 storm::expressions::Variable x;
721 storm::expressions::Variable b;
722
723 // (b == 1) => x >= 3, with b fixed to 1: the constraint must be enforced.
724 auto enforced = this->solveIndicatorScenario(storm::OptimizationDirection::Minimize, true, std::optional<bool>(true),
725 storm::expressions::RelationType::GreaterOrEqual, "3", x, b);
726 ASSERT_TRUE(enforced->isOptimal());
727 EXPECT_TRUE(enforced->getBinaryValue(b));
728 EXPECT_NEAR(this->parseNumber("3"), enforced->getContinuousValue(x), this->precision());
729
730 // (b == 1) => x >= 3, with b fixed to 0: the constraint must be inactive.
731 auto relaxed = this->solveIndicatorScenario(storm::OptimizationDirection::Minimize, true, std::optional<bool>(false),
732 storm::expressions::RelationType::GreaterOrEqual, "3", x, b);
733 ASSERT_TRUE(relaxed->isOptimal());
734 EXPECT_FALSE(relaxed->getBinaryValue(b));
735 EXPECT_NEAR(this->parseNumber("0"), relaxed->getContinuousValue(x), this->precision());
736}
737
738TYPED_TEST(LpSolverTest, IndicatorConstraintEq) {
739 if (!this->supportsIndicator()) {
740 GTEST_SKIP();
741 }
742 storm::expressions::Variable x;
743 storm::expressions::Variable b;
744
745 // (b == 1) => x == 3, with b fixed to 1: the constraint must be enforced.
746 auto enforcedMin = this->solveIndicatorScenario(storm::OptimizationDirection::Minimize, true, std::optional<bool>(true),
747 storm::expressions::RelationType::Equal, "3", x, b);
748 ASSERT_TRUE(enforcedMin->isOptimal());
749 EXPECT_TRUE(enforcedMin->getBinaryValue(b));
750 EXPECT_NEAR(this->parseNumber("3"), enforcedMin->getContinuousValue(x), this->precision());
751 auto enforcedMax = this->solveIndicatorScenario(storm::OptimizationDirection::Maximize, true, std::optional<bool>(true),
752 storm::expressions::RelationType::Equal, "3", x, b);
753 ASSERT_TRUE(enforcedMax->isOptimal());
754 EXPECT_TRUE(enforcedMax->getBinaryValue(b));
755 EXPECT_NEAR(this->parseNumber("3"), enforcedMax->getContinuousValue(x), this->precision());
756
757 // (b == 1) => x == 3, with b fixed to 0: the constraint must be inactive.
758 auto relaxedMin = this->solveIndicatorScenario(storm::OptimizationDirection::Minimize, true, std::optional<bool>(false),
759 storm::expressions::RelationType::Equal, "3", x, b);
760 ASSERT_TRUE(relaxedMin->isOptimal());
761 EXPECT_FALSE(relaxedMin->getBinaryValue(b));
762 EXPECT_NEAR(this->parseNumber("0"), relaxedMin->getContinuousValue(x), this->precision());
763 auto relaxedMax = this->solveIndicatorScenario(storm::OptimizationDirection::Maximize, true, std::optional<bool>(false),
764 storm::expressions::RelationType::Equal, "3", x, b);
765 ASSERT_TRUE(relaxedMax->isOptimal());
766 EXPECT_FALSE(relaxedMax->getBinaryValue(b));
767 EXPECT_NEAR(this->parseNumber("5"), relaxedMax->getContinuousValue(x), this->precision());
768}
769
770} // namespace
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::expressions::RelationType
RelationType
An enum type specifying the different relations applicable.
Definition BinaryRelationType.h:7
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:55
storm::utility::solver::getLpSolverFactory
std::unique_ptr< LpSolverFactory< ValueType > > getLpSolverFactory(storm::Environment const &env, storm::solver::LpSolverTypeSelection solvType)
Definition solver.cpp:115
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:143
storm::OptimizationDirection
solver::OptimizationDirection OptimizationDirection
Definition OptimizationDirection.h:29
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:64
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:14