From 5e2366d542e17ba5064a56f2581ada99c0046ddc Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 10 May 2018 19:34:30 -0700 Subject: [PATCH] Support multiple sets of command line args in regs (#1902) This commit adds support for multiple sets of command line arguments for regressions. Each use of a `COMMAND-LINE` directive is interpreted as a separate set of command line arguments. --- test/regress/README.md | 3 ++ test/regress/run_regression.py | 71 ++++++++++++++++++++-------------- 2 files changed, 44 insertions(+), 30 deletions(-) diff --git a/test/regress/README.md b/test/regress/README.md index 34cf7efde..f6ff3c68b 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -87,6 +87,9 @@ executing CVC4, for example: % COMMAND-LINE: --incremental ``` +If multiple `COMMAND-LINE` directives are used, the regression is run with each +set of options separately. + Sometimes, the expected output or error output may need some processing. This is done with the `SCRUBBER` and `ERROR-SCRUBBER` directives. The command specified by the `SCRUBBER`/`ERROR-SCRUBBER` directive is applied to the output diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index ea744d838..7226e7453 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -166,7 +166,7 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout): expected_output = '' expected_error = '' expected_exit_status = None - command_line = '' + command_lines = [] for line in metadata_lines: # Skip lines that do not start with a comment character. if line[0] != comment_char: @@ -184,7 +184,7 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout): elif line.startswith(EXIT): expected_exit_status = int(line[len(EXIT):]) elif line.startswith(COMMAND_LINE): - command_line += line[len(COMMAND_LINE):] + command_lines.append(line[len(COMMAND_LINE):]) expected_output = expected_output.strip() expected_error = expected_error.strip() @@ -207,41 +207,52 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout): if 'CVC4_REGRESSION_ARGS' in os.environ: basic_command_line_args += shlex.split( os.environ['CVC4_REGRESSION_ARGS']) - basic_command_line_args += shlex.split(command_line) - command_line_args_configs = [basic_command_line_args] + if not proof and ('(get-unsat-core)' in benchmark_content or '(get-unsat-assumptions)' in benchmark_content or '--check-proofs' in basic_command_line_args or '--dump-proofs' in basic_command_line_args): print( - '1..0 # Skipped: unsat cores not supported without proof support') + '1..0 # Skipped regression: unsat cores not supported without proof support' + ) return - extra_command_line_args = [] - if benchmark_ext == '.sy' and \ - '--no-check-synth-sol' not in basic_command_line_args and \ - '--check-synth-sol' not in basic_command_line_args: - extra_command_line_args = ['--check-synth-sol'] - if re.search(r'^(sat|invalid|unknown)$', expected_output) and \ - '--no-check-models' not in basic_command_line_args: - extra_command_line_args = ['--check-models'] - if proof and re.search(r'^(unsat|valid)$', expected_output): - if '--no-check-proofs' not in basic_command_line_args and \ - '--incremental' not in basic_command_line_args and \ - '--unconstrained-simp' not in basic_command_line_args and \ - not cvc4_binary.endswith('pcvc4'): - extra_command_line_args = [ - '--check-proofs', '--no-bv-eq', '--no-bv-ineq', - '--no-bv-algebraic' - ] - if '--no-check-unsat-cores' not in basic_command_line_args and \ - '--incremental' not in basic_command_line_args and \ - '--unconstrained-simp' not in basic_command_line_args and \ - not cvc4_binary.endswith('pcvc4'): - extra_command_line_args += ['--check-unsat-cores'] - if extra_command_line_args: - command_line_args_configs.append( - basic_command_line_args + extra_command_line_args) + if not command_lines: + command_lines.append('') + + command_line_args_configs = [] + for command_line in command_lines: + args = shlex.split(command_line) + if proof or ('--check-proofs' not in args + and '--dump-proofs' not in args): + all_args = basic_command_line_args + args + command_line_args_configs.append(all_args) + + extra_command_line_args = [] + if benchmark_ext == '.sy' and \ + '--no-check-synth-sol' not in all_args and \ + '--check-synth-sol' not in all_args: + extra_command_line_args = ['--check-synth-sol'] + if re.search(r'^(sat|invalid|unknown)$', expected_output) and \ + '--no-check-models' not in all_args: + extra_command_line_args = ['--check-models'] + if proof and re.search(r'^(unsat|valid)$', expected_output): + if '--no-check-proofs' not in all_args and \ + '--incremental' not in all_args and \ + '--unconstrained-simp' not in all_args and \ + not cvc4_binary.endswith('pcvc4'): + extra_command_line_args = [ + '--check-proofs', '--no-bv-eq', '--no-bv-ineq', + '--no-bv-algebraic' + ] + if '--no-check-unsat-cores' not in all_args and \ + '--incremental' not in all_args and \ + '--unconstrained-simp' not in all_args and \ + 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) # 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