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 (?).

35 files changed, 180 insertions, 107 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index a805f8c85..97c66ac89 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -14,7 +14,7 @@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
 
 AM_CPPFLAGS =
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/include -I@srcdir@
+	-I@srcdir@/include -I@srcdir@ -I@builddir@
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = expr util context theory prop smt . parser main
diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index 3d912e685..7a40bab1b 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/..
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libcontext.la
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 225624a8b..db863440c 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/..
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libexpr.la
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index e1b515ba5..8375f7571 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4_PUBLIC_H
 #define __CVC4_PUBLIC_H
 
+#include <stdint.h>
+
 #if defined _WIN32 || defined __CYGWIN__
 #  ifdef BUILDING_DLL
 #    ifdef __GNUC__
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 9ffa43ca0..82ff00a60 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -1,5 +1,5 @@
 AM_CPPFLAGS = \
-	-I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
 
 bin_PROGRAMS = cvc4
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index a323ec3cb..b1f265b56 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -14,7 +14,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
 
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
-	-I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = smt smt2 cvc
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 9754c1063..cfe983727 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
-	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
 
 # Compile generated C files using C++ compiler
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 418b204dc..f5ea3aae3 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
-	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
 
 # Compile generated C files using C++ compiler
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index 3066f2247..aabae5352 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
-	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
 
 # Compile generated C files using C++ compiler
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 48c9c3fd2..06504e73c 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/..
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libprop.la
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 77d1d602e..56f61adad 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include
+	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@builddir@/../.. -I@srcdir@/../../include
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG
 
 noinst_LTLIBRARIES = libminisat.la
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 72dd8f3df..90d58904a 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/..
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libsmt.la
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index bb9d19b25..a2a206d40 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/..
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libtheory.la
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 541426ac3..4d299e8af 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../..
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libarith.la
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index 0c6e9006f..8a0a180db 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../..
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libarrays.la
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index 478fca1cf..3bd8b5a39 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../..
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbooleans.la
diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am
index 5694dea84..d1df0e425 100644
--- a/src/theory/builtin/Makefile.am
+++ b/src/theory/builtin/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../..
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbuiltin.la
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 94941d406..cab90bbdb 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../..
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbv.la
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 39586345b..4e399aeb7 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../..
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libuf.la
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 1446412ce..b6ca5bcc6 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/..
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libutil.la
@@ -26,6 +26,30 @@ libutil_la_SOURCES = \
 	configuration.cpp \
 	rational.h \
 	integer.h \
+	bitvector.h \
+	bitvector.cpp \
+	gmp_util.h \
+	sexpr.h \
+	stats.h \
+	stats.cpp \
+	triple.h
+
+BUILT_SOURCES = \
+	rational.h \
+	integer.h
+
+if CVC4_CLN_IMP
+libutil_la_SOURCES += \
+	integer_cln_imp.cpp \
+	rational_cln_imp.cpp
+endif
+if CVC4_GMP_IMP
+libutil_la_SOURCES += \
+	integer_gmp_imp.cpp \
+	rational_gmp_imp.cpp
+endif
+
+EXTRA_DIST = \
 	rational_cln_imp.h \
 	integer_cln_imp.h \
 	rational_cln_imp.cpp \
@@ -34,10 +58,5 @@ libutil_la_SOURCES = \
 	integer_gmp_imp.h \
 	rational_gmp_imp.cpp \
 	integer_gmp_imp.cpp \
-	bitvector.h \
-	bitvector.cpp \
-	gmp_util.h \
-	sexpr.h \
-	stats.h \
-	stats.cpp \
-	triple.h
+	rational.h.in \
+	integer.h.in
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 928592d9e..0b5952481 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: cconway
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -24,7 +24,6 @@
 
 #include <iostream>
 #include "util/Assert.h"
-#include "util/gmp_util.h"
 #include "util/integer.h"
 
 namespace CVC4 {
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 2a7563f82..12908c672 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -100,7 +100,32 @@ Copyright (C) 2009, 2010\n\
   The ACSys Group\n\
   Courant Institute of Mathematical Sciences\n\
   New York University\n\
-  New York, NY  10012  USA\n");
+  New York, NY  10012  USA\n\n") +
+    (isBuiltWithCln() ? "\
+This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
+CVC4 is open-source and is covered by the BSD license (modified).\n\
+However, CLN, the Class Library for Numbers, is covered by the GPL.  Thus\n\
+this CVC4 library cannot be used in proprietary applications.  Please\n\
+consult the CVC4 documentation for instructions about building a version\n\
+of CVC4 that links against GMP, and can be used in such applications.\n" :
+"This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
+CVC4 is open-source and is covered by the BSD license (modified).\n");
+}
+
+bool Configuration::isBuiltWithGmp() {
+#ifdef CVC4_GMP_IMP
+  return true;
+#else /* CVC4_GMP_IMP */
+  return false;
+#endif /* CVC4_GMP_IMP */
+}
+
+bool Configuration::isBuiltWithCln() {
+#ifdef CVC4_CLN_IMP
+  return true;
+#else /* CVC4_CLN_IMP */
+  return false;
+#endif /* CVC4_CLN_IMP */
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 00651202d..6d5ac12a1 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -60,6 +60,10 @@ public:
   static unsigned getVersionRelease();
 
   static std::string about();
+
+  static bool isBuiltWithGmp();
+
+  static bool isBuiltWithCln();
 };
 
 }/* CVC4 namespace */
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index a425690a5..87102e644 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -17,24 +17,24 @@
  ** \todo document this file
  **/
 
