Browse Source

Picking a default SmtSolver, even if no CoreSettings are available.

tempestpy_adaptions
Tim Quatmann 6 years ago
parent
commit
c6fd015e6c
  1. 14
      src/storm/utility/solver.cpp

14
src/storm/utility/solver.cpp

@ -18,6 +18,7 @@
#include "storm/utility/NumberTraits.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/InvalidOperationException.h"
namespace storm {
namespace utility {
@ -89,7 +90,18 @@ namespace storm {
}
std::unique_ptr<storm::solver::SmtSolver> SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const {
storm::solver::SmtSolverType smtSolverType = storm::settings::getModule<storm::settings::modules::CoreSettings>().getSmtSolver();
storm::solver::SmtSolverType smtSolverType;
if (storm::settings::hasModule<storm::settings::modules::CoreSettings>()) {
smtSolverType = storm::settings::getModule<storm::settings::modules::CoreSettings>().getSmtSolver();
} else {
#ifdef STORM_HAVE_Z3
smtSolverType = storm::solver::SmtSolverType::Z3;
#elif STORM_HAVE_MSAT
smtSolverType = storm::solver::SmtSolverType::Mathsat;
#else
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Requested an SMT solver but none was installed.");
#endif
}
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));

Loading…
Cancel
Save