run_regression.py to fail on invalid requirements (#5264)

Currently, the following test is skipped when running ctest:

 ; REQUIRES: symfpuuuu
 ; EXPECT: sat
 (set-logic ALL)
 (assert true)
 (check-sat)
I think it is better for such a test to fail, because otherwise it might never run without anyone noticing (this almost happened to me here: c7e277b).

This PR makes such tests to fail by checking whether the REQUIRES value is valid. No regressions fail as a result.

Co-authored-by: Mathias Preiner mathias.preiner@gmail.com

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 8047a0ca898209b300604e42b3df7cfd83f438f4..17aa9e0c63d5b4b2728b6c466f595a7a169a54b1 100755 (executable)
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -114,14 +114,17 @@ def get_cvc4_features(cvc4_binary):
         output = output.decode()
 
     features = []
+    disabled_features = []
     for line in output.split('\n'):
         tokens = [t.strip() for t in line.split(':')]
         if len(tokens) == 2:
             key, value = tokens
             if value == 'yes':
                 features.append(key)
+            elif value == 'no':
+                disabled_features.append(key)
 
-    return features
+    return features, disabled_features
 
 
 def logic_supported_with_proofs(logic):
@@ -213,7 +216,7 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code,
     if not os.path.isfile(benchmark_path):
         sys.exit('"{}" does not exist or is not a file'.format(benchmark_path))
 
-    cvc4_features = get_cvc4_features(cvc4_binary)
+    cvc4_features, cvc4_disabled_features = get_cvc4_features(cvc4_binary)
 
     basic_command_line_args = []
 
@@ -315,11 +318,20 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code,
         return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
 
     for req_feature in requires:
+        is_negative = False
         if req_feature.startswith("no-"):
-            inv_feature = req_feature[len("no-"):]
-            if inv_feature in cvc4_features:
+            req_feature = req_feature[len("no-"):]
+            is_negative = True
+        if req_feature not in (cvc4_features + cvc4_disabled_features):
+            print(
+                'Illegal requirement in regression: {}\nAllowed requirements: {}'
+                .format(req_feature,
+                        ' '.join(cvc4_features + cvc4_disabled_features)))
+            return EXIT_FAILURE
+        if is_negative:
+            if req_feature in cvc4_features:
                 print('1..0 # Skipped regression: not valid with {}'.format(
-                    inv_feature))
+                    req_feature))
                 return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
         elif req_feature not in cvc4_features:
             print('1..0 # Skipped regression: {} not supported'.format(