* Added white-box TheoryEngine test that tests the rewriter

* Added regression documentation to test/regress/README

* Added ability to print types of vars in expr printouts
  with iomanipulator Node::printtypes(true)... for example,
    Warning() << Node::printtypes(true) << n << std::endl;

* Types-printing can be specified on the command line with
  --print-expr-types

* Improved type handling facilities and theoryOf().
  For now, SORT_TYPE moved from builtin theory to UF theory
  to match old behavior.

* Additional gdb debug functionality.  Now we have:

    debugPrintNode(Node)            debugPrintRawNode(Node)
    debugPrintTNode(TNode)          debugPrintRawTNode(TNode)
    debugPrintTypeNode(TypeNode)    debugPrintRawTypeNode(TypeNode)
    debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)

  they all print a {Node,TNode,NodeValue*} from the debugger.
  The "Raw" versions print a very low-level AST-like form.
  The regular versions do the same as operator<<, but force
  full printing on (no depth-limiting).

* Other trivial fixes

2 files changed, 30 insertions, 22 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 88840a8e8..e050a0dfb 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -68,7 +68,8 @@ enum OptionValue {
   USE_MMAP,
   SHOW_CONFIG,
   STRICT_PARSING,
-  DEFAULT_EXPR_DEPTH
+  DEFAULT_EXPR_DEPTH,
+  PRINT_EXPR_TYPES
 };/* enum OptionValue */
 
 /**
@@ -113,6 +114,7 @@ static struct option cmdlineOptions[] = {
   { "mmap",        no_argument      , NULL, USE_MMAP    },
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
+  { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
 };/* if you add things to the above, please remember to update usage.h! */
 
 /** Full argv[0] */
@@ -234,6 +236,17 @@ throw(OptionException) {
       }
       break;
 
+    case PRINT_EXPR_TYPES:
+      {
+        Debug.getStream() << Expr::printtypes(true);
+        Trace.getStream() << Expr::printtypes(true);
+        Notice.getStream() << Expr::printtypes(true);
+        Chat.getStream() << Expr::printtypes(true);
+        Message.getStream() << Expr::printtypes(true);
+        Warning.getStream() << Expr::printtypes(true);
+      }
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/usage.h b/src/main/usage.h
index ef37b7650..b56f083a5 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -30,27 +30,22 @@ usage: %s [options] [input-file]\n\
 Without an input file, or with `-', CVC4 reads from standard input.\n\
 \n\
 CVC4 options:\n\
-   --lang | -L      force input language (default is `auto'; see --lang help)\n\
-   --version | -V   identify this CVC4 binary\n\
-   --help | -h      this command line reference\n\
-   --parse-only     exit after parsing input\n\
-   --mmap           memory map file input\n\
-   --show-config    show CVC4 static configuration\n"
-#ifdef CVC4_DEBUG
-"\
-   --segv-nospin    don't spin on segfault waiting for gdb\n"
-#endif
-#ifndef CVC4_MUZZLE
-"\
-   --no-checking    disable semantic checks in the parser\n\
-   --strict-parsing fail on inputs that are not strictly conformant (SMT2 only)\n\
-   --verbose | -v   increase verbosity (repeatable)\n\
-   --quiet | -q     decrease verbosity (repeatable)\n\
-   --trace | -t     tracing for something (e.g. --trace pushpop)\n\
-   --debug | -d     debugging for something (e.g. --debug arith), implies -t\n\
-   --stats          give statistics on exit\n\
-   --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n"
-#endif
+   --lang | -L            force input language (default is `auto'; see --lang help)\n\
+   --version | -V         identify this CVC4 binary\n\
+   --help | -h            this command line reference\n\
+   --parse-only           exit after parsing input\n\
+   --mmap                 memory map file input\n\
+   --show-config          show CVC4 static configuration\n\
+   --segv-nospin          don't spin on segfault waiting for gdb\n\
+   --no-checking          disable semantic checks in the parser\n\
+   --strict-parsing       fail on inputs that are not strictly conformant (SMT2 only)\n\
+   --verbose | -v         increase verbosity (repeatable)\n\
+   --quiet | -q           decrease verbosity (repeatable)\n\
+   --trace | -t           tracing for something (e.g. --trace pushpop)\n\
+   --debug | -d           debugging for something (e.g. --debug arith), implies -t\n\
+   --stats                give statistics on exit\n\
+   --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
+   --print-expr-types     print types with variables when printing exprs\n"
 ;
 
 }/* CVC4::main namespace */