* 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

1 files changed, 56 insertions, 0 deletions

diff --git a/test/regress/README b/test/regress/README
new file mode 100644
index 000000000..bef93b140
--- /dev/null
+++ b/test/regress/README
@@ -0,0 +1,56 @@
+Regressions
+===========
+
+To insert a new regression, add the file to Subversion, for example:
+
+  svn add regress/regress0/testMyFunctionality.cvc
+
+Also add it to the relevant Makefile.am, here, in regress/regress0/Makefile.am.
+
+A number of regressions exist under test/regress that aren't listed in any
+Makefile.am.  These are regressions that may someday be included in the standard
+suite of tests, but aren't yet included (perhaps they test functionality not
+yet supported).
+
+If you want to add a new directory of regressions, add the directory name to
+SUBDIRS (with . running first, by convention), and set up the new directory
+with a new Makefile.am, adding all to the Subversion repository.
+
+=== EXPECTED OUTPUT, ERROR, AND EXIT CODES ===
+
+In the case of CVC input, you can specify expected stdout, stderr, and exit
+codes with the following lines directly in the CVC regression file:
+
+% EXPECT: stdout
+% EXPECT-ERROR: stderr
+% EXIT: 0
+
+expects an exit status of 0 from cvc4, the single line "stderr" on stderr,
+and the single line "stdout" on stdout.  You can repeat EXPECT and EXPECT-ERROR
+lines as many times as you like, and at different points of the file.  This is
+useful for multiple queries:
+
+% EXPECT: INVALID
+QUERY FALSE;
+% EXPECT: VALID
+QUERY TRUE;
+% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: Parse Error: regress.cvc:7.13: Unexpected token: 'error'.
+syntax error;
+% EXIT: 1
+
+Use of % gestures in CVC format is natural, as these are comments and ignored
+by the CVC presentation language lexer.  In SMT and SMT2 formats, you can do the
+same, putting % gestures in the file.  However, the run_regression script
+separates these from the benchmark before running cvc4, so the cvc4 SMT and SMT2
+lexers never see (and get tripped up on) the % gestures.  But there's then the
+annoyance that you can't run SMT and SMT2 regressions from the command line
+without the aid of the run_regression script.  So, if you prefer, you can separate
+the benchmark from the output expectations yourself, putting the benchmark in
+(e.g.) regress/regress0/benchmark.smt, and the % EXPECT: lines in
+regress/regress0/benchmark.smt.expect, which is specifically looked for by
+the run_regression script.  If such an .expect file exists, the benchmark
+is left verbatim (and never processed to remove the % EXPECT: lines) by the
+run_regression script.
+
+ -- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 01 Jul 2010 13:36:53 -0400