Regressions: Support for requiring CVC4 features (#2044)

This commit adds supprt for the `REQUIRES` directive in our regression
benchmarks. This directive can be used to enable certain benchmarks only
if CVC4 has been configured with certain features enabled.

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 0c5920951a7fc876dee67811dd09faf612b665e9..2eaa6fb813a98d308459130cf7518d2b075abc58 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -434,6 +434,7 @@ REG0_TESTS = \
        regress0/fmf/sc_bad_model_1221.smt2 \
        regress0/fmf/syn002-si-real-int.smt2 \
        regress0/fmf/tail_rec.smt2 \
+       regress0/fp/simple.smt2 \
        regress0/fuzz_1.smt \
        regress0/fuzz_3.smt \
        regress0/get-value-incremental.smt2 \
@@ -603,10 +604,10 @@ REG0_TESTS = \
        regress0/quantifiers/is-int.smt2 \
        regress0/quantifiers/issue2031-bv-var-elim.smt2 \
        regress0/quantifiers/issue1805.smt2 \
+       regress0/quantifiers/issue2033-macro-arith.smt2 \
        regress0/quantifiers/lra-triv-gn.smt2 \
        regress0/quantifiers/macros-int-real.smt2 \
        regress0/quantifiers/macros-real-arg.smt2 \
-       regress0/quantifiers/issue2033-macro-arith.smt2 \
        regress0/quantifiers/matching-lia-1arg.smt2 \
        regress0/quantifiers/mix-complete-strat.smt2 \
        regress0/quantifiers/mix-match.smt2 \

diff --git a/test/regress/README.md b/test/regress/README.md
index f6ff3c68bb01ee1ca3b960bb4e4a15ff67e1cd9a..d0c9b2b7a9da91009a24332d40ae0c8782c5b945 100644 (file)
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -108,6 +108,19 @@ string `TERM` to make the regression test robust to the actual term printed
 (e.g. there could be multiple non-linear facts and it is ok if any of them is
 printed).
 
+Sometimes, certain benchmarks only apply to certain CVC4
+configurations. The `REQUIRES` directive can be used to only run
+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.
+
 Sometimes it is useful to keep the directives separate. You can separate the
 benchmark from the output expectations by putting the benchmark in `<benchmark
 file>.smt` and the directives in `<benchmark file>.smt.expect`, which is looked

diff --git a/test/regress/regress0/fp/simple.smt2 b/test/regress/regress0/fp/simple.smt2
new file mode 100644 (file)
index 0000000..0b4a11f
--- /dev/null
+++ b/test/regress/regress0/fp/simple.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+(set-logic QF_FP)    
+(declare-const x Float32)
+(assert (not (= x (fp.neg (fp.neg x)))))
+(check-sat)

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 7226e7453064b09f1fbbeaa9c296b18881d507e3..9bd3de9f061fef915f901f5440ccdc27cfefc902 100755 (executable)
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -23,6 +23,7 @@ EXPECT = 'EXPECT: '
 EXPECT_ERROR = 'EXPECT-ERROR: '
 EXIT = 'EXIT: '
 COMMAND_LINE = 'COMMAND-LINE: '
+REQUIRES = 'REQUIRES: '
 
 
 def run_process(args, cwd, timeout, s_input=None):
@@ -42,17 +43,37 @@ def run_process(args, cwd, timeout, s_input=None):
     out = ''
     err = ''
     exit_status = 124
-    timer = threading.Timer(timeout, lambda p: p.kill(), [proc])
     try:
-        timer.start()
+        if timeout:
+            timer = threading.Timer(timeout, lambda p: p.kill(), [proc])
+            timer.start()
         out, err = proc.communicate(input=s_input)
         exit_status = proc.returncode
     finally:
-        timer.cancel()
+        if timeout:
+            timer.cancel()
 
     return out, err, exit_status
 
 
+def get_cvc4_features(cvc4_binary):
+    """Returns a list of features supported by the CVC4 binary `cvc4_binary`."""
+
+    output, _, _ = run_process([cvc4_binary, '--show-config'], None, None)
+    if isinstance(output, bytes):
+        output = output.decode()
+
+    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)
+
+    return features
+
+
 def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary,
                   command_line, benchmark_dir, benchmark_filename, timeout):
     """Runs CVC4 on the file `benchmark_filename` in the directory
@@ -113,6 +134,8 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
     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)
+
     basic_command_line_args = []
 
     benchmark_basename = os.path.basename(benchmark_path)
@@ -167,6 +190,7 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
     expected_error = ''
     expected_exit_status = None
     command_lines = []
+    requires = []
     for line in metadata_lines:
         # Skip lines that do not start with a comment character.
         if line[0] != comment_char:
@@ -185,6 +209,8 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
             expected_exit_status = int(line[len(EXIT):])
         elif line.startswith(COMMAND_LINE):
             command_lines.append(line[len(COMMAND_LINE):])
+        elif line.startswith(REQUIRES):
+            requires.append(line[len(REQUIRES):].strip())
     expected_output = expected_output.strip()
     expected_error = expected_error.strip()
 
@@ -217,6 +243,12 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
         )
         return
 
+    for req_feature in requires:
+        if req_feature not in cvc4_features:
+            print('1..0 # Skipped regression: {} not supported'.format(
+                req_feature))
+            return
+
     if not command_lines:
         command_lines.append('')
 
@@ -251,8 +283,8 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
                    not cvc4_binary.endswith('pcvc4'):
                     extra_command_line_args += ['--check-unsat-cores']
             if extra_command_line_args:
-                command_line_args_configs.append(
-                    all_args + extra_command_line_args)
+                command_line_args_configs.append(all_args +
+                                                 extra_command_line_args)
 
     # Run CVC4 on the benchmark with the different option sets and check
     # whether the exit status, stdout output, stderr output are as expected.