diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-04 14:55:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-04 19:55:13 +0000 |
| commit | e680a299ac1da58b8fee27e3733d5e5eea255d94 (patch) | |
| tree | f04aa45a3dd49064010bf0c883f1b9a508cda996 /test | |
| parent | 67559f3b3e42dc1937f809e56ee57daa4bd8bd89 (diff) | |
Replace the old dump infrastructure (#7572)
This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks.
This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain.
This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync.
The other dumping tags are deleted for now, and will be reimplemented as needed.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/options/invalid_dump.smt2 | 5 | ||||
| -rw-r--r-- | test/regress/regress0/print_define_fun_internal.smt2 | 4 |
3 files changed, 2 insertions, 8 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f97575808..99c65e973 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -775,7 +775,6 @@ set(regress_0_tests regress0/opt-abd-no-use.smt2 regress0/options/ast-and-sexpr.smt2 regress0/options/interactive-mode.smt2 - regress0/options/invalid_dump.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 diff --git a/test/regress/regress0/options/invalid_dump.smt2 b/test/regress/regress0/options/invalid_dump.smt2 deleted file mode 100644 index ab6f6db31..000000000 --- a/test/regress/regress0/options/invalid_dump.smt2 +++ /dev/null @@ -1,5 +0,0 @@ -; REQUIRES: dumping -; COMMAND-LINE: --dump invalidDumpTag -; ERROR-SCRUBBER: grep -o "unknown option for --dump" -; EXPECT-ERROR: unknown option for --dump -; EXIT: 1 diff --git a/test/regress/regress0/print_define_fun_internal.smt2 b/test/regress/regress0/print_define_fun_internal.smt2 index 47b08da23..997096561 100644 --- a/test/regress/regress0/print_define_fun_internal.smt2 +++ b/test/regress/regress0/print_define_fun_internal.smt2 @@ -1,5 +1,5 @@ -; REQUIRES: dumping -; COMMAND-LINE: --solve-real-as-int --dump=assertions:post-real-to-int +; REQUIRES: tracing +; COMMAND-LINE: --solve-real-as-int -t assertions::post-real-to-int --produce-assertions ; EXIT: 0 ; SCRUBBER: grep -v -E '.*' (set-logic QF_NRA) |