Clean up glpk detection a little, fix a detection bug.

diff --git a/config/glpk.m4 b/config/glpk.m4
index c5592ab195a223d62ae71bbd1d6465a1f0ab4e88..cc2a3be71c85acc2ea43db00665140682d6c4c1b 100644 (file)
--- a/config/glpk.m4
+++ b/config/glpk.m4
@@ -34,10 +34,7 @@ elif test "$with_glpk" = yes; then
 
   dnl Try a bunch of combinations until something works :-/
   GLPK_LIBS=
-  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_CHECK_HEADER([glpk.h], [], [AC_MSG_FAILURE([cannot find glpk.h, the GLPK header!])])
   AC_MSG_CHECKING([how to link glpk])
   CVC4_TRY_GLPK_WITH([])
   CVC4_TRY_GLPK_WITH([-lgmp])
@@ -115,11 +112,7 @@ if test -z "$GLPK_LIBS"; then
   CPPFLAGS="$CVC4CPPFLAGS $CPPFLAGS"
   LDFLAGS="$GLPK_LDFLAGS $LDFLAGS"
   LIBS="-lglpk $1"
-  AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H]
-                                  [#include <glpk/glpk.h>]
-                                  [#else]
-                                  [#include <glpk.h>]
-                                  [#endif],
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <glpk.h>],
                                   [int i = glp_ios_get_cut(NULL, 0, NULL, NULL, NULL, NULL, NULL)])],
     [GLPK_LIBS="-lglpk $1"],
     [])
@@ -139,22 +132,14 @@ if test -z "$GLPK_LIBS"; then
   cvc4_save_LIBS="$LIBS"
   cvc4_save_CPPFLAGS="$CPPFLAGS"
   cvc4_save_LDFLAGS="$LDFLAGS"
-  CPPFLAGS="$CVC4_CPPFLAGS $CPPFLAGS"
+  CPPFLAGS="$CVC4CPPFLAGS $CPPFLAGS"
   LDFLAGS="-static $GLPK_LDFLAGS $LDFLAGS"
   LIBS="-lglpk-static $1"
-  AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H]
-                                  [#include <glpk/glpk.h>]
-                                  [#else]
-                                  [#include <glpk.h>]
-                                  [#endif],
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <glpk.h>],
                                   [int i = glp_ios_get_cut(NULL, 0, NULL, NULL, NULL, NULL, NULL)])],
     [GLPK_LIBS="-lglpk-static $1"],
     [ LIBS="-lglpk $1"
-      AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H]
-                                      [#include <glpk/glpk.h>]
-                                      [#else]
-                                      [#include <glpk.h>]
-                                      [#endif],
+      AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <glpk.h>],
                                       [int i = glp_ios_get_cut(NULL, 0, NULL, NULL, NULL, NULL, NULL)])],
 
         [GLPK_LIBS="-lglpk $1"]) ])

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 9f6b1796ed5b05cc18091fe81f2414aeeb9fdba4..676c5cb252ae672cb71fcf9b173f83f3e30bf1f0 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -431,13 +431,7 @@ public:
 /* Begin the declaration of GLPK specific code. */
 #ifdef CVC4_USE_GLPK
 extern "C" {
-/* 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 */
+#include <glpk.h>
 }/* extern "C" */
 
 namespace CVC4 {