diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-21 11:48:22 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-21 11:48:22 -0600 |
| commit | ccda071a9605baa42602d580affa296cbc674807 (patch) | |
| tree | b45ff0d8259292895367c7f35754f54f402dd49d /src/smt/process_assertions.cpp | |
| parent | 0c2a43ab616c3670f3077758defcaa1f61cbe291 (diff) | |
Move ownership of theory preprocessor to TheoryProxy (#5690)
With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.
No significant behavior changes in this PR.
The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.
Diffstat (limited to 'src/smt/process_assertions.cpp')
| -rw-r--r-- | src/smt/process_assertions.cpp | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 77c7d450e..8b9b0a53c 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -328,13 +328,8 @@ bool ProcessAssertions::apply(Assertions& as) // ensure rewritten d_passes["rewrite"]->apply(&assertions); - // apply theory preprocess + // apply theory preprocess, which includes ITE removal d_passes["theory-preprocess"]->apply(&assertions); - // Must remove ITEs again since theory preprocessing may introduce them. - // Notice that we alternatively could ensure that the theory-preprocess - // pass above calls TheoryPreprocess::preprocess instead of - // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal. - d_passes["ite-removal"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may // introduce skolems that were solved for earlier and thus appear in the // substitution map. |