Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LpSolver.h
Go to the documentation of this file.
1#pragma once
2
3#include <cstdint>
4#include <memory>
5#include <optional>
6#include <string>
7#include <vector>
9
10namespace storm {
11namespace expressions {
13class Variable;
14class Expression;
15enum class RelationType;
16} // namespace expressions
17
18namespace solver {
19
20template<typename ValueType>
22 using VariableIndexType = uint64_t;
23
30 RawLpConstraint(storm::expressions::RelationType relationType, ValueType const& rhs = {}, uint64_t reservedSize = 0);
31
37 void addToLhs(VariableIndexType const& variable, ValueType const& coefficient);
38
39 std::vector<VariableIndexType> lhsVariableIndices;
40 std::vector<ValueType> lhsCoefficients;
42 ValueType rhs;
43};
44
49template<typename ValueType, bool RawMode = false>
50class LpSolver {
51 public:
52 using Variable = std::conditional_t<RawMode, typename RawLpConstraint<ValueType>::VariableIndexType, storm::expressions::Variable>;
53 using Constant = std::conditional_t<RawMode, ValueType, storm::expressions::Expression>;
54 using Constraint = std::conditional_t<RawMode, RawLpConstraint<ValueType>, storm::expressions::Expression>;
55
60
64 LpSolver();
71 LpSolver(OptimizationDirection const& optDir);
72
73 virtual ~LpSolver() = default;
74
87 Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0);
88
100 Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0);
101
113 Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0);
114
124 Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0);
125
137 Variable addContinuousVariable(std::string const& name, std::optional<ValueType> const& lowerBound = std::nullopt,
138 std::optional<ValueType> const& upperBound = std::nullopt, ValueType objectiveFunctionCoefficient = 0);
139
152 Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0);
153
165 Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0);
166
178 Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0);
179
189 Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0);
190
202 Variable addIntegerVariable(std::string const& name, std::optional<ValueType> const& lowerBound = std::nullopt,
203 std::optional<ValueType> const& upperBound = std::nullopt, ValueType objectiveFunctionCoefficient = 0);
204
214 Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0);
215
228 virtual Variable addVariable(std::string const& name, VariableType const& type, std::optional<ValueType> const& lowerBound = std::nullopt,
229 std::optional<ValueType> const& upperBound = std::nullopt, ValueType objectiveFunctionCoefficient = 0) = 0;
230
238 Constant getConstant(ValueType value) const;
239
244 virtual void update() const = 0;
245
253 virtual void addConstraint(std::string const& name, Constraint const& constraint) = 0;
254
265 virtual void addIndicatorConstraint(std::string const& name, Variable indicatorVariable, bool indicatorValue, Constraint const& constraint) = 0;
266
271 virtual void optimize() const = 0;
272
279 virtual bool isInfeasible() const = 0;
280
287 virtual bool isUnbounded() const = 0;
288
296 virtual bool isOptimal() const = 0;
297
305 virtual int_fast64_t getIntegerValue(Variable const& variable) const = 0;
306
314 virtual bool getBinaryValue(Variable const& variable) const = 0;
315
323 virtual ValueType getContinuousValue(Variable const& variable) const = 0;
324
331 virtual ValueType getObjectiveValue() const = 0;
332
338 virtual void writeModelToFile(std::string const& filename) const = 0;
339
345 void setOptimizationDirection(OptimizationDirection const& optimizationDirection);
346
353
360
365 virtual void push() = 0;
366
371 virtual void pop() = 0;
372
379 virtual void setMaximalMILPGap(ValueType const& gap, bool relative) = 0;
380
384 virtual ValueType getMILPGap(bool relative) const = 0;
385
386 protected:
388
389 // The manager responsible for the variables.
390 std::shared_ptr<storm::expressions::ExpressionManager> manager;
391
392 // A flag indicating whether the current model has been optimized and not changed afterwards.
394
395 private:
396 // A flag that indicates the model sense.
397 OptimizationDirection optimizationDirection;
398};
399} // namespace solver
400} // namespace storm
This class is responsible for managing a set of typed variables and all expressions using these varia...
Variable addUnboundedIntegerVariable(std::string const &name, ValueType objectiveFunctionCoefficient=0)
Registers an unbounded integer variable, i.e.
Definition LpSolver.cpp:89
virtual void setMaximalMILPGap(ValueType const &gap, bool relative)=0
Specifies the maximum difference between lower- and upper objective bounds that triggers termination.
OptimizationDirection getOptimizationDirection() const
Retrieves whether the objective function of this model is to be minimized or maximized.
Definition LpSolver.cpp:125
virtual bool getBinaryValue(Variable const &variable) const =0
Retrieves the value of the binary variable with the given name.
Variable addIntegerVariable(std::string const &name, std::optional< ValueType > const &lowerBound=std::nullopt, std::optional< ValueType > const &upperBound=std::nullopt, ValueType objectiveFunctionCoefficient=0)
Registers an integer variable, i.e.
Definition LpSolver.cpp:95
Variable addContinuousVariable(std::string const &name, std::optional< ValueType > const &lowerBound=std::nullopt, std::optional< ValueType > const &upperBound=std::nullopt, ValueType objectiveFunctionCoefficient=0)
Registers a continuous variable, i.e.
Definition LpSolver.cpp:62
virtual void update() const =0
Updates the model to make the variables that have been declared since the last call to update usable.
virtual void addConstraint(std::string const &name, Constraint const &constraint)=0
Adds a the given constraint to the LP problem.
virtual Variable addVariable(std::string const &name, VariableType const &type, std::optional< ValueType > const &lowerBound=std::nullopt, std::optional< ValueType > const &upperBound=std::nullopt, ValueType objectiveFunctionCoefficient=0)=0
Registers a variable of the given type.
virtual void writeModelToFile(std::string const &filename) const =0
Writes the current LP problem to the given file.
virtual void pop()=0
Pops a backtracking point from the solver's stack.
Variable addUpperBoundedIntegerVariable(std::string const &name, ValueType upperBound, ValueType objectiveFunctionCoefficient=0)
Registers an upper-bounded integer variable, i.e.
Definition LpSolver.cpp:83
virtual ValueType getMILPGap(bool relative) const =0
Returns the obtained gap after a call to optimize().
storm::expressions::Variable declareOrGetExpressionVariable(std::string const &name, VariableType const &type)
Definition LpSolver.cpp:136
Variable addBoundedIntegerVariable(std::string const &name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient=0)
Registers an upper- and lower-bounded integer variable, i.e.
Definition LpSolver.cpp:70
storm::expressions::ExpressionManager const & getManager() const
Retrieves the manager for the variables created for this solver.
Definition LpSolver.cpp:130
virtual void push()=0
Pushes a backtracking point on the solver's stack.
void setOptimizationDirection(OptimizationDirection const &optimizationDirection)
Sets whether the objective function of this model is to be minimized or maximized.
Definition LpSolver.cpp:117
LpSolver()
Creates an empty LP solver.
Definition LpSolver.cpp:25
std::conditional_t< RawMode, RawLpConstraint< ValueType >, storm::expressions::Expression > Constraint
Definition LpSolver.h:54
std::conditional_t< RawMode, ValueType, storm::expressions::Expression > Constant
Definition LpSolver.h:53
Variable addLowerBoundedContinuousVariable(std::string const &name, ValueType lowerBound, ValueType objectiveFunctionCoefficient=0)
Registers a lower-bounded continuous variable, i.e.
Definition LpSolver.cpp:44
virtual int_fast64_t getIntegerValue(Variable const &variable) const =0
Retrieves the value of the integer variable with the given name.
std::conditional_t< RawMode, typename RawLpConstraint< ValueType >::VariableIndexType, storm::expressions::Variable > Variable
Definition LpSolver.h:52
Constant getConstant(ValueType value) const
Retrieves an expression that characterizes the given constant value.
Definition LpSolver.cpp:108
std::shared_ptr< storm::expressions::ExpressionManager > manager
Definition LpSolver.h:390
virtual bool isInfeasible() const =0
Retrieves whether the model was found to be infeasible.
virtual void addIndicatorConstraint(std::string const &name, Variable indicatorVariable, bool indicatorValue, Constraint const &constraint)=0
Adds the given indicator constraint to the LP problem: "If indicatorVariable == indicatorValue,...
Variable addLowerBoundedIntegerVariable(std::string const &name, ValueType lowerBound, ValueType objectiveFunctionCoefficient=0)
Registers a lower-bounded integer variable, i.e.
Definition LpSolver.cpp:77
virtual bool isUnbounded() const =0
Retrieves whether the model was found to be infeasible.
Variable addBoundedContinuousVariable(std::string const &name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient=0)
Registers an upper- and lower-bounded continuous variable, i.e.
Definition LpSolver.cpp:37
virtual ValueType getContinuousValue(Variable const &variable) const =0
Retrieves the value of the continuous variable with the given name.
virtual ~LpSolver()=default
VariableType
Enumerates the different types of variables.
Definition LpSolver.h:59
virtual void optimize() const =0
Optimizes the LP problem previously constructed.
Variable addUnboundedContinuousVariable(std::string const &name, ValueType objectiveFunctionCoefficient=0)
Registers a unbounded continuous variable, i.e.
Definition LpSolver.cpp:56
virtual ValueType getObjectiveValue() const =0
Retrieves the value of the objective function.
Variable addUpperBoundedContinuousVariable(std::string const &name, ValueType upperBound, ValueType objectiveFunctionCoefficient=0)
Registers an upper-bounded continuous variable, i.e.
Definition LpSolver.cpp:50
Variable addBinaryVariable(std::string const &name, ValueType objectiveFunctionCoefficient=0)
Registers a boolean variable, i.e.
Definition LpSolver.cpp:102
virtual bool isOptimal() const =0
Retrieves whether the model was found to be optimal, i.e.
RelationType
An enum type specifying the different relations applicable.
std::vector< VariableIndexType > lhsVariableIndices
Definition LpSolver.h:39
void addToLhs(VariableIndexType const &variable, ValueType const &coefficient)
Adds the summand 'coefficient * variable' to the left hand side.
Definition LpSolver.cpp:19
RawLpConstraint(storm::expressions::RelationType relationType, ValueType const &rhs={}, uint64_t reservedSize=0)
Creates a RawLpConstraint which represents a linear (in)equality of the form a_1*x_1 + ....
Definition LpSolver.cpp:12
storm::expressions::RelationType relationType
Definition LpSolver.h:41
std::vector< ValueType > lhsCoefficients
Definition LpSolver.h:40