[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.

diff --git a/test/regress/README.md b/test/regress/README.md
index 6997afbd340da4a7465c8db9c20a27a0b5a03df3..34330fa151c6286f7f32d0ff5cc393902f047e1d 100644 (file)
--- 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 4a5825a500e97bf063e524e69ff24d9f4cd264c6..519b81a4022bd5effb7d664cf68a587262898c17 100755 (executable)
--- 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()