diff options
| -rw-r--r-- | config/glpk.m4 | 46 | ||||
| -rw-r--r-- | configure.ac | 1 | ||||
| -rwxr-xr-x | contrib/get-glpk-cut-log | 57 | ||||
| -rw-r--r-- | src/Makefile.am | 1 |
4 files changed, 101 insertions, 4 deletions
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 |