From 138e0f2cee8c3dd10e6de88b509dcd9eb6fee3b4 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 25 Apr 2019 17:23:37 +0200 Subject: [PATCH] solver: Implemented incremental support for LP solvers (Z3 and Gurobi) --- src/storm/solver/GlpkLpSolver.cpp | 12 ++++++ src/storm/solver/GlpkLpSolver.h | 12 ++++++ src/storm/solver/GurobiLpSolver.cpp | 61 ++++++++++++++++++++++++++++- src/storm/solver/GurobiLpSolver.h | 17 ++++++++ src/storm/solver/LpSolver.cpp | 34 ++++++++++++++++ src/storm/solver/LpSolver.h | 36 +++++++++++++++++ src/storm/solver/Z3LpSolver.cpp | 19 ++++++++- src/storm/solver/Z3LpSolver.h | 3 ++ 8 files changed, 191 insertions(+), 3 deletions(-) diff --git a/src/storm/solver/GlpkLpSolver.cpp b/src/storm/solver/GlpkLpSolver.cpp index 707883c05..3bec1c426 100644 --- a/src/storm/solver/GlpkLpSolver.cpp +++ b/src/storm/solver/GlpkLpSolver.cpp @@ -378,6 +378,18 @@ namespace storm { glp_write_lp(this->lp, 0, filename.c_str()); } + + template + void GlpkLpSolver::push() { + throw storm::exceptions::NotImplementedException() << "The glpk interface currently does not support push() operations. Select another LP solver."; + } + + template + void GlpkLpSolver::pop() { + throw storm::exceptions::NotImplementedException() << "The glpk interface currently does not support pop() operations. Select another LP solver."; + } + + template class GlpkLpSolver; template class GlpkLpSolver; #endif diff --git a/src/storm/solver/GlpkLpSolver.h b/src/storm/solver/GlpkLpSolver.h index a0c30b39a..6594c2a45 100644 --- a/src/storm/solver/GlpkLpSolver.h +++ b/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 } diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index 23866ea46..3fef398f0 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/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 - GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), env(nullptr), model(nullptr), nextVariableIndex(0) { + GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(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 @@ -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 + void GurobiLpSolver::push() { + IncrementalLevel lvl; + lvl.firstConstraintIndex = nextConstraintIndex; + incrementalData.push_back(lvl); + } + + template + void GurobiLpSolver::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 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 indicesToBeRemoved = storm::utility::vector::buildVectorForRange(firstIndex, nextVariableIndex); + GRBdelvars(model, indicesToBeRemoved.size(), indicesToBeRemoved.data()); + nextVariableIndex = firstIndex; + } + incrementalData.pop_back(); + update(); + } + } + + #else template GurobiLpSolver::GurobiLpSolver(std::string const&, OptimizationDirection const&) { @@ -514,6 +563,16 @@ namespace storm { void GurobiLpSolver::toggleOutput(bool) const { 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 + void GurobiLpSolver::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 + void GurobiLpSolver::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; diff --git a/src/storm/solver/GurobiLpSolver.h b/src/storm/solver/GurobiLpSolver.h index f1ca786f3..955e4c5ff 100644 --- a/src/storm/solver/GurobiLpSolver.h +++ b/src/storm/solver/GurobiLpSolver.h @@ -56,6 +56,12 @@ namespace storm { */ GurobiLpSolver(); + /*! + * Creates a (deep) copy of this solver. + * @param other + */ + GurobiLpSolver(GurobiLpSolver 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 variableToIndexMap; + + struct IncrementalLevel { + std::vector variables; + int firstConstraintIndex; + }; + std::vector incrementalData; }; } diff --git a/src/storm/solver/LpSolver.cpp b/src/storm/solver/LpSolver.cpp index 7d5e6c60a..ae7318013 100644 --- a/src/storm/solver/LpSolver.cpp +++ b/src/storm/solver/LpSolver.cpp @@ -19,6 +19,40 @@ namespace storm { // Intentionally left empty. } + template + storm::expressions::Variable LpSolver::addContinuousVariable(std::string const& name, boost::optional const& lowerBound, boost::optional 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 + storm::expressions::Variable LpSolver::addIntegerVariable(std::string const& name, boost::optional const& lowerBound, boost::optional 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 storm::expressions::Expression LpSolver::getConstant(ValueType value) const { return manager->rational(value); diff --git a/src/storm/solver/LpSolver.h b/src/storm/solver/LpSolver.h index 08d91c463..f397352fe 100644 --- a/src/storm/solver/LpSolver.h +++ b/src/storm/solver/LpSolver.h @@ -5,6 +5,7 @@ #include #include #include +#include #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 const& lowerBound = boost::none, boost::optional 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 const& lowerBound = boost::none, boost::optional 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 manager; diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index bd37e1baa..c152a9d20 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -257,6 +257,16 @@ namespace storm { void Z3LpSolver::writeModelToFile(std::string const& filename) const { STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3."); } + + template + void Z3LpSolver::push() { + solver->push(); + } + + template + void Z3LpSolver::pop() { + solver->pop(); + } #else template @@ -382,9 +392,14 @@ namespace storm { ValueType Z3LpSolver::getObjectiveValue() const { 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 + void Z3LpSolver::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 - void Z3LpSolver::writeModelToFile(std::string const&) const { + void Z3LpSolver::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 diff --git a/src/storm/solver/Z3LpSolver.h b/src/storm/solver/Z3LpSolver.h index 38922987c..a1877091c 100644 --- a/src/storm/solver/Z3LpSolver.h +++ b/src/storm/solver/Z3LpSolver.h @@ -95,6 +95,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;