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.

diff --git a/test/regress/README.md b/test/regress/README.md
index d0c9b2b7a9da91009a24332d40ae0c8782c5b945..772332c3e4286024b79f7dc3ee7896fc39a596a3 100644 (file)
--- 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 1fedd95acbcb542c9544ab90d067e6953333fc21..bc89dd0eb6a92556cd93d62629a7f33c42a21805 100644 (file)
--- 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 23e658e6c78b05cf42c4764547c5314f83bd3916..90c13c615d005c2852e9b322357689f62a3d20a4 100644 (file)
--- 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 6b8a0a8f313365f2fefcc2189ebb6b9c04284395..78df4324e3d55fc1addab54cd472df9ba7a94500 100644 (file)
--- 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 9bd3de9f061fef915f901f5440ccdc27cfefc902..c29a97956cb7283f8e1b5df4641902253da4c5ea 100755 (executable)
--- 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