From 91951f6714f99e2ff13a3fe4cd8a2fbdb3663380 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 29 Apr 2019 09:29:29 +0200
Subject: [PATCH 1/2] GurobiLpSolver: Fixed an issue when popping and pushing
variables with the same name.
---
src/storm/solver/GurobiLpSolver.cpp | 21 ++++++++++++---------
1 file changed, 12 insertions(+), 9 deletions(-)
diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp
index 3fef398f0..3e0db5333 100644
--- a/src/storm/solver/GurobiLpSolver.cpp
+++ b/src/storm/solver/GurobiLpSolver.cpp
@@ -93,69 +93,72 @@ namespace storm {
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, lowerBound, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
- storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
+ storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_BINARY, 0, 1, objectiveFunctionCoefficient);
return newVariable;
}
template<typename ValueType>
void GurobiLpSolver<ValueType>::addVariable(storm::expressions::Variable const& variable, char variableType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
+ // Assert whether the variable does not exist yet.
+ // Due to incremental usage (push(), pop()), a variable might be declared in the manager but not in the lp model.
+ STORM_LOG_ASSERT(variableToIndexMap.count(variable) == 0, "Variable " << variable.getName() << " exists already in the model.");
// Check for valid variable type.
STORM_LOG_ASSERT(variableType == GRB_CONTINUOUS || variableType == GRB_INTEGER || variableType == GRB_BINARY, "Illegal type '" << variableType << "' for Gurobi variable.");
From ca9102616bfd5d873c4b0f1b5cd616ef278872aa Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 29 Apr 2019 09:43:31 +0200
Subject: [PATCH 2/2] ExpressionManager: Asserted that when getting a variable
with declareOrGetVariable, the returned type is as expected (part 2...).
---
src/storm/storage/expressions/ExpressionManager.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp
index ce10152e4..219e5a521 100644
--- a/src/storm/storage/expressions/ExpressionManager.cpp
+++ b/src/storm/storage/expressions/ExpressionManager.cpp
@@ -167,7 +167,7 @@ namespace storm {
STORM_LOG_THROW(!checkName || isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'.");
auto nameIndexPair = nameToIndexMapping.find(name);
if (nameIndexPair != nameToIndexMapping.end()) {
- STORM_LOG_ASSERT(indexToTypeMapping.at(nameIndexPair->second) == variableType, "Tried to declareOrGet variable '" << name << "' of type '" << variableType << "' but there is a variable with that name and different type '" << indexToTypeMapping.at(nameIndexPair->second)"'.");
+ STORM_LOG_ASSERT(indexToTypeMapping.at(nameIndexPair->second) == variableType, "Tried to declareOrGet variable '" << name << "' of type '" << variableType << "' but there is a variable with that name and different type '" << indexToTypeMapping.at(nameIndexPair->second) << "'.");
return Variable(this->getSharedPointer(), nameIndexPair->second);
} else {
uint_fast64_t offset = 0;