Started working on adapting LP solver interface to new expressions.

Former-commit-id: 6131736a7f

src/solver/GlpkLpSolver.cpp

@@ -4,13 +4,10 @@
 
 #include <iostream>
 
-#include "src/exceptions/InvalidStateException.h"
 #include "src/settings/Settings.h"
-
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-
-extern log4cplus::Logger logger;
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/InvalidAccessException.h"
+#include "src/exceptions/InvalidStateException.h"
 
 bool GlpkLpSolverOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool {
 	instance->addOption(storm::settings::OptionBuilder("GlpkLpSolver", "glpkoutput", "", "If set, the glpk output will be printed to the command line.").build());
@@ -22,7 +19,7 @@ bool GlpkLpSolverOptionsRegistered = storm::settings::Settings::registerNewModul
 
 namespace storm {
     namespace solver {
-        GlpkLpSolver::GlpkLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), lp(nullptr), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() {
+        GlpkLpSolver::GlpkLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), lp(nullptr), variableNameToIndexMap(), nextVariableIndex(0), nextConstraintIndex(0), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() {
             // Create the LP problem for glpk.
             lp = glp_create_prob();
             
@@ -38,11 +35,11 @@ namespace storm {
             coefficientValues.push_back(0);
         }
         
-        GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, MINIMIZE) {
+        GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, ModelSense::MINIMIZE) {
             // Intentionally left empty.
         }
         
-        GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", MINIMIZE) {
+        GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", ModelSense::MINIMIZE) {
             // Intentionally left empty.
         }
         
@@ -56,69 +53,126 @@ namespace storm {
             glp_free_env();
         }
         
-        uint_fast64_t GlpkLpSolver::createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
+        void GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
             glp_add_cols(this->lp, 1);
             glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
-            switch (variableType) {
-                case LpSolver::BOUNDED:
-                    glp_set_col_bnds(lp, nextVariableIndex, GLP_DB, lowerBound, upperBound);
-                    break;
-                case LpSolver::UNBOUNDED:
-                    glp_set_col_bnds(lp, nextVariableIndex, GLP_FR, 0, 0);
-                    break;
-                case LpSolver::UPPER_BOUND:
-                    glp_set_col_bnds(lp, nextVariableIndex, GLP_UP, 0, upperBound);
-                    break;
-                case LpSolver::LOWER_BOUND:
-                    glp_set_col_bnds(lp, nextVariableIndex, GLP_LO, lowerBound, 0);
-                    break;
-            }
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_DB, lowerBound, upperBound);
             glp_set_col_kind(this->lp, nextVariableIndex, GLP_CV);
             glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
-            ++nextVariableIndex;
-            
-            this->currentModelHasBeenOptimized = false;
-            return nextVariableIndex - 1;
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
         }
         
-        uint_fast64_t GlpkLpSolver::createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
-            uint_fast64_t index = this->createContinuousVariable(name, variableType, lowerBound, upperBound, objectiveFunctionCoefficient);
-            glp_set_col_kind(this->lp, index, GLP_IV);
+        void GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_LO, lowerBound, 0);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_CV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
+        }
+        
+        void GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_UP, 0, upperBound);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_CV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
+        }
+        
+        void GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_FR, 0, 0);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_CV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
+        }
+        
+        void GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_DB, lowerBound, upperBound);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_IV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
             this->modelContainsIntegerVariables = true;
-            return index;
         }
         
-        uint_fast64_t GlpkLpSolver::createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
-            uint_fast64_t index = this->createContinuousVariable(name, UNBOUNDED, 0, 1, objectiveFunctionCoefficient);
-            glp_set_col_kind(this->lp, index, GLP_BV);
+        void GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_LO, lowerBound, 0);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_IV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
+            this->modelContainsIntegerVariables = true;
+        }
+
+        void GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_UP, 0, upperBound);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_IV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
+            this->modelContainsIntegerVariables = true;
+        }
+        
+        void GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_FR, 0, 0);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_IV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
+            this->modelContainsIntegerVariables = true;
+        }
+        
+        void GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
+            glp_add_cols(this->lp, 1);
+            glp_set_col_name(this->lp, nextVariableIndex, name.c_str());
+            glp_set_col_bnds(lp, nextVariableIndex, GLP_FR, 0, 0);
+            glp_set_col_kind(this->lp, nextVariableIndex, GLP_BV);
+            glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
+            this->variableNameToIndexMap.emplace(name, this->nextVariableIndex);
+            ++this->nextVariableIndex;
             this->modelContainsIntegerVariables = true;
