From ee4b6c96a893d608b1cb317ac7e64fbe0df56963 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 3 Nov 2016 17:58:23 +0100
Subject: [PATCH] Use operator<< from carl

Former-commit-id: 733c029ebe03f2bbd56323deb62913f1ff2da6d7
---
 src/builder/ExplicitDFTModelBuilderApprox.cpp |  8 ++--
 src/utility/logging.h                         | 10 +++++
 src/utility/vector.cpp                        | 43 -------------------
 src/utility/vector.h                          |  6 ---
 4 files changed, 14 insertions(+), 53 deletions(-)
 delete mode 100644 src/utility/vector.cpp

diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 9d802829b..2f302b0db 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -167,10 +167,10 @@ namespace storm {
             // Fix the entries in the transition matrix according to the mapping of ids to row group indices
             STORM_LOG_ASSERT(matrixBuilder.stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped.");
             // TODO Matthias: do not consider all rows?
-            //STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset);
+            STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset);
             matrixBuilder.remap();
 
-            //STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping);
+            STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping);
             STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
             STORM_LOG_DEBUG("Model has " << stateSize << " states");
             STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
@@ -239,7 +239,7 @@ namespace storm {
                     matrixBuilder.stateRemapping[id] = indexRemapping[index];
                 }
             }
-            //STORM_LOG_TRACE("New state remapping: " << matrixBuilder.stateRemapping);
+            STORM_LOG_TRACE("New state remapping: " << matrixBuilder.stateRemapping);
             std::stringstream ss;
             ss << "Index remapping:" << std::endl;
             for (auto tmp : indexRemapping) {
@@ -477,7 +477,7 @@ namespace storm {
                         modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
                     }
                 }
-                //STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
+                STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
 
                 std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma;
                 if (copy) {
diff --git a/src/utility/logging.h b/src/utility/logging.h
index 2fc58a008..951935e46 100644
--- a/src/utility/logging.h
+++ b/src/utility/logging.h
@@ -1,6 +1,16 @@
 #ifndef STORM_UTILITY_LOGGING_H_
 #define STORM_UTILITY_LOGGING_H_
 
+// Include config to know whether CARL is available or not.
+#include "storm-config.h"
+#ifdef STORM_HAVE_CARL
+// Load streaming operator from CARL
+#include <carl/io/streamingOperators.h>
+namespace l3pp {
+    using carl::operator<<;
+}
+#endif
+
 #include <l3pp.h>
 
 #if !defined(STORM_LOG_DISABLE_DEBUG) && !defined(STORM_LOG_DISABLE_TRACE)
diff --git a/src/utility/vector.cpp b/src/utility/vector.cpp
deleted file mode 100644
index 595af193e..000000000
--- a/src/utility/vector.cpp
+++ /dev/null
@@ -1,43 +0,0 @@
-#include "src/utility/vector.h"
-
-// Template was causing problems as Carl has the same function
-/*
-template<typename ValueType>
-std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector) {
-    out << "vector (" << vector.size() << ") [ ";
-    for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
-        out << vector[i] << ", ";
-    }
-    out << vector.back();
-    out << " ]";
-    return out;
-}
-
-// Explicitly instantiate functions.
-template std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
-template std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector);
-*/
-
-std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector) {
-    out << "vector (" << vector.size() << ") [ ";
-    for (size_t i = 0; i + 1 < vector.size(); ++i) {
-        out << vector[i] << ", ";
-    }
-    if (!vector.empty()) {
-        out << vector.back();
-    }
-    out << " ]";
-    return out;
-}
-
-std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector) {
-    out << "vector (" << vector.size() << ") [ ";
-    for (size_t i = 0; i + 1 < vector.size(); ++i) {
-        out << vector[i] << ", ";
-    }
-    if (!vector.empty()) {
-        out << vector.back();
-    }
-    out << " ]";
-    return out;
-}
diff --git a/src/utility/vector.h b/src/utility/vector.h
index 059bf46ac..3257c3516 100644
--- a/src/utility/vector.h
+++ b/src/utility/vector.h
@@ -16,12 +16,6 @@
 #include "src/utility/macros.h"
 #include "src/solver/OptimizationDirection.h"
 
-// Template was causing problems as Carl has the same function
-//template<typename ValueType>
-//std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector);
-std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
-std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector);
-
 namespace storm {
     namespace utility {
         namespace vector {