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, 102 insertions, 0 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