sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Test for incremental LP solving.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
078eb86c48
commit
1323c099dd
3 changed files with 195 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 64
      src/test/storm/solver/GlpkLpSolverTest.cpp
  2. 64
      src/test/storm/solver/GurobiLpSolverTest.cpp
  3. 67
      src/test/storm/solver/Z3LpSolverTest.cpp

64
src/test/storm/solver/GlpkLpSolverTest.cpp
View File

@ -246,4 +246,68 @@ TEST(GlpkLpSolver, MILPUnbounded) {
ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
} }
TEST(GlpkLpSolver, Incremental) {
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x,y,z;
ASSERT_NO_THROW(x = solver.addUnboundedContinuousVariable("x", 1));
solver.push();
ASSERT_NO_THROW(solver.addConstraint("", x <= solver.getConstant(12)));
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y"));
solver.push();
ASSERT_NO_THROW(solver.addConstraint("", y <= solver.getConstant(6)));
ASSERT_NO_THROW(solver.addConstraint("", x <= y));
// max x s.t. x<=12 and y <= 6 and x <= y
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(6.0, solver.getContinuousValue(x));
EXPECT_EQ(6.0, solver.getContinuousValue(y));
solver.pop();
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y", 10));
ASSERT_NO_THROW(solver.addConstraint("", y <= solver.getConstant(20)));
ASSERT_NO_THROW(solver.addConstraint("", y <= -x));
// max x+10y s.t. x<=12 and y<=20 and y<=-x
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(-20, solver.getContinuousValue(x));
EXPECT_EQ(20, solver.getContinuousValue(y));
solver.pop();
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(z = solver.addUnboundedIntegerVariable("z"));
ASSERT_NO_THROW(solver.addConstraint("", z <= solver.getConstant(6)));
ASSERT_NO_THROW(solver.addConstraint("", x <= z));
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12 and y <= 6 and x <= y
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(6.0, solver.getContinuousValue(x));
EXPECT_EQ(6, solver.getIntegerValue(z));
solver.pop();
solver.pop();
// max x s.t. true
ASSERT_NO_THROW(solver.optimize());
ASSERT_FALSE(solver.isOptimal());
ASSERT_TRUE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
}
#endif #endif

64
src/test/storm/solver/GurobiLpSolverTest.cpp
View File

@ -257,4 +257,68 @@ TEST(GurobiLpSolver, MILPUnbounded) {
double objectiveValue = 0; double objectiveValue = 0;
ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
} }
TEST(GurobiLpSolver, Incremental) {
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x, y, z;
ASSERT_NO_THROW(x = solver.addUnboundedContinuousVariable("x", 1));
solver.push();
ASSERT_NO_THROW(solver.addConstraint("", x <= solver.getConstant(12)));
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y"));
ASSERT_NO_THROW(solver.addConstraint("", y <= solver.getConstant(6)));
ASSERT_NO_THROW(solver.addConstraint("", x <= y));
// max x s.t. x<=12 and y <= 6 and x <= y
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(6.0, solver.getContinuousValue(x));
EXPECT_EQ(6.0, solver.getContinuousValue(y));
solver.pop();
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y", 10));
ASSERT_NO_THROW(solver.addConstraint("", y <= solver.getConstant(20)));
ASSERT_NO_THROW(solver.addConstraint("", y <= -x));
// max x+10y s.t. x<=12 and y<=20 and y<=-x
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(-20, solver.getContinuousValue(x));
EXPECT_EQ(20, solver.getContinuousValue(y));
solver.pop();
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(z = solver.addUnboundedIntegerVariable("z"));
ASSERT_NO_THROW(solver.addConstraint("", z <= solver.getConstant(6)));
ASSERT_NO_THROW(solver.addConstraint("", x <= z));
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12 and z <= 6 and x <= z
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(6.0, solver.getContinuousValue(x));
EXPECT_EQ(6, solver.getIntegerValue(z));
solver.pop();
solver.pop();
// max x s.t. true
ASSERT_NO_THROW(solver.optimize());
ASSERT_FALSE(solver.isOptimal());
ASSERT_TRUE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
}
#endif #endif

67
src/test/storm/solver/Z3LpSolverTest.cpp
View File

@ -246,4 +246,71 @@ TEST(Z3LpSolver, MILPUnbounded) {
ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
} }
TEST(Z3LpSolver, Incremental) {
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x, y, z;
ASSERT_NO_THROW(x = solver.addUnboundedContinuousVariable("x", 1));
solver.push();
ASSERT_NO_THROW(solver.addConstraint("", x <= solver.getConstant(12)));
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y"));
ASSERT_NO_THROW(solver.addConstraint("", y <= solver.getConstant(6)));
ASSERT_NO_THROW(solver.addConstraint("", x <= y));
// max x s.t. x<=12 and y <= 6 and x <= y
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(6.0, solver.getContinuousValue(x));
EXPECT_EQ(6.0, solver.getContinuousValue(y));
solver.pop();
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y", 10));
ASSERT_NO_THROW(solver.addConstraint("", y <= solver.getConstant(20)));
ASSERT_NO_THROW(solver.addConstraint("", y <= -x));
// max x+10y s.t. x<=12 and y<=20 and y<=-x
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(-20, solver.getContinuousValue(x));
EXPECT_EQ(20, solver.getContinuousValue(y));
solver.pop();
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12
ASSERT_FALSE(solver.isInfeasible());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(12.0, solver.getContinuousValue(x));
solver.push();
ASSERT_NO_THROW(z = solver.addUnboundedIntegerVariable("z"));
ASSERT_NO_THROW(solver.addConstraint("", z <= solver.getConstant(6)));
ASSERT_NO_THROW(solver.addConstraint("", x <= z));
ASSERT_NO_THROW(solver.optimize());
// max x s.t. x<=12 and z <= 6 and x <= z
ASSERT_TRUE(solver.isOptimal());
EXPECT_EQ(6.0, solver.getContinuousValue(x));
EXPECT_EQ(6, solver.getIntegerValue(z));
solver.pop();
solver.pop();
// max x s.t. true
ASSERT_NO_THROW(solver.optimize());
ASSERT_FALSE(solver.isOptimal());
ASSERT_TRUE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
}
#endif #endif
Write Preview
Loading…
Cancel
Save