Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

1 files changed, 141 insertions, 95 deletions

diff --git a/configure.ac b/configure.ac
index 192bfcff2..1b23bf1f0 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1,10 +1,11 @@
 #                                               -*- Autoconf -*-
 # Process this file with autoconf to produce a configure script.
 
-m4_define(_CVC4_MAJOR,          0 )      dnl version (major)
-m4_define(_CVC4_MINOR,          0 )      dnl version (minor)
-m4_define(_CVC4_RELEASE,        0 )      dnl version (alpha)
-m4_define(_CVC4_RELEASE_STRING, [prerelease]) dnl version string
+m4_define(_CVC4_MAJOR,          0)       dnl version (major)
+m4_define(_CVC4_MINOR,          0)       dnl version (minor)
+m4_define(_CVC4_RELEASE,        0)       dnl version (alpha)
+m4_define(_CVC4_EXTRAVERSION,   [prerelease])      dnl version (extra)
+m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[0],,[.]_CVC4_RELEASE)_CVC4_EXTRAVERSION) dnl version string
 
 dnl Preprocess CL args. Defined in config/cvc4.m4
 CVC4_AC_INIT
@@ -21,6 +22,7 @@ m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
 CVC4_MAJOR=_CVC4_MAJOR
 CVC4_MINOR=_CVC4_MINOR
 CVC4_RELEASE=_CVC4_RELEASE
+CVC4_EXTRAVERSION=_CVC4_EXTRAVERSION
 CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING
 
 # Libtool version numbers for libraries
@@ -41,8 +43,10 @@ CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING
 # For guidance on when to change the version number, refer to the
 # developer's guide.
 
-CVC4_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
-CVC4_PARSER_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
+CVC4_LIBRARY_VERSION=0:0:0
+CVC4_PARSER_LIBRARY_VERSION=0:0:0
+CVC4_COMPAT_LIBRARY_VERSION=0:0:0
+CVC4_BINDINGS_LIBRARY_VERSION=0:0:0
 
 # Using the AC_CANONICAL_* macros destroy the command line you get
 # from $@, which we want later for determining the build profile.  So
@@ -77,6 +81,8 @@ AC_CANONICAL_BUILD
 AC_CANONICAL_HOST
 AC_CANONICAL_TARGET
 
+as_me=configure
+
 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
   enable_static=yes
 fi
@@ -90,7 +96,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_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}"; then
   custom_build_profile=no
 else
   custom_build_profile=yes
@@ -131,6 +137,13 @@ if test -n "${enable_tracing+set}"; then
     btargs="$btargs notracing"
   fi
 fi
+if test -n "${enable_dumping+set}"; then
+  if test "$enable_dumping" = yes; then
+    btargs="$btargs dumping"
+  else
+    btargs="$btargs nodumping"
+  fi
+fi
 if test -n "${enable_muzzle+set}"; then
   if test "$enable_muzzle" = yes; then
     btargs="$btargs muzzle"
@@ -327,10 +340,12 @@ else
   AC_MSG_RESULT([this one (user-specified)])
 fi
 
+as_me=configure
+
 # Unpack standard build types. Any particular options can be overriden with
 # --enable/disable-X options
 case "$with_build" in
-  production) # highly optimized, no assertions, no tracing
+  production) # highly optimized, no assertions, no tracing, dumping
     CVC4CPPFLAGS=
     CVC4CXXFLAGS=
     CVC4CFLAGS=
@@ -343,9 +358,10 @@ case "$with_build" in
     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
+    if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
-  debug) # unoptimized, debug symbols, assertions, tracing
+  debug) # unoptimized, debug symbols, assertions, tracing, dumping
     CVC4CPPFLAGS=-DCVC4_DEBUG
     CVC4CXXFLAGS='-fno-inline'
     CVC4CFLAGS='-fno-inline'
@@ -357,9 +373,10 @@ case "$with_build" in
     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
+    if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
-  default) # moderately optimized, assertions, tracing
+  default) # moderately optimized, assertions, tracing, dumping
     CVC4CPPFLAGS=
     CVC4CXXFLAGS=
     CVC4CFLAGS=
@@ -372,9 +389,10 @@ case "$with_build" in
     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
+    if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
-  competition) # maximally optimized, no assertions, no tracing, muzzled
+  competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
     CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
     CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
     CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
@@ -387,6 +405,7 @@ case "$with_build" in
     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
+    if test -z "${enable_dumping+set}"      ; then enable_dumping=no                ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
     if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
     if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
@@ -520,6 +539,21 @@ if test "$enable_tracing" = yes; then
   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
 fi
 
+AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
+AC_ARG_ENABLE([dumping],
+  [AS_HELP_STRING([--disable-dumping],
+     [remove all dumping code from CVC4])])
+
+if test -z "${enable_dumping+set}"; then
+  enable_dumping=yes
+fi
+
+AC_MSG_RESULT([$enable_dumping])
+
+if test "$enable_dumping" = yes; then
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
+fi
+
 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 AC_ARG_ENABLE([muzzle],
   [AS_HELP_STRING([--enable-muzzle],
@@ -603,11 +637,27 @@ fi
 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 AC_PROG_ANTLR
 
+# Doxygen configuration
+AC_ARG_ENABLE([internals-documentation],
+  [AS_HELP_STRING([--enable-internals-documentation],
+     [build Doxygen documentation for static and private member functions])])
+if test "$enable_internals_documentation" = yes; then
+  DOXYGEN_EXTRACT_PRIVATE=YES
+  DOXYGEN_EXTRACT_STATIC=YES
+else
+  DOXYGEN_EXTRACT_PRIVATE=NO
+  DOXYGEN_EXTRACT_STATIC=NO
+fi
+AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
+AC_SUBST([DOXYGEN_EXTRACT_STATIC])
+
+DX_MAN_FEATURE(OFF)
 DX_PDF_FEATURE(OFF)
 DX_PS_FEATURE(OFF)
 DX_DOT_FEATURE(OFF)
 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
 
+AC_ARG_ENABLE([unit-testing], AS_HELP_STRING([--disable-unit-testing], [don't build support for unit testing, even if available]), , [enable_unit_testing=check])
 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
 
 AC_SUBST([CXXTEST])
@@ -631,7 +681,11 @@ AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 if test -z "$CXXTESTGEN"; then
   AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
 fi
-if test -z "$CXXTESTGEN"; then
+if test "$enable_unit_testing" = "no"; then
+  AC_MSG_NOTICE([unit tests disabled by user request.])
+  CXXTESTGEN=
+  CXXTEST=
+elif test -z "$CXXTESTGEN"; then
   AC_MSG_NOTICE([unit tests disabled, neither cxxtestgen.pl nor cxxtestgen.py found.])
 elif test -z "$CXXTEST"; then
   CXXTEST=`dirname "$CXXTESTGEN"`
@@ -650,6 +704,10 @@ elif test -z "$CXXTEST"; then
   fi
 fi
 
+if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
+  AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
+fi
+
 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 
 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
@@ -684,67 +742,18 @@ AC_SEARCH_LIBS([clock_gettime], [rt],
                           [Defined to 1 if clock_gettime() is supported by the platform.])],
                [AC_LIBOBJ([clock_gettime])])
 
-CUDD_CPPFLAGS=
-CUDD_LDFLAGS=
-cvc4cudd=no
-AC_MSG_CHECKING([whether user requested CUDD support])
-AC_ARG_WITH([cudd], [AS_HELP_STRING([--with-cudd], [force linking/not linking against CUDD])], [], [with_cudd=check])
-if test "$with_cudd" = no; then
-  AC_MSG_RESULT([no, CUDD disabled by user])
-else
-  if test "$with_cudd" = check; then
-    AC_MSG_RESULT([no preference by user, will auto-detect])
-  else
-    AC_MSG_RESULT([yes, CUDD enabled by user])
-  fi
-  AC_ARG_WITH([cudd-dir],
-    [AS_HELP_STRING([--with-cudd-dir=DIR], [path to cudd installation])],
-    [CUDD_DIR="$withval"])
-  if test -z "$CUDD_DIR"; then
-    CUDD_DIR=/usr
-  fi
-  AC_MSG_CHECKING([for cudd includes under $CUDD_DIR])
-  result="not found"
-  for cuddinc in "$CUDD_DIR/include" "$CUDD_DIR/include/cudd" "$CUDD_DIR"; do
-    if test -r "$cuddinc/cudd.h"; then
-      dnl TODO - should do a TRY_COMPILE instead
-      CUDD_CPPFLAGS="\"-I$cuddinc\""
-      result="$cuddinc"
-      cvc4cudd=yes
-      break
-    fi
-  done
-  AC_MSG_RESULT([$result])
-  if test $cvc4cudd = yes; then
-    AC_MSG_CHECKING([for cudd libraries under $CUDD_DIR])
-    cvc4cudd=no
-    result="not found"
-    for cuddlib in "$CUDD_DIR/lib" "$CUDD_DIR/lib/cudd" "$CUDD_DIR"; do
-      if test -r "$cuddlib/libcuddxx.la"; then
-        dnl TODO - should do a TRY_LINK instead, that has the extra benefit
-        dnl of making sure both shared & static work
-        CUDD_LDFLAGS="\"-L$cuddlib\" -lcuddxx"
-        result="$cuddlib"
-        cvc4cudd=yes
-        break
-      fi
-    done
-    AC_MSG_RESULT([$result]);
-    if test $cvc4cudd = yes; then
-      AC_DEFINE_UNQUOTED(CVC4_CUDD, [], [Defined if using the CU Decision Diagram package (cudd).])
-    fi
-  fi
-fi
-AC_SUBST([CUDD_CPPFLAGS])
-AC_SUBST([CUDD_LDFLAGS])
-
-if test "$with_cudd" = yes -a "$cvc4cudd" = no; then
-  AC_ERROR([--with-cudd was given, but cudd not available])
-fi
+# Check for the presence of CUDD libraries
+CVC4_CHECK_CUDD
 
 # Check for antlr C++ runtime (defined in config/antlr.m4)
 AC_LIB_ANTLR
 
+# Check for user preferences for language bindings to build, and for
+# build support.  The arg list is the default set if unspecified by
+# the user (the actual built set is the subset that appears to be
+# supported by the build host).
+CVC4_CHECK_BINDINGS dnl ([java csharp perl php python ruby tcl ocaml])
+
 # Checks for header files.
 AC_CHECK_HEADERS([getopt.h unistd.h])
 
@@ -756,28 +765,19 @@ AC_CHECK_HEADERS([getopt.h unistd.h])
 #AC_TYPE_UINT64_T
 #AC_TYPE_SIZE_T
 
-# Whether to compile with google profiling tools
-cvc4_use_google_perftools=0
-AC_ARG_WITH(
-    [google_perftools],
-    AS_HELP_STRING(
-        [--with-google-perftools],
-        [use Google Performance Tools]
-    ),
-    [if test "$withval" != no; then
-        cvc4_use_google_perftools=1
-     fi
-    ]
-)
-
-AC_MSG_CHECKING([whether to link in google perftools libraries])
-if test $cvc4_use_google_perftools = 1; then
+# Whether to build compatibility library
+CVC4_BUILD_LIBCOMPAT=yes
+AC_ARG_WITH([compat],
+    AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
+    [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
+AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
+if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
   AC_MSG_RESULT([yes])
-  AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
-  AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
 else
-  AC_MSG_RESULT([no (user didn't request it)])
+  AC_MSG_RESULT([no, disabled by user])
 fi
+AC_SUBST(CVC4_BUILD_LIBCOMPAT)
+AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
 
 # Check for availability of TLS support (e.g. __thread storage class)
 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
@@ -798,11 +798,27 @@ fi
 AC_SUBST([CVC4_TLS])
 AC_SUBST([CVC4_TLS_SUPPORTED])
 
-# Checks for library functions.
-# (empty)
-
-# Some definitions for config.h
-# (empty)
+# Whether to compile with google profiling tools
+cvc4_use_google_perftools=0
+AC_ARG_WITH(
+    [google_perftools],
+    AS_HELP_STRING(
+        [--with-google-perftools],
+        [use Google Performance Tools]
+    ),
+    [if test "$withval" != no; then
+        cvc4_use_google_perftools=1
+     fi
+    ]
+)
+AC_MSG_CHECKING([whether to link in google perftools libraries])
+if test $cvc4_use_google_perftools = 1; then
+  AC_MSG_RESULT([yes])
+  AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
+  AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
+else
+  AC_MSG_RESULT([no (user didn't request it)])
+fi
 
 # Prepare configure output
 
@@ -817,10 +833,13 @@ AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
 
 AC_SUBST(CVC4_LIBRARY_VERSION)
 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
+AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
+AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
 
 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
+AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
 
 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
@@ -863,6 +882,9 @@ fi
 AC_SUBST(CVC4_USE_CLN_IMP)
 AC_SUBST(CVC4_USE_GMP_IMP)
 
+MAN_DATE=`date '+%B %Y'`
+AC_SUBST(MAN_DATE)
+
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile]
@@ -873,6 +895,12 @@ CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
 
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
+
 AC_OUTPUT
 
 # Final information to the user
@@ -889,6 +917,8 @@ fi
 support_unit_tests='cxxtest not found; unit tests not supported'
 if test -n "$CXXTEST"; then
   support_unit_tests='unit testing infrastructure enabled in build directory'
+elif test "$enable_unit_testing" = no; then
+  support_unit_tests='unit testing disabled by user'
 fi
 
 if test "$enable_optimized" = yes; then
@@ -912,6 +942,15 @@ else
   mplibrary='gmp (LGPL)'
 fi
 
+CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
+CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
+if test "$CVC4_BUILD_LIBCOMPAT" = no; then
+  CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
+fi
+if test -z "$CVC4_LANGUAGE_BINDINGS"; then
+  CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
+fi
+
 cat <<EOF
 
 CVC4 $VERSION
@@ -924,6 +963,7 @@ Statistics   : $enable_statistics
 Replay       : $enable_replay
 Assertions   : $enable_assertions
 Tracing      : $enable_tracing
+Dumping      : $enable_dumping
 Muzzle       : $enable_muzzle
 
 Unit tests   : $support_unit_tests
@@ -936,6 +976,8 @@ TLS support  : $CVC4_TLS
 Static libs  : $enable_static
 Shared libs  : $enable_shared
 Static binary: $enable_static_binary
+Compat lib   : $CVC4_BUILD_LIBCOMPAT
+Bindings     : ${CVC4_LANGUAGE_BINDINGS:-none}
 
 MP library   : $mplibrary
 
@@ -945,8 +987,12 @@ CFLAGS       : $CFLAGS
 LIBS         : $LIBS
 LDFLAGS      : $LDFLAGS
 
-libcvc4 version      : $CVC4_LIBRARY_VERSION
-libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
+libcvc4 version        : $CVC4_LIBRARY_VERSION
+libcvc4parser version  : $CVC4_PARSER_LIBRARY_VERSION
+libcvc4compat version  : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
+libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
+
+Install into : $prefix
 
 ${licensewarn}Now just type make, followed by make check or make install, as you like.