With this commit come a number of changes to build system to support

building with CLN or with GMP, the contrib/switch-config script
(enabling "fast switching" of different configurations in the same
builds/ directory), and also some minor changes.

./configure --with-gmp     (or --without-cln) forces building with GMP
and doesn't even look for CLN.  Configure fails if GMP isn't installed.

./configure --with-cln     (or --without-gmp) forces building with CLN
and doesn't even look for GMP.  Configure fails if CLN isn't installed.

./configure [no arguments] will detect what's installed.  CLN is
default, if it isn't installed, or is too old, GMP is looked for (and
configure fails if neither is available).

It is an error to specify --with-gmp --with-cln (or --without-* for
both) at the same time.

Building with CLN (whether forced or detected) adds a note to the
configure output mentioning the fact that the build of CVC4 will be
linked against a GPLed library and notifying the user of the
--without-cln option.

Building with GMP (whether forced or detected) affects the build
directory, so CLN and GMP builds are kept separate.

./configure --with-cln debug     builds in builds/$arch/debug
./configure --with-gmp debug     builds in builds/$arch/debug-gmp

The final binaries are linked explicitly against either gmp or cln,
but not both.  If linked against cln, cln pulls in gmp as a
dependency, so the result will be linked against both.

=== Details that you probably don't care about ===

The headers src/util/{integer,rational}.h are generated from the
corresponding .in versions.  A user installing a CVC4-devel package
will get the headers for rational and integer that match the library
that s/he installs.

The preprocessor #defines CVC4_GMP_IMP and CVC4_CLN_IMP are added to
cvc4autoconfig.h.  Only one is ever #defined.  cvc4autoconfig.h
doesn't need to be #included directly; you get it through #including
cvc4_private.h (or the parser version).

AM_CONDITIONALs are also defined so that Makefiles get the cln/gmp
configuration.  AC_SUBSTs are defined so that public headers (see
src/util/{integer,rational}.h.in) can use the setting.

*Public* headers that need to depend on the cln/gmp configuration
can't use cvc4autoconfig.h, because we're keeping that in the private,
internal-only space, never to be installed on users' machines.  Here,
something special is required, like the configure-level generation of
headers that I used for src/util/{integer,rational}.h.in.

Tim's Integer and Rational wrappers are the only bits of code that
should care which library is used (and also src/util/configuration.h,
which gives the user of the library information about how CVC4 is
built), and possibly some unit tests (?).

2 files changed, 96 insertions, 1 deletions

diff --git a/contrib/addsourcedir b/contrib/addsourcedir
index 8c7d74d90..190864469 100644
--- a/contrib/addsourcedir
+++ b/contrib/addsourcedir
@@ -81,7 +81,7 @@ EOF
     clibtarget="lib${clibbase}_la"
     cat >"$srcdir/Makefile.am" <<EOF
 AM_CPPFLAGS = \\
-$definitions	-I@srcdir@/$topsrcdir/include -I@srcdir@/$topsrcdir
+$definitions	-I@srcdir@/$topsrcdir/include -I@srcdir@/$topsrcdir -I@builddir@/$topsrcdir
 AM_CXXFLAGS = -Wall$visibility
 
 noinst_LTLIBRARIES = $clibname
diff --git a/contrib/switch-config b/contrib/switch-config
new file mode 100755
index 000000000..ad28464e7
--- /dev/null
+++ b/contrib/switch-config
@@ -0,0 +1,95 @@
+#!/bin/bash
+#
+# usage: switch-config [configuration]
+#        switch-config -l
+#
+# Script to switch the "current" configuration of the CVC4 builds directory
+# to another one.  Without an argument, it switches to the next alphabetically.
+# With an argument, it switches to that configuration.  With -l, it lists the
+# available configurations.
+#
+# Only configurations in the "current" architecture (that for which the build directory is currently
+# configured) are considered.
+#
+# This script is useful because it's faster that re-configuring.
+#
+# Script assumes it lives under contrib/ in the root of the CVC4 source
+# tree.
+
+function usage {
+  echo "usage: `basename \"$0\"` [configuration]"
+  echo "       `basename \"$0\"` -l"
+}
+
+if [ $# -gt 1 ]; then
+  usage
+  exit 1
+fi
+
+cd `dirname "$0"`/..
+
+if ! [ -d builds ]; then
+  echo "No configurations are available (no builds/ directory)."
+  exit
+fi
+
+if ! [ -e builds/current ]; then
+  echo "Cannot get current configuration."
+  exit 1
+fi
+
+current=(`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]\+\)/\(.*\),\1 \2,'`)
+arch=${current[0]}
+build=${current[1]}
+
+builds=(`ls "builds/$arch/"`)
+
+if ! [ -d "builds/$arch" ] || ! [ -d "builds/$arch/$build" ] || [ ${#builds[@]} -eq 0 ]; then
+  echo "builds/ directory in malformed state."
+  echo "You might want to blow it away and start from scratch."
+  exit 1
+fi
+
+function switchto {
+  perl -pi -e 's,^CURRENT_BUILD *= *.*,CURRENT_BUILD = '$arch/$1',' builds/current
+  echo "Current build switched to \`$1'."
+}
+
+if [ $# -eq 0 ]; then
+  first=
+  last=
+  setbuild=
+  for d in `ls "builds/$arch/"`; do
+    if [ -z "$first" ]; then first=$d; fi
+    if [ "$last" = "$build" ]; then setbuild=$d; break; fi
+    last=$d
+  done
+  if [ -z "$setbuild" ]; then setbuild=$first; fi
+  if [ "$setbuild" = "$build" ]; then
+    echo "There is only one build profile (\`$build'), and it is current."
+  else
+    switchto "$setbuild"
+  fi
+else
+  case $1 in
+    -l) for config in `ls -1 "builds/$arch/"`; do
+          if [ "$config" = "$build" ]; then
+            echo "$config" '*'
+          else
+            echo "$config"
+          fi
+        done ;;
+    -*) usage; exit 1 ;;
+    *)  if ! [ -d "builds/$arch/$1" ]; then
+          echo "Build \`$1' does not exist."
+          exit 1
+        else
+          if [ "$1" = "$build" ]; then
+            echo "Build \`$1' is already the current build profile."
+          else
+            switchto "$1"
+          fi
+        fi ;;
+  esac
+fi
+