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.

5 files changed, 226 insertions, 6 deletions

diff --git a/config/bindings.m4 b/config/bindings.m4
new file mode 100644
index 000000000..cdab33e3e
--- /dev/null
+++ b/config/bindings.m4
@@ -0,0 +1,102 @@
+# CVC4_SUPPORTED_BINDINGS
+# -----------------------
+# Supported language bindings for CVC4.
+AC_DEFUN([CVC4_SUPPORTED_BINDINGS],
+[java,csharp,perl,php,python,ruby,tcl,ocaml])
+
+# CVC4_CHECK_BINDINGS(DEFAULT_BINDINGS_LIST)
+# ------------------------------------------
+# Check for user language binding preferences, and what is possible
+# to build on the build host.
+AC_DEFUN([CVC4_CHECK_BINDINGS], [
+dnl Check for SWIG (for building language bindings)
+noswig=no
+
+m4_foreach(lang,[CVC4_SUPPORTED_BINDINGS],
+[[cvc4_build_]]lang[[_bindings=no
+]])
+
+AC_ARG_VAR(SWIG, [SWIG binary (used to generate language bindings)])
+AC_ARG_WITH([swig],
+  [AS_HELP_STRING([--with-swig=BINARY], [path to swig binary])],
+  [if test "$withval" = no; then noswig=yes; else SWIG="$withval"; fi])
+AC_ARG_ENABLE([language-bindings],
+  [AS_HELP_STRING([--enable-language-bindings=][CVC4_SUPPORTED_BINDINGS], [specify language bindings to build])],
+  [cvc4_check_for_bindings=no; if test "$enableval" = no; then try_bindings=; else try_bindings="$enableval"; fi],
+  [cvc4_check_for_bindings=yes; try_bindings=])
+CVC4_LANGUAGE_BINDINGS=
+if test "$noswig" = yes; then
+  AC_MSG_WARN([use of swig disabled by user.])
+  SWIG=
+  if test "$cvc4_check_for_bindings" = no -a -n "$try_bindings"; then
+    AC_MSG_ERROR([language bindings requested by user, but swig disabled.])
+  fi
+else
+  if test -z "$SWIG"; then
+    AC_CHECK_PROGS(SWIG, swig, swig, [])
+  else
+    AC_CHECK_PROG(SWIG, "$SWIG", "$SWIG", [])
+  fi
+  if test -z "$SWIG"; then
+    AC_MSG_WARN([language bindings disabled, swig not found.])
+    if test "$cvc4_check_for_bindings" = no -a -n "$try_bindings"; then
+      AC_MSG_ERROR([language bindings requested by user, but swig disabled.])
+    fi
+  else
+    AC_MSG_CHECKING([for requested user language bindings])
+    if test "$cvc4_check_for_bindings" = yes; then
+      try_bindings='$1'
+    else
+      try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
+    fi
+    AC_MSG_RESULT([$try_bindings])
+    JAVA_INCLUDES=
+    for binding in $try_bindings; do
+      binding_error=no
+      AC_MSG_CHECKING([for availability of $binding binding])
+      case "$binding" in
+        c++) AC_MSG_RESULT([C++ is built by default]);;
+        java)
+          JAVA_INCLUDES="-I/usr/lib/jvm/java-6-sun-1.6.0.26/include -I/usr/lib/jvm/java-6-sun-1.6.0.26/include/linux"
+          cvc4_build_java_binding=yes
+          AC_MSG_RESULT([Java support will be built]);;
+        csharp)
+          binding_error=yes
+          AC_MSG_RESULT([$binding not supported yet]);;
+        perl)
+          binding_error=yes
+          AC_MSG_RESULT([$binding not supported yet]);;
+        php)
+          binding_error=yes
+          AC_MSG_RESULT([$binding not supported yet]);;
+        python)
+          binding_error=yes
+          AC_MSG_RESULT([$binding not supported yet]);;
+        ruby)
+          binding_error=yes
+          AC_MSG_RESULT([$binding not supported yet]);;
+        tcl)
+          binding_error=yes
+          AC_MSG_RESULT([$binding not supported yet]);;
+        ocaml)
+          binding_error=yes
+          AC_MSG_RESULT([$binding not supported yet]);;
+        *) AC_MSG_RESULT([unknown binding]); binding_error=yes;;
+      esac
+      if test "$binding_error" = yes -a "$cvc4_check_for_bindings" = no; then
+        AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built.])
+      fi
+      CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
+    done
+  fi
+fi
+
+m4_foreach([lang], [CVC4_SUPPORTED_BINDINGS],
+[AM_CONDITIONAL([CVC4_LANGUAGE_BINDING_]m4_toupper(lang), [test "$cvc4_build_]lang[_bindings" = yes])
+])dnl
+
+AC_SUBST(SWIG)
+AC_SUBST(JAVA_INCLUDES)
+AC_SUBST(CVC4_LANGUAGE_BINDINGS)
+
+])# CVC4_CHECK_BINDINGS
diff --git a/config/cudd.m4 b/config/cudd.m4
new file mode 100644
index 000000000..7a569a3e9
--- /dev/null
+++ b/config/cudd.m4
@@ -0,0 +1,116 @@
+# CVC4_CHECK_CUDD
+# ---------------
+# Check for CUDD libraries and headers.  Complicated because different
+# packagers have packaged it differently.
+AC_DEFUN([CVC4_CHECK_CUDD], [
+CUDD_CPPFLAGS=
+CUDD_LDFLAGS=
+CUDD_LIBS=
+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_set=yes],
+  [with_cudd=check; with_cudd_set=no])
+AC_ARG_WITH([cudd-dir],
+  [AS_HELP_STRING([--with-cudd-dir=DIR], [path to cudd installation])],
+  [CUDD_DIR="$withval"],
+  [if test "$with_cudd_set" = yes -a "$with_cudd" != yes -a "$with_cudd" != no -a "$with_cudd" != check; then
+     dnl maybe the user gave --with-cudd=DIR ?
+     CUDD_DIR="$with_cudd"
+     with_cudd=yes
+   fi])
+if test -n "$CUDD_DIR" -a "$with_cudd_set" = no; then
+  dnl if --with-cudd-dir or CUDD_DIR given, force --with-cudd
+  dnl unless --with-cudd=... given explicitly
+  with_cudd=yes
+fi
+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
+  if test -z "$CUDD_DIR"; then
+    dnl default location if unspecified
+    CUDD_DIR=/usr
+  fi
+  AC_MSG_CHECKING([for C++ cudd includes under $CUDD_DIR])
+  result="not found"
+  cvc4save_CPPFLAGS="$CPPFLAGS"
+  AC_LANG_PUSH([C++])
+  for cuddinc in "$CUDD_DIR/include" "$CUDD_DIR/include/cudd" "$CUDD_DIR"; do
+    CPPFLAGS="$cvc4save_CPPFLAGS -I$cuddinc"
+    AC_COMPILE_IFELSE(
+      [AC_LANG_PROGRAM([
+#include <stdio.h>
+#include "cuddObj.hh"],
+         [
+Cudd c;
+BDD b = c.bddVar() | c.bddOne();
+])],
+      [ CUDD_CPPFLAGS="-I$cuddinc"
+        result="$cuddinc"
+        cvc4cudd=yes
+        break
+      ])
+  done
+  CPPFLAGS="$cvc4save_CPPFLAGS"
+  AC_MSG_RESULT([$result])
+  if test $cvc4cudd = yes; then
+    AC_MSG_CHECKING([for C++ cudd libraries under $CUDD_DIR])
+    cvc4cudd=no
+    result="not found"
+    cvc4save_CPPFLAGS="$CPPFLAGS"
+    CPPFLAGS="$CPPFLAGS $CUDD_CPPFLAGS"
+    cvc4save_LDFLAGS="$LDFLAGS"
+    cvc4save_LIBS="$LIBS"
+    cvc4save_ac_link="$ac_link"
+    ac_link="libtool --mode=link $ac_link"
+    dnl This is messy.  We try to find Fedora packages, Debian packages, and
+    dnl a built CUDD source directory.  We can't -lutil or -lst because these
+    dnl names of CUDD libraries conflict with other libraries commonly
+    dnl installed.  So we fall back to naming them directly.  The CUDD
+    dnl sources build static libs only, so we go with that.
+    for cuddlibdirs in "-L$CUDD_DIR/lib" "-L$CUDD_DIR/lib/cudd" "-L$CUDD_DIR"; do
+      for cuddlibs in -lcuddxx -lcuddobj; do
+        LDFLAGS="$cvc4save_LDFLAGS $cuddlibdirs"
+        LIBS="$cvc4save_LIBS $cuddlibs"
+        AC_LINK_IFELSE(
+          [AC_LANG_PROGRAM([
+#include <stdio.h>
+#include "cuddObj.hh"],
+             [
+Cudd c;
+BDD b = c.bddVar() | c.bddOne();
+])],
+          [ CUDD_LDFLAGS="$cuddlibdirs"
+            CUDD_LIBS="$cuddlibs"
+            result="$cuddlibdirs $cuddlibs"
+            cvc4cudd=yes
+            break
+          ])
+      done
+      if test -n "$CUDD_LDFLAGS"; then break; fi
+    done
+    CPPFLAGS="$cvc4save_CPPFLAGS"
+    LDFLAGS="$cvc4save_LDFLAGS"
+    LIBS="$cvc4save_LIBS"
+    ac_link="$cvc4save_ac_link"
+    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
+  AC_LANG_POP([C++])
+fi
+AC_SUBST([CUDD_CPPFLAGS])
+AC_SUBST([CUDD_LDFLAGS])
+AC_SUBST([CUDD_LIBS])
+
+if test "$with_cudd" = yes -a "$cvc4cudd" = no; then
+  AC_ERROR([--with-cudd was given, but cudd not available])
+fi
+])# CVC4_CHECK_CUDD
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index c58d976b5..4adc88c61 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -22,8 +22,9 @@ do
       # regexp `\?' not supported on Mac OS X
       ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
       ac_cvc4_build_profile_set=yes
