From bf727a28fd925ded1e54918377f4208bcb7ad6f4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 13 Oct 2017 09:18:38 +0200
Subject: [PATCH] remove debug output and choose sylvan automatically in exact
 mode

---
 src/storm-cli-utilities/model-handling.h       | 8 ++++++--
 src/storm/settings/modules/CoreSettings.cpp    | 4 ++++
 src/storm/settings/modules/CoreSettings.h      | 7 +++++++
 src/storm/solver/EigenLinearEquationSolver.cpp | 7 -------
 4 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 5bfb7ab7a..f702667b7 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -645,8 +645,12 @@ namespace storm {
         template <typename ValueType>
         void processInputWithValueType(SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
-            
-            if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
+            auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+
+            if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && generalSettings.isExactSet()) {
+                STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);
+            } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
                 processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, ValueType>(input);
             } else {
                 STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library.");
diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp
index 836943dae..b01aee3f7 100644
--- a/src/storm/settings/modules/CoreSettings.cpp
+++ b/src/storm/settings/modules/CoreSettings.cpp
@@ -129,6 +129,10 @@ namespace storm {
                 }
             }
             
+            bool CoreSettings::isDdLibraryTypeSetFromDefaultValue() const {
+                return !this->getOption(ddLibraryOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(ddLibraryOptionName).getArgumentByName("name").wasSetFromDefaultValue();
+            }
+            
             bool CoreSettings::isShowStatisticsSet() const {
                 return this->getOption(statisticsOptionName).getHasOptionBeenSet();
             }
diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h
index 1880ee109..e0359bf62 100644
--- a/src/storm/settings/modules/CoreSettings.h
+++ b/src/storm/settings/modules/CoreSettings.h
@@ -109,6 +109,13 @@ namespace storm {
                  */
                 storm::dd::DdType getDdLibraryType() const;
                 
+                /*!
+                 * Retrieves whether the selected DD library is set from its default value.
+                 *
+                 * @return True iff if it is set from its default value.
+                 */
+                bool isDdLibraryTypeSetFromDefaultValue() const;
+                
                 /*!
                  * Retrieves whether statistics are to be shown for counterexample generation.
                  *
diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp
index c285423e1..16b0faf42 100644
--- a/src/storm/solver/EigenLinearEquationSolver.cpp
+++ b/src/storm/solver/EigenLinearEquationSolver.cpp
@@ -359,13 +359,6 @@ namespace storm {
             solver.compute(*eigenA);
             solver._solve_impl(eigenB, eigenX);
             
-            std::cout << "solution" << std::endl;
-            uint64_t pos = 0;
-            for (auto const& e : x) {
-                std::cout << "[" << pos << "] " << e << std::endl;
-                ++pos;
-            }
-
             return solver.info() == StormEigen::ComputationInfo::Success;
         }