From 8b7a4af93226b2ecb82814a7609855deea0230cd Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 4 Jun 2018 10:56:19 -0700 Subject: [PATCH] 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. --- test/regress/Makefile.tests | 3 +- test/regress/README.md | 13 +++++++++ test/regress/regress0/fp/simple.smt2 | 6 ++++ test/regress/run_regression.py | 42 ++++++++++++++++++++++++---- 4 files changed, 58 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress0/fp/simple.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 0c5920951..2eaa6fb81 100644 --- 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 f6ff3c68b..d0c9b2b7a 100644 --- 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 `.smt` and the directives in `.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 index 000000000..0b4a11f08 --- /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 7226e7453..9bd3de9f0 100755 --- 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. -- 2.30.2