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 /src/smt/preprocessor.h | |
| 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 'src/smt/preprocessor.h')
| -rw-r--r-- | src/smt/preprocessor.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 40a84981a..957b5e36e 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -62,6 +62,8 @@ class Preprocessor : protected EnvObj /** * Process the assertions that have been asserted in argument as. Returns * true if no conflict was discovered while preprocessing them. + * + * @param as The assertions. */ bool process(Assertions& as); /** |