Adapted LP solver interface to new variable handling.

Former-commit-id: c2a7eea5db

src/parser/ExpressionParser.h

@@ -5,6 +5,7 @@
 
 #include "src/parser/SpiritParserDefinitions.h"
 #include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/ExpressionManager.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/WrongFormatException.h"
 

src/solver/GlpkLpSolver.cpp

@@ -72,49 +72,54 @@ namespace storm {
         }
         
         storm::expressions::Variable GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GLP_IV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient);
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GLP_IV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
             return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GLP_IV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient);
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GLP_IV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
+            return newVariable;
         }
 
         storm::expressions::Variable GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GLP_IV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient);
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GLP_IV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
+            return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GLP_IV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GLP_IV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
+            return newVariable;
         }
         
         storm::expressions::Variable GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GLP_BV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GLP_BV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
             this->modelContainsIntegerVariables = true;
+            return newVariable;
         }
         
         void GlpkLpSolver::addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            // Check whether variable already exists.
-            auto nameIndexPair = this->variableToIndexMap.find(name);
-            STORM_LOG_THROW(nameIndexPair == this->variableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists.");
-            
             // Check for valid variable type.
             STORM_LOG_ASSERT(variableType == GLP_CV || variableType == GLP_IV || variableType == GLP_BV, "Illegal type '" << variableType << "' for glpk variable.");
             
             // Check for valid bound type.
-            STORM_LOG_ASSERT(boundType == GLP_FR || boundType == GLP_UP || boundType == GLP_LO || boundType == GLP_DB, "Illegal bound type for variable '" << name << "'.");
+            STORM_LOG_ASSERT(boundType == GLP_FR || boundType == GLP_UP || boundType == GLP_LO || boundType == GLP_DB, "Illegal bound type for variable '" << variable.getName() << "'.");
             
             // Finally, create the actual variable.
             glp_add_cols(this->lp, 1);
-            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_name(this->lp, nextVariableIndex, variable.getName().c_str());
             glp_set_col_bnds(lp, nextVariableIndex, boundType, lowerBound, upperBound);
             glp_set_col_kind(this->lp, nextVariableIndex, variableType);
             glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
-            this->variableToIndexMap.emplace(name, this->nextVariableIndex);
+            this->variableToIndexMap.emplace(variable, this->nextVariableIndex);
             ++this->nextVariableIndex;
         }
         
@@ -127,6 +132,7 @@ namespace storm {
             glp_add_rows(this->lp, 1);
             glp_set_row_name(this->lp, nextConstraintIndex, name.c_str());
             
+            STORM_LOG_THROW(constraint.getManager() == this->getManager(), storm::exceptions::InvalidArgumentException, "Constraint was not built over the proper variables.");
             STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
             STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
             
@@ -139,27 +145,26 @@ namespace storm {
             std::vector<double> coefficients;
             for (auto const& variableCoefficientPair : leftCoefficients) {
                 auto variableIndexPair = this->variableToIndexMap.find(variableCoefficientPair.first);
-                STORM_LOG_THROW(identifierIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'.");
-                variables.push_back(identifierIndexPair->second);
-                coefficients.push_back(leftCoefficients.first.getDoubleValue(identifier));
+                variables.push_back(variableIndexPair->second);
+                coefficients.push_back(leftCoefficients.getCoefficient(variableIndexPair->first));
             }
             
             // Determine the type of the constraint and add it properly.
             switch (constraint.getOperator()) {
                 case storm::expressions::OperatorType::Less:
-                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightCoefficients.second - storm::settings::glpkSettings().getIntegerTolerance());
+                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightCoefficients.getConstantPart() - storm::settings::glpkSettings().getIntegerTolerance());
                     break;
                 case storm::expressions::OperatorType::LessOrEqual:
-                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightCoefficients.second);
+                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightCoefficients.getConstantPart());
                     break;
                 case storm::expressions::OperatorType::Greater:
