From 2cb7b5769e32c5b0fb436ee86c826e796d1ffb9c Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 29 Jul 2019 16:31:12 +0200
Subject: [PATCH] Jit: Fixed issues when CLN and/or GMP is installed via carl

---
 resources/3rdparty/CMakeLists.txt             | 13 +++++----
 .../jit/ExplicitJitJaniModelBuilder.cpp       | 27 ++++++++++++++++---
 .../builder/jit/ExplicitJitJaniModelBuilder.h |  6 +++++
 storm-config.h.in                             |  7 +++++
 4 files changed, 43 insertions(+), 10 deletions(-)

diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 6bfcde1b0..fbdaadb8c 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -374,10 +374,6 @@ endif()
 ##	gmp
 ##
 #############################################################
-#
-#find_package(GMP QUIET REQUIRED)
-#
-
 
 get_target_property(GMPXX_LIB GMPXX_SHARED IMPORTED_LIB_LOCATION)
 get_target_property(GMP_LIB GMP_SHARED IMPORTED_LIB_LOCATION)
@@ -387,10 +383,13 @@ get_filename_component(GMP_LIB_LOCATION ${GMP_LIB} DIRECTORY)
 get_filename_component(GMPXX_LIB_LOCATION ${GMPXX_LIB} DIRECTORY)
 
 
+#############################################################
+##
+##	cln
+##
+#############################################################
 
-#message(STATUS "Storm - Linking with gmp.")
-#include_directories("${GMP_INCLUDE_DIR}")
-#list(APPEND STORM_LINK_LIBRARIES ${GMP_LIBRARY})
+get_target_property(CLN_INCLUDE_DIR CLN_SHARED INTERFACE_INCLUDE_DIRECTORIES)
 
 #############################################################
 ##
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index a3eaf8b35..67852f292 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -99,6 +99,16 @@ namespace storm {
                 } else {
                     carlIncludeDirectory = STORM_CARL_INCLUDE_DIR;
                 }
+#ifdef STORM_HAVE_CLN
+                clnIncludeDirectory = CLN_INCLUDE_DIR;
+#else
+                clnIncludeDirectory = "";
+#endif
+#ifdef STORM_HAVE_GMP
+                gmpIncludeDirectory = GMP_INCLUDE_DIR;
+#else
+                gmpIncludeDirectory = "";
+#endif
                 sparseppIncludeDirectory = STORM_BUILD_DIR "/include/resources/3rdparty/sparsepp/";
                 
                 // Register all transient variables as transient.
@@ -393,7 +403,13 @@ namespace storm {
                     boost::filesystem::path outputFile = temporaryFile;
                     outputFile += ".out";
                     std::string outputFilename = boost::filesystem::absolute(outputFile).string();
-                    boost::optional<std::string> error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormIncludeDirectory + " -I" + carlIncludeDirectory + " -o " + outputFilename);
+                    std::string includes = "";
+                    for (std::string const& dir : {stormIncludeDirectory, carlIncludeDirectory, clnIncludeDirectory, gmpIncludeDirectory}) {
+                        if (dir != "") {
+                            includes += " -I" + dir;
+                        }
+                    }
+                    boost::optional<std::string> error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + includes + " -o " + outputFilename);
                     
                     if (error) {
                         result = false;
@@ -2488,8 +2504,13 @@ namespace storm {
                 auto dynamicLibraryPath = sourceFile;
                 dynamicLibraryPath += DYLIB_EXTENSION;
                 std::string dynamicLibraryFilename = boost::filesystem::absolute(dynamicLibraryPath).string();
-                
-                std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormIncludeDirectory + " -I" + sparseppIncludeDirectory + " -I" + boostIncludeDirectory + " -I" + carlIncludeDirectory + " -o " + dynamicLibraryFilename;
+                std::string includes = "";
+                for (std::string const& dir : {stormIncludeDirectory, sparseppIncludeDirectory, boostIncludeDirectory, carlIncludeDirectory, clnIncludeDirectory, gmpIncludeDirectory}) {
+                    if (dir != "") {
+                        includes += " -I" + dir;
+                    }
+                }
+                std::string command = compiler + " " + sourceFilename + " " + compilerFlags + includes + " -o " + dynamicLibraryFilename;
                 boost::optional<std::string> error = execute(command);
                 
                 if (error) {
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h
index 63509aa44..3c5c4a4ce 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h
@@ -195,6 +195,12 @@ namespace storm {
                 /// The include directory of sparsepp.
                 std::string sparseppIncludeDirectory;
                 
+                /// The include directory for cln
+                std::string clnIncludeDirectory;
+                
+                /// The include directory for gmp
+                std::string gmpIncludeDirectory;
+                
                 /// A cache that is used by carl.
                 std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
             };
diff --git a/storm-config.h.in b/storm-config.h.in
index 128e5a497..78164aa05 100644
--- a/storm-config.h.in
+++ b/storm-config.h.in
@@ -66,9 +66,16 @@
 // Whether CLN is available and to be used (define/undef)
 #cmakedefine STORM_HAVE_CLN
 
+// Include directory for CLN headers
+#cmakedefine CLN_INCLUDE_DIR "@CLN_INCLUDE_DIR@"
+
 // Whether GMP is available  (it is always available nowadays)
 #define STORM_HAVE_GMP
 
+// Include directory for GMP headers
+#cmakedefine GMP_INCLUDE_DIR "@GMP_INCLUDE_DIR@"
+#cmakedefine GMPXX_INCLUDE_DIR "@GMPXX_INCLUDE_DIR@"
+
 // Whether carl is available and to be used.
 #cmakedefine STORM_HAVE_CARL