Replace the old dump infrastructure (#7572)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 4 Nov 2021 19:55:13 +0000 (14:55 -0500)
committerGitHub <noreply@github.com>
Thu, 4 Nov 2021 19:55:13 +0000 (19:55 +0000)
commite680a299ac1da58b8fee27e3733d5e5eea255d94
treef04aa45a3dd49064010bf0c883f1b9a508cda996
parent67559f3b3e42dc1937f809e56ee57daa4bd8bd89
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.
41 files changed:
src/CMakeLists.txt
src/expr/node_manager.cpp
src/expr/node_manager.h
src/options/options_handler.cpp
src/options/options_handler.h
src/options/smt_options.toml
src/preprocessing/passes/sort_infer.cpp
src/preprocessing/preprocessing_pass.cpp
src/preprocessing/preprocessing_pass.h
src/printer/ast/ast_printer.cpp
src/printer/printer.cpp
src/printer/smt2/smt2_printer.cpp
src/printer/tptp/tptp_printer.cpp
src/prop/cnf_stream.cpp
src/smt/check_models.cpp
src/smt/command.cpp
src/smt/dump.cpp [deleted file]
src/smt/dump.h [deleted file]
src/smt/dump_manager.cpp [deleted file]
src/smt/dump_manager.h [deleted file]
src/smt/env.cpp
src/smt/env.h
src/smt/listeners.cpp
src/smt/listeners.h
src/smt/node_command.cpp [deleted file]
src/smt/node_command.h [deleted file]
src/smt/output_manager.cpp [deleted file]
src/smt/output_manager.h [deleted file]
src/smt/preprocessor.cpp
src/smt/preprocessor.h
src/smt/print_benchmark.cpp
src/smt/process_assertions.cpp
src/smt/process_assertions.h
src/smt/solver_engine.cpp
src/smt/solver_engine.h
src/theory/bv/theory_bv_rewrite_rules.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
test/regress/CMakeLists.txt
test/regress/regress0/options/invalid_dump.smt2 [deleted file]
test/regress/regress0/print_define_fun_internal.smt2