+      as_me=configure
       AC_MSG_NOTICE([CVC4: building profile $ac_option_build])
-      for x in optimized statistics replay assertions tracing muzzle coverage profiling; do
+      for x in optimized statistics replay assertions tracing dumping muzzle coverage profiling; 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 }\"--disable-$x\""'
         fi
diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index 65d3c3103..6787ea7f9 100644
--- a/config/doxygen.cfg
+++ b/config/doxygen.cfg
@@ -302,12 +302,12 @@ EXTRACT_ALL            = YES
 # If the EXTRACT_PRIVATE tag is set to YES all private members of a class
 # will be included in the documentation.
 
-EXTRACT_PRIVATE        = YES
+EXTRACT_PRIVATE        = $(DOXYGEN_EXTRACT_PRIVATE)
 
 # If the EXTRACT_STATIC tag is set to YES all static members of a file
 # will be included in the documentation.
 
-EXTRACT_STATIC         = YES
+EXTRACT_STATIC         = $(DOXYGEN_EXTRACT_STATIC)
 
 # If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs)
 # defined locally in source files will be included in the documentation.
diff --git a/config/mkbuilddir b/config/mkbuilddir
index ddec67023..87cd3460e 100755
--- a/config/mkbuilddir
+++ b/config/mkbuilddir
@@ -21,23 +21,24 @@ fi
 target=$1
 build_type=$2
 
+: ${as_me:=mkbuilddir}
 : ${as_echo:=echo}
 : ${RM:=rm -f}
 : ${MKDIR_P:=mkdir -p}
 : ${LN_S:=ln -s}
 
-$as_echo "Setting up builds/$target/$build_type..."
+$as_echo "$as_me: Setting up builds/$target/$build_type..."
 $RM config.log config.status confdefs.h builds/Makefile
 $MKDIR_P "builds/$target/$build_type"
 $LN_S "$target/$build_type/Makefile.builds" builds/Makefile
 
-$as_echo "Creating builds/current..."
+$as_echo "$as_me: Creating builds/current..."
 (echo "# This is the most-recently-configured CVC4 build"; \
  echo "# 'make' in the top-level source directory applies to this build"; \
  echo "CURRENT_BUILD = $target/$build_type") > builds/current
 
 for dir in src test; do
-  $as_echo "Linking builds/$dir..."
+  $as_echo "$as_me: Linking builds/$dir..."
   $RM "builds/$dir"
   $LN_S "$target/$build_type/$dir" "builds/$dir"
 done