-                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightCoefficients.second + storm::settings::glpkSettings().getIntegerTolerance(), 0);
+                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightCoefficients.getConstantPart() + storm::settings::glpkSettings().getIntegerTolerance(), 0);
                     break;
                 case storm::expressions::OperatorType::GreaterOrEqual:
-                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightCoefficients.second, 0);
+                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightCoefficients.getConstantPart(), 0);
                     break;
                 case storm::expressions::OperatorType::Equal:
-                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_FX, rightCoefficients.second, rightCoefficients.second);
+                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_FX, rightCoefficients.getConstantPart(), rightCoefficients.getConstantPart());
                     break;
                 default:
                     STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
@@ -250,15 +255,15 @@ namespace storm {
             return status == GLP_OPT;
         }
         
-        double GlpkLpSolver::getContinuousValue(std::string const& name) const {
+        double GlpkLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
             if (!this->isOptimal()) {
                 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
                 STORM_LOG_THROW(!this->isUnbounded(),  storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
                 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
             }
             
-            auto variableIndexPair = this->variableToIndexMap.find(name);
-            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            auto variableIndexPair = this->variableToIndexMap.find(variable);
+            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'.");
             
             double value = 0;
             if (this->modelContainsIntegerVariables) {
@@ -269,15 +274,15 @@ namespace storm {
             return value;
         }
         
-        int_fast64_t GlpkLpSolver::getIntegerValue(std::string const& name) const {
+        int_fast64_t GlpkLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const {
             if (!this->isOptimal()) {
                 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
                 STORM_LOG_THROW(!this->isUnbounded(),  storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
                 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
             }
            
-            auto variableIndexPair = this->variableToIndexMap.find(name);
-            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            auto variableIndexPair = this->variableToIndexMap.find(variable);
+            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'.");
 
             double value = 0;
             if (this->modelContainsIntegerVariables) {
@@ -292,15 +297,15 @@ namespace storm {
             return static_cast<int_fast64_t>(value);
         }
         
-        bool GlpkLpSolver::getBinaryValue(std::string const& name) const {
+        bool GlpkLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const {
             if (!this->isOptimal()) {
                 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
                 STORM_LOG_THROW(!this->isUnbounded(),  storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
                 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
             }
 
-            auto variableIndexPair = this->variableToIndexMap.find(name);
-            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            auto variableIndexPair = this->variableToIndexMap.find(variable);
+            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'.");
             
             double value = 0;
             if (this->modelContainsIntegerVariables) {

src/solver/GurobiLpSolver.cpp

@@ -74,55 +74,69 @@ namespace storm {
             this->currentModelHasBeenOptimized = false;
         }
         
-        void GurobiLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_CONTINUOUS, lowerBound, upperBound, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, upperBound, objectiveFunctionCoefficient);
+            return newVariable;
         }
         
-        void GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_CONTINUOUS, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
+            return newVariable;
         }
 
-        void GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_CONTINUOUS, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
+            return newVariable;
         }
 
-        void GurobiLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_CONTINUOUS, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
+            this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
+            return newVariable;
         }
         
-        void GurobiLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_INTEGER, lowerBound, upperBound, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GRB_INTEGER, lowerBound, upperBound, objectiveFunctionCoefficient);
+            return newVariable;
         }
         
-        void GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_INTEGER, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GRB_INTEGER, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
+            return newVariable;
         }
         
-        void GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_INTEGER, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
+            return newVariable;
         }
         
-        void GurobiLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_INTEGER, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
+            return newVariable;
         }
         
-        void GurobiLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            this->addVariable(name, GRB_BINARY, 0, 1, objectiveFunctionCoefficient);
+        storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
+            this->addVariable(newVariable, GRB_BINARY, 0, 1, objectiveFunctionCoefficient);
+            return newVariable;
         }
 
