From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 16 May 2013 22:55:08 +0000 (-0400)
Subject: configure fix for building with glpk on redhat, perhaps others
X-Git-Tag: cvc5-1.0.0~7287^2~113^2~13
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=790bd94058f65c20f6adc57fc9eeeb12a3955015;p=cvc5.git

configure fix for building with glpk on redhat, perhaps others
---

diff --git a/config/glpk.m4 b/config/glpk.m4
index 7380ad0e2..6c59a3094 100644
--- a/config/glpk.m4
+++ b/config/glpk.m4
@@ -13,8 +13,10 @@ elif test "$with_glpk" = yes; then
 
   dnl Try a bunch of combinations until something works :-/
   GLPK_LIBS=
-  AC_CHECK_HEADER([glpk.h], [],
-    [AC_MSG_FAILURE([cannot find glpk.h, the GLPK header!])])
+  AC_CHECK_HEADERS([glpk/glpk.h glpk.h], [break])
+  if test x$ac_cv_header_glpk_glpk_h = xno && test x$ac_cv_header_glpk_h = xno; then
+    AC_MSG_FAILURE([cannot find glpk.h, the GLPK header!])
+  fi
   AC_MSG_CHECKING([how to link glpk])
   CVC4_TRY_GLPK_WITH([])
   CVC4_TRY_GLPK_WITH([-lgmp])
@@ -88,7 +90,11 @@ if test -z "$GLPK_LIBS"; then
   AC_LANG_PUSH([C++])
   cvc4_save_LIBS="$LIBS"
   LIBS="-lglpk $1"
-  AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <glpk.h>],
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H]
+                                  [#include <glpk/glpk.h>]
+                                  [#else]
+                                  [#include <glpk.h>]
+                                  [#endif],
                                   [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])],
     [GLPK_LIBS="-lglpk $1"],
     [])
@@ -107,7 +113,11 @@ if test -z "$GLPK_LIBS"; then
   cvc4_save_LDFLAGS="$LDFLAGS"
   LDFLAGS="-static $LDFLAGS"
   LIBS="-lglpk $1"
-  AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <glpk.h>],
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H]
+                                  [#include <glpk/glpk.h>]
+                                  [#else]
+                                  [#include <glpk.h>]
+                                  [#endif],
                                   [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])],
     [GLPK_LIBS="-lglpk $1"],
     [])
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 47f15d8c7..0f5a0fd4e 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -116,8 +116,14 @@ public:
 /* Begin the declaration of GLPK specific code. */
 #ifdef CVC4_USE_GLPK
 extern "C" {
-#include <glpk.h>
-}
+/* Sometimes the header is in a subdirectory glpk/, sometimes not.
+ * The configure script figures it out. */
+#ifdef HAVE_GLPK_GLPK_H
+#  include <glpk/glpk.h>
+#else /* HAVE_GLPK_GLPK_H */
+#  include <glpk.h>
+#endif /* HAVE_GLPK_GLPK_H */
+}/* extern "C" */
 
 namespace CVC4 {
 namespace theory {