-#ifndef __CVC4__GMP_H_
-#define __CVC4__GMP_H_
+#ifndef __CVC4__GMP_UTIL_H
+#define __CVC4__GMP_UTIL_H
 
 #include <gmpxx.h>
 
 namespace CVC4 {
 
-  /** Hashes the gmp integer primitive in a word by word fashion. */
-  inline size_t gmpz_hash(const mpz_t toHash) {
-    size_t hash = 0;
-    for (int i=0, n=mpz_size(toHash); i<n; ++i){
-      mp_limb_t limb = mpz_getlimbn(toHash, i);
-      hash = hash * 2;
-      hash = hash xor limb;
-    }
-    return hash;
+/** Hashes the gmp integer primitive in a word by word fashion. */
+inline size_t gmpz_hash(const mpz_t toHash) {
+  size_t hash = 0;
+  for (int i = 0, n = mpz_size(toHash); i < n; ++i){
+    mp_limb_t limb = mpz_getlimbn(toHash, i);
+    hash = hash * 2;
+    hash = hash xor limb;
   }
+  return hash;
+}/* gmpz_hash() */
 
-}
+}/* CVC4 namespace */
 
-#endif /* __CVC4__GMP_H_ */
+#endif /* __CVC4__GMP_UTIL_H */
diff --git a/src/util/integer.h b/src/util/integer.h.in
index c57450d5f..7e1b9a1aa 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file integer.h
+/*! \file integer.h.in
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
@@ -16,9 +16,18 @@
  ** A multiprecision integer constant.
  **/
 
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/integer_gmp_imp.h"
-#endif
-#ifdef __CVC4__USE_CLN_IMP
-#include "util/integer_cln_imp.h"
-#endif
+// this is used to avoid a public header dependence on cvc4autoconfig.h
+#if /* use CLN */ @CVC4_USE_CLN_IMP@
+#  define CVC4_CLN_IMP
+#endif /* @CVC4_USE_CLN_IMP@ */
+#if /* use GMP */ @CVC4_USE_GMP_IMP@
+#  define CVC4_GMP_IMP
+#endif /* @CVC4_USE_GMP_IMP@ */
+
+#ifdef CVC4_CLN_IMP
+#  include "util/integer_cln_imp.h"
+#endif /* CVC4_CLN_IMP */
+
+#ifdef CVC4_GMP_IMP
+#  include "util/integer_gmp_imp.h"
+#endif /* CVC4_GMP_IMP */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 35293bb84..a6cad96d1 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file integer.cpp
+/*! \file integer_cln_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -21,14 +21,17 @@
  ** literature.) A consquence is that that the numerator and denominator may be
  ** different than the values used to construct the Rational.
  **/
-#ifdef __CVC4__USE_CLN_IMP
 
+#include "cvc4autoconfig.h"
 #include "util/integer.h"
 
+#ifndef CVC4_CLN_IMP
+#  error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
 using namespace CVC4;
 
 std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
 }
 
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 2154952f0..8551d0a6a 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file integer.h
+/*! \file integer_cln_imp.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,13 +11,12 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A multiprecision integer constant.
+ ** \brief A multiprecision integer constant; wraps a CLN multiprecision
+ ** integer.
  **
- ** A multiprecision integer constant.
+ ** A multiprecision integer constant; wraps a CLN multiprecision integer.
  **/
 
-#ifdef __CVC4__USE_CLN_IMP
-
 #include "cvc4_public.h"
 
 #ifndef __CVC4__INTEGER_H
@@ -30,7 +29,6 @@
 #include <cln/input.h>
 #include <cln/integer_io.h>
 #include "util/Assert.h"
-#include "util/gmp_util.h"
 
 namespace CVC4 {
 
@@ -226,4 +224,3 @@ std::ostream& operator<<(std::ostream& os, const Integer& n);
 
 #endif /* __CVC4__INTEGER_H */
 
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 7bda7f02a..112713aa5 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file integer.cpp
+/*! \file integer_gmp_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -22,12 +22,16 @@
  ** different than the values used to construct the Rational.
  **/
 
-#ifdef __CVC4__USE_GMP_IMP
+#include "cvc4autoconfig.h"
 #include "util/integer.h"
 
+#ifndef CVC4_GMP_IMP
+#  error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
 using namespace CVC4;
 
 std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
 }
