solver.cpp

Go to the documentation of this file.

#include "storm/utility/solver.h"
 
#include <type_traits>
 
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/MissingLibraryException.h"
#include "storm/solver/Cvc5SmtSolver.h"
#include "storm/solver/GlpkLpSolver.h"
#include "storm/solver/GurobiLpSolver.h"
#include "storm/solver/HighsLpSolver.h"
#include "storm/solver/MathsatSmtSolver.h"
#include "storm/solver/SoplexLpSolver.h"
#include "storm/solver/Z3LpSolver.h"
#include "storm/solver/Z3SmtSolver.h"
#include "storm/utility/NumberTraits.h"
 
namespace storm {
namespace utility {
namespace solver {
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> GlpkLpSolverFactory<ValueType>::create(storm::Environment const& env, std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType>>(
        new storm::solver::GlpkLpSolver<ValueType>(env.solver().glpk(), env.solver().isDebugSet(), name));
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType, true>> GlpkLpSolverFactory<ValueType>::createRaw(storm::Environment const& env,
                                                                                                    std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType, true>>(
        new storm::solver::GlpkLpSolver<ValueType, true>(env.solver().glpk(), env.solver().isDebugSet(), name));
}
 
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> GlpkLpSolverFactory<ValueType>::clone() const {
    return std::make_unique<GlpkLpSolverFactory<ValueType>>(*this);
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> SoplexLpSolverFactory<ValueType>::create(storm::Environment const&, std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType>>(new storm::solver::SoplexLpSolver<ValueType>(name));
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType, true>> SoplexLpSolverFactory<ValueType>::createRaw(storm::Environment const&,
                                                                                                      std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType, true>>(new storm::solver::SoplexLpSolver<ValueType, true>(name));
}
 
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> SoplexLpSolverFactory<ValueType>::clone() const {
    return std::make_unique<SoplexLpSolverFactory<ValueType>>(*this);
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> HighsLpSolverFactory<ValueType>::create(storm::Environment const&, std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType>>(new storm::solver::HighsLpSolver<ValueType>(name));
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType, true>> HighsLpSolverFactory<ValueType>::createRaw(storm::Environment const&, std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType, true>>(new storm::solver::HighsLpSolver<ValueType, true>(name));
}
 
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> HighsLpSolverFactory<ValueType>::clone() const {
    return std::make_unique<HighsLpSolverFactory<ValueType>>(*this);
}
 
template<typename ValueType>
std::shared_ptr<storm::solver::GurobiEnvironment> const& GurobiLpSolverFactory<ValueType>::getOrCreateGurobiEnvironment(storm::Environment const& env) const {
    if (!environment) {
        environment = std::make_shared<storm::solver::GurobiEnvironment>();
        environment->initialize(env.solver().gurobi(), env.solver().isDebugSet());
    }
    return environment;
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> GurobiLpSolverFactory<ValueType>::create(storm::Environment const& env, std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType>>(new storm::solver::GurobiLpSolver<ValueType>(getOrCreateGurobiEnvironment(env), name));
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType, true>> GurobiLpSolverFactory<ValueType>::createRaw(storm::Environment const& env,
                                                                                                      std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType, true>>(
        new storm::solver::GurobiLpSolver<ValueType, true>(getOrCreateGurobiEnvironment(env), name));
}
 
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> GurobiLpSolverFactory<ValueType>::clone() const {
    return std::make_unique<GurobiLpSolverFactory<ValueType>>(*this);
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> Z3LpSolverFactory<ValueType>::create(storm::Environment const&, std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType>>(new storm::solver::Z3LpSolver<ValueType>(name));
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType, true>> Z3LpSolverFactory<ValueType>::createRaw(storm::Environment const&, std::string const& name) const {
    return std::unique_ptr<storm::solver::LpSolver<ValueType, true>>(new storm::solver::Z3LpSolver<ValueType, true>(name));
}
 
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> Z3LpSolverFactory<ValueType>::clone() const {
    return std::make_unique<Z3LpSolverFactory<ValueType>>(*this);
}
 
template<typename ValueType>
std::unique_ptr<LpSolverFactory<ValueType>> getLpSolverFactory(storm::Environment const& env, storm::solver::LpSolverTypeSelection solvType) {
    storm::solver::LpSolverType t;
    if (solvType == storm::solver::LpSolverTypeSelection::FROMSETTINGS) {
        t = env.solver().getLpSolverType();
        bool useExact = storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact();
        if (useExact && t != storm::solver::LpSolverType::Z3 && env.solver().isLpSolverTypeSetFromDefaultValue()) {
            t = storm::solver::LpSolverType::Z3;
        }
    } else {
        t = convert(solvType);
    }
    switch (t) {
        case storm::solver::LpSolverType::Glpk:
            return std::unique_ptr<LpSolverFactory<ValueType>>(new GlpkLpSolverFactory<ValueType>());
        case storm::solver::LpSolverType::Gurobi:
            return std::unique_ptr<LpSolverFactory<ValueType>>(new GurobiLpSolverFactory<ValueType>());
        case storm::solver::LpSolverType::Highs:
            if constexpr (std::is_same_v<ValueType, double>) {
                return std::unique_ptr<LpSolverFactory<ValueType>>(new HighsLpSolverFactory<ValueType>());
            } else {
                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "The HiGHS LP solver only supports double precision.");
            }
            break;
        case storm::solver::LpSolverType::Soplex:
            return std::unique_ptr<LpSolverFactory<ValueType>>(new SoplexLpSolverFactory<ValueType>());
        case storm::solver::LpSolverType::Z3:
            return std::unique_ptr<LpSolverFactory<ValueType>>(new Z3LpSolverFactory<ValueType>());
    }
    return nullptr;
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType>> getLpSolver(storm::Environment const& env, std::string const& name,
                                                                storm::solver::LpSolverTypeSelection solvType) {
    std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> factory = getLpSolverFactory<ValueType>(env, solvType);
    return factory->create(env, name);
}
 
template<typename ValueType>
std::unique_ptr<storm::solver::LpSolver<ValueType, true>> getRawLpSolver(storm::Environment const& env, std::string const& name,
                                                                         storm::solver::LpSolverTypeSelection solvType) {
    std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> factory = getLpSolverFactory<ValueType>(env, solvType);
    return factory->createRaw(env, name);
}
 
namespace {
std::unique_ptr<storm::solver::SmtSolver> createSmtSolver(storm::solver::SmtSolverType smtSolverType, storm::expressions::ExpressionManager& manager) {
    switch (smtSolverType) {
        case storm::solver::SmtSolverType::Z3:
            return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Z3SmtSolver(manager));
        case storm::solver::SmtSolverType::Mathsat:
            return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::MathsatSmtSolver(manager));
        case storm::solver::SmtSolverType::Cvc5:
            return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Cvc5SmtSolver(manager));
    }
    STORM_LOG_THROW_UNCONDITIONALLY(storm::exceptions::MissingLibraryException, "Requested an SMT solver but none was installed.");
}
}  // namespace
 
std::unique_ptr<storm::solver::SmtSolver> SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
    // Without an environment to consult, we use the SMT solver that was selected at compile time.
#ifdef STORM_DEFAULT_SMT_SOLVER_Z3
    return createSmtSolver(storm::solver::SmtSolverType::Z3, manager);
#elif defined STORM_DEFAULT_SMT_SOLVER_MATHSAT
    return createSmtSolver(storm::solver::SmtSolverType::Mathsat, manager);
#elif defined STORM_DEFAULT_SMT_SOLVER_CVC5
    return createSmtSolver(storm::solver::SmtSolverType::Cvc5, manager);
#else
    STORM_LOG_THROW_UNCONDITIONALLY(storm::exceptions::MissingLibraryException, "Requested an SMT solver but none was installed.");
#endif
}
 
std::unique_ptr<storm::solver::SmtSolver> SmtSolverFactory::create(storm::Environment const& env, storm::expressions::ExpressionManager& manager) const {
    // If an environment is available, we use the SMT solver that was selected in it.
    return createSmtSolver(env.solver().getSmtSolverType(), manager);
}
 
std::unique_ptr<storm::solver::SmtSolver> Z3SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
    return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Z3SmtSolver(manager));
}
 
std::unique_ptr<storm::solver::SmtSolver> Z3SmtSolverFactory::create(storm::Environment const&, storm::expressions::ExpressionManager& manager) const {
    return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Z3SmtSolver(manager));
}
 
std::unique_ptr<storm::solver::SmtSolver> MathsatSmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
    return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::MathsatSmtSolver(manager));
}
 
std::unique_ptr<storm::solver::SmtSolver> MathsatSmtSolverFactory::create(storm::Environment const&, storm::expressions::ExpressionManager& manager) const {
    return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::MathsatSmtSolver(manager));
}
 
std::unique_ptr<storm::solver::SmtSolver> Cvc5SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
    return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Cvc5SmtSolver(manager));
}
 
