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<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
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<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&) {
@@ -514,6 +563,16 @@ namespace storm {
void GurobiLpSolver<ValueType>::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<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>;
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<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;
};
}
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<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);
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 <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;
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<ValueType>::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<typename ValueType>
+ void Z3LpSolver<ValueType>::push() {
+ solver->push();
+ }
+
+ template<typename ValueType>
+ void Z3LpSolver<ValueType>::pop() {
+ solver->pop();
+ }
#else
template<typename ValueType>
@@ -382,9 +392,14 @@ namespace storm {
ValueType Z3LpSolver<ValueType>::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<typename ValueType>
+ 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>::writeModelToFile(std::string const&) const {
+ 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
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;