-            return index;
         }
         
         void GlpkLpSolver::update() const {
             // Intentionally left empty.
         }
         
-        void GlpkLpSolver::addConstraint(std::string const& name, std::vector<uint_fast64_t> const& variables, std::vector<double> const& coefficients, BoundType const& boundType, double rightHandSideValue) {
-            if (variables.size() != coefficients.size()) {
-                LOG4CPLUS_ERROR(logger, "Sizes of variable indices vector and coefficients vector do not match.");
-                throw storm::exceptions::InvalidStateException() << "Sizes of variable indices vector and coefficients vector do not match.";
-            }
-
+        void GlpkLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {
             // Add the row that will represent this constraint.
             glp_add_rows(this->lp, 1);
             glp_set_row_name(this->lp, nextConstraintIndex, name.c_str());
             
+            LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
+            LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
+            
+            // TODO: get variable/coefficients vector from constraint.
+            
+            
             // Determine the type of the constraint and add it properly.
-            switch (boundType) {
-                case LESS:
-                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue - storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+            switch (constraint.getOperator()) {
+                case storm::expressions::OperatorType::Less:
+                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue - storm::settings::Settings::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble());
                     break;
                 case LESS_EQUAL:
                     glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue);
                     break;
                 case GREATER:
-                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightHandSideValue + storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble(), 0);
+                    glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightHandSideValue + storm::settings::Settings::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble(), 0);
                     break;
                 case GREATER_EQUAL:
                     glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightHandSideValue, 0);