std::unique_ptr<storm::solver::SmtSolver> Cvc5SmtSolverFactory::create(storm::Environment const&, storm::expressions::ExpressionManager& manager) const {
    return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Cvc5SmtSolver(manager));
}
 
std::unique_ptr<storm::solver::SmtSolver> getSmtSolver(storm::expressions::ExpressionManager& manager) {
    std::unique_ptr<storm::utility::solver::SmtSolverFactory> factory = std::make_unique<SmtSolverFactory>();
    return factory->create(manager);
}
 
std::unique_ptr<storm::solver::SmtSolver> getSmtSolver(storm::Environment const& env, storm::expressions::ExpressionManager& manager) {
    std::unique_ptr<storm::utility::solver::SmtSolverFactory> factory = std::make_unique<SmtSolverFactory>();
    return factory->create(env, manager);
}
 
template class LpSolverFactory<double>;
template class LpSolverFactory<storm::RationalNumber>;
template class GlpkLpSolverFactory<double>;
template class GlpkLpSolverFactory<storm::RationalNumber>;
template class GurobiLpSolverFactory<double>;
template class GurobiLpSolverFactory<storm::RationalNumber>;
template class Z3LpSolverFactory<double>;
template class Z3LpSolverFactory<storm::RationalNumber>;
template class SoplexLpSolverFactory<double>;
template class SoplexLpSolverFactory<storm::RationalNumber>;
template class HighsLpSolverFactory<double>;
 
template std::unique_ptr<LpSolverFactory<double>> getLpSolverFactory(storm::Environment const& env, storm::solver::LpSolverTypeSelection solvType);
template std::unique_ptr<LpSolverFactory<storm::RationalNumber>> getLpSolverFactory(storm::Environment const& env,
                                                                                    storm::solver::LpSolverTypeSelection solvType);
template std::unique_ptr<storm::solver::LpSolver<double>> getLpSolver(storm::Environment const& env, std::string const& name,
                                                                      storm::solver::LpSolverTypeSelection solvType);
template std::unique_ptr<storm::solver::LpSolver<storm::RationalNumber>> getLpSolver(storm::Environment const& env, std::string const& name,
                                                                                     storm::solver::LpSolverTypeSelection solvType);
template std::unique_ptr<storm::solver::LpSolver<double, true>> getRawLpSolver(storm::Environment const& env, std::string const& name,
                                                                               storm::solver::LpSolverTypeSelection solvType);
template std::unique_ptr<storm::solver::LpSolver<storm::RationalNumber, true>> getRawLpSolver(storm::Environment const& env, std::string const& name,
                                                                                              storm::solver::LpSolverTypeSelection solvType);
}  // namespace solver
}  // namespace utility
}  // namespace storm