glpk: fixes for incremental solving

src/storm/solver/GlpkLpSolver.cpp

@@ -419,6 +419,23 @@ namespace storm {
                 }
                 incrementalData.pop_back();
                 update();
+                // Check whether we need to adapt the current basis (i.e. the number of basic variables does not equal the number of constraints)
+                int n = glp_get_num_rows(lp);
+                int m = glp_get_num_cols(lp);
+                int nb(0), mb(0);
+                for (int i = 1; i <= n; ++i) {
+                    if (glp_get_row_stat(lp, i) == GLP_BS) {
+                        ++nb;
+                    }
+                }
+                for (int j = 1; j <= m; ++j) {
+                    if (glp_get_col_stat(lp, j) == GLP_BS) {
+                        ++mb;
+                    }
+                }
+                if (n != (nb + mb)) {
+                    glp_std_basis(this->lp);
+                }
             }
         }
 

src/test/storm/solver/GlpkLpSolverTest.cpp

@@ -259,8 +259,8 @@ TEST(GlpkLpSolver, Incremental) {
     ASSERT_TRUE(solver.isOptimal());
     EXPECT_EQ(12.0, solver.getContinuousValue(x));
     
-    ASSERT_NO_THROW(y = solver.addUnboundedContinuousVariable("y"));
     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
@@ -296,12 +296,17 @@ TEST(GlpkLpSolver, Incremental) {
     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
+    // 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();
+    ASSERT_NO_THROW(solver.optimize());
+    // max x s.t. x<=12
+    ASSERT_TRUE(solver.isOptimal());
+    EXPECT_EQ(12.0, solver.getContinuousValue(x));
+    
     solver.pop();
     // max x s.t. true
     ASSERT_NO_THROW(solver.optimize());