-#endif /* __CVC4__USE_GMP_IMP */
+
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 7217d0c5a..b065dca23 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file integer.h
+/*! \file integer_gmp_imp.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,12 +11,12 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A multiprecision integer constant.
+ ** \brief A multiprecision integer constant; wraps a GMP multiprecision
+ ** integer.
  **
- ** A multiprecision integer constant.
+ ** A multiprecision integer constant; wraps a GMP multiprecision integer.
  **/
 
-#ifdef __CVC4__USE_GMP_IMP
 #include "cvc4_public.h"
 
 #ifndef __CVC4__INTEGER_H
@@ -165,4 +165,4 @@ std::ostream& operator<<(std::ostream& os, const Integer& n);
 }/* CVC4 namespace */
 
 #endif /* __CVC4__INTEGER_H */
-#endif /* __CVC4__USE_GMP_IMP */
+
diff --git a/src/util/rational.h b/src/util/rational.h.in
index 73fcb73a3..88c488290 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file rational.h
+/*! \file rational.h.in
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
@@ -16,9 +16,18 @@
  ** Multi-precision rational constants.
  **/
 
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/rational_gmp_imp.h"
-#endif
-#ifdef __CVC4__USE_CLN_IMP
-#include "util/rational_cln_imp.h"
-#endif
+// this is used to avoid a public header dependence on cvc4autoconfig.h
+#if /* use CLN */ @CVC4_USE_CLN_IMP@
+#  define CVC4_CLN_IMP
+#endif /* @CVC4_USE_CLN_IMP@ */
+#if /* use GMP */ @CVC4_USE_GMP_IMP@
+#  define CVC4_GMP_IMP
+#endif /* @CVC4_USE_GMP_IMP@ */
+
+#ifdef CVC4_CLN_IMP
+#  include "util/rational_cln_imp.h"
+#endif /* CVC4_CLN_IMP */
+
+#ifdef CVC4_GMP_IMP
+#  include "util/rational_gmp_imp.h"
+#endif /* CVC4_GMP_IMP */
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 0960b79b9..7baf8d3bf 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -2,7 +2,7 @@
 /*! \file rational_cln_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters, cconway
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
@@ -16,13 +16,15 @@
  ** A multi-precision rational constant.
  **/
 
-#ifdef __CVC4__USE_CLN_IMP
-
-
-#include "util/integer.h"
+#include "cvc4autoconfig.h"
 #include "util/rational.h"
+#include "util/integer.h"
 #include <string>
 
+#ifndef CVC4_CLN_IMP
+#  error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
 using namespace std;
 using namespace CVC4;
 
@@ -51,4 +53,3 @@ std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
   return os << q.toString();
 }
 
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 347c1d195..ae172f262 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file rational.h
+/*! \file rational_cln_imp.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,13 +11,12 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Multi-precision rational constants.
+ ** \brief Multiprecision rational constants; wraps a CLN multiprecision
+ ** rational.
  **
- ** Multi-precision rational constants.
+ ** Multiprecision rational constants; wraps a CLN multiprecision rational.
  **/
 
-#ifdef __CVC4__USE_CLN_IMP
-
 #include "cvc4_public.h"
 
 #ifndef __CVC4__RATIONAL_H
@@ -283,4 +282,3 @@ std::ostream& operator<<(std::ostream& os, const Rational& n);
 
 #endif /* __CVC4__RATIONAL_H */
 
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index e5ff11c07..a0af69b4c 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file rational.cpp
+/*! \file rational_gmp_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters, cconway
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
@@ -15,12 +15,16 @@
  **
  ** A multi-precision rational constant.
  **/
-#ifdef __CVC4__USE_GMP_IMP
 
-#include "util/integer.h"
+#include "cvc4autoconfig.h"
 #include "util/rational.h"
+#include "util/integer.h"
 #include <string>
 
+#ifndef CVC4_GMP_IMP
+#  error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
 using namespace std;
 using namespace CVC4;
 
@@ -49,4 +53,3 @@ std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
   return os << q.toString();
 }
 
-#endif /* __CVC4__USE_GMP_IMP */
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index ab88a0d52..ce94dfe24 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file rational.h
+/*! \file rational_gmp_imp.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,11 +11,11 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Multi-precision rational constants.
+ ** \brief Multiprecision rational constants; wraps a GMP multiprecision
+ ** rational.
  **
- ** Multi-precision rational constants.
+ ** Multiprecision rational constants; wraps a GMP multiprecision rational.
  **/
-#ifdef __CVC4__USE_GMP_IMP
 
 #include "cvc4_public.h"
 
@@ -259,4 +259,4 @@ std::ostream& operator<<(std::ostream& os, const Rational& n);
 }/* CVC4 namespace */
 
 #endif /* __CVC4__RATIONAL_H */
-#endif /* __CVC4__USE_GMP_IMP */
+
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 6b32c46bb..607075658 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences