Browse Source

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: badef77583
tempestpy_adaptions
sjunges 9 years ago
parent
commit
92082dc970
  1. 2
      src/models/sparse/StateLabeling.cpp
  2. 1
      src/settings/Argument.h
  3. 1
      src/settings/ArgumentBase.cpp
  4. 2
      src/settings/ArgumentType.h
  5. 1
      src/settings/SettingMemento.h
  6. 1
      src/settings/modules/ModuleSettings.cpp
  7. 1
      src/settings/modules/ModuleSettings.h
  8. 2
      src/solver/GmmxxMinMaxLinearEquationSolver.h
  9. 107
      src/solver/GurobiLpSolver.cpp
  10. 108
      src/solver/GurobiLpSolver.h
  11. 1
      src/solver/LpSolver.h
  12. 1
      src/solver/NativeMinMaxLinearEquationSolver.h
  13. 2
      test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp

2
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"

1
src/settings/Argument.h

@ -11,6 +11,7 @@
#include <vector>
#include <memory>
#include "src/utility/macros.h"
#include "src/settings/ArgumentBase.h"
#include "src/settings/ArgumentType.h"

1
src/settings/ArgumentBase.cpp

@ -2,6 +2,7 @@
#include <boost/algorithm/string.hpp>
#include <iomanip>
#include <sstream>
namespace storm {
namespace settings {

2
src/settings/ArgumentType.h

@ -3,8 +3,6 @@
#include <iostream>
#include "src/utility/macros.h"
namespace storm {
namespace settings {

1
src/settings/SettingMemento.h

@ -2,6 +2,7 @@
#define STORM_SETTINGS_SETTINGMEMENTO_H_
#include <string>
#include <memory>
namespace storm {

1
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"

1
src/settings/modules/ModuleSettings.h

@ -4,6 +4,7 @@
#include <string>
#include <unordered_map>
#include <vector>
#include <memory>
namespace storm {

2
src/solver/GmmxxMinMaxLinearEquationSolver.h

@ -2,7 +2,7 @@
#define STORM_SOLVER_GMMXXMINMAXLINEAREQUATIONSOLVER_H_
#include "gmm/gmm_matrix.h"
#include <memory>
#include "src/solver/MinMaxLinearEquationSolver.h"
namespace storm {

107
src/solver/GurobiLpSolver.cpp

@ -1,6 +1,5 @@
#include "src/solver/GurobiLpSolver.h"
#ifdef STORM_HAVE_GUROBI
#include <numeric>
#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

108
src/solver/GurobiLpSolver.h

@ -3,11 +3,10 @@
#include <map>
#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<storm::expressions::Variable, int> variableToIndexMap;
};
#else
// If Gurobi is not available, we provide a stub implementation that emits an error if any of its methods is called.
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
}
}

1
src/solver/LpSolver.h

@ -4,6 +4,7 @@
#include <string>
#include <vector>
#include <cstdint>
#include <memory>
namespace storm {
namespace expressions {
class ExpressionManager;

1
src/solver/NativeMinMaxLinearEquationSolver.h

@ -1,6 +1,7 @@
#ifndef STORM_SOLVER_NATIVEMINMAXLINEAREQUATIONSOLVER_H_
#define STORM_SOLVER_NATIVEMINMAXLINEAREQUATIONSOLVER_H_
#include <cstdint>
#include "src/solver/MinMaxLinearEquationSolver.h"
namespace storm {

2
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"

Loading…
Cancel
Save