+++ /dev/null
-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 <mdeters@cs.nyu.edu> 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]
--- /dev/null
+# 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 `<benchmark
+file>.smt` and the directives in `<benchmark file>.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).
projects / cvc5.git / commitdiff