Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LpSolver.cpp
Go to the documentation of this file.
1#include "storm/solver/LpSolver.h"
2
3#include "storm/adapters/RationalNumberAdapter.h"
4#include "storm/storage/expressions/Expression.h"
5#include "storm/storage/expressions/ExpressionManager.h"
6#include "storm/utility/macros.h"
7
8namespace storm {
9namespace solver {
10
11template<typename ValueType>
12RawLpConstraint<ValueType>::RawLpConstraint(storm::expressions::RelationType relationType, ValueType const& rhs, uint64_t reservedSize)
13 : relationType(relationType), rhs(rhs) {
14 lhsCoefficients.reserve(reservedSize);
15 lhsVariableIndices.reserve(reservedSize);
16}
17
18template<typename ValueType>
19void RawLpConstraint<ValueType>::addToLhs(VariableIndexType const& variable, ValueType const& coefficient) {
20 lhsCoefficients.push_back(coefficient);
21 lhsVariableIndices.push_back(variable);
22}
23
24template<typename ValueType, bool RawMode>
25LpSolver<ValueType, RawMode>::LpSolver()
26 : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(OptimizationDirection::Minimize) {
27 // Intentionally left empty.
28}
29
30template<typename ValueType, bool RawMode>
31LpSolver<ValueType, RawMode>::LpSolver(OptimizationDirection const& optimizationDir)
32 : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(optimizationDir) {
33 // Intentionally left empty.
34}
35
36template<typename ValueType, bool RawMode>
37typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound,
38 ValueType upperBound,
39 ValueType objectiveFunctionCoefficient) {
40 return addVariable(name, VariableType::Continuous, lowerBound, upperBound, objectiveFunctionCoefficient);
41}
42
43template<typename ValueType, bool RawMode>
44typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound,
45 ValueType objectiveFunctionCoefficient) {
46 return addVariable(name, VariableType::Continuous, lowerBound, std::nullopt, objectiveFunctionCoefficient);
47}
48
49template<typename ValueType, bool RawMode>
50typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound,
51 ValueType objectiveFunctionCoefficient) {
52 return addVariable(name, VariableType::Continuous, std::nullopt, upperBound, objectiveFunctionCoefficient);
53}
54
55template<typename ValueType, bool RawMode>
56typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addUnboundedContinuousVariable(std::string const& name,
57 ValueType objectiveFunctionCoefficient) {
58 return addVariable(name, VariableType::Continuous, std::nullopt, std::nullopt, objectiveFunctionCoefficient);
59}
60
61template<typename ValueType, bool RawMode>
62typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addContinuousVariable(std::string const& name,
63 std::optional<ValueType> const& lowerBound,
64 std::optional<ValueType> const& upperBound,
65 ValueType objectiveFunctionCoefficient) {
66 return addVariable(name, VariableType::Continuous, lowerBound, upperBound, objectiveFunctionCoefficient);
67}
68
69template<typename ValueType, bool RawMode>
70typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound,
71 ValueType upperBound,
72 ValueType objectiveFunctionCoefficient) {
73 return addVariable(name, VariableType::Integer, lowerBound, upperBound, objectiveFunctionCoefficient);
74}
75
76template<typename ValueType, bool RawMode>
77typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound,
78 ValueType objectiveFunctionCoefficient) {
79 return addVariable(name, VariableType::Integer, lowerBound, std::nullopt, objectiveFunctionCoefficient);
80}
81
82template<typename ValueType, bool RawMode>
83typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound,
84 ValueType objectiveFunctionCoefficient) {
85 return addVariable(name, VariableType::Integer, std::nullopt, upperBound, objectiveFunctionCoefficient);
86}
87
88template<typename ValueType, bool RawMode>
89typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addUnboundedIntegerVariable(std::string const& name,
90 ValueType objectiveFunctionCoefficient) {
91 return addVariable(name, VariableType::Integer, std::nullopt, std::nullopt, objectiveFunctionCoefficient);
92}
93
94template<typename ValueType, bool RawMode>
95typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addIntegerVariable(std::string const& name,
96 std::optional<ValueType> const& lowerBound,
97 std::optional<ValueType> const& upperBound,
98 ValueType objectiveFunctionCoefficient) {
99 return addVariable(name, VariableType::Integer, lowerBound, upperBound, objectiveFunctionCoefficient);
100}
101template<typename ValueType, bool RawMode>
102typename LpSolver<ValueType, RawMode>::Variable LpSolver<ValueType, RawMode>::addBinaryVariable(std::string const& name,
103 ValueType objectiveFunctionCoefficient) {
104 return addVariable(name, VariableType::Binary, std::nullopt, std::nullopt, objectiveFunctionCoefficient);
105}
106
107template<typename ValueType, bool RawMode>
108typename LpSolver<ValueType, RawMode>::Constant LpSolver<ValueType, RawMode>::getConstant(ValueType value) const {
109 if constexpr (RawMode) {
110 return value;
111 } else {
112 return manager->rational(value);
113 }
114}
115
116template<typename ValueType, bool RawMode>
117void LpSolver<ValueType, RawMode>::setOptimizationDirection(OptimizationDirection const& optimizationDirection) {
118 if (optimizationDirection != this->optimizationDirection) {
119 currentModelHasBeenOptimized = false;
120 }
121 this->optimizationDirection = optimizationDirection;
122}
123
124template<typename ValueType, bool RawMode>
125OptimizationDirection LpSolver<ValueType, RawMode>::getOptimizationDirection() const {
126 return optimizationDirection;
127}
128
129template<typename ValueType, bool RawMode>
130storm::expressions::ExpressionManager const& LpSolver<ValueType, RawMode>::getManager() const {
131 STORM_LOG_ASSERT(!RawMode, "Asking for a manager in raw mode which does not make sense.");
132 return *manager;
133}
134
135template<typename ValueType, bool RawMode>
136storm::expressions::Variable LpSolver<ValueType, RawMode>::declareOrGetExpressionVariable(std::string const& name, VariableType const& type) {
137 switch (type) {
138 case VariableType::Continuous:
139 return this->manager->declareOrGetVariable(name, this->manager->getRationalType());
140 case VariableType::Integer:
141 case VariableType::Binary:
142 return this->manager->declareOrGetVariable(name, this->manager->getIntegerType());
143 }
144 STORM_LOG_ASSERT(false, "Unable to declare or get expression variable: Unknown type");
145 return {};
146}
147
148template struct RawLpConstraint<double>;
149template struct RawLpConstraint<storm::RationalNumber>;
150template class LpSolver<double, true>;
151template class LpSolver<double, false>;
152template class LpSolver<storm::RationalNumber, true>;
153template class LpSolver<storm::RationalNumber, false>;
154
155} // namespace solver
156} // namespace storm
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:72
storm::solver::LpSolver
An interface that captures the functionality of an LP solver.
Definition LpSolver.h:51
storm::solver::LpSolver::addUnboundedIntegerVariable
Variable addUnboundedIntegerVariable(std::string const &name, ValueType objectiveFunctionCoefficient=0)
Registers an unbounded integer variable, i.e.
Definition LpSolver.cpp:89
storm::solver::LpSolver::getOptimizationDirection
OptimizationDirection getOptimizationDirection() const
Retrieves whether the objective function of this model is to be minimized or maximized.
Definition LpSolver.cpp:125
storm::solver::LpSolver::addIntegerVariable
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
storm::solver::LpSolver::addContinuousVariable
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
storm::solver::LpSolver::addUpperBoundedIntegerVariable
Variable addUpperBoundedIntegerVariable(std::string const &name, ValueType upperBound, ValueType objectiveFunctionCoefficient=0)
Registers an upper-bounded integer variable, i.e.
Definition LpSolver.cpp:83
storm::solver::LpSolver::declareOrGetExpressionVariable
storm::expressions::Variable declareOrGetExpressionVariable(std::string const &name, VariableType const &type)
Definition LpSolver.cpp:136
storm::solver::LpSolver::addBoundedIntegerVariable
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::solver::LpSolver::getManager
storm::expressions::ExpressionManager const & getManager() const
Retrieves the manager for the variables created for this solver.
Definition LpSolver.cpp:130
storm::solver::LpSolver::setOptimizationDirection
void setOptimizationDirection(OptimizationDirection const &optimizationDirection)
Sets whether the objective function of this model is to be minimized or maximized.
Definition LpSolver.cpp:117
storm::solver::LpSolver::LpSolver
LpSolver()
Creates an empty LP solver.
Definition LpSolver.cpp:25
storm::solver::LpSolver::Constant
std::conditional_t< RawMode, ValueType, storm::expressions::Expression > Constant
Definition LpSolver.h:54
storm::solver::LpSolver::addLowerBoundedContinuousVariable
Variable addLowerBoundedContinuousVariable(std::string const &name, ValueType lowerBound, ValueType objectiveFunctionCoefficient=0)
Registers a lower-bounded continuous variable, i.e.
Definition LpSolver.cpp:44
storm::solver::LpSolver::Variable
std::conditional_t< RawMode, typename RawLpConstraint< ValueType >::VariableIndexType, storm::expressions::Variable > Variable
Definition LpSolver.h:53
storm::solver::LpSolver::getConstant
Constant getConstant(ValueType value) const
Retrieves an expression that characterizes the given constant value.
Definition LpSolver.cpp:108
storm::solver::LpSolver::addLowerBoundedIntegerVariable
Variable addLowerBoundedIntegerVariable(std::string const &name, ValueType lowerBound, ValueType objectiveFunctionCoefficient=0)
Registers a lower-bounded integer variable, i.e.
Definition LpSolver.cpp:77
storm::solver::LpSolver::addBoundedContinuousVariable
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
storm::solver::LpSolver::VariableType
VariableType
Enumerates the different types of variables.
Definition LpSolver.h:60
storm::solver::LpSolver::addUnboundedContinuousVariable
Variable addUnboundedContinuousVariable(std::string const &name, ValueType objectiveFunctionCoefficient=0)
Registers a unbounded continuous variable, i.e.
Definition LpSolver.cpp:56
storm::solver::LpSolver::addUpperBoundedContinuousVariable
Variable addUpperBoundedContinuousVariable(std::string const &name, ValueType upperBound, ValueType objectiveFunctionCoefficient=0)
Registers an upper-bounded continuous variable, i.e.
Definition LpSolver.cpp:50
storm::solver::LpSolver::addBinaryVariable
Variable addBinaryVariable(std::string const &name, ValueType objectiveFunctionCoefficient=0)
Registers a boolean variable, i.e.
Definition LpSolver.cpp:102
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
storm::expressions::RelationType
RelationType
An enum type specifying the different relations applicable.
Definition BinaryRelationType.h:7
storm::solver::RawLpConstraint::lhsVariableIndices
std::vector< VariableIndexType > lhsVariableIndices
Definition LpSolver.h:40
storm::solver::RawLpConstraint::addToLhs
void addToLhs(VariableIndexType const &variable, ValueType const &coefficient)
Adds the summand 'coefficient * variable' to the left hand side.
Definition LpSolver.cpp:19
storm::solver::RawLpConstraint::RawLpConstraint
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::solver::RawLpConstraint::lhsCoefficients
std::vector< ValueType > lhsCoefficients
Definition LpSolver.h:41