summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-05-16 18:55:08 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-05-20 16:53:25 -0400
commit67cd7748e776bcceefe7b06edcfc316876cca9bd (patch)
tree29ab82d71c94c293de494c9805b102325f36ea06
parentf1e9c2f91b021b695afad733c44945b6c779bfd5 (diff)
configure fix for building with glpk on redhat, perhaps others
-rw-r--r--config/glpk.m418
-rw-r--r--src/theory/arith/approx_simplex.cpp10
2 files changed, 22 insertions, 6 deletions
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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback