From 9ca14a54fcb78ed070bd10113479f1552b7b8139 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 3 Aug 2017 16:24:26 +0200 Subject: [PATCH] templated the LpSolvers --- .../MILPMinimalLabelSetGenerator.h | 42 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 8 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 8 +- .../MILPPermissiveSchedulers.h | 4 +- .../permissivesched/PermissiveSchedulers.cpp | 2 +- src/storm/solver/GlpkLpSolver.cpp | 117 +++-- src/storm/solver/GlpkLpSolver.h | 49 +- src/storm/solver/GurobiLpSolver.cpp | 350 +++++++++------ src/storm/solver/GurobiLpSolver.h | 27 +- .../solver/LpMinMaxLinearEquationSolver.cpp | 26 +- .../solver/LpMinMaxLinearEquationSolver.h | 12 +- src/storm/solver/LpSolver.cpp | 14 +- src/storm/solver/LpSolver.h | 25 +- .../solver/MinMaxLinearEquationSolver.cpp | 2 +- src/storm/solver/Z3LpSolver.cpp | 423 +++++++----------- src/storm/solver/Z3LpSolver.h | 39 +- src/storm/storage/geometry/NativePolytope.cpp | 12 +- src/storm/utility/solver.cpp | 64 ++- src/storm/utility/solver.h | 33 +- src/test/storm/solver/GlpkLpSolverTest.cpp | 16 +- src/test/storm/solver/GurobiLpSolverTest.cpp | 16 +- src/test/storm/solver/Z3LpSolverTest.cpp | 16 +- 22 files changed, 671 insertions(+), 634 deletions(-) diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h index c028f0e5a..dff7a2808 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h @@ -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, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { + static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { std::stringstream variableNameBuffer; std::unordered_map 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>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map> 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, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation) { + static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map 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, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) { + static std::pair, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map 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 createVirtualInitialStateVariable(storm::solver::LpSolver& solver) { + static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& 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, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map 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, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map, 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 const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static VariableInformation createVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp 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& 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& 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 const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> 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& 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 const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::sparse::Mdp 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::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 const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertUnproblematicStateReachable(storm::solver::LpSolver& solver, storm::models::sparse::Mdp 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& 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 const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { storm::storage::SparseMatrix 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 const& mdp, std::vector> 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& solver, storm::models::sparse::Mdp const& mdp, std::vector> 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 getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { + static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { boost::container::flat_set 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 getChoices(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static std::map getChoices(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { std::map 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 getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, VariableInformation const& variableInformation) { + static std::pair getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp 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 solver = storm::utility::solver::getLpSolver("MinimalLabelSetCounterexample"); + std::shared_ptr> solver = storm::utility::solver::getLpSolver("MinimalLabelSetCounterexample"); // (4.1) Create variables. VariableInformation variableInformation = createVariables(*solver, mdp, stateInformation, choiceInformation); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 1ca0b3728..3aaeec73d 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -427,8 +427,8 @@ namespace storm { template ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) { - std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); - std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); + std::unique_ptr> lpSolverFactory(new storm::utility::solver::LpSolverFactory()); + std::unique_ptr> 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()); solver->update(); // Now we encode the problem as constraints. @@ -487,7 +487,7 @@ namespace storm { } solver->optimize(); - return storm::utility::convertNumber(solver->getContinuousValue(k)); + return solver->getContinuousValue(k); } template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index c8dab63c4..2b186fdca 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -801,7 +801,7 @@ namespace storm { template template ValueType SparseMdpPrctlHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) { - std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); + std::shared_ptr> solver = storm::utility::solver::getLpSolver("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(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(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(solver->getContinuousValue(lambda)); + return solver->getContinuousValue(lambda); } template diff --git a/src/storm/permissivesched/MILPPermissiveSchedulers.h b/src/storm/permissivesched/MILPPermissiveSchedulers.h index fe5a48e11..ed85e4d9f 100644 --- a/src/storm/permissivesched/MILPPermissiveSchedulers.h +++ b/src/storm/permissivesched/MILPPermissiveSchedulers.h @@ -25,7 +25,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation private: bool mCalledOptimizer = false; - storm::solver::LpSolver& solver; + storm::solver::LpSolver& solver; std::unordered_map multistrategyVariables; std::unordered_map mProbVariables; std::unordered_map mAlphaVariables; @@ -34,7 +34,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation public: - MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) + MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) : PermissiveSchedulerComputation(mdp, goalstates, sinkstates), solver(milpsolver) { diff --git a/src/storm/permissivesched/PermissiveSchedulers.cpp b/src/storm/permissivesched/PermissiveSchedulers.cpp index 1a7e7061b..5454eeb6e 100644 --- a/src/storm/permissivesched/PermissiveSchedulers.cpp +++ b/src/storm/permissivesched/PermissiveSchedulers.cpp @@ -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("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); MilpPermissiveSchedulerComputation> 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()); diff --git a/src/storm/solver/GlpkLpSolver.cpp b/src/storm/solver/GlpkLpSolver.cpp index 51faf7eea..707883c05 100644 --- a/src/storm/solver/GlpkLpSolver.cpp +++ b/src/storm/solver/GlpkLpSolver.cpp @@ -1,13 +1,13 @@ #include "storm/solver/GlpkLpSolver.h" -#ifdef STORM_HAVE_GLPK - #include +#include #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 + 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 + 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() { // 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 + GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) { + template + GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } - GlpkLpSolver::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) { + template + GlpkLpSolver::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) { // Intentionally left empty. } - GlpkLpSolver::~GlpkLpSolver() { + template + GlpkLpSolver::~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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + storm::expressions::Variable GlpkLpSolver::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 + void GlpkLpSolver::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(lowerBound), storm::utility::convertNumber(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(objectiveFunctionCoefficient)); this->variableToIndexMap.emplace(variable, this->nextVariableIndex); ++this->nextVariableIndex; } - void GlpkLpSolver::update() const { + template + void GlpkLpSolver::update() const { // Intentionally left empty. } - void GlpkLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + template + void GlpkLpSolver::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 + void GlpkLpSolver::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 + bool GlpkLpSolver::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 + bool GlpkLpSolver::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 + bool GlpkLpSolver::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 + ValueType GlpkLpSolver::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(variableIndexPair->second)); } - return value; + return storm::utility::convertNumber(value); } - int_fast64_t GlpkLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + template + int_fast64_t GlpkLpSolver::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(value); } - bool GlpkLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { + template + bool GlpkLpSolver::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(value); } - double GlpkLpSolver::getObjectiveValue() const { + template + ValueType GlpkLpSolver::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(value); } - void GlpkLpSolver::writeModelToFile(std::string const& filename) const { + template + void GlpkLpSolver::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; + template class GlpkLpSolver; +#endif } } -#endif diff --git a/src/storm/solver/GlpkLpSolver.h b/src/storm/solver/GlpkLpSolver.h index 63be0ede7..a0c30b39a 100644 --- a/src/storm/solver/GlpkLpSolver.h +++ b/src/storm/solver/GlpkLpSolver.h @@ -18,7 +18,8 @@ namespace storm { /*! * A class that implements the LpSolver interface using glpk as the background solver. */ - class GlpkLpSolver : public LpSolver { + template + class GlpkLpSolver : public LpSolver { 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."; } diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index 76713be08..23866ea46 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/src/storm/solver/GurobiLpSolver.cpp @@ -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 + GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(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 + GurobiLpSolver::GurobiLpSolver(std::string const& name) : GurobiLpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - GurobiLpSolver::GurobiLpSolver(OptimizationDirection const& optDir) : GurobiLpSolver("", optDir) { + template + GurobiLpSolver::GurobiLpSolver(OptimizationDirection const& optDir) : GurobiLpSolver("", optDir) { // Intentionally left empty. } - GurobiLpSolver::GurobiLpSolver() : GurobiLpSolver("", OptimizationDirection::Minimize) { + template + GurobiLpSolver::GurobiLpSolver() : GurobiLpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } - GurobiLpSolver::~GurobiLpSolver() { + template + GurobiLpSolver::~GurobiLpSolver() { // Dispose of the objects allocated inside Gurobi. GRBfreemodel(model); GRBfreeenv(env); } - void GurobiLpSolver::setGurobiEnvironmentProperties() const { + template + void GurobiLpSolver::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 + void GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + void GurobiLpSolver::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(objectiveFunctionCoefficient), storm::utility::convertNumber(lowerBound), storm::utility::convertNumber(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 + void GurobiLpSolver::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 + void GurobiLpSolver::optimize() const { // First incorporate all recent changes. this->update(); @@ -203,9 +224,10 @@ namespace storm { this->currentModelHasBeenOptimized = true; } - bool GurobiLpSolver::isInfeasible() const { + template + bool GurobiLpSolver::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::isInfeasible: model has not been optimized."; } int optimalityStatus = 0; @@ -231,9 +253,10 @@ namespace storm { return optimalityStatus == GRB_INFEASIBLE; } - bool GurobiLpSolver::isUnbounded() const { + template + bool GurobiLpSolver::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::isUnbounded: model has not been optimized."; } int optimalityStatus = 0; @@ -259,7 +282,8 @@ namespace storm { return optimalityStatus == GRB_UNBOUNDED; } - bool GurobiLpSolver::isOptimal() const { + template + bool GurobiLpSolver::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 + ValueType GurobiLpSolver::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(value); } - int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + template + int_fast64_t GurobiLpSolver::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(value); } - bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { + template + bool GurobiLpSolver::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(value); } - double GurobiLpSolver::getObjectiveValue() const { + template + ValueType GurobiLpSolver::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(value); } - void GurobiLpSolver::writeModelToFile(std::string const& filename) const { + template + void GurobiLpSolver::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 + void GurobiLpSolver::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 + 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."; + } + + template + 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."; + } + + template + 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."; + } + + template + 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."; + } + + template + GurobiLpSolver::~GurobiLpSolver() { + + } + + template + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + storm::expressions::Variable GurobiLpSolver::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 + 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."; + } + + template + 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."; + } + + template + 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."; + } + + template + 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."; + } + + template + 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."; + } + + template + 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."; + } + + template + ValueType 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."; + } + + template + 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."; + } + + template + 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."; + } + + template + ValueType 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."; + } + + template + 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."; + } - 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 + 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."; + } -#endif +#endif + template class GurobiLpSolver; + template class GurobiLpSolver; } } diff --git a/src/storm/solver/GurobiLpSolver.h b/src/storm/solver/GurobiLpSolver.h index 41d6e3800..f1ca786f3 100644 --- a/src/storm/solver/GurobiLpSolver.h +++ b/src/storm/solver/GurobiLpSolver.h @@ -22,7 +22,8 @@ namespace storm { /*! * A class that implements the LpSolver interface using Gurobi. */ - class GurobiLpSolver : public LpSolver { + template + class GurobiLpSolver : public LpSolver { 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; diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index bb3ae4887..35de0902d 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -10,12 +10,12 @@ namespace storm { namespace solver { template - LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty. } template - LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty. } @@ -23,7 +23,7 @@ namespace storm { bool LpMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { // Set up the LP solver - std::unique_ptr solver = lpSolverFactory->create(""); + std::unique_ptr> 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(this->lowerBound.get()), storm::utility::convertNumber(this->upperBound.get()), 1.0)); + variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one())); } else { - variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::convertNumber(this->lowerBound.get()), 1.0)); + variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), storm::utility::one())); } } else { if (this->upperBound) { - variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::convertNumber(this->upperBound.get()), 1.0)); + variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->upperBound.get(), storm::utility::one())); } 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())); } } } @@ -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(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(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(solver->getContinuousValue(*vIt)); + *xIt = solver->getContinuousValue(*vIt); } // If requested, we store the scheduler for retrieval. @@ -104,17 +104,17 @@ namespace storm { } template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique()) { + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique>()) { // Intentionally left empty } template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty } template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty } diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index bd15326cb..540fe89c1 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -10,23 +10,23 @@ namespace storm { template class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { public: - LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr&& lpSolverFactory); - LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr&& lpSolverFactory); + LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); + LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); virtual bool solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const override; virtual void clearCache() const override; private: - std::unique_ptr lpSolverFactory; + std::unique_ptr> lpSolverFactory; }; template class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { public: LpMinMaxLinearEquationSolverFactory(bool trackScheduler = false); - LpMinMaxLinearEquationSolverFactory(std::unique_ptr&& lpSolverFactory, bool trackScheduler = false); - LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr&& lpSolverFactory, bool trackScheduler = false); + LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory, bool trackScheduler = false); + LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory, bool trackScheduler = false); virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; @@ -35,7 +35,7 @@ namespace storm { virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override; private: - std::unique_ptr lpSolverFactory; + std::unique_ptr> lpSolverFactory; }; } } diff --git a/src/storm/solver/LpSolver.cpp b/src/storm/solver/LpSolver.cpp index 1828d0a43..7d5e6c60a 100644 --- a/src/storm/solver/LpSolver.cpp +++ b/src/storm/solver/LpSolver.cpp @@ -8,16 +8,24 @@ namespace storm { namespace solver { - LpSolver::LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(OptimizationDirection::Minimize) { + + template + LpSolver::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 + LpSolver::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 + storm::expressions::Expression LpSolver::getConstant(ValueType value) const { return manager->rational(value); } + + template class LpSolver; + template class LpSolver; + } } diff --git a/src/storm/solver/LpSolver.h b/src/storm/solver/LpSolver.h index 398169085..7ec7cb906 100644 --- a/src/storm/solver/LpSolver.h +++ b/src/storm/solver/LpSolver.h @@ -18,6 +18,7 @@ namespace storm { /*! * An interface that captures the functionality of an LP solver. */ + template 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 update @@ -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. diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 180f91cf8..08c70bd58 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -197,7 +197,7 @@ namespace storm { } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(std::forward(matrix)); } else if (method == MinMaxMethod::LinearProgramming) { - result = std::make_unique>(std::forward(matrix), std::make_unique>(), std::make_unique()); + result = std::make_unique>(std::forward(matrix), std::make_unique>(), std::make_unique>()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index 45ffbd7be..1dcc1a7f0 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -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 + Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(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()); } - Z3LpSolver::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) { + template + Z3LpSolver::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - Z3LpSolver::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) { + template + Z3LpSolver::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) { // Intentionally left empty. } - Z3LpSolver::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) { + template + Z3LpSolver::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } - Z3LpSolver::~Z3LpSolver() { + template + Z3LpSolver::~Z3LpSolver() { // Intentionally left empty. } - void Z3LpSolver::update() const { + template + void Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one())))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + template + void Z3LpSolver::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 + void Z3LpSolver::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 + bool Z3LpSolver::isInfeasible() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::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 + bool Z3LpSolver::isUnbounded() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::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 + bool Z3LpSolver::isOptimal() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isOptimal: model has not been optimized."); return !lastCheckInfeasible && !lastCheckUnbounded; } - storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { + template + storm::expressions::Expression Z3LpSolver::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 + ValueType Z3LpSolver::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(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(value.getBaseExpression().asRationalLiteralExpression().getValue()); } - int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + template + int_fast64_t Z3LpSolver::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 + bool Z3LpSolver::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 + ValueType Z3LpSolver::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(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(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 + 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."); } - 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 + 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."; } - 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 + 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."; } - 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 + 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."; } - 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 + 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."; } - 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 + Z3LpSolver::~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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one())))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; + template + storm::expressions::Variable Z3LpSolver::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(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 + storm::expressions::Variable Z3LpSolver::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(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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + storm::expressions::Variable Z3LpSolver::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 + 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."; + } - 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 + 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."; + } - 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 + 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."; + } - 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 + 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."; + } - 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 + 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."; + } - 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 + 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."; + } + + template + 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."; + } - 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 + ValueType 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."; + } - 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 + 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."; + } - 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 + 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."; + } - 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 + ValueType 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 + 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."; + } +#endif -#endif + template class Z3LpSolver; + template class Z3LpSolver; } } diff --git a/src/storm/solver/Z3LpSolver.h b/src/storm/solver/Z3LpSolver.h index d3a04598f..38922987c 100644 --- a/src/storm/solver/Z3LpSolver.h +++ b/src/storm/solver/Z3LpSolver.h @@ -21,7 +21,8 @@ namespace storm { /*! * A class that implements the LpSolver interface using Z3. */ - class Z3LpSolver : public LpSolver { + template + class Z3LpSolver : public LpSolver { 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; diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index 11ed760fc..1f7c94567 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -1,4 +1,3 @@ -#include #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 solver(storm::solver::OptimizationDirection::Maximize); std::vector 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((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 solver(storm::solver::OptimizationDirection::Maximize); std::vector 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(direction(i)))); } std::vector 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(solver.getExactContinuousValue(variables[i])); + result.first(i) = solver.getContinuousValue(variables[i]); } return result; } else { diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index bc632ce9d..763bc9826 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -27,7 +27,8 @@ namespace storm { return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); } - std::unique_ptr LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { + template + std::unique_ptr> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { t = storm::settings::getModule().getLpSolver(); @@ -35,47 +36,56 @@ namespace storm { t = convert(solvT); } switch (t) { - case storm::solver::LpSolverType::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); - case storm::solver::LpSolverType::Glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); - case storm::solver::LpSolverType::Z3: return std::unique_ptr(new storm::solver::Z3LpSolver(name)); + case storm::solver::LpSolverType::Gurobi: return std::unique_ptr>(new storm::solver::GurobiLpSolver(name)); + case storm::solver::LpSolverType::Glpk: return std::unique_ptr>(new storm::solver::GlpkLpSolver(name)); + case storm::solver::LpSolverType::Z3: return std::unique_ptr>(new storm::solver::Z3LpSolver(name)); } return nullptr; } - std::unique_ptr LpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::FROMSETTINGS); + template + std::unique_ptr> LpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::FROMSETTINGS); } - std::unique_ptr LpSolverFactory::clone() const { - return std::make_unique(*this); + template + std::unique_ptr> LpSolverFactory::clone() const { + return std::make_unique>(*this); } - std::unique_ptr GlpkLpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Glpk); + template + std::unique_ptr> GlpkLpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Glpk); } - std::unique_ptr GlpkLpSolverFactory::clone() const { - return std::make_unique(*this); + template + std::unique_ptr> GlpkLpSolverFactory::clone() const { + return std::make_unique>(*this); } - std::unique_ptr GurobiLpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Gurobi); + template + std::unique_ptr> GurobiLpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Gurobi); } - std::unique_ptr GurobiLpSolverFactory::clone() const { - return std::make_unique(*this); + template + std::unique_ptr> GurobiLpSolverFactory::clone() const { + return std::make_unique>(*this); } - std::unique_ptr Z3LpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Z3); + template + std::unique_ptr> Z3LpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Z3); } - std::unique_ptr Z3LpSolverFactory::clone() const { - return std::make_unique(*this); + template + std::unique_ptr> Z3LpSolverFactory::clone() const { + return std::make_unique>(*this); } - std::unique_ptr getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType) { - std::unique_ptr factory(new LpSolverFactory()); + template + std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType) { + std::unique_ptr> factory(new LpSolverFactory()); return factory->create(name, solvType); } @@ -103,6 +113,16 @@ namespace storm { template class SymbolicGameSolverFactory; template class SymbolicGameSolverFactory; + template class LpSolverFactory; + template class LpSolverFactory; + template class GlpkLpSolverFactory; + template class GlpkLpSolverFactory; + template class GurobiLpSolverFactory; + template class GurobiLpSolverFactory; + template class Z3LpSolverFactory; + template class Z3LpSolverFactory; + template std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType); + template std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType); } } } diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 3f2bd6f28..757305e29 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -30,7 +30,9 @@ namespace storm { template class MinMaxLinearEquationSolver; + template class LpSolver; + class SmtSolver; } @@ -60,6 +62,7 @@ namespace storm { virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; + template 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 create(std::string const& name) const; - virtual std::unique_ptr create(std::string const& name, storm::solver::LpSolverTypeSelection solvType) const; + virtual std::unique_ptr> create(std::string const& name) const; + virtual std::unique_ptr> create(std::string const& name, storm::solver::LpSolverTypeSelection solvType) const; - virtual std::unique_ptr clone() const; + virtual std::unique_ptr> clone() const; }; - class GlpkLpSolverFactory : public LpSolverFactory { + template + class GlpkLpSolverFactory : public LpSolverFactory { public: - virtual std::unique_ptr create(std::string const& name) const override; - virtual std::unique_ptr clone() const override; + virtual std::unique_ptr> create(std::string const& name) const override; + virtual std::unique_ptr> clone() const override; }; - class GurobiLpSolverFactory : public LpSolverFactory { + template + class GurobiLpSolverFactory : public LpSolverFactory { public: - virtual std::unique_ptr create(std::string const& name) const override; - virtual std::unique_ptr clone() const override; + virtual std::unique_ptr> create(std::string const& name) const override; + virtual std::unique_ptr> clone() const override; }; - class Z3LpSolverFactory : public LpSolverFactory { + template + class Z3LpSolverFactory : public LpSolverFactory { public: - virtual std::unique_ptr create(std::string const& name) const override; - virtual std::unique_ptr clone() const override; + virtual std::unique_ptr> create(std::string const& name) const override; + virtual std::unique_ptr> clone() const override; }; - std::unique_ptr getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ; + template + std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ; class SmtSolverFactory { public: diff --git a/src/test/storm/solver/GlpkLpSolverTest.cpp b/src/test/storm/solver/GlpkLpSolverTest.cpp index 404e76032..8e751aacf 100644 --- a/src/test/storm/solver/GlpkLpSolverTest.cpp +++ b/src/test/storm/solver/GlpkLpSolverTest.cpp @@ -16,7 +16,7 @@ #include TEST(GlpkLpSolver, LPOptimizeMax) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GlpkLpSolver 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 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 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 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 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 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 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 solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; diff --git a/src/test/storm/solver/GurobiLpSolverTest.cpp b/src/test/storm/solver/GurobiLpSolverTest.cpp index b0163e3d9..b879aa30b 100644 --- a/src/test/storm/solver/GurobiLpSolverTest.cpp +++ b/src/test/storm/solver/GurobiLpSolverTest.cpp @@ -11,7 +11,7 @@ #include "storm/storage/expressions/Expressions.h" TEST(GurobiLpSolver, LPOptimizeMax) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GurobiLpSolver 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 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 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 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 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 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 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 solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; diff --git a/src/test/storm/solver/Z3LpSolverTest.cpp b/src/test/storm/solver/Z3LpSolverTest.cpp index b8786013b..b6ced15bc 100644 --- a/src/test/storm/solver/Z3LpSolverTest.cpp +++ b/src/test/storm/solver/Z3LpSolverTest.cpp @@ -16,7 +16,7 @@ #include TEST(Z3LpSolver, LPOptimizeMax) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver 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 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 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 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 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 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 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 solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z;