From 8a937aee4b238eb23c5358b3534f3e3a770ed057 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 6 Jan 2022 20:13:56 -0800 Subject: [PATCH] [Regressions] Add directive for disabling testers (#7892) This commit adds a directive for regressions (`DISABLE-TESTER`) that allows disabling a given tester for a regression. Currently, we disable testers based on properties such as command line arguments, which can be error prone. --- test/regress/README.md | 11 ++++++++++- test/regress/run_regression.py | 8 ++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/test/regress/README.md b/test/regress/README.md index 6997afbd3..34330fa15 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -51,7 +51,7 @@ The following types of regression files are supported: - `*.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 +## Directives In the regression file, you can specify expected stdout, stderr, and exit codes with the following directives: @@ -122,3 +122,12 @@ This benchmark is only run when CryptoMiniSat has been configured. Multiple as a requirement, refer to cvc5's `--show-config` output. Features can also be excluded by adding the `no-` prefix, e.g. `no-cryptominisat` means that the test is not valid for builds that include CryptoMiniSat support. + +To disable a specific type of test, the `DISABLE-TESTER` directive can be used. +The following example disables the proof tester for a regression: + +``` +; DISABLE-TESTER: proof +``` + +Multiple testers can be disabled using multiple `DISABLE-TESTER` directives. diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 4a5825a50..519b81a40 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -339,6 +339,7 @@ EXPECT_ERROR = "EXPECT-ERROR:" EXIT = "EXIT:" COMMAND_LINE = "COMMAND-LINE:" REQUIRES = "REQUIRES:" +DISABLE_TESTER = "DISABLE-TESTER:" EXIT_OK = 0 EXIT_FAILURE = 1 @@ -545,6 +546,13 @@ def run_regression( command_lines.append(line[len(COMMAND_LINE) :].strip()) elif line.startswith(REQUIRES): requires.append(line[len(REQUIRES) :].strip()) + elif line.startswith(DISABLE_TESTER): + disable_tester = line[len(DISABLE_TESTER) :].strip() + if disable_tester not in g_testers: + print("Unknown tester: {}".format(disable_tester)) + return EXIT_FAILURE + testers.remove(disable_tester) + expected_output = expected_output.strip() expected_error = expected_error.strip() -- 2.30.2