diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
commit | 83a143b1dd78e5d7f07666fbec1362dd60348116 (patch) | |
tree | 08400222d94f4760c7155fea787ac7e78b7b0dfc /test/regress | |
parent | a8566c313e9b5eb8248eaeea642a9c72c803dcfa (diff) |
* 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
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/README | 56 |
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 |