GLPK build identifier, license warnings.

diff --git a/config/build-type b/config/build-type
index 2f1b27cc2f9b53151a30bd1a3f62f0cc32c05422..f982b0020fe928766fb977214a0298718b21f7b6 100755 (executable)
--- a/config/build-type
+++ b/config/build-type
@@ -33,6 +33,8 @@
 # Also you can specify "cln" or "gmp".  If "cln", the build dir
 # contains the string "cln".  (gmp is considered the default.)
 #
+# Also for glpk.
+#
 
 if [ $# -eq 0 ]; then
   echo "usage: build-type profile [ overrides... ]" >&2
@@ -53,7 +55,7 @@ while [ $# -gt 0 ]; do
 done
 
 build_type_suffix=
-for arg in cln staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do
+for arg in cln glpk staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do
   if eval [ -n '"${'$arg'+set}"' ]; then
     if eval [ '"${'$arg'}"' -eq 0 ]; then
       build_type_suffix=$build_type_suffix-no$arg

diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 27ac51521cd9e29a45f21964f881f5e46db0d898..aefce193af9e950eee0a0e87fb31735824877cbe 100644 (file)
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -43,6 +43,12 @@ handle_option() {
       if expr "$ac_option" : '.*-debugsymbols$' >/dev/null || expr "$ac_option" : '.*-debugsymbols-' >/dev/null; then
         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-debug-symbols\""'
       fi
+      if expr "$ac_option" : '.*-noglpk' >/dev/null || expr "$ac_option" : '.*-noglpk-' >/dev/null; then
+        eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-glpk\""'
+      fi
+      if expr "$ac_option" : '.*-glpk' >/dev/null || expr "$ac_option" : '.*-glpk-' >/dev/null; then
+        eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-glpk\""'
+      fi
       for x in cln gmp; do
         if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then
           eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-$x\""'

diff --git a/configure.ac b/configure.ac
index f1fd797a027ee5b8d8509006ba7ecdc1bb9afd46..89d59cfff842f3b7fbec3bdd22e895336edb5e58 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -112,7 +112,7 @@ AC_ARG_WITH([build],
 if test -z "${with_build+set}" -o "$with_build" = default; then
   with_build=default
 fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}"; then
   custom_build_profile=no
 else
   custom_build_profile=yes
@@ -202,6 +202,11 @@ if test -n "${enable_replay+set}"; then
     btargs="$btargs noreplay"
   fi
 fi
+if test -n "${with_glpk+set}"; then
+  if test "$with_glpk" = yes; then
+    btargs="$btargs glpk"
+  fi
+fi
 AC_MSG_RESULT([$with_build])
 
 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
@@ -1321,6 +1326,17 @@ else
   optimized="no"
 fi
 
+if test $have_libglpk -eq 1; then
+  licensewarn="${licensewarn}Please note that CVC4 will be built against the GNU Linear Programming
+Kit (GLPK).  This library is covered under the GPL, so use of this build
+of CVC4 will be more restrictive than CVC4's license would normally
+suggest.  For full details of GLPK and its license, please visit
+  http://www.gnu.org/software/glpk/
+To build CVC4 without GLPK, configure --without-glpk (which is the default).
+
+"
+fi
+
 if test $cvc4_cln_or_gmp = cln; then
   mplibrary='cln (GPL)'
   licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for