From 1ec453e587605bbba7d30a713ed584635089651d Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 30 Jul 2015 18:13:02 +0200
Subject: [PATCH] support for intervals in matrices

Former-commit-id: e8d9d851627009d67be9ded4ba50b9b4015e3572
---
 src/adapters/CarlAdapter.h   |  7 +++++++
 src/storage/SparseMatrix.cpp | 37 +++++++++++++++++++++---------------
 src/utility/constants.cpp    |  3 +++
 3 files changed, 32 insertions(+), 15 deletions(-)

diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h
index 81ddf2f8a..856ca1504 100644
--- a/src/adapters/CarlAdapter.h
+++ b/src/adapters/CarlAdapter.h
@@ -34,6 +34,12 @@ namespace carl {
         std::hash<Pol> h;
         return h(f.nominator()) ^ h(f.denominator());
     }
+    
+    template<typename Number>
+    inline size_t hash_value(carl::Interval<Number> const& i) {
+        std::hash<Interval<Number>> h;
+        return h(i);
+    }
 }
 
 namespace storm {
@@ -43,6 +49,7 @@ namespace storm {
     typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
     typedef carl::Relation CompareRelation;
     typedef carl::RationalFunction<Polynomial> RationalFunction;
+    typedef carl::Interval<double> Interval;
 }
 
 #endif
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 58a842cd3..6684db2a8 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -993,30 +993,37 @@ namespace storm {
         }
         
         // Explicitly instantiate the entry, builder and the matrix.
-		//double
-		template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;
-		template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, double> const& entry);
-		template class SparseMatrixBuilder<double>;
-		template class SparseMatrix<double>;
-		template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
-		//float
-		template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
-		template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, float> const& entry);
-		template class SparseMatrixBuilder<float>;
-		template class SparseMatrix<float>;
-		template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
-		//int
-		template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
-		template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, int> const& entry);
+        //double
+        template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, double> const& entry);
+        template class SparseMatrixBuilder<double>;
+        template class SparseMatrix<double>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
+        //float
+        template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, float> const& entry);
+        template class SparseMatrixBuilder<float>;
+        template class SparseMatrix<float>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
+        //int
+        template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, int> const& entry);
         template class SparseMatrixBuilder<int>;
         template class SparseMatrix<int>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
 #ifdef STORM_HAVE_CARL
+        // Rat Function
         template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);
         template class SparseMatrixBuilder<RationalFunction>;
         template class SparseMatrix<RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalFunction> const& matrix);
+        // Intervals
+        template class MatrixEntry<typename SparseMatrix<Interval>::index_type, Interval>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, Interval> const& entry);
+        template class SparseMatrixBuilder<Interval>;
+        template class SparseMatrix<Interval>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix);
 #endif
         
         
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 76ee74592..4604b3cb2 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -259,6 +259,9 @@ namespace storm {
         template RationalFunction& simplify(RationalFunction& value);
         template RationalFunction&& simplify(RationalFunction&& value);
         
+        template Interval one();
+        template Interval zero();
+        
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);