From 92082dc970d69fd1737368a629f28732140c9b43 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 17 Aug 2015 16:22:09 +0200 Subject: [PATCH] gurobi lp solver refactored in case gurobi is not found, and fixes for linux - sorry about earlier lack of checks on linux Former-commit-id: badef7758302fb2d577803e4f059c9f62ae90b95 --- src/models/sparse/StateLabeling.cpp | 2 +- src/settings/Argument.h | 1 + src/settings/ArgumentBase.cpp | 1 + src/settings/ArgumentType.h | 2 - src/settings/SettingMemento.h | 1 + src/settings/modules/ModuleSettings.cpp | 1 + src/settings/modules/ModuleSettings.h | 1 + src/solver/GmmxxMinMaxLinearEquationSolver.h | 2 +- src/solver/GurobiLpSolver.cpp | 107 ++++++++++++++++- src/solver/GurobiLpSolver.h | 108 +----------------- src/solver/LpSolver.h | 1 + src/solver/NativeMinMaxLinearEquationSolver.h | 1 + .../NativeDtmcPrctlModelCheckerTest.cpp | 2 + 13 files changed, 120 insertions(+), 110 deletions(-) diff --git a/src/models/sparse/StateLabeling.cpp b/src/models/sparse/StateLabeling.cpp index 3f1504496..7957e6a99 100644 --- a/src/models/sparse/StateLabeling.cpp +++ b/src/models/sparse/StateLabeling.cpp @@ -1,5 +1,5 @@ #include "src/models/sparse/StateLabeling.h" -#include "src/storage/BitVector.h" + #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/InvalidArgumentException.h" diff --git a/src/settings/Argument.h b/src/settings/Argument.h index e50b25dfc..089c47d1b 100644 --- a/src/settings/Argument.h +++ b/src/settings/Argument.h @@ -11,6 +11,7 @@ #include #include +#include "src/utility/macros.h" #include "src/settings/ArgumentBase.h" #include "src/settings/ArgumentType.h" diff --git a/src/settings/ArgumentBase.cpp b/src/settings/ArgumentBase.cpp index f307e1f93..0267b9b8d 100644 --- a/src/settings/ArgumentBase.cpp +++ b/src/settings/ArgumentBase.cpp @@ -2,6 +2,7 @@ #include #include +#include namespace storm { namespace settings { diff --git a/src/settings/ArgumentType.h b/src/settings/ArgumentType.h index a1424ac73..261b79b34 100644 --- a/src/settings/ArgumentType.h +++ b/src/settings/ArgumentType.h @@ -3,8 +3,6 @@ #include -#include "src/utility/macros.h" - namespace storm { namespace settings { diff --git a/src/settings/SettingMemento.h b/src/settings/SettingMemento.h index bfbbcf9c3..3bbad196f 100644 --- a/src/settings/SettingMemento.h +++ b/src/settings/SettingMemento.h @@ -2,6 +2,7 @@ #define STORM_SETTINGS_SETTINGMEMENTO_H_ #include +#include namespace storm { diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp index befea1589..f4ccbc2b6 100644 --- a/src/settings/modules/ModuleSettings.cpp +++ b/src/settings/modules/ModuleSettings.cpp @@ -1,5 +1,6 @@ #include "src/settings/modules/ModuleSettings.h" +#include "src/utility/macros.h" #include "src/settings/SettingMemento.h" #include "src/settings/Option.h" #include "src/exceptions/InvalidStateException.h" diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h index 89776ce46..d4cf18724 100644 --- a/src/settings/modules/ModuleSettings.h +++ b/src/settings/modules/ModuleSettings.h @@ -4,6 +4,7 @@ #include #include #include +#include namespace storm { diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.h b/src/solver/GmmxxMinMaxLinearEquationSolver.h index a6bdb8281..4d151d706 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.h +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.h @@ -2,7 +2,7 @@ #define STORM_SOLVER_GMMXXMINMAXLINEAREQUATIONSOLVER_H_ #include "gmm/gmm_matrix.h" - +#include #include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp index bb1a070fb..c8f97febf 100644 --- a/src/solver/GurobiLpSolver.cpp +++ b/src/solver/GurobiLpSolver.cpp @@ -1,6 +1,5 @@ #include "src/solver/GurobiLpSolver.h" -#ifdef STORM_HAVE_GUROBI #include #include "src/storage/expressions/LinearCoefficientVisitor.h" @@ -16,10 +15,13 @@ #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidAccessException.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/NotImplementedException.h" + namespace storm { namespace solver { +#ifdef STORM_HAVE_GUROBI GurobiLpSolver::GurobiLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), env(nullptr), model(nullptr), nextVariableIndex(0) { // Create the environment. int error = GRBloadenv(&env, ""); @@ -350,7 +352,108 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Unable to write Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ") to file."; } } +#else + GurobiLpSolver::GurobiLpSolver(std::string const& name, ModelSense const& modelSense) { + 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."; + } + + GurobiLpSolver::GurobiLpSolver(std::string const& name) { + 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."; + } + + GurobiLpSolver::GurobiLpSolver(ModelSense const& modelSense) { + 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."; + } + + GurobiLpSolver::GurobiLpSolver() { + 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."; + } + + GurobiLpSolver::~GurobiLpSolver() { + + } + + storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient ) { + 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."; + } + + storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient ) { + 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."; } + + storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient ) { + 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."; + } + + storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient ) { + 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."; + } + + storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient ) { + 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."; + } + + storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient ) { + 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."; + } + + storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient ) { + 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."; + } + + storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient ) { + 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."; + } + + storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient ) { + 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."; + } + + void GurobiLpSolver::update() const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + void GurobiLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + 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."; + } + + void GurobiLpSolver::optimize() const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + bool GurobiLpSolver::isInfeasible() const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + bool GurobiLpSolver::isUnbounded() const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + bool GurobiLpSolver::isOptimal() const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + double GurobiLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + double GurobiLpSolver::getObjectiveValue() const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + void GurobiLpSolver::writeModelToFile(std::string const& filename) const { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + +#endif } } -#endif \ No newline at end of file diff --git a/src/solver/GurobiLpSolver.h b/src/solver/GurobiLpSolver.h index 186715922..d060036c8 100644 --- a/src/solver/GurobiLpSolver.h +++ b/src/solver/GurobiLpSolver.h @@ -3,11 +3,10 @@ #include #include "src/solver/LpSolver.h" -#include "src/exceptions/NotImplementedException.h" - // To detect whether the usage of Gurobi is possible, this include is neccessary. #include "storm-config.h" + #ifdef STORM_HAVE_GUROBI extern "C" { #include "gurobi_c.h" @@ -16,10 +15,10 @@ extern "C" { } #endif + namespace storm { namespace solver { -#ifdef STORM_HAVE_GUROBI /*! * A class that implements the LpSolver interface using Gurobi. */ @@ -113,12 +112,13 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient of the variable in the objective function. */ void addVariable(storm::expressions::Variable const& variable, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient); - +#ifdef STORM_HAVE_GUROBI // The Gurobi environment. GRBenv* env; // The Gurobi model. GRBmodel* model; +#endif // The index of the next variable. int nextVariableIndex; @@ -126,106 +126,6 @@ namespace storm { // A mapping from variables to their indices. std::map variableToIndexMap; }; -#else - // If Gurobi is not available, we provide a stub implementation that emits an error if any of its methods is called. - class GurobiLpSolver : public LpSolver { - public: - GurobiLpSolver(std::string const& name, ModelSense const& modelSense) { - 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."; - } - - GurobiLpSolver(std::string const& name) { - 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."; - } - - GurobiLpSolver(ModelSense const& modelSense) { - 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."; - } - - GurobiLpSolver() { - 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 storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } - - virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - 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."; - } - - virtual void optimize() 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 isInfeasible() 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 isUnbounded() 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 isOptimal() 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(storm::expressions::Variable const& variable) const override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual bool getBinaryValue(storm::expressions::Variable const& variable) const override { - throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - virtual double getObjectiveValue() 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 writeModelToFile(std::string const& filename) 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."; - } - }; -#endif } } diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index 2ea06af2c..816b0f097 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -4,6 +4,7 @@ #include #include #include +#include namespace storm { namespace expressions { class ExpressionManager; diff --git a/src/solver/NativeMinMaxLinearEquationSolver.h b/src/solver/NativeMinMaxLinearEquationSolver.h index 682f79cca..c3fa66b35 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.h +++ b/src/solver/NativeMinMaxLinearEquationSolver.h @@ -1,6 +1,7 @@ #ifndef STORM_SOLVER_NATIVEMINMAXLINEAREQUATIONSOLVER_H_ #define STORM_SOLVER_NATIVEMINMAXLINEAREQUATIONSOLVER_H_ +#include #include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index f58b4259e..ced23c35e 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -7,6 +7,8 @@ #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" + +#include "src/settings/modules/GeneralSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h"