From: Andres Noetzli Date: Thu, 5 Apr 2018 05:43:48 +0000 (-0700) Subject: Update README for regression tests (#1746) X-Git-Tag: cvc5-1.0.0~5177 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1548aadcc83a8b25f16a9ed4530b21f5a325b908;p=cvc5.git Update README for regression tests (#1746) --- diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index e1a3d7e7f..f068ce9ad 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -56,4 +56,4 @@ EXTRA_DIST = \ Makefile.levels \ Makefile.tests \ run_regression \ - README + README.md diff --git a/test/regress/README b/test/regress/README deleted file mode 100644 index 6fcdf16a3..000000000 --- a/test/regress/README +++ /dev/null @@ -1,63 +0,0 @@ -Regressions -=========== - -To insert a new regression, add the file to Subversion, for example: - - git 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 - -[Outdated: please also see edit below as an addendum.] -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 Thu, 01 Jul 2010 13:36:53 -0400 - -[Edit 2014/03/14: No support for '%' in .smt2 files any -longer. Please use ';' or create separate .expect files. Very few test -were using this "feature" and was causing issues because temp file -name changed the expected error output string. '%' works for .smt files ---Kshitij] diff --git a/test/regress/README.md b/test/regress/README.md new file mode 100644 index 000000000..2c347bc48 --- /dev/null +++ b/test/regress/README.md @@ -0,0 +1,103 @@ +# Regression + +## Regression Levels and Running Regression Tests + +CVC4's regression tests are divided into 5 levels (level 0 to 4). Higher +regression levels are reserved for longer running regressions. To run +regressions up to a certain level use `make regressX` where `X` designates the +level. `make regress` by default runs levels 0 and 1. On Travis, we only run +regression level 0 to keep the time short. During our nightly builds, we run +regression level 2. + +To only run some benchmarks, you can use the `TEST_REGEX` environment variable. +For example: + +``` +TEST_REGEX=quantifiers make regress0 +``` + +Runs regression tests from level 0 that have "quantifiers" in their name. + +## Adding New Regressions + +To add a new regression file, add the file to git, for example: + +``` +git add regress/regress0/testMyFunctionality.cvc +``` + +Also add it to [Makefile.tests](Makefile.tests) in this directory. + +A number of regressions exist under test/regress that are not listed in +[Makefile.tests](Makefile.tests). These are regressions that may someday be +included in the standard suite of tests, but are not yet included (perhaps they +test functionality not yet supported). + +The following types of regression files are supported: + +- `*.smt`: An [SMT1.x](http://smtlib.cs.uiowa.edu/papers/format-v1.2-r06.08.30.pdf) benchmark +- `*.smt2`: An [SMT 2.x](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf) benchmark +- `*.cvc`: A benchmark that uses [CVC4's native input language](https://github.com/CVC4/CVC4/wiki/CVC4-Native-Input-Language) +- `*.sy`: A [SyGuS](http://sygus.seas.upenn.edu/files/SyGuS-IF.pdf) benchmark +- `*.p`: A [TPTP](http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html) benchmark + +## Expected Output, Error, and Exit Codes + +In the regression file, you can specify expected stdout, stderr, and exit codes +with the following directives: + +``` +% EXPECT: stdout +% EXPECT-ERROR: stderr +% EXIT: 0 +``` + +This example 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 +``` + +Note that the directives are in comments, so if the benchmark file is an smt2 +file for example, the first character would be `;` instead of `%`. + +Benchmark files can also specify the command line options to be used when +executing CVC4, for example: + +``` +% COMMAND-LINE: --incremental +``` + +Sometimes, the expected output or error output may need some processing. This +is done with the `SCRUBBER` and `ERROR-SCRUBBER` directives. The command +specified by the `SCRUBBER`/`ERROR-SCRUBBER` directive is applied to the output +before the the output is matched against the `EXPECT`/`EXPECT-ERROR` directives +respectively. For example: + +``` +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. +; EXPECT: The fact in question: TERM +; EXPECT: ") +``` + +The `SCRUBBER` directive in this example replaces the actual term by a fixed +string `TERM` to make the regression test robust to the actual term printed +(e.g. there could be multiple non-linear facts and it is ok if any of them is +printed). + +Sometimes it is useful to keep the directives separate. You can separate the +benchmark from the output expectations by putting the benchmark in `.smt` and the directives in `.smt.expect`, which is looked +for by the regression script. Note that `*.expect` files should be added to the +`EXTRA_DIST` variable in [Makefile.am](Makefile.am).