From c6fd015e6c11645f2df6875ef6028a8fdf1e72f0 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 18 Mar 2019 14:09:37 +0100
Subject: [PATCH] Picking a default SmtSolver, even if no CoreSettings are
available.
---
src/storm/utility/solver.cpp | 14 +++++++++++++-
1 file changed, 13 insertions(+), 1 deletion(-)
diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp
index 67bef02ef..e944d4bd6 100644
--- a/src/storm/utility/solver.cpp
+++ b/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));