-        void GurobiLpSolver::addVariable(std::string const& name, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            // Check whether variable already exists.
-            auto nameIndexPair = this->variableNameToIndexMap.find(name);
-            STORM_LOG_THROW(nameIndexPair == this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Variable '" << nameIndexPair->first << "' already exists.");
-            
+        void GurobiLpSolver::addVariable(storm::expressions::Variable const& variable, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
             // Check for valid variable type.
             STORM_LOG_ASSERT(variableType == GRB_CONTINUOUS || variableType == GRB_INTEGER || variableType == GRB_BINARY, "Illegal type '" << variableType << "' for Gurobi variable.");
             
             // Finally, create the actual variable.
             int error = 0;
-            error = GRBaddvar(model, 0, nullptr, nullptr, objectiveFunctionCoefficient, lowerBound, upperBound, variableType, name.c_str());
+            error = GRBaddvar(model, 0, nullptr, nullptr, objectiveFunctionCoefficient, lowerBound, upperBound, variableType, variable.getName().c_str());
             STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ", error code " << error << ").");
-            this->variableNameToIndexMap.emplace(name, nextVariableIndex);
+            this->variableToIndexMap.emplace(variable, nextVariableIndex);
             ++nextVariableIndex;
         }
                 
@@ -130,44 +144,36 @@ namespace storm {
             STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
             STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
             
-            std::pair<storm::expressions::SimpleValuation, double> leftCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(0));
-            std::pair<storm::expressions::SimpleValuation, double> rightCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(1));
-            for (auto const& identifier : rightCoefficients.first.getDoubleIdentifiers()) {
-                if (leftCoefficients.first.containsDoubleIdentifier(identifier)) {
-                    leftCoefficients.first.setDoubleValue(identifier, leftCoefficients.first.getDoubleValue(identifier) - rightCoefficients.first.getDoubleValue(identifier));
-                } else {
-                    leftCoefficients.first.addDoubleIdentifier(identifier, -rightCoefficients.first.getDoubleValue(identifier));
-                }
-            }
-            rightCoefficients.second -= leftCoefficients.second;
+            storm::expressions::LinearCoefficientVisitor::VariableCoefficients leftCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(0));
+            storm::expressions::LinearCoefficientVisitor::VariableCoefficients rightCoefficients = storm::expressions::LinearCoefficientVisitor().getLinearCoefficients(constraint.getOperand(1));
+            leftCoefficients.separateVariablesFromConstantPart(rightCoefficients);
             
             // Now we need to transform the coefficients to the vector representation.
             std::vector<int> variables;
             std::vector<double> coefficients;
-            for (auto const& identifier : leftCoefficients.first.getDoubleIdentifiers()) {
-                auto identifierIndexPair = this->variableNameToIndexMap.find(identifier);
-                STORM_LOG_THROW(identifierIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Constraint contains illegal identifier '" << identifier << "'.");
-                variables.push_back(identifierIndexPair->second);
-                coefficients.push_back(leftCoefficients.first.getDoubleValue(identifier));
+            for (auto const& variableCoefficientPair : leftCoefficients) {
+                auto variableIndexPair = this->variableToIndexMap.find(variableCoefficientPair.first);
+                variables.push_back(variableIndexPair->second);
+                coefficients.push_back(leftCoefficients.getCoefficient(variableIndexPair->first));
             }
             
             // Determine the type of the constraint and add it properly.
             int error = 0;
             switch (constraint.getOperator()) {
                 case storm::expressions::OperatorType::Less:
-                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_LESS_EQUAL, rightCoefficients.second - storm::settings::gurobiSettings().getIntegerTolerance(), name == "" ? nullptr : name.c_str());
+                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_LESS_EQUAL, rightCoefficients.getConstantPart() - storm::settings::gurobiSettings().getIntegerTolerance(), name == "" ? nullptr : name.c_str());
                     break;
                 case storm::expressions::OperatorType::LessOrEqual:
-                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_LESS_EQUAL, rightCoefficients.second, name == "" ? nullptr : name.c_str());
+                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_LESS_EQUAL, rightCoefficients.getConstantPart(), name == "" ? nullptr : name.c_str());
                     break;
                 case storm::expressions::OperatorType::Greater:
