solver: Implemented incremental support for LP solvers (Z3 and Gurobi)

src/storm/solver/GlpkLpSolver.cpp

@@ -378,6 +378,18 @@ namespace storm {
             glp_write_lp(this->lp, 0, filename.c_str());
         }
         
+        
+        template<typename ValueType>
+        void GlpkLpSolver<ValueType>::push()  {
+            throw storm::exceptions::NotImplementedException() << "The glpk interface currently does not support push() operations. Select another LP solver.";
+        }
+        
+        template<typename ValueType>
+        void GlpkLpSolver<ValueType>::pop()  {
+            throw storm::exceptions::NotImplementedException() << "The glpk interface currently does not support pop() operations. Select another LP solver.";
+        }
+
+        
         template class GlpkLpSolver<double>;
         template class GlpkLpSolver<storm::RationalNumber>;
 #endif

src/storm/solver/GlpkLpSolver.h

@@ -93,6 +93,9 @@ namespace storm {
             // Methods to print the LP problem to a file.
             virtual void writeModelToFile(std::string const& filename) const override;
             
+            virtual void push() override;
+            virtual void pop() override;
+
         private:
             /*!
              * Adds a variable with the given name, type, lower and upper bound and objective function coefficient.
@@ -233,6 +236,15 @@ namespace storm {
             virtual void writeModelToFile(std::string const& filename) const override {
                 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
             }
+            
+            virtual void push() override {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+            }
+            
+            virtual void pop() override {
+                throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+            }
+
         };
 #endif
     }

src/storm/solver/GurobiLpSolver.cpp

@@ -10,6 +10,7 @@
 
 #include "storm/utility/macros.h"
 #include "storm/utility/constants.h"
+#include "storm/utility/vector.h"
 
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/ExpressionManager.h"
@@ -25,7 +26,7 @@ namespace storm {
         
 #ifdef STORM_HAVE_GUROBI
         template<typename ValueType>
-        GurobiLpSolver<ValueType>::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver<ValueType>(optDir), env(nullptr), model(nullptr), nextVariableIndex(0) {
+        GurobiLpSolver<ValueType>::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver<ValueType>(optDir), env(nullptr), model(nullptr), nextVariableIndex(0), nextConstraintIndex(0) {
             // Create the environment.
             int error = GRBloadenv(&env, "");
             if (error || env == nullptr) {
@@ -164,6 +165,9 @@ namespace storm {
             STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ", error code " << error << ").");
             this->variableToIndexMap.emplace(variable, nextVariableIndex);
             ++nextVariableIndex;
+            if (!incrementalData.empty()) {
+                incrementalData.back().variables.push_back(variable);
+            }
         }
         
         template<typename ValueType>
@@ -205,6 +209,7 @@ namespace storm {
                 default:
                     STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
             }
+            ++nextConstraintIndex;
             STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not assert constraint (" << GRBgeterrormsg(env) << ", error code " << error << ").");
         }
         
@@ -385,6 +390,50 @@ namespace storm {
             int error = GRBsetintparam(env, "OutputFlag", set);
             STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ").");
         }
+        
+        template<typename ValueType>
+        void GurobiLpSolver<ValueType>::push() {
+            IncrementalLevel lvl;
+            lvl.firstConstraintIndex = nextConstraintIndex;
+            incrementalData.push_back(lvl);
+        }
+        
+        template<typename ValueType>
+        void GurobiLpSolver<ValueType>::pop() {
+            if (incrementalData.empty()) {
+                STORM_LOG_ERROR("Tried to pop from a solver without pushing before.");
+            } else {
+                // TODO: check if we need to update before deleting
+                IncrementalLevel const& lvl = incrementalData.back();
+                
+                std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(lvl.firstConstraintIndex, nextConstraintIndex);
+                GRBdelconstrs(model, indicesToBeRemoved.size(), indicesToBeRemoved.data());
+                nextConstraintIndex = lvl.firstConstraintIndex;
+                indicesToBeRemoved.clear();
+                
+                if (!lvl.variables.empty()) {
+                    int firstIndex = -1;
+                    bool first = true;
+                    for (auto const& var : lvl.variables) {
+                        if (first) {
+                            auto it = variableToIndexMap.find(var);
+                            firstIndex = it->second;
+                            variableToIndexMap.erase(it);
+                            first = false;
+                        } else {
+                            variableToIndexMap.erase(var);
+                        }
+                    }
+                    std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(firstIndex, nextVariableIndex);
+                    GRBdelvars(model, indicesToBeRemoved.size(), indicesToBeRemoved.data());
+                    nextVariableIndex = firstIndex;
+                }
+                incrementalData.pop_back();
+                update();
+            }
+        }
+        
+        
 #else
         template<typename ValueType>
         GurobiLpSolver<ValueType>::GurobiLpSolver(std::string const&, OptimizationDirection const&) {
@@ -515,6 +564,16 @@ namespace storm {
             throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
         }
         
+        template<typename ValueType>
+        void GurobiLpSolver<ValueType>::push() {
+            throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+        }
+        
+        template<typename ValueType>
+        void GurobiLpSolver<ValueType>::pop() {
+            throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+        }
+
 #endif
         template class GurobiLpSolver<double>;
         template class GurobiLpSolver<storm::RationalNumber>;

src/storm/solver/GurobiLpSolver.h

@@ -56,6 +56,12 @@ namespace storm {
              */
             GurobiLpSolver();
             
+            /*!
+             * Creates a (deep) copy of this solver.
+             * @param other
+             */
+            GurobiLpSolver(GurobiLpSolver<ValueType> const& other);
+            
             /*!
              * Destructs a solver by freeing the pointers to Gurobi's structures.
              */
@@ -99,6 +105,8 @@ namespace storm {
 
             virtual void toggleOutput(bool set) const;
             
+            virtual void push() override;
+            virtual void pop() override;
         private:
             /*!
              * Sets some properties of the Gurobi environment according to parameters given by the options.
@@ -126,8 +134,17 @@ namespace storm {
             // The index of the next variable.
             int nextVariableIndex;
             
+            // The index of the next constraint.
+            int nextConstraintIndex;
+            
             // A mapping from variables to their indices.
             std::map<storm::expressions::Variable, int> variableToIndexMap;
+            
+            struct IncrementalLevel {
+                std::vector<storm::expressions::Variable> variables;
+                int firstConstraintIndex;
+            };
+            std::vector<IncrementalLevel> incrementalData;
         };
 
     }

src/storm/solver/LpSolver.cpp

@@ -19,6 +19,40 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        template<typename ValueType>
+        storm::expressions::Variable LpSolver<ValueType>::addContinuousVariable(std::string const& name, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound, ValueType objectiveFunctionCoefficient) {
+            if (lowerBound) {
+                if (upperBound) {
+                    return addBoundedContinuousVariable(name, lowerBound.get(), upperBound.get(), objectiveFunctionCoefficient);
+                } else {
+                    return addLowerBoundedContinuousVariable(name, lowerBound.get(), objectiveFunctionCoefficient);
+                }
+            } else {
+                if (upperBound) {
+                    return addUpperBoundedContinuousVariable(name, upperBound.get(), objectiveFunctionCoefficient);
+                } else {
+                    return addUnboundedContinuousVariable(name, objectiveFunctionCoefficient);
+                }
+            }
+        }
+        
+        template<typename ValueType>
+        storm::expressions::Variable LpSolver<ValueType>::addIntegerVariable(std::string const& name, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound, ValueType objectiveFunctionCoefficient) {
+            if (lowerBound) {
+                if (upperBound) {
+                    return addBoundedIntegerVariable(name, lowerBound.get(), upperBound.get(), objectiveFunctionCoefficient);
+                } else {
+                    return addLowerBoundedIntegerVariable(name, lowerBound.get(), objectiveFunctionCoefficient);
+                }
+            } else {
+                if (upperBound) {
+                    return addUpperBoundedIntegerVariable(name, upperBound.get(), objectiveFunctionCoefficient);
+                } else {
+                    return addUnboundedIntegerVariable(name, objectiveFunctionCoefficient);
+                }
+            }
+        }
+        
         template<typename ValueType>
         storm::expressions::Expression LpSolver<ValueType>::getConstant(ValueType value) const {
             return manager->rational(value);

src/storm/solver/LpSolver.h

@@ -5,6 +5,7 @@
 #include <vector>
 #include <cstdint>
 #include <memory>
+#include <boost/optional.hpp>
 #include "OptimizationDirection.h"
 
 namespace storm {
@@ -81,6 +82,18 @@ namespace storm {
              */
             virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0;
             
+           
+            /*!
+             * Registers a continuous variable, i.e. a variable that may take all real values within its bounds (if given).
+             *
+             * @param name The name of the variable.
+             * @param lowerBound The lower bound of the variable (unbounded if not given).
+             * @param upperBound The upper bound of the variable (unbounded if not given).
+             * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective
+             * function. If omitted (or set to zero), the variable is irrelevant for the objective value.
+             */
+            storm::expressions::Variable addContinuousVariable(std::string const& name, boost::optional<ValueType> const& lowerBound = boost::none, boost::optional<ValueType> const& upperBound = boost::none, ValueType objectiveFunctionCoefficient = 0);
+            
             /*!
              * Registers an upper- and lower-bounded integer variable, i.e. a variable that may take all integer values
              * within its bounds.
@@ -124,6 +137,17 @@ namespace storm {
              */
             virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0;
             
+            /*!
+             * Registers an integer variable, i.e. a variable that may take all integer values within its bounds (if given).
+             *
+             * @param name The name of the variable.
+             * @param lowerBound The lower bound of the variable.
+             * @param upperBound The upper bound of the variable.
+             * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective
+             * function. If omitted (or set to zero), the variable is irrelevant for the objective value.
+             */
+            virtual storm::expressions::Variable addIntegerVariable(std::string const& name, boost::optional<ValueType> const& lowerBound = boost::none, boost::optional<ValueType> const& upperBound = boost::none, ValueType objectiveFunctionCoefficient = 0);
+            
             /*!
              * Registers a boolean variable, i.e. a variable that may be either 0 or 1.
              *
@@ -259,6 +283,18 @@ namespace storm {
                 return *manager;
             }
             
+			/*!
+             * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those
+             * assertions from the solver's stack that were added after this call.
+             */
+			virtual void push() = 0;
+   
+			/*!
+             * Pops a backtracking point from the solver's stack. This deletes all assertions from the solver's stack
+             * that were added after the last call to push().
+             */
+			virtual void pop() = 0;
+        
         protected:
             // The manager responsible for the variables.
             std::shared_ptr<storm::expressions::ExpressionManager> manager;

src/storm/solver/Z3LpSolver.cpp

@@ -258,6 +258,16 @@ namespace storm {
             STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3.");
         }
         
+        template<typename ValueType>
+        void Z3LpSolver<ValueType>::push()  {
+            solver->push();
+        }
+        
+        template<typename ValueType>
+        void Z3LpSolver<ValueType>::pop()  {
+            solver->pop();
+        }
+
 #else
         template<typename ValueType>
         Z3LpSolver<ValueType>::Z3LpSolver(std::string const&, OptimizationDirection const&) {
@@ -384,7 +394,12 @@ namespace storm {
         }
         
         template<typename ValueType>
-        void Z3LpSolver<ValueType>::writeModelToFile(std::string const&) const {
+        void Z3LpSolver<ValueType>::push()  {
+            throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
+        }
+        
+        template<typename ValueType>
+        void Z3LpSolver<ValueType>::pop()  {
             throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
         }
 #endif

src/storm/solver/Z3LpSolver.h

@@ -96,6 +96,9 @@ namespace storm {
             // Methods to print the LP problem to a file.
             virtual void writeModelToFile(std::string const& filename) const override;
             
+            virtual void push() override;
+            virtual void pop() override;
+
         private:
              virtual storm::expressions::Expression getValue(storm::expressions::Variable const& variable) const;