diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp new file mode 100644 index 000000000..2787a1b6f --- /dev/null +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -0,0 +1,141 @@ +#include "storm/solver/LpMinMaxLinearEquationSolver.h" + +#include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/UnexpectedException.h" + +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)) { + // 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)) { + // Intentionally left empty. + } + + template + bool LpMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + + // Set up the LP solver + std::unique_ptr solver = lpSolverFactory->create("MinMaxLinearEquationSolver"); + solver->setOptimizationDirection(invert(dir)); + + // Create a variable for each row group + std::vector variables; + variables.reserve(this->A.getRowGroupCount()); + 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)); + } else { + variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::convertNumber(this->lowerBound.get()), 1.0)); + } + } else { + if (this->upperBound) { + variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::convertNumber(this->upperBound.get()), 1.0)); + } else { + variables.push_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), 1.0)); + } + } + } + solver->update(); + + // 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])); + for (auto const& entry : this->A.getRow(row)) { + rowConstraint = rowConstraint + (solver->getConstant(storm::utility::convertNumber(entry.getValue())) * variables[entry.getColumn()].getExpression()); + } + if (minimize(dir)) { + rowConstraint = variables[rowGroup].getExpression() <= rowConstraint; + } else { + rowConstraint = variables[rowGroup].getExpression() >= rowConstraint; + } + solver->addConstraint("row" + std::to_string(row), rowConstraint); + } + } + + // Invoke optimization + solver->optimize(); + STORM_LOG_THROW(!solver->isInfeasible(), storm::exceptions::UnexpectedException, "The MinMax equation system is infeasible."); + STORM_LOG_THROW(!solver->isUnbounded(), storm::exceptions::UnexpectedException, "The MinMax equation system is unbounded."); + STORM_LOG_THROW(solver->isOptimal(), storm::exceptions::UnexpectedException, "Unable to find optimal solution for MinMax equation system."); + + // write the solution into the solution vector + STORM_LOG_ASSERT(x.size() == variables.size(), "Dimension of x-vector does not match number of varibales."); + auto xIt = x.begin(); + auto vIt = variables.begin(); + for (; xIt != x.end(); ++xIt, ++vIt) { + *xIt = storm::utility::convertNumber(solver->getContinuousValue(*vIt)); + } + return true; + } + + template + void LpMinMaxLinearEquationSolver::clearCache() const { + StandardMinMaxLinearEquationSolver::clearCache(); + } + + template + 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)) { + // 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)) { + // Intentionally left empty + } + + template + std::unique_ptr> LpMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); + STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); + + std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); + result->setTrackScheduler(this->isTrackSchedulerSet()); + return result; + } + + template + std::unique_ptr> LpMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { + STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); + STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); + + std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); + result->setTrackScheduler(this->isTrackSchedulerSet()); + return result; + } + + template + void LpMinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethodSelection const& newMethod) { + STORM_LOG_THROW(newMethod == MinMaxMethodSelection::LinearProgramming, storm::exceptions::InvalidOperationException, "The factory can only create linear programming based MinMax solvers."); + MinMaxLinearEquationSolverFactory::setMinMaxMethod(newMethod); + } + + template + void LpMinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethod const& newMethod) { + STORM_LOG_THROW(newMethod == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidOperationException, "The factory can only create linear programming based MinMax solvers."); + MinMaxLinearEquationSolverFactory::setMinMaxMethod(newMethod); + } + + template class LpMinMaxLinearEquationSolver; + template class LpMinMaxLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL + template class LpMinMaxLinearEquationSolver; + template class LpMinMaxLinearEquationSolverFactory; +#endif + } +} diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h new file mode 100644 index 000000000..bd15326cb --- /dev/null +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -0,0 +1,41 @@ +#pragma once + +#include "storm/solver/LpSolver.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" +#include "storm/utility/solver.h" + +namespace storm { + namespace solver { + + 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); + + virtual bool solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const override; + + virtual void clearCache() const override; + + private: + 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); + + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + + virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod) override; + virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override; + + private: + std::unique_ptr lpSolverFactory; + }; + } +} diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index fcee52548..bc632ce9d 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -46,18 +46,34 @@ namespace storm { return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::FROMSETTINGS); } + 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); } + 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); } - + + 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); } + 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()); return factory->create(name, solvType); diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 4fbc0745e..3f2bd6f28 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -70,21 +70,27 @@ namespace storm { */ 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; + }; class GlpkLpSolverFactory : public LpSolverFactory { public: virtual std::unique_ptr create(std::string const& name) const override; + virtual std::unique_ptr clone() const override; }; class GurobiLpSolverFactory : public LpSolverFactory { public: virtual std::unique_ptr create(std::string const& name) const override; + virtual std::unique_ptr clone() const override; }; class Z3LpSolverFactory : public LpSolverFactory { public: 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) ;