Add flag to skip regression if feature enabled (#2062)

This commit adds the option of skipping regressions when a specified
feature is enabled. It also changes some of the regression tests to be
skipped when it is a competition build because regressions fail
otherwise. In the tests changed in this commit, we do not care about
reproducing error messages in a competition build, so we can skip them.

5 files changed, 17 insertions, 8 deletions

diff --git a/test/regress/README.md b/test/regress/README.md
index d0c9b2b7a..772332c3e 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -116,10 +116,11 @@ a given benchmark when a feature is supported. For example:
 ; REQUIRES: symfpu
 ```
 
-This benchmark is only run when symfpu has been configured.
-Multiple `REQUIRES` directives are supported. For a list of
-features that can be listed as a requirement, refer to CVC4's
-`--show-config` output.
+This benchmark is only run when symfpu has been configured.  Multiple
+`REQUIRES` directives are supported. For a list of features that can be listed
+as a requirement, refer to CVC4's `--show-config` output. Features can also be
+excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is
+not valid for builds that include symfpu support.
 
 Sometimes it is useful to keep the directives separate. You can separate the
 benchmark from the output expectations by putting the benchmark in `<benchmark
diff --git a/test/regress/regress1/arrayinuf_error.smt2 b/test/regress/regress1/arrayinuf_error.smt2
index 1fedd95ac..bc89dd0eb 100644
--- a/test/regress/regress1/arrayinuf_error.smt2
+++ b/test/regress/regress1/arrayinuf_error.smt2
@@ -1,4 +1,5 @@
-; EXPECT: (error "Parse Error: arrayinuf_error.smt2:7.21: Symbol 'Array' not declared as a type
+; REQUIRES: no-competition
+; EXPECT: (error "Parse Error: arrayinuf_error.smt2:8.21: Symbol 'Array' not declared as a type
 ; EXPECT: 
 ; EXPECT:   (declare-fun a (Array Bool Bool))
 ; EXPECT:                   ^
diff --git a/test/regress/regress1/datatypes/error.cvc b/test/regress/regress1/datatypes/error.cvc
index 23e658e6c..90c13c615 100644
--- a/test/regress/regress1/datatypes/error.cvc
+++ b/test/regress/regress1/datatypes/error.cvc
@@ -1,7 +1,7 @@
+% REQUIRES: no-competition
 % EXPECT-ERROR: CVC4 Error:
 % EXPECT-ERROR: Parse Error: foo already declared in this datatype
 % EXIT: 1
 
 DATATYPE single_ctor = foo(bar:REAL) | foo(bar2:REAL) END;
 DATATYPE double_ctor = foo(bar:REAL) END;
-
diff --git a/test/regress/regress1/errorcrash.smt2 b/test/regress/regress1/errorcrash.smt2
index 6b8a0a8f3..78df4324e 100644
--- a/test/regress/regress1/errorcrash.smt2
+++ b/test/regress/regress1/errorcrash.smt2
@@ -1,5 +1,6 @@
+; REQUIRES: no-competition
 ; EXIT: 1
-; EXPECT: (error "Parse Error: errorcrash.smt2:5.29: Symbol 'Array' not declared as a type")
+; EXPECT: (error "Parse Error: errorcrash.smt2:6.29: Symbol 'Array' not declared as a type")
 (set-logic QF_UF)
 (declare-sort U 0)
 (declare-fun x () (Array U U))
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 9bd3de9f0..c29a97956 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -244,7 +244,13 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
         return
 
     for req_feature in requires:
-        if req_feature not in cvc4_features:
+        if req_feature.startswith("no-"):
+            inv_feature = req_feature[len("no-"):]
+            if inv_feature in cvc4_features:
+                print('1..0 # Skipped regression: not valid with {}'.format(
+                    inv_feature))
+                return
+        elif req_feature not in cvc4_features:
             print('1..0 # Skipped regression: {} not supported'.format(
                 req_feature))
             return