sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

templated the LpSolvers

main
TimQu 8 years ago
parent
f46e8bcccf
commit
9ca14a54fc
22 changed files with 671 additions and 634 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 42
      src/storm/counterexamples/MILPMinimalLabelSetGenerator.h
  2. 8
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  3. 8
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  4. 4
      src/storm/permissivesched/MILPPermissiveSchedulers.h
  5. 2
      src/storm/permissivesched/PermissiveSchedulers.cpp
  6. 117
      src/storm/solver/GlpkLpSolver.cpp
  7. 49
      src/storm/solver/GlpkLpSolver.h
  8. 350
      src/storm/solver/GurobiLpSolver.cpp
  9. 27
      src/storm/solver/GurobiLpSolver.h
  10. 26
      src/storm/solver/LpMinMaxLinearEquationSolver.cpp
  11. 12
      src/storm/solver/LpMinMaxLinearEquationSolver.h
  12. 14
      src/storm/solver/LpSolver.cpp
  13. 25
      src/storm/solver/LpSolver.h
  14. 2
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  15. 423
      src/storm/solver/Z3LpSolver.cpp
  16. 39
      src/storm/solver/Z3LpSolver.h
  17. 12
      src/storm/storage/geometry/NativePolytope.cpp
  18. 64
      src/storm/utility/solver.cpp
  19. 33
      src/storm/utility/solver.h
  20. 16
      src/test/storm/solver/GlpkLpSolverTest.cpp
  21. 16
      src/test/storm/solver/GurobiLpSolverTest.cpp
  22. 16
      src/test/storm/solver/Z3LpSolverTest.cpp