@@ -143,13 +197,13 @@ namespace storm {
             this->isUnboundedFlag = false;
             
             // Start by setting the model sense.
-            glp_set_obj_dir(this->lp, this->getModelSense() == MINIMIZE ? GLP_MIN : GLP_MAX);
+            glp_set_obj_dir(this->lp, this->getModelSense() == LpSolver::ModelSense::MINIMIZE ? GLP_MIN : GLP_MAX);
             
             glp_load_matrix(this->lp, rowIndices.size() - 1, rowIndices.data(), columnIndices.data(), coefficientValues.data());
             
             int error = 0;
             if (this->modelContainsIntegerVariables) {
-                glp_iocp* parameters = new glp_iocp;
+                glp_iocp* parameters = new glp_iocp();
                 glp_init_iocp(parameters);
                 parameters->presolve = GLP_ON;
                 parameters->tol_int = storm::settings::Settings::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble();
@@ -171,11 +225,7 @@ namespace storm {
                 error = glp_simplex(this->lp, nullptr);
             }
             
-            if (error != 0) {
-                LOG4CPLUS_ERROR(logger, "Unable to optimize glpk model (" << error << ").");
-                throw storm::exceptions::InvalidStateException() << "Unable to optimize glpk model (" << error << ").";
-            }
-            
+            LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize glpk model (" << error << ").");
             this->currentModelHasBeenOptimized = true;
         }
         
@@ -217,103 +267,75 @@ namespace storm {
             return status == GLP_OPT;
         }
         
-        int_fast64_t GlpkLpSolver::getIntegerValue(uint_fast64_t variableIndex) const {
+        double GlpkLpSolver::getContinuousValue(std::string const& name) const {
             if (!this->isOptimal()) {
-                if (this->isInfeasible()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from infeasible model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from infeasible model.";
-                } else if (this->isUnbounded()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unbounded model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unbounded model.";
-                } else {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unoptimized model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unoptimized model.";
-                }
+                LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+                LOG_THROW(!this->isUnbounded(),  storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+                LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
             }
-           
+            
+            auto variableIndexPair = this->variableNameToIndexMap.find(name);
+            LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            
             double value = 0;
             if (this->modelContainsIntegerVariables) {
-                value = glp_mip_col_val(this->lp, static_cast<int>(variableIndex));
+                value = glp_mip_col_val(this->lp, static_cast<int>(variableIndexPair->second));
             } else {
-                value = glp_get_col_prim(this->lp, static_cast<int>(variableIndex));
-            }
-
-            if (std::abs(value - static_cast<int>(value)) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
-                // Nothing to do in this case.
-            } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
-                LOG4CPLUS_ERROR(logger, "Illegal value for integer variable in glpk solution (" << value << ").");
-                throw storm::exceptions::InvalidStateException() << "Illegal value for integer variable in glpk solution (" << value << ").";
+                value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
             }
-            
-            return static_cast<int_fast64_t>(value);
+            return value;
         }
         
-        bool GlpkLpSolver::getBinaryValue(uint_fast64_t variableIndex) const {
+        int_fast64_t GlpkLpSolver::getIntegerValue(std::string const& name) const {
             if (!this->isOptimal()) {
-                if (this->isInfeasible()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from infeasible model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from infeasible model.";
-                } else if (this->isUnbounded()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unbounded model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unbounded model.";
-                } else {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unoptimized model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unoptimized model.";
-                }
+                LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+                LOG_THROW(!this->isUnbounded(),  storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+                LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
             }
+           
+            auto variableIndexPair = this->variableNameToIndexMap.find(name);
+            LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
 
             double value = 0;
             if (this->modelContainsIntegerVariables) {
-                value = glp_mip_col_val(this->lp, static_cast<int>(variableIndex));
+                value = glp_mip_col_val(this->lp, static_cast<int>(variableIndexPair->second));
             } else {
-                value = glp_get_col_prim(this->lp, static_cast<int>(variableIndex));
+                value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
             }
 
-            if (std::abs(value - 1) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
-                // Nothing to do in this case.
-            } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
-                LOG4CPLUS_ERROR(logger, "Illegal value for binary variable in Gurobi solution (" << value << ").");
-                throw storm::exceptions::InvalidStateException() << "Illegal value for binary variable in Gurobi solution (" << value << ").";
-            }
+            // Now check the desired precision was actually achieved.
+            LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::Settings::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
             
-            return static_cast<bool>(value);
+            return static_cast<int_fast64_t>(value);
         }
         
-        double GlpkLpSolver::getContinuousValue(uint_fast64_t variableIndex) const {
+        bool GlpkLpSolver::getBinaryValue(std::string const& name) const {
             if (!this->isOptimal()) {
-                if (this->isInfeasible()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from infeasible model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from infeasible model.";
-                } else if (this->isUnbounded()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unbounded model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unbounded model.";
-                } else {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unoptimized model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unoptimized model.";
-                }
+                LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+                LOG_THROW(!this->isUnbounded(),  storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+                LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
             }
 
+            auto variableIndexPair = this->variableNameToIndexMap.find(name);
+            LOG_THROW(variableIndexPair != this->variableNameToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << name << "'.");
+            
             double value = 0;
             if (this->modelContainsIntegerVariables) {
-                value = glp_mip_col_val(this->lp, static_cast<int>(variableIndex));
+                value = glp_mip_col_val(this->lp, static_cast<int>(variableIndexPair->second));
             } else {
-                value = glp_get_col_prim(this->lp, static_cast<int>(variableIndex));
+                value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
             }
-            return value;
+
+            LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::Settings::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
+            
+            return static_cast<bool>(value);
         }
         
         double GlpkLpSolver::getObjectiveValue() const {
             if (!this->isOptimal()) {
-                if (this->isInfeasible()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from infeasible model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from infeasible model.";
-                } else if (this->isUnbounded()) {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unbounded model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unbounded model.";
-                } else {
-                    LOG4CPLUS_ERROR(logger, "Unable to get glpk solution from unoptimized model.");
-                    throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution from unoptimized model.";
-                }
+                LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
+                LOG_THROW(!this->isUnbounded(),  storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
+                LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
             }
 
             double value = 0;

src/solver/GlpkLpSolver.h

@@ -14,7 +14,6 @@
 namespace storm {
     namespace solver {
 #ifdef STORM_HAVE_GLPK
-        
         /*!
          * A class that implements the LpSolver interface using glpk as the background solver.
          */
@@ -56,33 +55,53 @@ namespace storm {
              */
             virtual ~GlpkLpSolver();
             
-            virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override;
-            virtual uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override;
-            virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override;
+            // 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;
+            
+            // 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;
+
+            // Methods to add binary variables.
+            virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override;
+
+            // Methods to incorporate recent changes.
             virtual void update() const override;
             
-            virtual void addConstraint(std::string const& name, std::vector<uint_fast64_t> const& variables, std::vector<double> const& coefficients, BoundType const& boundType, double rightHandSideValue) override;
+            // Methods to add constraints
+            virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) override;
             
+            // Methods to optimize and retrieve optimality status.
             virtual void optimize() const override;
             virtual bool isInfeasible() const override;
             virtual bool isUnbounded() const override;
             virtual bool isOptimal() const override;
 
-            virtual int_fast64_t getIntegerValue(uint_fast64_t variableIndex) const override;
-            virtual bool getBinaryValue(uint_fast64_t variableIndex) const override;
-            virtual double getContinuousValue(uint_fast64_t variableIndex) 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 getObjectiveValue() const override;
 
+            // Methods to print the LP problem to a file.
             virtual void writeModelToFile(std::string const& filename) const override;
             
         private:
             // The glpk LP problem.
             glp_prob* lp;
             
-            // A counter that keeps track of the next free variable index.
+            // A mapping from variable names to their indices.
+            std::map<std::string, uint_fast64_t> variableNameToIndexMap;
+            
+            // A counter used for getting the next variable index.
             uint_fast64_t nextVariableIndex;
             
-            // A counter that keeps track of the next free constraint index.
+            // A counter used for getting the next constraint index.
             uint_fast64_t nextConstraintIndex;
             
             // A flag storing whether the model is an LP or an MILP.
@@ -121,15 +140,39 @@ namespace storm {
                 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 uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override {
+            virtual void 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 glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+            }
+            
+            virtual void addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) 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 addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) 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 addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) 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 uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override {
+            virtual void 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 glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
             }
             
-            virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override {
+            virtual void addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) 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 addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) 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 addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) 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 uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) 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.";
             }
             
@@ -137,14 +180,14 @@ namespace storm {
                 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 addConstraint(std::string const& name, std::vector<uint_fast64_t> const& variables, std::vector<double> const& coefficients, BoundType const& boundType, double rightHandSideValue) override {
+            virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) 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 optimize() 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 bool isInfeasible() 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.";
             }
@@ -157,15 +200,15 @@ namespace storm {
                 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 int_fast64_t getIntegerValue(uint_fast64_t variableIndex) const override {
+            virtual double getContinuousValue(std::string const& name) 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 bool getBinaryValue(uint_fast64_t variableIndex) const override {
+            virtual int_fast64_t getIntegerValue(std::string const& name) 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 double getContinuousValue(uint_fast64_t variableIndex) const override {
+            virtual bool getBinaryValue(std::string const& name) 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.";
             }
             

src/solver/GurobiLpSolver.h

@@ -60,23 +60,40 @@ namespace storm {
              */
             virtual ~GurobiLpSolver();
             
-            virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override;
-            virtual uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override;
-            virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override;
+            // 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;
+            
+            // 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;
+            
+            // Methods to add binary variables.
+            virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override;
+            
+            // Methods to incorporate recent changes.
             virtual void update() const override;
-
-            virtual void addConstraint(std::string const& name, std::vector<uint_fast64_t> const& variables, std::vector<double> const& coefficients, BoundType const& boundType, double rightHandSideValue) override;
             
+            // Methods to add constraints
+            virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) override;
+            
+            // Methods to optimize and retrieve optimality status.
             virtual void optimize() const override;
             virtual bool isInfeasible() const override;
             virtual bool isUnbounded() const override;
             virtual bool isOptimal() const override;
-
-            virtual int_fast64_t getIntegerValue(uint_fast64_t variableIndex) const override;
-            virtual bool getBinaryValue(uint_fast64_t variableIndex) const override;
-            virtual double getContinuousValue(uint_fast64_t variableIndex) 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 getObjectiveValue() const override;
-
+            
+            // Methods to print the LP problem to a file.
             virtual void writeModelToFile(std::string const& filename) const override;
             
         private:
@@ -91,8 +108,8 @@ namespace storm {
             // The Gurobi model.
             GRBmodel* model;
             
-            // A counter that keeps track of the next free variable index.
-            uint_fast64_t nextVariableIndex;
+            // A mapping from variable names to their indices.
+            std::map<std::string, uint_fast64_t> variableNameToIndexMap;
         };
 #else
         // If Gurobi is not available, we provide a stub implementation that emits an error if any of its methods is called.
@@ -114,27 +131,46 @@ 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 uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override {
+            virtual void 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 uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override {
+            virtual void 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 {
                 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 uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override {
+            virtual void 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 update() const override {
+            virtual void 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 {
                 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 addConstraint(std::string const& name, std::vector<uint_fast64_t> const& variables, std::vector<double> const& coefficients, BoundType const& boundType, double rightHandSideValue) override {
+            virtual void 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 setModelSense(ModelSense const& modelSense) {
+            virtual void 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 uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) 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 update() 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 void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) 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.";
             }
             
@@ -154,15 +190,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 int_fast64_t getIntegerValue(uint_fast64_t variableIndex) const override {
+            virtual double getContinuousValue(std::string const& name) 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(uint_fast64_t variableIndex) const override {
+            virtual int_fast64_t getIntegerValue(std::string const& name) 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 double getContinuousValue(uint_fast64_t variableIndex) const override {
+            virtual bool getBinaryValue(std::string const& name) 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.";
             }
             
@@ -175,7 +211,7 @@ namespace storm {
             }
         };
 #endif
-    
+
     }
 }
 

src/solver/LpSolver.h

@@ -5,34 +5,17 @@
 #include <vector>
 #include <cstdint>
 
+#include "src/storage/expressions/Expression.h"
+
 namespace storm {
     namespace solver {
-
         /*!
          * An interface that captures the functionality of an LP solver.
          */
         class LpSolver {
         public:
-            // An enumeration to represent the possible types of variables. Variables may be either unbounded, have only
-            // a lower or an upper bound, respectively, or be bounded from below and from above.
-            enum VariableType {
-                UNBOUNDED,
-                LOWER_BOUND,
-                UPPER_BOUND,
-                BOUNDED,
-            };
-            
-            // An enumeration to represent the possible types of constraints.
-            enum BoundType {
-                LESS,
-                LESS_EQUAL,
-                GREATER,
-                GREATER_EQUAL,
-                EQUAL
-            };
-            
             // An enumeration to represent whether the objective function is to be minimized or maximized.
-            enum ModelSense {
+            enum class ModelSense {
                 MINIMIZE,
                 MAXIMIZE
             };
@@ -40,7 +23,7 @@ namespace storm {
             /*!
              * Creates an empty LP solver. By default the objective function is assumed to be minimized.
              */
-            LpSolver() : currentModelHasBeenOptimized(false), modelSense(MINIMIZE) {
+            LpSolver() : currentModelHasBeenOptimized(false), modelSense(ModelSense::MINIMIZE) {
                 // Intentionally left empty.
             }
             
@@ -55,52 +38,99 @@ namespace storm {
             }
 
             /*!
-             * Creates a continuous variable, i.e. a variable that may take all real values within its bounds.
+             * Registers an upper- and lower-bounded continuous variable, i.e. a variable that may take all real values
+             * within its bounds.
+             *
+             * @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 void addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
+            
+            /*!
+             * Registers a lower-bounded continuous variable, i.e. a variable that may take all real values up to its
+             * lower bound.
+             *
+             * @param name The name of the variable.
+             * @param lowerBound The lower 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 void addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0;
+
+            /*!
+             * Registers an upper-bounded continuous variable, i.e. a variable that may take all real values up to its
+             * upper bound.
+             *
+             * @param name The name 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 void addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
+            
+            /*!
+             * Registers a unbounded continuous variable, i.e. a variable that may take all real values.
              *
              * @param name The name of the variable.
-             * @param variableType The type of the variable.
-             * @param lowerBound The lower bound of the variable. Note that this parameter is ignored if the variable 
-             * is not bounded from below.
-             * @param upperBound The upper bound of the variable. Note that this parameter is ignored if the variable
-             * is not bounded from above.
              * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective
-             * function. If set to zero, the variable is irrelevant for the objective value.
-             * @return The index of the newly created variable. This index can be used to retrieve the variables value
-             * in a solution after the model has been optimized.
+             * function. If omitted (or set to zero), the variable is irrelevant for the objective value.
              */
-            virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) = 0;
+            virtual void addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0;
             
             /*!
-             * Creates an integer variable.
+             * Registers an upper- and lower-bounded integer variable, i.e. a variable that may take all integer values
+             * within its bounds.
+             *
+             * @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 void addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
+            
+            /*!
+             * Registers a lower-bounded integer variable, i.e. a variable that may take all integer values up to its
+             * lower bound.
+             *
+             * @param name The name of the variable.
+             * @param lowerBound The lower 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 void addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0;
+            
+            /*!
+             * Registers an upper-bounded integer variable, i.e. a variable that may take all integer values up to its
+             * lower bound.
+             *
+             * @param name The name 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 void addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
+
+            /*!
+             * Registers an unbounded integer variable, i.e. a variable that may take all integer values.
              *
              * @param name The name of the variable.
-             * @param variableType The type of the variable.
-             * @param lowerBound The lower bound of the variable. Note that this parameter is ignored if the variable
-             * is not bounded from below.
-             * @param upperBound The upper bound of the variable. Note that this parameter is ignored if the variable
-             * is not bounded from above.
              * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective
-             * function. If set to zero, the variable is irrelevant for the objective value.
-             * @return The index of the newly created variable. This index can be used to retrieve the variables value
-             * in a solution after the model has been optimized.
+             * function. If omitted (or set to zero), the variable is irrelevant for the objective value.
              */
-            virtual uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) = 0;
+            virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0;
             
             /*!
-             * Creates a binary variable, i.e. a variable that may be either zero or one.
+             * Registers a boolean variable, i.e. a variable that may be either 0 or 1.
              *
              * @param name The name of the variable.
-             * @param variableType The type of the variable.
-             * @param lowerBound The lower bound of the variable. Note that this parameter is ignored if the variable
-             * is not bounded from below.
-             * @param upperBound The upper bound of the variable. Note that this parameter is ignored if the variable
-             * is not bounded from above.
              * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective
-             * function. If set to zero, the variable is irrelevant for the objective value.
-             * @return The index of the newly created variable. This index can be used to retrieve the variables value
-             * in a solution after the model has been optimized.
+             * function. If omitted (or set to zero), the variable is irrelevant for the objective value.
              */
-            virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) = 0;
+            virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) = 0;
             
             /*!
              * Updates the model to make the variables that have been declared since the last call to <code>update</code>
@@ -109,18 +139,13 @@ namespace storm {
             virtual void update() const = 0;
             
             /*!
-             * Adds a constraint of the form
-             *      a_1*x_1 + ... + a_n*x_n  op  c
-             * to the LP problem.
+             * Adds a the given constraint to the LP problem.
              *
              * @param name The name of the constraint. If empty, the constraint has no name.
-             * @param variables A vector of variable indices that define the appearing variables x_1, ..., x_n.
-             * @param coefficients A vector of coefficients that define the a_1, ..., a_n. The i-ith entry specifies the
-             * coefficient of the variable whose index appears at the i-th position in the vector of variable indices.
-             * @param boundType The bound type specifies the operator op used in the constraint.
-             * @param rhs This defines the value of the constant appearing on the right-hand side of the constraint.
+             * @param constraint An expression that represents the constraint. The given constraint must be a linear
+             * (in)equality over the registered variables.
              */
-            virtual void addConstraint(std::string const& name, std::vector<uint_fast64_t> const& variables, std::vector<double> const& coefficients, BoundType const& boundType, double rhs) = 0;
+            virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) = 0;
             
             /*!
              * Optimizes the LP problem previously constructed. Afterwards, the methods isInfeasible, isUnbounded and
@@ -154,34 +179,31 @@ namespace storm {
             virtual bool isOptimal() const = 0;
             
             /*!
-             * Retrieves the value of the integer variable with the given index. Note that this may only be called, if
+             * Retrieves the value of the integer variable with the given name. Note that this may only be called, if
              * the model was found to be optimal, i.e. iff isOptimal() returns true.
              *
-             * @param variableIndex The index of the integer variable whose value to query. If this index does not
-             * belong to a previously declared integer variable, the behaviour is undefined.
+             * @param name The name of the variable whose integer value (in the optimal solution) to retrieve.
              * @return The value of the integer variable in the optimal solution.
              */
-            virtual int_fast64_t getIntegerValue(uint_fast64_t variableIndex) const = 0;
+            virtual int_fast64_t getIntegerValue(std::string const& name) const = 0;
             
             /*!
-             * Retrieves the value of the binary variable with the given index. Note that this may only be called, if
+             * Retrieves the value of the binary variable with the given name. Note that this may only be called, if
              * the model was found to be optimal, i.e. iff isOptimal() returns true.
              *
-             * @param variableIndex The index of the binary variable whose value to query. If this index does not
-             * belong to a previously declared binary variable, the behaviour is undefined.
+             * @param name The name of the variable whose binary (boolean) value (in the optimal solution) to retrieve.
              * @return The value of the binary variable in the optimal solution.
              */
-            virtual bool getBinaryValue(uint_fast64_t variableIndex) const = 0;
+            virtual bool getBinaryValue(std::string const& name) const = 0;
             
             /*!
-             * Retrieves the value of the continuous variable with the given index. Note that this may only be called,
+             * Retrieves the value of the continuous variable with the given name. Note that this may only be called,
              * if the model was found to be optimal, i.e. iff isOptimal() returns true.
              *
-             * @param variableIndex The index of the continuous variable whose value to query. If this index does not
-             * belong to a previously declared continuous variable, the behaviour is undefined.
+             * @param name The name of the variable whose continuous value (in the optimal solution) to retrieve.
              * @return The value of the continuous variable in the optimal solution.
              */
-            virtual double getContinuousValue(uint_fast64_t variableIndex) const = 0;
+            virtual double getContinuousValue(std::string const& name) const = 0;
 
             /*!
              * Retrieves the value of the objective function. Note that this may only be called, if the model was found

src/storage/expressions/Expression.cpp

@@ -95,6 +95,16 @@ namespace storm {
             return this->getBaseExpression().isFalse();
         }
         
+        bool Expression::isRelationalExpression() const {
+            if (!this->isFunctionApplication()) {
+                return false;
+            }
+            
+            return this->getOperator() == OperatorType::Equal || this->getOperator() == OperatorType::NotEqual
+            || this->getOperator() == OperatorType::Less || this->getOperator() == OperatorType::LessOrEqual
+            || this->getOperator() == OperatorType::Greater || this->getOperator() == OperatorType::GreaterOrEqual;
+        }
+        
         std::set<std::string> Expression::getVariables() const {
             return this->getBaseExpression().getVariables();
         }

src/storage/expressions/Expression.h

@@ -230,6 +230,14 @@ namespace storm {
              */
             bool isFalse() const;
             
+            /*!
+             * Retrieves whether this expression is a relation expression, i.e., an expression that has a relation
+             * (equal, not equal, less, less or equal, etc.) as its top-level operator.
+             *
+             * @return True iff the expression is a relation expression.
+             */
+            bool isRelationalExpression() const;
+            
             /*!
              * Retrieves the set of all variables that appear in the expression.
              *

src/storage/expressions/LinearityCheckVisitor.cpp

@@ -0,0 +1,78 @@
+#include "src/storage/expressions/LinearityCheckVisitor.h"
+#include "src/storage/expressions/Expressions.h"
+
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/InvalidTypeException.h"
+
+namespace storm {
+    namespace expressions {
+        bool LinearityCheckVisitor::check(BaseExpression const* expression) {
+            expression->accept(this);
+            return resultStack.top();
+        }
+        
+        void LinearityCheckVisitor::visit(IfThenElseExpression const* expression) {
+            // An if-then-else expression is never linear.
+            resultStack.push(false);
+        }
+        
+        void LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const* expression) {
+            // Boolean function applications are not allowed in linear expressions.
+            resultStack.push(false);
+        }
+        
+        void LinearityCheckVisitor::visit(BinaryNumericalFunctionExpression const* expression) {
+            bool leftResult = true;
+            bool rightResult = true;
+            switch (expression->getOperatorType()) {
+                case BinaryNumericalFunctionExpression::OperatorType::Plus:
+                case BinaryNumericalFunctionExpression::OperatorType::Minus:
+                    expression->getFirstOperand()->accept(this);
+                    leftResult = resultStack.top();
+                    
+                    if (!leftResult) {
+                        
+                    } else {
+                        resultStack.pop();
+
+                        expression->getSecondOperand()->accept(this);
+                    }
+
+                case BinaryNumericalFunctionExpression::OperatorType::Times:
+                case BinaryNumericalFunctionExpression::OperatorType::Divide:
+                case BinaryNumericalFunctionExpression::OperatorType::Min: resultStack.push(false); break;
+                case BinaryNumericalFunctionExpression::OperatorType::Max: resultStack.push(false); break;
+            }
+        }
+        
+        void LinearityCheckVisitor::visit(BinaryRelationExpression const* expression) {
+            resultStack.push(false);
+        }
+        
+        void LinearityCheckVisitor::visit(VariableExpression const* expression) {
+            resultStack.push(true);
+        }
+        
+        void LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const* expression) {
+            // Boolean function applications are not allowed in linear expressions.
+            resultStack.push(false);
+        }
+        
+        void LinearityCheckVisitor::visit(UnaryNumericalFunctionExpression const* expression) {
+            // Intentionally left empty (just pass subresult one level further).
+        }
+        
+        void LinearityCheckVisitor::visit(BooleanLiteralExpression const* expression) {
+            // Boolean function applications are not allowed in linear expressions.
+            resultStack.push(false);
+        }
+        
+        void LinearityCheckVisitor::visit(IntegerLiteralExpression const* expression) {
+            resultStack.push(true);
+        }
+        
+        void LinearityCheckVisitor::visit(DoubleLiteralExpression const* expression) {
+            resultStack.push(true);
+        }
+    }
+}

src/storage/expressions/LinearityCheckVisitor.h

@@ -0,0 +1,41 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_LINEARITYCHECKVISITOR_H_
+#define STORM_STORAGE_EXPRESSIONS_LINEARITYCHECKVISITOR_H_
+
+#include <stack>
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/ExpressionVisitor.h"
+
+namespace storm {
+    namespace expressions {
+        class LinearityCheckVisitor : public ExpressionVisitor {
+        public:
+            /*!
+             * Creates a linearity check visitor.
+             */
+            LinearityCheckVisitor() = default;
+            
+            /*!
+             * Checks that the given expression is linear.
+             */
+            bool check(BaseExpression const* expression);
+            
+            virtual void visit(IfThenElseExpression const* expression) override;
+            virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BinaryRelationExpression const* expression) override;
+            virtual void visit(VariableExpression const* expression) override;
+            virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(UnaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BooleanLiteralExpression const* expression) override;
+            virtual void visit(IntegerLiteralExpression const* expression) override;
+            virtual void visit(DoubleLiteralExpression const* expression) override;
+            
+        private:
+            // A stack for communicating the results of the subexpressions.
+            std::stack<bool> resultStack;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_LINEARITYCHECKVISITOR_H_ */