From 3158d19123def9d2ba29374a9a8aadebcea5093f Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 7 May 2014 18:27:44 +0200 Subject: [PATCH] Started working on adapting LP solver interface to new expressions. Former-commit-id: 6131736a7fe0e9411a2cef385722d0619e63105c --- src/solver/GlpkLpSolver.cpp | 262 ++++++++++-------- src/solver/GlpkLpSolver.h | 81 ++++-- src/solver/GurobiLpSolver.h | 80 ++++-- src/solver/LpSolver.h | 166 ++++++----- src/storage/expressions/Expression.cpp | 10 + src/storage/expressions/Expression.h | 8 + .../expressions/LinearityCheckVisitor.cpp | 78 ++++++ .../expressions/LinearityCheckVisitor.h | 41 +++ 8 files changed, 493 insertions(+), 233 deletions(-) create mode 100644 src/storage/expressions/LinearityCheckVisitor.cpp create mode 100644 src/storage/expressions/LinearityCheckVisitor.h diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index e122fcb16..fc2c5f261 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -4,13 +4,10 @@ #include -#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 const& variables, std::vector 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(variableIndex)); + value = glp_mip_col_val(this->lp, static_cast(variableIndexPair->second)); } else { - value = glp_get_col_prim(this->lp, static_cast(variableIndex)); - } - - if (std::abs(value - static_cast(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(variableIndexPair->second)); } - - return static_cast(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(variableIndex)); + value = glp_mip_col_val(this->lp, static_cast(variableIndexPair->second)); } else { - value = glp_get_col_prim(this->lp, static_cast(variableIndex)); + value = glp_get_col_prim(this->lp, static_cast(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(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(value); + return static_cast(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(variableIndex)); + value = glp_mip_col_val(this->lp, static_cast(variableIndexPair->second)); } else { - value = glp_get_col_prim(this->lp, static_cast(variableIndex)); + value = glp_get_col_prim(this->lp, static_cast(variableIndexPair->second)); } - return value; + + LOG_THROW(std::abs(static_cast(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(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; diff --git a/src/solver/GlpkLpSolver.h b/src/solver/GlpkLpSolver.h index 2bc2bf397..0045ced73 100644 --- a/src/solver/GlpkLpSolver.h +++ b/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 const& variables, std::vector 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 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 const& variables, std::vector 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."; } diff --git a/src/solver/GurobiLpSolver.h b/src/solver/GurobiLpSolver.h index 18c5bbdbd..27ac66c52 100644 --- a/src/solver/GurobiLpSolver.h +++ b/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 const& variables, std::vector 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 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 const& variables, std::vector 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 - + } } diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index 311ee4b44..f775f2829 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -5,34 +5,17 @@ #include #include +#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 update @@ -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 const& variables, std::vector 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 diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index e30b53927..169578c34 100644 --- a/src/storage/expressions/Expression.cpp +++ b/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 Expression::getVariables() const { return this->getBaseExpression().getVariables(); } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 0c55408dc..81ae5cf54 100644 --- a/src/storage/expressions/Expression.h +++ b/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. * diff --git a/src/storage/expressions/LinearityCheckVisitor.cpp b/src/storage/expressions/LinearityCheckVisitor.cpp new file mode 100644 index 000000000..d4086abf1 --- /dev/null +++ b/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); + } + } +} \ No newline at end of file diff --git a/src/storage/expressions/LinearityCheckVisitor.h b/src/storage/expressions/LinearityCheckVisitor.h new file mode 100644 index 000000000..2b1c3937c --- /dev/null +++ b/src/storage/expressions/LinearityCheckVisitor.h @@ -0,0 +1,41 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_LINEARITYCHECKVISITOR_H_ +#define STORM_STORAGE_EXPRESSIONS_LINEARITYCHECKVISITOR_H_ + +#include + +#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 resultStack; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_LINEARITYCHECKVISITOR_H_ */ \ No newline at end of file