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, 21 insertions, 0 deletions

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 479ef6d11..69f7019ab 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -107,6 +107,25 @@ function endtheory {
   seen_endtheory=true
 }
 
+function typechecker {
+  # typechecker header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  typechecker_includes="${typechecker_includes}
+#include \"$1\""
+}
+
+function typerule {
+  # typerule OPERATOR typechecking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  typerules="${typerules}
+  case kind::$1:
+    typeNode = $2::computeType(nodeManager, n, check);
+    break;
+"
+}
+
 function sort {
   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
@@ -225,6 +244,8 @@ for var in \
     getConst_implementations \
     mkConst_instantiations \
     mkConst_implementations \
+    typechecker_includes \
+    typerules \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done