From 7cbab6a2602d1c312b90d951f23da74b129e6084 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Jun 2015 19:50:54 +0200
Subject: [PATCH] use gmpxx mpq_class for rational numbers

Former-commit-id: e79dac21dfb904f86bf4dcdf2f0fec59cf88a3ef
---
 src/adapters/CarlAdapter.h                          | 13 ++++++++-----
 .../expressions/ToRationalFunctionVisitor.cpp       |  4 ++--
 src/utility/constants.cpp                           |  2 +-
 3 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h
index d31802717..81ddf2f8a 100644
--- a/src/adapters/CarlAdapter.h
+++ b/src/adapters/CarlAdapter.h
@@ -7,11 +7,13 @@
 #ifdef STORM_HAVE_CARL
 
 #include <cln/cln.h>
+#include <gmpxx.h>
 #include <carl/core/MultivariatePolynomial.h>
 #include <carl/core/RationalFunction.h>
 #include <carl/core/VariablePool.h>
-#include <carl/core/Constraint.h>
 #include <carl/core/FactorizedPolynomial.h>
+#include <carl/formula/Relation.h>
+#include <carl/formula/Formula.h>
 
 namespace carl {
     // Define hash values for all polynomials and rational function.
@@ -35,11 +37,12 @@ namespace carl {
 }
 
 namespace storm {
-	typedef carl::Variable Variable;
-    typedef carl::MultivariatePolynomial<cln::cl_RA> RawPolynomial;
+    typedef mpq_class RationalNumber;
+    typedef carl::Variable Variable;
+    typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial;
     typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
-	typedef carl::CompareRelation CompareRelation;
-	typedef carl::RationalFunction<Polynomial> RationalFunction;
+    typedef carl::Relation CompareRelation;
+    typedef carl::RationalFunction<Polynomial> RationalFunction;
 }
 
 #endif
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp
index 187474663..55840c301 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -87,12 +87,12 @@ namespace storm {
         
         template<typename RationalFunctionType>
         boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IntegerLiteralExpression const& expression) {
-            return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::CoeffType(expression.getValue())));
+            return RationalFunctionType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue())));
         }
         
         template<typename RationalFunctionType>
         boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(DoubleLiteralExpression const& expression) {
-            return RationalFunctionType(carl::rationalize<cln::cl_RA>(expression.getValue()));
+            return RationalFunctionType(carl::rationalize<storm::RationalNumber>(expression.getValue()));
         }
 
         template class ToRationalFunctionVisitor<storm::RationalFunction>;
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index d4625b578..76ee74592 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -25,7 +25,7 @@ namespace storm {
         template<>
         storm::RationalFunction infinity() {
             // FIXME: this does not work.
-            return storm::RationalFunction(carl::rationalize<cln::cl_RA>(std::numeric_limits<double>::infinity()));
+            return storm::RationalFunction(carl::rationalize<storm::RationalNumber>(std::numeric_limits<double>::infinity()));
         }
 #endif