-                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_GREATER_EQUAL, rightCoefficients.second + storm::settings::gurobiSettings().getIntegerTolerance(), name == "" ? nullptr : name.c_str());
+                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_GREATER_EQUAL, rightCoefficients.getConstantPart() + storm::settings::gurobiSettings().getIntegerTolerance(), name == "" ? nullptr : name.c_str());
                     break;
                 case storm::expressions::OperatorType::GreaterOrEqual:
-                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_GREATER_EQUAL, rightCoefficients.second, name == "" ? nullptr : name.c_str());
+                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_GREATER_EQUAL, rightCoefficients.getConstantPart(), name == "" ? nullptr : name.c_str());
                     break;
                 case storm::expressions::OperatorType::Equal:
-                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_EQUAL, rightCoefficients.second, name == "" ? nullptr : name.c_str());
+                    error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_EQUAL, rightCoefficients.getConstantPart(), name == "" ? nullptr : name.c_str());
                     break;
                 default:
                     STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
@@ -258,15 +264,15 @@ namespace storm {
             return optimalityStatus == GRB_OPTIMAL;
         }
         
-        double GurobiLpSolver::getContinuousValue(std::string const& name) const {
+        double GurobiLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
             if (!this->isOptimal()) {
                 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
                 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
                 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
             }
             
-            auto variableIndexPair = this->variableNameToIndexMap.find(name);
-            STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            auto variableIndexPair = this->variableToIndexMap.find(variable);
+            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'.");
             
             double value = 0;
             int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);
@@ -275,15 +281,15 @@ namespace storm {
             return value;
         }
         