42
src/storm/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -175,7 +175,7 @@ namespace storm {
* @param relevantLabels The set of relevant labels of the model.
* @return A mapping from labels to variable indices.
*/
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set<uint_fast64_t> const& relevantLabels) {
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createLabelVariables(storm::solver::LpSolver<double>& solver, boost::container::flat_set<uint_fast64_t> const& relevantLabels) {
std::stringstream variableNameBuffer;
std::unordered_map<uint_fast64_t, storm::expressions::Variable> resultingMap;
for (auto const& label : relevantLabels) {
@ -195,7 +195,7 @@ namespace storm {
* @param choiceInformation The information about the choices of the model.
* @return A mapping from states to a list of choice variable indices.
*/
static std::pair<std::unordered_map<uint_fast64_t, std::list<storm::expressions::Variable>>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
static std::pair<std::unordered_map<uint_fast64_t, std::list<storm::expressions::Variable>>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver<double>& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
std::stringstream variableNameBuffer;
uint_fast64_t numberOfVariablesCreated = 0;
std::unordered_map<uint_fast64_t, std::list<storm::expressions::Variable>> resultingMap;
@ -223,7 +223,7 @@ namespace storm {
* @param stateInformation The information about the states of the model.
* @return A mapping from initial states to choice variable indices.
*/
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation) {
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation) {
std::stringstream variableNameBuffer;
uint_fast64_t numberOfVariablesCreated = 0;
std::unordered_map<uint_fast64_t, storm::expressions::Variable> resultingMap;
@ -248,7 +248,7 @@ namespace storm {
* @param stateInformation The information about the states in the model.
* @return A mapping from states to the index of the corresponding probability variables.
*/
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) {
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver<double>& solver, StateInformation const& stateInformation) {
std::stringstream variableNameBuffer;
uint_fast64_t numberOfVariablesCreated = 0;
std::unordered_map<uint_fast64_t, storm::expressions::Variable> resultingMap;
@ -269,7 +269,7 @@ namespace storm {
* @param solver The MILP solver.
* @return The index of the variable for the probability of the virtual initial state.
*/
static std::pair<storm::expressions::Variable, uint_fast64_t> createVirtualInitialStateVariable(storm::solver::LpSolver& solver) {
static std::pair<storm::expressions::Variable, uint_fast64_t> createVirtualInitialStateVariable(storm::solver::LpSolver<double>& solver) {
std::stringstream variableNameBuffer;
variableNameBuffer << "pinit";
storm::expressions::Variable variable = solver.addBoundedContinuousVariable(variableNameBuffer.str(), 0, 1);
@ -284,7 +284,7 @@ namespace storm {
* @param stateInformation The information about the states in the model.
* @return A mapping from problematic states to the index of the corresponding variables.
*/
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
static std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
std::stringstream variableNameBuffer;
uint_fast64_t numberOfVariablesCreated = 0;
std::unordered_map<uint_fast64_t, storm::expressions::Variable> resultingMap;
@ -327,7 +327,7 @@ namespace storm {
* @param choiceInformation The information about the choices in the model.
* @return A mapping from problematic choices to the index of the corresponding variables.
*/
static std::pair<std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
static std::pair<std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
std::stringstream variableNameBuffer;
uint_fast64_t numberOfVariablesCreated = 0;
std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable, PairHash> resultingMap;
@ -359,7 +359,7 @@ namespace storm {
* @param stateInformation The information about the states in the model.
* @param choiceInformation The information about the choices in the model.
*/
static VariableInformation createVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
static VariableInformation createVariables(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) {
// Create a struct that stores all information about variables.
VariableInformation result;
@ -423,7 +423,7 @@ namespace storm {
* @param strictBound A flag indicating whether the threshold must be exceeded or only matched.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver& solver, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) {
static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver<double>& solver, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) {
storm::expressions::Expression constraint;
if (strictBound) {
constraint = variableInformation.virtualInitialStateVariable > solver.getConstant(probabilityThreshold);
@ -442,7 +442,7 @@ namespace storm {
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertValidPolicy(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertValidPolicy(storm::solver::LpSolver<double>& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) {
// Assert that the policy chooses at most one action in each state of the system.
uint_fast64_t numberOfConstraintsCreated = 0;
for (auto state : stateInformation.relevantStates) {
@ -484,7 +484,7 @@ namespace storm {
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
@ -511,7 +511,7 @@ namespace storm {
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver<double>& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
for (auto state : stateInformation.relevantStates) {
storm::expressions::Expression constraint = variableInformation.stateToProbabilityVariableMap.at(state);
@ -536,7 +536,7 @@ namespace storm {
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
for (auto state : stateInformation.relevantStates) {
std::list<storm::expressions::Variable>::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin();
@ -581,7 +581,7 @@ namespace storm {
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertUnproblematicStateReachable(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertUnproblematicStateReachable(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
for (auto stateListPair : choiceInformation.problematicChoicesForProblematicStates) {
@ -629,7 +629,7 @@ namespace storm {
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertKnownLabels(storm::solver::LpSolver<double>& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
for (auto label : choiceInformation.knownLabels) {
@ -652,7 +652,7 @@ namespace storm {
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
storm::storage::SparseMatrix<T> backwardTransitions = mdp.getBackwardTransitions();
uint_fast64_t numberOfConstraintsCreated = 0;
@ -812,7 +812,7 @@ namespace storm {
* @param includeSchedulerCuts If set to true, additional constraints are asserted that reduce the set of
* possible choices.
*/
static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& mdp, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) {
static void buildConstraintSystem(storm::solver::LpSolver<double>& solver, storm::models::sparse::Mdp<T> const& mdp, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) {
// Assert that the reachability probability in the subsystem exceeds the given threshold.
uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, variableInformation, probabilityThreshold, strictBound);
STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold.");
@ -860,7 +860,7 @@ namespace storm {
* @param solver The MILP solver.
* @param variableInformation A struct with information about the variables of the model.
*/
static boost::container::flat_set<uint_fast64_t> getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) {
static boost::container::flat_set<uint_fast64_t> getUsedLabelsInSolution(storm::solver::LpSolver<double> const& solver, VariableInformation const& variableInformation) {
boost::container::flat_set<uint_fast64_t> result;
for (auto const& labelVariablePair : variableInformation.labelToVariableMap) {
@ -883,7 +883,7 @@ namespace storm {
* @param choiceInformation The information about the choices in the model.
* @param variableInformation A struct with information about the variables of the model.
*/
static std::map<uint_fast64_t, uint_fast64_t> getChoices(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static std::map<uint_fast64_t, uint_fast64_t> getChoices(storm::solver::LpSolver<double> const& solver, storm::models::sparse::Mdp<T> const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
std::map<uint_fast64_t, uint_fast64_t> result;
for (auto state : stateInformation.relevantStates) {
@ -907,7 +907,7 @@ namespace storm {
* @param mdp The MDP.
* @param variableInformation A struct with information about the variables of the model.
*/
static std::pair<uint_fast64_t, double> getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp<T> const& mdp, VariableInformation const& variableInformation) {
static std::pair<uint_fast64_t, double> getReachabilityProbability(storm::solver::LpSolver<double> const& solver, storm::models::sparse::Mdp<T> const& mdp, VariableInformation const& variableInformation) {
uint_fast64_t selectedInitialState = 0;
for (auto const& initialStateVariablePair : variableInformation.initialStateToChoiceVariableMap) {
bool initialStateChosen = solver.getBinaryValue(initialStateVariablePair.second);
@ -945,7 +945,7 @@ namespace storm {
ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(mdp, labelSets, stateInformation, psiStates);
// (4) Encode resulting system as MILP problem.
std::shared_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("MinimalLabelSetCounterexample");
std::shared_ptr<storm::solver::LpSolver<double>> solver = storm::utility::solver::getLpSolver<double>("MinimalLabelSetCounterexample");
// (4.1) Create variables.
VariableInformation variableInformation = createVariables(*solver, mdp, stateInformation, choiceInformation);

8
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -427,8 +427,8 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) {
std::unique_ptr<storm::utility::solver::LpSolverFactory> lpSolverFactory(new storm::utility::solver::LpSolverFactory());
std::unique_ptr<storm::solver::LpSolver> solver = lpSolverFactory->create("LRA for MEC");
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory(new storm::utility::solver::LpSolverFactory<ValueType>());
std::unique_ptr<storm::solver::LpSolver<ValueType>> solver = lpSolverFactory->create("LRA for MEC");
solver->setOptimizationDirection(invert(dir));
// First, we need to create the variables for the problem.
@ -437,7 +437,7 @@ namespace storm {
std::string variableName = "x" + std::to_string(stateChoicesPair.first);
stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName);
}
storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", 1);
storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", storm::utility::one<ValueType>());
solver->update();
// Now we encode the problem as constraints.
@ -487,7 +487,7 @@ namespace storm {
}
solver->optimize();
return storm::utility::convertNumber<ValueType>(solver->getContinuousValue(k));
return solver->getContinuousValue(k);
}
template<typename ValueType, typename RewardModelType>

8
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -801,7 +801,7 @@ namespace storm {
template<typename ValueType>
template<typename RewardModelType>
ValueType SparseMdpPrctlHelper<ValueType>::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) {
std::shared_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("LRA for MEC");
std::shared_ptr<storm::solver::LpSolver<ValueType>> solver = storm::utility::solver::getLpSolver<ValueType>("LRA for MEC");
solver->setOptimizationDirection(invert(dir));
// First, we need to create the variables for the problem.
@ -822,10 +822,10 @@ namespace storm {
storm::expressions::Expression constraint = -lambda;
for (auto element : transitionMatrix.getRow(choice)) {
constraint = constraint + stateToVariableMap.at(element.getColumn()) * solver->getConstant(storm::utility::convertNumber<double>(element.getValue()));
constraint = constraint + stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue());
}
typename RewardModelType::ValueType r = rewardModel.getTotalStateActionReward(state, choice, transitionMatrix);
constraint = solver->getConstant(storm::utility::convertNumber<double>(r)) + constraint;
constraint = solver->getConstant(r) + constraint;
if (dir == OptimizationDirection::Minimize) {
constraint = stateToVariableMap.at(state) <= constraint;
@ -837,7 +837,7 @@ namespace storm {
}
solver->optimize();
return storm::utility::convertNumber<ValueType>(solver->getContinuousValue(lambda));
return solver->getContinuousValue(lambda);
}
template<typename ValueType>

4
src/storm/permissivesched/MILPPermissiveSchedulers.h
View File

@ -25,7 +25,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
private:
bool mCalledOptimizer = false;
storm::solver::LpSolver& solver;
storm::solver::LpSolver<double>& solver;
std::unordered_map<storm::storage::StateActionPair, storm::expressions::Variable> multistrategyVariables;
std::unordered_map<uint_fast64_t, storm::expressions::Variable> mProbVariables;
std::unordered_map<uint_fast64_t, storm::expressions::Variable> mAlphaVariables;
@ -34,7 +34,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
public:
MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, storm::models::sparse::Mdp<double, RM> const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates)
MilpPermissiveSchedulerComputation(storm::solver::LpSolver<double>& milpsolver, storm::models::sparse::Mdp<double, RM> const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates)
: PermissiveSchedulerComputation<RM>(mdp, goalstates, sinkstates), solver(milpsolver)
{

2
src/storm/permissivesched/PermissiveSchedulers.cpp
View File

@ -23,7 +23,7 @@ namespace storm {
goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi);
auto solver = storm::utility::solver::getLpSolver<double>("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi);
MilpPermissiveSchedulerComputation<storm::models::sparse::StandardRewardModel<double>> comp(*solver, mdp, goalstates, sinkstates);
STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported");
comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getThresholdAs<double>());

117
src/storm/solver/GlpkLpSolver.cpp
View File

@ -1,13 +1,13 @@
#include "storm/solver/GlpkLpSolver.h"
#ifdef STORM_HAVE_GLPK
#include <iostream>
#include <cmath>
#include "storm/storage/expressions/LinearCoefficientVisitor.h"
#include "storm/settings/SettingsManager.h"
#include "storm/utility/macros.h"
#include "storm/utility/constants.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/ExpressionManager.h"
@ -18,11 +18,14 @@
#include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/GlpkSettings.h"
#include <cmath>
namespace storm {
namespace solver {
GlpkLpSolver::GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() {
#ifdef STORM_HAVE_GLPK
template<typename ValueType>
GlpkLpSolver<ValueType>::GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver<ValueType>(optDir), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() {
// Create the LP problem for glpk.
lp = glp_create_prob();
@ -38,84 +41,98 @@ namespace storm {
coefficientValues.push_back(0);
}
GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, OptimizationDirection::Minimize) {
template<typename ValueType>
GlpkLpSolver<ValueType>::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, OptimizationDirection::Minimize) {
// Intentionally left empty.
}
GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) {
template<typename ValueType>
GlpkLpSolver<ValueType>::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) {
// Intentionally left empty.
}
GlpkLpSolver::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) {
template<typename ValueType>
GlpkLpSolver<ValueType>::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) {
// Intentionally left empty.
}
GlpkLpSolver::~GlpkLpSolver() {
template<typename ValueType>
GlpkLpSolver<ValueType>::~GlpkLpSolver() {
// Dispose of all objects allocated dynamically by glpk.
glp_delete_prob(this->lp);
glp_free_env();
}
storm::expressions::Variable GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name);
this->addVariable(newVariable, GLP_CV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name);
this->addVariable(newVariable, GLP_CV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name);
this->addVariable(newVariable, GLP_CV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareRationalVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name);
this->addVariable(newVariable, GLP_CV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name);
this->addVariable(newVariable, GLP_IV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient);
this->modelContainsIntegerVariables = true;
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name);
this->addVariable(newVariable, GLP_IV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient);
this->modelContainsIntegerVariables = true;
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name);
this->addVariable(newVariable, GLP_IV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient);
this->modelContainsIntegerVariables = true;
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name);
this->addVariable(newVariable, GLP_IV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
this->modelContainsIntegerVariables = true;
return newVariable;
}
storm::expressions::Variable GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(name);
template<typename ValueType>
storm::expressions::Variable GlpkLpSolver<ValueType>::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name);
this->addVariable(newVariable, GLP_BV, GLP_FR, 0, 0, objectiveFunctionCoefficient);
this->modelContainsIntegerVariables = true;
return newVariable;
}
void GlpkLpSolver::addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
template<typename ValueType>
void GlpkLpSolver<ValueType>::addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
// Check for valid variable type.
STORM_LOG_ASSERT(variableType == GLP_CV || variableType == GLP_IV || variableType == GLP_BV, "Illegal type '" << variableType << "' for glpk variable.");
@ -125,18 +142,20 @@ namespace storm {
// Finally, create the actual variable.
glp_add_cols(this->lp, 1);
glp_set_col_name(this->lp, nextVariableIndex, variable.getName().c_str());
glp_set_col_bnds(lp, nextVariableIndex, boundType, lowerBound, upperBound);
glp_set_col_bnds(lp, nextVariableIndex, boundType, storm::utility::convertNumber<double>(lowerBound), storm::utility::convertNumber<double>(upperBound));
glp_set_col_kind(this->lp, nextVariableIndex, variableType);
glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient);
glp_set_obj_coef(this->lp, nextVariableIndex, storm::utility::convertNumber<double>(objectiveFunctionCoefficient));
this->variableToIndexMap.emplace(variable, this->nextVariableIndex);
++this->nextVariableIndex;
}
void GlpkLpSolver::update() const {
template<typename ValueType>
void GlpkLpSolver<ValueType>::update() const {
// Intentionally left empty.
}
void GlpkLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {
template<typename ValueType>
void GlpkLpSolver<ValueType>::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());
@ -188,7 +207,8 @@ namespace storm {
this->currentModelHasBeenOptimized = false;
}
void GlpkLpSolver::optimize() const {
template<typename ValueType>
void GlpkLpSolver<ValueType>::optimize() const {
// First, reset the flags.
this->isInfeasibleFlag = false;
this->isUnboundedFlag = false;
@ -226,7 +246,8 @@ namespace storm {
this->currentModelHasBeenOptimized = true;
}
bool GlpkLpSolver::isInfeasible() const {
template<typename ValueType>
bool GlpkLpSolver<ValueType>::isInfeasible() const {
if (!this->currentModelHasBeenOptimized) {
throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isInfeasible: model has not been optimized.";
}
@ -238,7 +259,8 @@ namespace storm {
}
}
bool GlpkLpSolver::isUnbounded() const {
template<typename ValueType>
bool GlpkLpSolver<ValueType>::isUnbounded() const {
if (!this->currentModelHasBeenOptimized) {
throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isUnbounded: model has not been optimized.";
}
@ -250,7 +272,8 @@ namespace storm {
}
}
bool GlpkLpSolver::isOptimal() const {
template<typename ValueType>
bool GlpkLpSolver<ValueType>::isOptimal() const {
if (!this->currentModelHasBeenOptimized) {
return false;
}
@ -264,7 +287,8 @@ namespace storm {
return status == GLP_OPT;
}
double GlpkLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
ValueType GlpkLpSolver<ValueType>::getContinuousValue(storm::expressions::Variable const& variable) const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
@ -280,10 +304,11 @@ namespace storm {
} else {
value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
}
return value;
return storm::utility::convertNumber<ValueType>(value);
}
int_fast64_t GlpkLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
int_fast64_t GlpkLpSolver<ValueType>::getIntegerValue(storm::expressions::Variable const& variable) const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
@ -306,7 +331,8 @@ namespace storm {
return static_cast<int_fast64_t>(value);
}
bool GlpkLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
bool GlpkLpSolver<ValueType>::getBinaryValue(storm::expressions::Variable const& variable) const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
@ -328,7 +354,8 @@ namespace storm {
return static_cast<bool>(value);
}
double GlpkLpSolver::getObjectiveValue() const {
template<typename ValueType>
ValueType GlpkLpSolver<ValueType>::getObjectiveValue() const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
@ -342,14 +369,18 @@ namespace storm {
value = glp_get_obj_val(this->lp);
}
return value;
return storm::utility::convertNumber<ValueType>(value);
}
void GlpkLpSolver::writeModelToFile(std::string const& filename) const {
template<typename ValueType>
void GlpkLpSolver<ValueType>::writeModelToFile(std::string const& filename) const {
glp_load_matrix(this->lp, rowIndices.size() - 1, rowIndices.data(), columnIndices.data(), coefficientValues.data());
glp_write_lp(this->lp, 0, filename.c_str());
}
template class GlpkLpSolver<double>;
template class GlpkLpSolver<storm::RationalNumber>;
#endif
}
}
#endif

49
src/storm/solver/GlpkLpSolver.h
View File

@ -18,7 +18,8 @@ namespace storm {
/*!
* A class that implements the LpSolver interface using glpk as the background solver.
*/
class GlpkLpSolver : public LpSolver {
template<typename ValueType>
class GlpkLpSolver : public LpSolver<ValueType> {
public:
/*!
* Constructs a solver with the given name and model sense.
@ -57,19 +58,19 @@ namespace storm {
virtual ~GlpkLpSolver();
// Methods to add continuous variables.
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to add integer variables.
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to add binary variables.
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to incorporate recent changes.
virtual void update() const override;
@ -84,10 +85,10 @@ namespace storm {
virtual bool isOptimal() const override;
// Methods to retrieve values of variables and the objective function in the optimal solutions.
virtual double getContinuousValue(storm::expressions::Variable const& name) const override;
virtual ValueType getContinuousValue(storm::expressions::Variable const& name) const override;
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override;
virtual bool getBinaryValue(storm::expressions::Variable const& name) const override;
virtual double getObjectiveValue() const override;
virtual ValueType getObjectiveValue() const override;
// Methods to print the LP problem to a file.
virtual void writeModelToFile(std::string const& filename) const override;
@ -103,7 +104,7 @@ namespace storm {
* @param upperBound The upper bound of the range of the variable.
* @param objectiveFunctionCoefficient The coefficient of the variable in the objective function.
*/
void addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient);
void addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient);
// The glpk LP problem.
glp_prob* lp;
@ -153,39 +154,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 storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType 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 storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType 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 storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType 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 storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType 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 storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType 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 storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType 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 storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType 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 storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType 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 storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType 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.";
}
@ -213,7 +214,7 @@ 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 double getContinuousValue(storm::expressions::Variable const& variable) const override {
virtual ValueType getContinuousValue(storm::expressions::Variable const& variable) 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.";
}
@ -225,7 +226,7 @@ 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 double getObjectiveValue() const override {
virtual ValueType getObjectiveValue() 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.";
}

350
src/storm/solver/GurobiLpSolver.cpp
View File

@ -9,6 +9,8 @@
#include "storm/settings/modules/GurobiSettings.h"
#include "storm/utility/macros.h"
#include "storm/utility/constants.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/ExpressionManager.h"
@ -22,7 +24,8 @@ namespace storm {
namespace solver {
#ifdef STORM_HAVE_GUROBI
GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), env(nullptr), model(nullptr), nextVariableIndex(0) {
template<typename ValueType>
GurobiLpSolver<ValueType>::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver<ValueType>(optDir), env(nullptr), model(nullptr), nextVariableIndex(0) {
// Create the environment.
int error = GRBloadenv(&env, "");
if (error || env == nullptr) {
@ -41,25 +44,30 @@ namespace storm {
}
}
GurobiLpSolver::GurobiLpSolver(std::string const& name) : GurobiLpSolver(name, OptimizationDirection::Minimize) {
template<typename ValueType>
GurobiLpSolver<ValueType>::GurobiLpSolver(std::string const& name) : GurobiLpSolver(name, OptimizationDirection::Minimize) {
// Intentionally left empty.
}
GurobiLpSolver::GurobiLpSolver(OptimizationDirection const& optDir) : GurobiLpSolver("", optDir) {
template<typename ValueType>
GurobiLpSolver<ValueType>::GurobiLpSolver(OptimizationDirection const& optDir) : GurobiLpSolver("", optDir) {
// Intentionally left empty.
}
GurobiLpSolver::GurobiLpSolver() : GurobiLpSolver("", OptimizationDirection::Minimize) {
template<typename ValueType>
GurobiLpSolver<ValueType>::GurobiLpSolver() : GurobiLpSolver("", OptimizationDirection::Minimize) {
// Intentionally left empty.
}
GurobiLpSolver::~GurobiLpSolver() {
template<typename ValueType>
GurobiLpSolver<ValueType>::~GurobiLpSolver() {
// Dispose of the objects allocated inside Gurobi.
GRBfreemodel(model);
GRBfreeenv(env);
}
void GurobiLpSolver::setGurobiEnvironmentProperties() const {
template<typename ValueType>
void GurobiLpSolver<ValueType>::setGurobiEnvironmentProperties() const {
int error = 0;
// Enable the following line to only print the output of Gurobi if the debug flag is set.
@ -73,7 +81,8 @@ namespace storm {
STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
void GurobiLpSolver::update() const {
template<typename ValueType>
void GurobiLpSolver<ValueType>::update() const {
int error = GRBupdatemodel(model);
STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to update Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
@ -81,73 +90,84 @@ namespace storm {
this->currentModelHasBeenOptimized = false;
}
storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, lowerBound, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient);
return newVariable;
}
storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
this->addVariable(newVariable, GRB_BINARY, 0, 1, objectiveFunctionCoefficient);
return newVariable;
}
void GurobiLpSolver::addVariable(storm::expressions::Variable const& variable, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
template<typename ValueType>
void GurobiLpSolver<ValueType>::addVariable(storm::expressions::Variable const& variable, char variableType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
// Check for valid variable type.
STORM_LOG_ASSERT(variableType == GRB_CONTINUOUS || variableType == GRB_INTEGER || variableType == GRB_BINARY, "Illegal type '" << variableType << "' for Gurobi variable.");
// Finally, create the actual variable.
int error = 0;
error = GRBaddvar(model, 0, nullptr, nullptr, objectiveFunctionCoefficient, lowerBound, upperBound, variableType, variable.getName().c_str());
error = GRBaddvar(model, 0, nullptr, nullptr, storm::utility::convertNumber<double>(objectiveFunctionCoefficient), storm::utility::convertNumber<double>(lowerBound), storm::utility::convertNumber<double>(upperBound), variableType, variable.getName().c_str());
STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ", error code " << error << ").");
this->variableToIndexMap.emplace(variable, nextVariableIndex);
++nextVariableIndex;
}
void GurobiLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {
template<typename ValueType>
void GurobiLpSolver<ValueType>::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {
STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
@ -188,7 +208,8 @@ namespace storm {
STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not assert constraint (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
void GurobiLpSolver::optimize() const {
template<typename ValueType>
void GurobiLpSolver<ValueType>::optimize() const {
// First incorporate all recent changes.
this->update();
@ -203,9 +224,10 @@ namespace storm {
this->currentModelHasBeenOptimized = true;
}
bool GurobiLpSolver::isInfeasible() const {
template<typename ValueType>
bool GurobiLpSolver<ValueType>::isInfeasible() const {
if (!this->currentModelHasBeenOptimized) {
throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver::isInfeasible: model has not been optimized.";
throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver<ValueType>::isInfeasible: model has not been optimized.";
}
int optimalityStatus = 0;
@ -231,9 +253,10 @@ namespace storm {
return optimalityStatus == GRB_INFEASIBLE;
}
bool GurobiLpSolver::isUnbounded() const {
template<typename ValueType>
bool GurobiLpSolver<ValueType>::isUnbounded() const {
if (!this->currentModelHasBeenOptimized) {
throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver::isUnbounded: model has not been optimized.";
throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver<ValueType>::isUnbounded: model has not been optimized.";
}
int optimalityStatus = 0;
@ -259,7 +282,8 @@ namespace storm {
return optimalityStatus == GRB_UNBOUNDED;
}
bool GurobiLpSolver::isOptimal() const {
template<typename ValueType>
bool GurobiLpSolver<ValueType>::isOptimal() const {
if (!this->currentModelHasBeenOptimized) {
return false;
}
@ -271,7 +295,8 @@ namespace storm {
return optimalityStatus == GRB_OPTIMAL;
}
double GurobiLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
ValueType GurobiLpSolver<ValueType>::getContinuousValue(storm::expressions::Variable const& variable) const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
@ -285,10 +310,11 @@ namespace storm {
int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);
STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
return value;
return storm::utility::convertNumber<ValueType>(value);
}
int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
int_fast64_t GurobiLpSolver<ValueType>::getIntegerValue(storm::expressions::Variable const& variable) const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
@ -306,7 +332,8 @@ namespace storm {
return static_cast<int_fast64_t>(value);
}
bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
bool GurobiLpSolver<ValueType>::getBinaryValue(storm::expressions::Variable const& variable) const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
@ -329,7 +356,8 @@ namespace storm {
return static_cast<bool>(value);
}
double GurobiLpSolver::getObjectiveValue() const {
template<typename ValueType>
ValueType GurobiLpSolver<ValueType>::getObjectiveValue() const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ").");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ").");
@ -340,10 +368,11 @@ namespace storm {
int error = GRBgetdblattr(model, GRB_DBL_ATTR_OBJVAL, &value);
STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
return value;
return storm::utility::convertNumber<ValueType>(value);
}
void GurobiLpSolver::writeModelToFile(std::string const& filename) const {
template<typename ValueType>
void GurobiLpSolver<ValueType>::writeModelToFile(std::string const& filename) const {
int error = GRBwrite(model, filename.c_str());
if (error) {
STORM_LOG_ERROR("Unable to write Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ") to file.");
@ -351,115 +380,144 @@ namespace storm {
}
}
void GurobiLpSolver::toggleOutput(bool set) const {
template<typename ValueType>
void GurobiLpSolver<ValueType>::toggleOutput(bool set) const {
int error = GRBsetintparam(env, "OutputFlag", set);
STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
#else
GurobiLpSolver::GurobiLpSolver(std::string const&, OptimizationDirection 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.";
}
GurobiLpSolver::GurobiLpSolver(std::string 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.";
}
GurobiLpSolver::GurobiLpSolver(OptimizationDirection 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.";
}
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&, double, double, double) {
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&, double, double ) {
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&, double, double ) {
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&, double ) {
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&, double, double, double) {
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&, double, double) {
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&, double, double) {
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&, double) {
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&, double) {
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&, storm::expressions::Expression 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::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&) 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&) 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&) 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&) 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.";
}
#else
template<typename ValueType>
GurobiLpSolver<ValueType>::GurobiLpSolver(std::string const&, OptimizationDirection 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.";
}
template<typename ValueType>
GurobiLpSolver<ValueType>::GurobiLpSolver(std::string 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.";
}
template<typename ValueType>
GurobiLpSolver<ValueType>::GurobiLpSolver(OptimizationDirection 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.";
}
template<typename ValueType>
GurobiLpSolver<ValueType>::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.";
}
template<typename ValueType>
GurobiLpSolver<ValueType>::~GurobiLpSolver() {
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBoundedContinuousVariable(std::string const&, ValueType, ValueType, ValueType) {
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.";
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addLowerBoundedContinuousVariable(std::string const&, ValueType, ValueType ) {
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."; }
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUpperBoundedContinuousVariable(std::string const&, ValueType, ValueType ) {
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.";
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUnboundedContinuousVariable(std::string const&, ValueType ) {
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.";
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBoundedIntegerVariable(std::string const&, ValueType, ValueType, ValueType) {
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.";
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addLowerBoundedIntegerVariable(std::string const&, ValueType, ValueType) {
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.";
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUpperBoundedIntegerVariable(std::string const&, ValueType, ValueType) {
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.";
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addUnboundedIntegerVariable(std::string const&, ValueType) {
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.";
}
template<typename ValueType>
storm::expressions::Variable GurobiLpSolver<ValueType>::addBinaryVariable(std::string const&, ValueType) {
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.";
}
template<typename ValueType>
void GurobiLpSolver<ValueType>::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.";
}
template<typename ValueType>
void GurobiLpSolver<ValueType>::addConstraint(std::string const&, storm::expressions::Expression 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.";
}
template<typename ValueType>
void GurobiLpSolver<ValueType>::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.";
}
template<typename ValueType>
bool GurobiLpSolver<ValueType>::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.";
}
template<typename ValueType>
bool GurobiLpSolver<ValueType>::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.";
}
template<typename ValueType>
bool GurobiLpSolver<ValueType>::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.";
}
template<typename ValueType>
ValueType GurobiLpSolver<ValueType>::getContinuousValue(storm::expressions::Variable const&) 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.";
}
template<typename ValueType>
int_fast64_t GurobiLpSolver<ValueType>::getIntegerValue(storm::expressions::Variable const&) 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.";
}
template<typename ValueType>
bool GurobiLpSolver<ValueType>::getBinaryValue(storm::expressions::Variable const&) 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.";
}
template<typename ValueType>
ValueType GurobiLpSolver<ValueType>::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.";
}
template<typename ValueType>
void GurobiLpSolver<ValueType>::writeModelToFile(std::string const&) 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::toggleOutput(bool) 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.";
}
template<typename ValueType>
void GurobiLpSolver<ValueType>::toggleOutput(bool) 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
template class GurobiLpSolver<double>;
template class GurobiLpSolver<storm::RationalNumber>;
}
}

27
src/storm/solver/GurobiLpSolver.h
View File

@ -22,7 +22,8 @@ namespace storm {
/*!
* A class that implements the LpSolver interface using Gurobi.
*/
class GurobiLpSolver : public LpSolver {
template<typename ValueType>
class GurobiLpSolver : public LpSolver<ValueType> {
public:
/*!
* Constructs a solver with the given name and model sense.
@ -61,19 +62,19 @@ namespace storm {
virtual ~GurobiLpSolver();
// Methods to add continuous variables.
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to add integer variables.
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to add binary variables.
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to incorporate recent changes.
virtual void update() const override;
@ -88,10 +89,10 @@ namespace storm {
virtual bool isOptimal() const override;
// Methods to retrieve values of variables and the objective function in the optimal solutions.
virtual double getContinuousValue(storm::expressions::Variable const& name) const override;
virtual ValueType getContinuousValue(storm::expressions::Variable const& name) const override;
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override;
virtual bool getBinaryValue(storm::expressions::Variable const& name) const override;
virtual double getObjectiveValue() const override;
virtual ValueType getObjectiveValue() const override;
// Methods to print the LP problem to a file.
virtual void writeModelToFile(std::string const& filename) const override;
@ -113,7 +114,7 @@ namespace storm {
* @param upperBound The upper bound of the range of the variable.
* @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);
void addVariable(storm::expressions::Variable const& variable, char variableType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient);
#ifdef STORM_HAVE_GUROBI
// The Gurobi environment.
GRBenv* env;

26
src/storm/solver/LpMinMaxLinearEquationSolver.cpp
View File

@ -10,12 +10,12 @@ namespace storm {
namespace solver {
template<typename ValueType>
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty.
}
template<typename ValueType>
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty.
}
@ -23,7 +23,7 @@ namespace storm {
bool LpMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// Set up the LP solver
std::unique_ptr<storm::solver::LpSolver> solver = lpSolverFactory->create("");
std::unique_ptr<storm::solver::LpSolver<ValueType>> solver = lpSolverFactory->create("");
solver->setOptimizationDirection(invert(dir));
// Create a variable for each row group
@ -32,15 +32,15 @@ namespace storm {
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) {
if (this->lowerBound) {
if (this->upperBound) {
variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::convertNumber<double>(this->lowerBound.get()), storm::utility::convertNumber<double>(this->upperBound.get()), 1.0));
variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one<ValueType>()));
} else {
variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::convertNumber<double>(this->lowerBound.get()), 1.0));
variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), storm::utility::one<ValueType>()));
}
} else {
if (this->upperBound) {
variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::convertNumber<double>(this->upperBound.get()), 1.0));
variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->upperBound.get(), storm::utility::one<ValueType>()));
} else {
variables.push_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), 1.0));
variables.push_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::one<ValueType>()));
}
}
}
@ -49,9 +49,9 @@ namespace storm {
// Add a constraint for each row
for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) {
for (uint64_t row = this->A.getRowGroupIndices()[rowGroup]; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row) {
storm::expressions::Expression rowConstraint = solver->getConstant(storm::utility::convertNumber<double>(b[row]));
storm::expressions::Expression rowConstraint = solver->getConstant(b[row]);
for (auto const& entry : this->A.getRow(row)) {
rowConstraint = rowConstraint + (solver->getConstant(storm::utility::convertNumber<double>(entry.getValue())) * variables[entry.getColumn()].getExpression());
rowConstraint = rowConstraint + (solver->getConstant(entry.getValue()) * variables[entry.getColumn()].getExpression());
}
if (minimize(dir)) {
rowConstraint = variables[rowGroup].getExpression() <= rowConstraint;
@ -73,7 +73,7 @@ namespace storm {
auto xIt = x.begin();
auto vIt = variables.begin();
for (; xIt != x.end(); ++xIt, ++vIt) {
*xIt = storm::utility::convertNumber<ValueType>(solver->getContinuousValue(*vIt));
*xIt = solver->getContinuousValue(*vIt);
}
// If requested, we store the scheduler for retrieval.
@ -104,17 +104,17 @@ namespace storm {
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory>()) {
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
// Intentionally left empty
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty
}

12
src/storm/solver/LpMinMaxLinearEquationSolver.h
View File

@ -10,23 +10,23 @@ namespace storm {
template<typename ValueType>
class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> {
public:
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
virtual bool solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void clearCache() const override;
private:
std::unique_ptr<storm::utility::solver::LpSolverFactory> lpSolverFactory;
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
template<typename ValueType>
class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
public:
LpMinMaxLinearEquationSolverFactory(bool trackScheduler = false);
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory, bool trackScheduler = false);
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory>&& lpSolverFactory, bool trackScheduler = false);
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler = false);
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler = false);
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
@ -35,7 +35,7 @@ namespace storm {
virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override;
private:
std::unique_ptr<storm::utility::solver::LpSolverFactory> lpSolverFactory;
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
}
}

14
src/storm/solver/LpSolver.cpp
View File

@ -8,16 +8,24 @@
namespace storm {
namespace solver {
LpSolver::LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(OptimizationDirection::Minimize) {
template<typename ValueType>
LpSolver<ValueType>::LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(OptimizationDirection::Minimize) {
// Intentionally left empty.
}
LpSolver::LpSolver(OptimizationDirection const& optimizationDir) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(optimizationDir) {
template<typename ValueType>
LpSolver<ValueType>::LpSolver(OptimizationDirection const& optimizationDir) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(optimizationDir) {
// Intentionally left empty.
}
storm::expressions::Expression LpSolver::getConstant(double value) const {
template<typename ValueType>
storm::expressions::Expression LpSolver<ValueType>::getConstant(ValueType value) const {
return manager->rational(value);
}
template class LpSolver<double>;
template class LpSolver<storm::RationalNumber>;
}
}

25
src/storm/solver/LpSolver.h
View File

@ -18,6 +18,7 @@ namespace storm {
/*!
* An interface that captures the functionality of an LP solver.
*/
template<typename ValueType>
class LpSolver {
public:
// An enumeration to represent whether the objective function is to be minimized or maximized.
@ -45,7 +46,7 @@ namespace storm {
* @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 storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers a lower-bounded continuous variable, i.e. a variable that may take all real values up to its
@ -56,7 +57,7 @@ namespace storm {
* @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 storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers an upper-bounded continuous variable, i.e. a variable that may take all real values up to its
@ -67,7 +68,7 @@ namespace storm {
* @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 storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers a unbounded continuous variable, i.e. a variable that may take all real values.
@ -76,7 +77,7 @@ namespace storm {
* @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 storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers an upper- and lower-bounded integer variable, i.e. a variable that may take all integer values
@ -88,7 +89,7 @@ namespace storm {
* @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 storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers a lower-bounded integer variable, i.e. a variable that may take all integer values up to its
@ -99,7 +100,7 @@ namespace storm {
* @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 storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers an upper-bounded integer variable, i.e. a variable that may take all integer values up to its
@ -110,7 +111,7 @@ namespace storm {
* @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 storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers an unbounded integer variable, i.e. a variable that may take all integer values.
@ -119,7 +120,7 @@ namespace storm {
* @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 storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Registers a boolean variable, i.e. a variable that may be either 0 or 1.
@ -128,7 +129,7 @@ namespace storm {
* @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 storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0;
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0;
/*!
* Retrieves an expression that characterizes the given constant value.
@ -136,7 +137,7 @@ namespace storm {
* @param value The value of the constant.
* @return The resulting expression.
*/
storm::expressions::Expression getConstant(double value) const;
storm::expressions::Expression getConstant(ValueType value) const;
/*!
* Updates the model to make the variables that have been declared since the last call to <code>update</code>
@ -209,7 +210,7 @@ namespace storm {
* @param variable The variable whose integer value (in the optimal solution) to retrieve.
* @return The value of the continuous variable in the optimal solution.
*/
virtual double getContinuousValue(storm::expressions::Variable const& variable) const = 0;
virtual ValueType getContinuousValue(storm::expressions::Variable const& variable) const = 0;
/*!
* Retrieves the value of the objective function. Note that this may only be called, if the model was found
@ -217,7 +218,7 @@ namespace storm {
*
* @return The value of the objective function in the optimal solution.
*/
virtual double getObjectiveValue() const = 0;
virtual ValueType getObjectiveValue() const = 0;
/*!
* Writes the current LP problem to the given file.

2
src/storm/solver/MinMaxLinearEquationSolver.cpp
View File

@ -197,7 +197,7 @@ namespace storm {
} else if (method == MinMaxMethod::Topological) {
result = std::make_unique<TopologicalMinMaxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix));
} else if (method == MinMaxMethod::LinearProgramming) {
result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(), std::make_unique<storm::utility::solver::LpSolverFactory>());
result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(), std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}

423
src/storm/solver/Z3LpSolver.cpp
View File

@ -23,7 +23,9 @@ namespace storm {
namespace solver {
#ifdef STORM_HAVE_Z3_OPTIMIZE
Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir) {
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver<ValueType>(optDir) {
STORM_LOG_WARN_COND(name == "", "Z3 does not support names for solvers");
z3::config config;
config.set("model", true);
@ -33,98 +35,114 @@ namespace storm {
optimizationFunction = this->getManager().rational(storm::utility::zero<storm::RationalNumber>());
}
Z3LpSolver::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) {
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) {
// Intentionally left empty.
}
Z3LpSolver::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) {
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) {
// Intentionally left empty.
}
Z3LpSolver::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) {
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) {
// Intentionally left empty.
}
Z3LpSolver::~Z3LpSolver() {
template<typename ValueType>
Z3LpSolver<ValueType>::~Z3LpSolver() {
// Intentionally left empty.
}
void Z3LpSolver::update() const {
template<typename ValueType>
void Z3LpSolver<ValueType>::update() const {
// Since the model changed, we erase the optimality flag.
lastCheckObjectiveValue.reset(nullptr);
lastCheckModel.reset(nullptr);
this->currentModelHasBeenOptimized = false;
}
storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound))));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType());
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound))));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType());
solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(storm::utility::one<storm::RationalNumber>())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one<storm::RationalNumber>()))));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {
template<typename ValueType>
void Z3LpSolver<ValueType>::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) {
STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator.");
STORM_LOG_WARN_COND(name == "", "Z3 does not support names for constraints");
solver->add(expressionAdapter->translateExpression(constraint));
}
void Z3LpSolver::optimize() const {
template<typename ValueType>
void Z3LpSolver<ValueType>::optimize() const {
// First incorporate all recent changes.
this->update();
@ -140,7 +158,7 @@ namespace storm {
// Check feasibility
lastCheckInfeasible = (chkRes == z3::unsat);
if(lastCheckInfeasible) {
if (lastCheckInfeasible) {
lastCheckUnbounded = false;
} else {
// Get objective result
@ -148,7 +166,7 @@ namespace storm {
// Check boundedness
STORM_LOG_ASSERT(lastCheckObjectiveValue->is_app(), "Failed to convert Z3 expression. Encountered unknown expression type.");
lastCheckUnbounded = (lastCheckObjectiveValue->decl().decl_kind() != Z3_OP_ANUM);
if(lastCheckUnbounded) {
if (lastCheckUnbounded) {
lastCheckObjectiveValue.reset(nullptr);
} else {
// Assert that the upper approximation equals the lower one
@ -161,22 +179,26 @@ namespace storm {
this->currentModelHasBeenOptimized = true;
}
bool Z3LpSolver::isInfeasible() const {
STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isInfeasible: model has not been optimized.");
template<typename ValueType>
bool Z3LpSolver<ValueType>::isInfeasible() const {
STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver<ValueType>::isInfeasible: model has not been optimized.");
return lastCheckInfeasible;
}
bool Z3LpSolver::isUnbounded() const {
STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isUnbounded: model has not been optimized.");
template<typename ValueType>
bool Z3LpSolver<ValueType>::isUnbounded() const {
STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver<ValueType>::isUnbounded: model has not been optimized.");
return lastCheckUnbounded;
}
bool Z3LpSolver::isOptimal() const {
STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isOptimal: model has not been optimized.");
template<typename ValueType>
bool Z3LpSolver<ValueType>::isOptimal() const {
STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver<ValueType>::isOptimal: model has not been optimized.");
return !lastCheckInfeasible && !lastCheckUnbounded;
}
storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
storm::expressions::Expression Z3LpSolver<ValueType>::getValue(storm::expressions::Variable const& variable) const {
STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model.");
@ -189,31 +211,35 @@ namespace storm {
return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true));
}
double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
ValueType Z3LpSolver<ValueType>::getContinuousValue(storm::expressions::Variable const& variable) const {
storm::expressions::Expression value = getValue(variable);
if(value.getBaseExpression().isIntegerLiteralExpression()) {
return value.getBaseExpression().asIntegerLiteralExpression().getValue();
if (value.getBaseExpression().isIntegerLiteralExpression()) {
return storm::utility::convertNumber<ValueType>(value.getBaseExpression().asIntegerLiteralExpression().getValue());
}
STORM_LOG_THROW(value.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the value of a continuous variable. Got " << value << "instead.");
return value.getBaseExpression().asRationalLiteralExpression().getValueAsDouble();
return storm::utility::convertNumber<ValueType>(value.getBaseExpression().asRationalLiteralExpression().getValue());
}
int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
int_fast64_t Z3LpSolver<ValueType>::getIntegerValue(storm::expressions::Variable const& variable) const {
storm::expressions::Expression value = getValue(variable);
STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected an integer literal while obtaining the value of an integer variable. Got " << value << "instead.");
return value.getBaseExpression().asIntegerLiteralExpression().getValue();
}
bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const& variable) const {
template<typename ValueType>
bool Z3LpSolver<ValueType>::getBinaryValue(storm::expressions::Variable const& variable) const {
storm::expressions::Expression value = getValue(variable);
// Binary variables are in fact represented as integer variables!
STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected an integer literal while obtaining the value of a binary variable. Got " << value << "instead.");
int_fast64_t val = value.getBaseExpression().asIntegerLiteralExpression().getValue();
STORM_LOG_THROW((val==0 || val==1), storm::exceptions::ExpressionEvaluationException, "Tried to get a binary value for a variable that is neither 0 nor 1.");
return val==1;
return val == 1;
}
double Z3LpSolver::getObjectiveValue() const {
template<typename ValueType>
ValueType Z3LpSolver<ValueType>::getObjectiveValue() const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model.");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model.");
@ -222,253 +248,150 @@ namespace storm {
STORM_LOG_ASSERT(lastCheckObjectiveValue, "Objective value has not been stored.");
storm::expressions::Expression result = this->expressionAdapter->translateExpression(*lastCheckObjectiveValue);
if(result.getBaseExpression().isIntegerLiteralExpression()) {
return result.getBaseExpression().asIntegerLiteralExpression().getValue();
if (result.getBaseExpression().isIntegerLiteralExpression()) {
return storm::utility::convertNumber<ValueType>(result.getBaseExpression().asIntegerLiteralExpression().getValue());
}
STORM_LOG_THROW(result.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the objective result. Got " << result << "instead.");
return result.getBaseExpression().asRationalLiteralExpression().getValueAsDouble();
return storm::utility::convertNumber<ValueType>(result.getBaseExpression().asRationalLiteralExpression().getValue());
}
void Z3LpSolver::writeModelToFile(std::string const& filename) const {
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3.");
template<typename ValueType>
void Z3LpSolver<ValueType>::writeModelToFile(std::string const& filename) const {
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3.");
}
storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound))));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
#else
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver(std::string const&, OptimizationDirection const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver(std::string const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver(OptimizationDirection const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType());
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
template<typename ValueType>
Z3LpSolver<ValueType>::Z3LpSolver() {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound))));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
template<typename ValueType>
Z3LpSolver<ValueType>::~Z3LpSolver() {
storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound)));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addBoundedContinuousVariable(std::string const&, ValueType, ValueType, ValueType) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
}
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addLowerBoundedContinuousVariable(std::string const&, ValueType, ValueType ) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; }
storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) {
storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType());
solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(storm::utility::one<storm::RationalNumber>())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one<storm::RationalNumber>()))));
optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable;
return newVariable;
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUpperBoundedContinuousVariable(std::string const&, ValueType, ValueType ) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::RationalNumber Z3LpSolver::getExactContinuousValue(storm::expressions::Variable const& variable) const {
storm::expressions::Expression value = getValue(variable);
if(value.getBaseExpression().isIntegerLiteralExpression()) {
return storm::utility::convertNumber<storm::RationalNumber>(value.getBaseExpression().asIntegerLiteralExpression().getValue());
}
STORM_LOG_ASSERT(value.getBaseExpression().isRationalLiteralExpression(), "Expected a rational literal while obtaining the value of a continuous variable. Got " << value << "instead.");
return value.getBaseExpression().asRationalLiteralExpression().getValue();
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUnboundedContinuousVariable(std::string const&, ValueType ) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::RationalNumber Z3LpSolver::getExactObjectiveValue() const {
if (!this->isOptimal()) {
STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model.");
STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model.");
STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model.");
}
STORM_LOG_ASSERT(lastCheckObjectiveValue, "Objective value has not been stored.");
storm::expressions::Expression result = this->expressionAdapter->translateExpression(*lastCheckObjectiveValue);
if(result.getBaseExpression().isIntegerLiteralExpression()) {
return storm::utility::convertNumber<storm::RationalNumber>(result.getBaseExpression().asIntegerLiteralExpression().getValue());
}
STORM_LOG_THROW(result.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the objective result. Got " << result << "instead.");
return result.getBaseExpression().asRationalLiteralExpression().getValue();
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addBoundedIntegerVariable(std::string const&, ValueType, ValueType, ValueType) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
#else
Z3LpSolver::Z3LpSolver(std::string const&, OptimizationDirection const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
Z3LpSolver::Z3LpSolver(std::string const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
Z3LpSolver::Z3LpSolver(OptimizationDirection const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
Z3LpSolver::Z3LpSolver() {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
Z3LpSolver::~Z3LpSolver() {
}
storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const&, double, double, double) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const&, double, double ) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; }
storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const&, double, double ) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const&, double ) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const&, double, double, double) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const&, double, double) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const&, double, double) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const&, double) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const&, double) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
void Z3LpSolver::update() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
void Z3LpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
void Z3LpSolver::optimize() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
bool Z3LpSolver::isInfeasible() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
bool Z3LpSolver::isUnbounded() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
bool Z3LpSolver::isOptimal() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
double Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
double Z3LpSolver::getObjectiveValue() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addLowerBoundedIntegerVariable(std::string const&, ValueType, ValueType) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
void Z3LpSolver::writeModelToFile(std::string const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUpperBoundedIntegerVariable(std::string const&, ValueType, ValueType) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addUnboundedIntegerVariable(std::string const&, ValueType) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
template<typename ValueType>
storm::expressions::Variable Z3LpSolver<ValueType>::addBinaryVariable(std::string const&, ValueType) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
}
template<typename ValueType>
void Z3LpSolver<ValueType>::update() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
void Z3LpSolver<ValueType>::addConstraint(std::string const&, storm::expressions::Expression const&) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
void Z3LpSolver<ValueType>::optimize() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
bool Z3LpSolver<ValueType>::isInfeasible() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
bool Z3LpSolver<ValueType>::isUnbounded() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
bool Z3LpSolver<ValueType>::isOptimal() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
storm::expressions::Expression Z3LpSolver<ValueType>::getValue(storm::expressions::Variable const& variable) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
ValueType Z3LpSolver<ValueType>::getContinuousValue(storm::expressions::Variable const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
int_fast64_t Z3LpSolver<ValueType>::getIntegerValue(storm::expressions::Variable const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::RationalNumber Z3LpSolver::getExactContinuousValue(storm::expressions::Variable const& variable) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
bool Z3LpSolver<ValueType>::getBinaryValue(storm::expressions::Variable const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
storm::RationalNumber Z3LpSolver::getExactObjectiveValue() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
ValueType Z3LpSolver<ValueType>::getObjectiveValue() const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
template<typename ValueType>
void Z3LpSolver<ValueType>::writeModelToFile(std::string const&) const {
throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";
}
#endif
#endif
template class Z3LpSolver<double>;
template class Z3LpSolver<storm::RationalNumber>;
}
}

39
src/storm/solver/Z3LpSolver.h
View File

@ -21,7 +21,8 @@ namespace storm {
/*!
* A class that implements the LpSolver interface using Z3.
*/
class Z3LpSolver : public LpSolver {
template<typename ValueType>
class Z3LpSolver : public LpSolver<ValueType> {
public:
/*!
* Constructs a solver with the given name and optimization direction
@ -60,19 +61,19 @@ namespace storm {
virtual ~Z3LpSolver();
// Methods to add continuous variables.
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to add integer variables.
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to add binary variables.
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override;
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override;
// Methods to incorporate recent changes.
virtual void update() const override;
@ -87,28 +88,14 @@ namespace storm {
virtual bool isOptimal() const override;
// Methods to retrieve values of variables and the objective function in the optimal solutions.
virtual double getContinuousValue(storm::expressions::Variable const& variable) const override;
virtual ValueType getContinuousValue(storm::expressions::Variable const& variable) const override;
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
virtual bool getBinaryValue(storm::expressions::Variable const& variable) const override;
virtual double getObjectiveValue() const override;
virtual ValueType getObjectiveValue() const override;
// Methods to print the LP problem to a file.
virtual void writeModelToFile(std::string const& filename) const override;
// Methods for exact solving
storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::expressions::Variable addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0);
storm::RationalNumber getExactContinuousValue(storm::expressions::Variable const& variable) const;
storm::RationalNumber getExactObjectiveValue() const;
private:
virtual storm::expressions::Expression getValue(storm::expressions::Variable const& variable) const;

12
src/storm/storage/geometry/NativePolytope.cpp
View File

@ -1,4 +1,3 @@
#include <storm/exceptions/NotImplementedException.h>
#include "storm/storage/geometry/NativePolytope.h"
#include "storm/utility/macros.h"
@ -11,6 +10,7 @@
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace storage {
@ -307,7 +307,7 @@ namespace storm {
return std::make_pair(Point(), false);
}
storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<ValueType> solver(storm::solver::OptimizationDirection::Maximize);
std::vector<storm::expressions::Variable> variables;
variables.reserve(A.cols());
for (StormEigen::Index i = 0; i < A.cols(); ++i) {
@ -323,7 +323,7 @@ namespace storm {
auto result = std::make_pair(Point(), true);
result.first.reserve(variables.size());
for (auto const& var : variables) {
result.first.push_back(storm::utility::convertNumber<ValueType>((solver.getExactContinuousValue(var))));
result.first.push_back(solver.getContinuousValue(var));
}
return result;
} else {
@ -338,11 +338,11 @@ namespace storm {
return std::make_pair(EigenVector(), false);
}
storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<ValueType> solver(storm::solver::OptimizationDirection::Maximize);
std::vector<storm::expressions::Variable> variables;
variables.reserve(A.cols());
for (StormEigen::Index i = 0; i < A.cols(); ++i) {
variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction(i)));
variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), static_cast<ValueType>(direction(i))));
}
std::vector<storm::expressions::Expression> constraints = getConstraints(solver.getManager(), variables);
for (auto const& constraint: constraints) {
@ -353,7 +353,7 @@ namespace storm {
if (solver.isOptimal()) {
auto result = std::make_pair(EigenVector(A.cols()), true);
for (StormEigen::Index i = 0; i < A.cols(); ++i) {
result.first(i) = storm::utility::convertNumber<ValueType>(solver.getExactContinuousValue(variables[i]));
result.first(i) = solver.getContinuousValue(variables[i]);
}
return result;
} else {

64
src/storm/utility/solver.cpp
View File

@ -27,7 +27,8 @@ namespace storm {
return std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>>(new storm::solver::SymbolicGameSolver<Type, ValueType>(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables));
}
std::unique_ptr<storm::solver::LpSolver> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const {
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> LpSolverFactory<ValueType>::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const {
storm::solver::LpSolverType t;
if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) {
t = storm::settings::getModule<storm::settings::modules::CoreSettings>().getLpSolver();
@ -35,47 +36,56 @@ namespace storm {
t = convert(solvT);
}
switch (t) {
case storm::solver::LpSolverType::Gurobi: return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
case storm::solver::LpSolverType::Glpk: return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GlpkLpSolver(name));
case storm::solver::LpSolverType::Z3: return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::Z3LpSolver(name));
case storm::solver::LpSolverType::Gurobi: return std::unique_ptr<storm::solver::LpSolver<ValueType>>(new storm::solver::GurobiLpSolver<ValueType>(name));
case storm::solver::LpSolverType::Glpk: return std::unique_ptr<storm::solver::LpSolver<ValueType>>(new storm::solver::GlpkLpSolver<ValueType>(name));
case storm::solver::LpSolverType::Z3: return std::unique_ptr<storm::solver::LpSolver<ValueType>>(new storm::solver::Z3LpSolver<ValueType>(name));
}
return nullptr;
}
std::unique_ptr<storm::solver::LpSolver> LpSolverFactory::create(std::string const& name) const {
return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::FROMSETTINGS);
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> LpSolverFactory<ValueType>::create(std::string const& name) const {
return LpSolverFactory<ValueType>::create(name, storm::solver::LpSolverTypeSelection::FROMSETTINGS);
}
std::unique_ptr<LpSolverFactory> LpSolverFactory::clone() const {
return std::make_unique<LpSolverFactory>(*this);
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> LpSolverFactory<ValueType>::clone() const {
return std::make_unique<LpSolverFactory<ValueType>>(*this);
}
std::unique_ptr<storm::solver::LpSolver> GlpkLpSolverFactory::create(std::string const& name) const {
return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Glpk);
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> GlpkLpSolverFactory<ValueType>::create(std::string const& name) const {
return LpSolverFactory<ValueType>::create(name, storm::solver::LpSolverTypeSelection::Glpk);
}
std::unique_ptr<LpSolverFactory> GlpkLpSolverFactory::clone() const {
return std::make_unique<GlpkLpSolverFactory>(*this);
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> GlpkLpSolverFactory<ValueType>::clone() const {
return std::make_unique<GlpkLpSolverFactory<ValueType>>(*this);
}
std::unique_ptr<storm::solver::LpSolver> GurobiLpSolverFactory::create(std::string const& name) const {
return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Gurobi);
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> GurobiLpSolverFactory<ValueType>::create(std::string const& name) const {
return LpSolverFactory<ValueType>::create(name, storm::solver::LpSolverTypeSelection::Gurobi);
}
std::unique_ptr<LpSolverFactory> GurobiLpSolverFactory::clone() const {
return std::make_unique<GurobiLpSolverFactory>(*this);
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> GurobiLpSolverFactory<ValueType>::clone() const {
return std::make_unique<GurobiLpSolverFactory<ValueType>>(*this);
}
std::unique_ptr<storm::solver::LpSolver> Z3LpSolverFactory::create(std::string const& name) const {
return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Z3);
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> Z3LpSolverFactory<ValueType>::create(std::string const& name) const {
return LpSolverFactory<ValueType>::create(name, storm::solver::LpSolverTypeSelection::Z3);
}
std::unique_ptr<LpSolverFactory> Z3LpSolverFactory::clone() const {
return std::make_unique<Z3LpSolverFactory>(*this);
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> Z3LpSolverFactory<ValueType>::clone() const {
return std::make_unique<Z3LpSolverFactory<ValueType>>(*this);
}
std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType) {
std::unique_ptr<storm::utility::solver::LpSolverFactory> factory(new LpSolverFactory());
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType) {
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> factory(new LpSolverFactory<ValueType>());
return factory->create(name, solvType);
}
@ -103,6 +113,16 @@ namespace storm {
template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;
template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>;
template class LpSolverFactory<double>;
template class LpSolverFactory<storm::RationalNumber>;
template class GlpkLpSolverFactory<double>;
template class GlpkLpSolverFactory<storm::RationalNumber>;
template class GurobiLpSolverFactory<double>;
template class GurobiLpSolverFactory<storm::RationalNumber>;
template class Z3LpSolverFactory<double>;
template class Z3LpSolverFactory<storm::RationalNumber>;
template std::unique_ptr<storm::solver::LpSolver<double>> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType);
template std::unique_ptr<storm::solver::LpSolver<storm::RationalNumber>> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType);
}
}
}

33
src/storm/utility/solver.h
View File

@ -30,7 +30,9 @@ namespace storm {
template<typename V>
class MinMaxLinearEquationSolver;
template<typename ValueType>
class LpSolver;
class SmtSolver;
}
@ -60,6 +62,7 @@ namespace storm {
virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const;
};
template<typename ValueType>
class LpSolverFactory {
public:
/*!
@ -68,32 +71,36 @@ namespace storm {
* @param name The name of the LP solver.
* @return A pointer to the newly created solver.
*/
virtual std::unique_ptr<storm::solver::LpSolver> create(std::string const& name) const;
virtual std::unique_ptr<storm::solver::LpSolver> create(std::string const& name, storm::solver::LpSolverTypeSelection solvType) const;
virtual std::unique_ptr<storm::solver::LpSolver<ValueType>> create(std::string const& name) const;
virtual std::unique_ptr<storm::solver::LpSolver<ValueType>> create(std::string const& name, storm::solver::LpSolverTypeSelection solvType) const;
virtual std::unique_ptr<LpSolverFactory> clone() const;
virtual std::unique_ptr<LpSolverFactory<ValueType>> clone() const;
};
class GlpkLpSolverFactory : public LpSolverFactory {
template<typename ValueType>
class GlpkLpSolverFactory : public LpSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::LpSolver> create(std::string const& name) const override;
virtual std::unique_ptr<LpSolverFactory> clone() const override;
virtual std::unique_ptr<storm::solver::LpSolver<ValueType>> create(std::string const& name) const override;
virtual std::unique_ptr<LpSolverFactory<ValueType>> clone() const override;
};
class GurobiLpSolverFactory : public LpSolverFactory {
template<typename ValueType>
class GurobiLpSolverFactory : public LpSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::LpSolver> create(std::string const& name) const override;
virtual std::unique_ptr<LpSolverFactory> clone() const override;
virtual std::unique_ptr<storm::solver::LpSolver<ValueType>> create(std::string const& name) const override;
virtual std::unique_ptr<LpSolverFactory<ValueType>> clone() const override;
};
class Z3LpSolverFactory : public LpSolverFactory {
template<typename ValueType>
class Z3LpSolverFactory : public LpSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::LpSolver> create(std::string const& name) const override;
virtual std::unique_ptr<LpSolverFactory> clone() const override;
virtual std::unique_ptr<storm::solver::LpSolver<ValueType>> create(std::string const& name) const override;
virtual std::unique_ptr<LpSolverFactory<ValueType>> clone() const override;
};
std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ;
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ;
class SmtSolverFactory {
public:

16
src/test/storm/solver/GlpkLpSolverTest.cpp
View File

@ -16,7 +16,7 @@
#include <cmath>
TEST(GlpkLpSolver, LPOptimizeMax) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -49,7 +49,7 @@ TEST(GlpkLpSolver, LPOptimizeMax) {
}
TEST(GlpkLpSolver, LPOptimizeMin) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Minimize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -82,7 +82,7 @@ TEST(GlpkLpSolver, LPOptimizeMin) {
}
TEST(GlpkLpSolver, MILPOptimizeMax) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -115,7 +115,7 @@ TEST(GlpkLpSolver, MILPOptimizeMax) {
}
TEST(GlpkLpSolver, MILPOptimizeMin) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Minimize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -148,7 +148,7 @@ TEST(GlpkLpSolver, MILPOptimizeMin) {
}
TEST(GlpkLpSolver, LPInfeasible) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -174,7 +174,7 @@ TEST(GlpkLpSolver, LPInfeasible) {
}
TEST(GlpkLpSolver, MILPInfeasible) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -200,7 +200,7 @@ TEST(GlpkLpSolver, MILPInfeasible) {
}
TEST(GlpkLpSolver, LPUnbounded) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -224,7 +224,7 @@ TEST(GlpkLpSolver, LPUnbounded) {
}
TEST(GlpkLpSolver, MILPUnbounded) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GlpkLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;

16
src/test/storm/solver/GurobiLpSolverTest.cpp
View File

@ -11,7 +11,7 @@
#include "storm/storage/expressions/Expressions.h"
TEST(GurobiLpSolver, LPOptimizeMax) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -44,7 +44,7 @@ TEST(GurobiLpSolver, LPOptimizeMax) {
}
TEST(GurobiLpSolver, LPOptimizeMin) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Minimize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -77,7 +77,7 @@ TEST(GurobiLpSolver, LPOptimizeMin) {
}
TEST(GurobiLpSolver, MILPOptimizeMax) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -110,7 +110,7 @@ TEST(GurobiLpSolver, MILPOptimizeMax) {
}
TEST(GurobiLpSolver, MILPOptimizeMin) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Minimize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -143,7 +143,7 @@ TEST(GurobiLpSolver, MILPOptimizeMin) {
}
TEST(GurobiLpSolver, LPInfeasible) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -173,7 +173,7 @@ TEST(GurobiLpSolver, LPInfeasible) {
}
TEST(GurobiLpSolver, MILPInfeasible) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -203,7 +203,7 @@ TEST(GurobiLpSolver, MILPInfeasible) {
}
TEST(GurobiLpSolver, LPUnbounded) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -231,7 +231,7 @@ TEST(GurobiLpSolver, LPUnbounded) {
}
TEST(GurobiLpSolver, MILPUnbounded) {
storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::GurobiLpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;

16
src/test/storm/solver/Z3LpSolverTest.cpp
View File

@ -16,7 +16,7 @@
#include <cmath>
TEST(Z3LpSolver, LPOptimizeMax) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -49,7 +49,7 @@ TEST(Z3LpSolver, LPOptimizeMax) {
}
TEST(Z3LpSolver, LPOptimizeMin) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Minimize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -82,7 +82,7 @@ TEST(Z3LpSolver, LPOptimizeMin) {
}
TEST(Z3LpSolver, MILPOptimizeMax) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -115,7 +115,7 @@ TEST(Z3LpSolver, MILPOptimizeMax) {
}
TEST(Z3LpSolver, MILPOptimizeMin) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Minimize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -148,7 +148,7 @@ TEST(Z3LpSolver, MILPOptimizeMin) {
}
TEST(Z3LpSolver, LPInfeasible) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -174,7 +174,7 @@ TEST(Z3LpSolver, LPInfeasible) {
}
TEST(Z3LpSolver, MILPInfeasible) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -200,7 +200,7 @@ TEST(Z3LpSolver, MILPInfeasible) {
}
TEST(Z3LpSolver, LPUnbounded) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;
@ -224,7 +224,7 @@ TEST(Z3LpSolver, LPUnbounded) {
}
TEST(Z3LpSolver, MILPUnbounded) {
storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize);
storm::solver::Z3LpSolver<double> solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
storm::expressions::Variable y;
storm::expressions::Variable z;

Write Preview
Loading…
Cancel
Save