From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 16 Jun 2014 20:05:12 +0000 (-0400)
Subject: get-glpk-cut-log script, and configure code.
X-Git-Tag: cvc5-1.0.0~6797
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=967a6e7a7be80e76c9fcf76f6a5b1b90f38156b3;p=cvc5.git

get-glpk-cut-log script, and configure code.
---

diff --git a/config/glpk.m4 b/config/glpk.m4
index f854830d3..c5592ab19 100644
--- a/config/glpk.m4
+++ b/config/glpk.m4
@@ -6,11 +6,32 @@ AC_MSG_CHECKING([whether user requested glpk support])
 LIBGLPK=
 have_libglpk=0
 GLPK_LIBS=
+GLPK_LDFLAGS=
 if test "$with_glpk" = no; then
   AC_MSG_RESULT([no, glpk disabled by user])
 elif test "$with_glpk" = yes; then
   AC_MSG_RESULT([yes, glpk requested by user])
 
+  # Get the location of all the GLPK stuff
+  AC_ARG_VAR(GLPK_HOME, [path to top level of glpk installation])
+  AC_ARG_WITH(
+    [glpk-dir],
+    AS_HELP_STRING(
+      [--with-glpk-dir=PATH],
+      [path to top level of glpk installation]
+    ),
+    [GLPK_HOME="$withval"],
+    [ if test -z "$GLPK_HOME"; then
+        AC_MSG_FAILURE([must give --with-glpk-dir=PATH or define environment variable GLPK_HOME!])
+      fi
+    ]
+  )
+
+  if test -n "$GLPK_HOME"; then
+    CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$GLPK_HOME/include"
+    GLPK_LDFLAGS="-L$GLPK_HOME/lib"
+  fi
+
   dnl Try a bunch of combinations until something works :-/
   GLPK_LIBS=
   AC_CHECK_HEADERS([glpk/glpk.h glpk.h], [break])
@@ -89,6 +110,10 @@ AC_DEFUN([CVC4_TRY_GLPK_WITH], [
 if test -z "$GLPK_LIBS"; then
   AC_LANG_PUSH([C++])
   cvc4_save_LIBS="$LIBS"
+  cvc4_save_CPPFLAGS="$LDFLAGS"
+  cvc4_save_LDFLAGS="$LDFLAGS"
+  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>]
@@ -99,6 +124,8 @@ if test -z "$GLPK_LIBS"; then
     [GLPK_LIBS="-lglpk $1"],
     [])
   LIBS="$cvc4_save_LIBS"
+  CPPFLAGS="$cvc4_save_CPPFLAGS"
+  LDFLAGS="$cvc4_save_LDFLAGS"
   AC_LANG_POP([C++])
 fi
 ])# CVC4_TRY_GLPK_WITH
@@ -110,18 +137,29 @@ AC_DEFUN([CVC4_TRY_STATIC_GLPK_WITH], [
 if test -z "$GLPK_LIBS"; then
   AC_LANG_PUSH([C++])
   cvc4_save_LIBS="$LIBS"
+  cvc4_save_CPPFLAGS="$CPPFLAGS"
   cvc4_save_LDFLAGS="$LDFLAGS"
-  LDFLAGS="-static $LDFLAGS"
-  LIBS="-lglpk $1"
+  CPPFLAGS="$CVC4_CPPFLAGS $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],
                                   [int i = glp_ios_get_cut(NULL, 0, NULL, NULL, NULL, NULL, NULL)])],
-    [GLPK_LIBS="-lglpk $1"],
-    [])
+    [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],
+                                      [int i = glp_ios_get_cut(NULL, 0, NULL, NULL, NULL, NULL, NULL)])],
+
+        [GLPK_LIBS="-lglpk $1"]) ])
   LIBS="$cvc4_save_LIBS"
+  CPPFLAGS="$cvc4_save_CPPFLAGS"
   LDFLAGS="$cvc4_save_LDFLAGS"
   AC_LANG_POP([C++])
 fi
diff --git a/configure.ac b/configure.ac
index 92a9c10ce..57e5d46dc 100644
--- a/configure.ac
+++ b/configure.ac
@@ -748,6 +748,7 @@ if test $have_libglpk -eq 1; then
   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
 fi
 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
+AC_SUBST([GLPK_LDFLAGS])
 AC_SUBST([GLPK_LIBS])
 
 # Build with libabc (defined in config/abc.m4)
diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log
new file mode 100755
index 000000000..5ca18c66d
--- /dev/null
+++ b/contrib/get-glpk-cut-log
@@ -0,0 +1,57 @@
+#!/bin/bash
+#
+set -e
+
+commit=b420454e732f4b3d229c552ef7cd46fec75fe65c
+
+cd "$(dirname "$0")/.."
+
+if ! [ -e src/parser/cvc/Cvc.g ]; then
+  echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2
+  echo "but apparently:" >&2
+  echo >&2
+  echo "  $(pwd)" >&2
+  echo >&2
+  echo "is not a CVC4 source tree ?!" >&2
+  exit 1
+fi
+
+function webget {
+  if which wget &>/dev/null; then
+    wget -c -O "$2" "$1"
+  elif which curl &>/dev/null; then
+    curl "$1" >"$2"
+  else
+    echo "Can't figure out how to download from web.  Please install wget or curl." >&2
+    exit 1
+  fi
+}
+
+if [ -e glpk-cut-log ]; then
+  echo 'error: file or directory "glpk-cut-log" exists; please move it out of the way.' >&2
+  exit 1
+fi
+
+mkdir glpk-cut-log
+cd glpk-cut-log
+webget https://github.com/timothy-king/glpk-cut-log/archive/$commit.zip glpk-cut-log-$commit.zip
+unzip glpk-cut-log-$commit.zip
+cd glpk-cut-log-$commit
+
+libtoolize
+aclocal
+autoheader
+autoconf
+automake --add-missing
+./configure --without-pic --prefix=`pwd`/.. --disable-shared --enable-static --disable-dependency-tracking
+make && make install
+mv `pwd`/../lib/libglpk.a `pwd`/../lib/libglpk-static.a
+make distclean
+./configure --with-pic --prefix=`pwd`/.. --disable-shared --enable-static --disable-dependency-tracking
+make && make install
+
+cd ..
+
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --enable-gpl --with-glpk --with-glpk-dir=`pwd`
diff --git a/src/Makefile.am b/src/Makefile.am
index b1a2032c0..fb7994699 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -434,6 +434,7 @@ endif
 
 if CVC4_USE_GLPK
 libcvc4_la_LIBADD += $(GLPK_LIBS)
+libcvc4_la_LDFLAGS += $(GLPK_LDFLAGS)
 endif
 
 if CVC4_USE_ABC