-        int_fast64_t GurobiLpSolver::getIntegerValue(std::string const& name) const {
+        int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const {
             if (!this->isOptimal()) {
                 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
                 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
                 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
             }
             
-            auto variableIndexPair = this->variableNameToIndexMap.find(name);
-            STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            auto variableIndexPair = this->variableToIndexMap.find(variable);
+            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'.");
             
             double value = 0;
             int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);
@@ -293,15 +299,15 @@ namespace storm {
             return static_cast<int_fast64_t>(value);
         }
         
-        bool GurobiLpSolver::getBinaryValue(std::string const& name) const {
+        bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const {
             if (!this->isOptimal()) {
                 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
                 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
                 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ").");
             }
 
-            auto variableIndexPair = this->variableNameToIndexMap.find(name);
-            STORM_LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            auto variableIndexPair = this->variableToIndexMap.find(variable);
+            STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'.");
             
             double value = 0;
             int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);

src/solver/GurobiLpSolver.h

@@ -61,19 +61,19 @@ namespace storm {
             virtual ~GurobiLpSolver();
             
             // Methods to add continuous variables.
-            virtual void addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
-            virtual void addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
-            virtual void addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
-            virtual void addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
             
             // Methods to add integer variables.
-            virtual void addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
-            virtual void addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
-            virtual void addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
-            virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
             
             // Methods to add binary variables.
-            virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
+            virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
             
             // Methods to incorporate recent changes.
             virtual void update() const override;
@@ -88,9 +88,9 @@ namespace storm {
             virtual bool isOptimal() const override;
             
             // Methods to retrieve values of variables and the objective function in the optimal solutions.
-            virtual double getContinuousValue(std::string const& name) const override;
-            virtual int_fast64_t getIntegerValue(std::string const& name) const override;
-            virtual bool getBinaryValue(std::string const& name) const override;
+            virtual double getContinuousValue(storm::expressions::Variable const& name) const override;
+            virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override;
+            virtual bool getBinaryValue(storm::expressions::Variable const& name) const override;
             virtual double getObjectiveValue() const override;
             
             // Methods to print the LP problem to a file.
@@ -105,13 +105,13 @@ namespace storm {
             /*!
              * Adds a variable with the given name, type, lower and upper bound and objective function coefficient.
              *
-             * @param name The name of the variable.
+             * @param variable The variable to add.
              * @param variableType The type of the variable in terms of Gurobi's constants.
              * @param lowerBound The lower bound of the range of the variable.
              * @param upperBound The upper bound of the range of the variable.
              * @param objectiveFunctionCoefficient The coefficient of the variable in the objective function.
              */
-            void addVariable(std::string const& name, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient);
+            void addVariable(storm::expressions::Variable const& variable, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient);
             
             // The Gurobi environment.
             GRBenv* env;
@@ -122,8 +122,8 @@ namespace storm {
             // The index of the next variable.
             int nextVariableIndex;
             
-            // A mapping from variable names to their indices.
-            std::map<std::string, int> variableNameToIndexMap;
+            // A mapping from variables to their indices.
+            std::map<storm::expressions::Variable, int> variableToIndexMap;
         };
 #else
         // If Gurobi is not available, we provide a stub implementation that emits an error if any of its methods is called.
@@ -145,38 +145,38 @@ 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.";
             }
             
-            virtual void addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
-            virtual void addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
                 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.";            }
             
-            virtual void addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
-            virtual void addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
-            virtual void addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
-            virtual void addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
-            virtual void addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
-            virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
-            virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
+            virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
                 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.";
             }
             
@@ -204,15 +204,15 @@ 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.";
             }
             
-            virtual double getContinuousValue(std::string const& name) const override {
+            virtual double getContinuousValue(storm::expressions::Variable const& variable) const override {
                 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.";
             }
             
-            virtual int_fast64_t getIntegerValue(std::string const& name) const override {
+            virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override {
                 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.";
             }
             
-            virtual bool getBinaryValue(std::string const& name) const override {
+            virtual bool getBinaryValue(storm::expressions::Variable const& variable) const override {
                 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.";
             }
             

src/solver/LpSolver.h

@@ -242,6 +242,15 @@ namespace storm {
                 return modelSense;
             }
             
+            /*!
+             * Retrieves the manager for the variables created for this solver.
+             *
+             * @return The manager for the variables created for this solver.
+             */
+            storm::expressions::ExpressionManager const& getManager() const {
+                return *manager;
+            }
+            
         protected:
             // The manager responsible for the variables.
             std::shared_ptr<storm::expressions::ExpressionManager> manager;

src/storage/expressions/Expression.cpp

@@ -109,6 +109,10 @@ namespace storm {
             return this->expressionPtr;
         }
         
+        ExpressionManager const& Expression::getManager() const {
+            return *this->manager;
+        }
+        
         Type const& Expression::getType() const {
             return this->getBaseExpression().getType();
         }

src/storage/expressions/Expression.h

@@ -224,6 +224,13 @@ namespace storm {
              */
             std::shared_ptr<BaseExpression const> const& getBaseExpressionPointer() const;
 
+            /*!
+             * Retrieves the manager responsible for this expression.
+             *
+             * @return The manager responsible for this expression.
+             */
+            ExpressionManager const& getManager() const;
+            
             /*!
              * Retrieves the type of the expression.
              *

src/storage/expressions/LinearCoefficientVisitor.cpp

@@ -63,6 +63,10 @@ namespace storm {
             return variableToCoefficientMapping[variable];
         }
         
+        double LinearCoefficientVisitor::VariableCoefficients::getConstantPart() const {
+            return this->constantPart;
+        }
+        
         void LinearCoefficientVisitor::VariableCoefficients::separateVariablesFromConstantPart(VariableCoefficients& rhs) {
             for (auto const& rhsVariableCoefficientPair : rhs.variableToCoefficientMapping) {
                 this->variableToCoefficientMapping[rhsVariableCoefficientPair.first] -= rhsVariableCoefficientPair.second;

src/storage/expressions/LinearCoefficientVisitor.h

@@ -29,6 +29,7 @@ namespace storm {
                 void negate();
                 void setCoefficient(storm::expressions::Variable const& variable, double coefficient);
                 double getCoefficient(storm::expressions::Variable const& variable);
+                double getConstantPart() const;
                 
                 /*!
                  * Brings all variables of the right-hand side coefficients to the left-hand side by negating them and