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/preprocessing/passes/ite_removal.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/preprocessing/passes/ite_removal.cpp')
| -rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 3531497e8..d2f053379 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -38,15 +38,13 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) IteSkolemMap& imap = assertions->getIteSkolemMap(); // Remove all of the ITE occurrences and normalize - theory::TheoryPreprocessor* tpp = - d_preprocContext->getTheoryEngine()->getTheoryPreprocess(); + prop::PropEngine* pe = d_preprocContext->getPropEngine(); for (unsigned i = 0, size = assertions->size(); i < size; ++i) { Node assertion = (*assertions)[i]; std::vector<theory::TrustNode> newAsserts; std::vector<Node> newSkolems; - // TODO (project #42): this will call the prop engine - TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false); + TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false); if (!trn.isNull()) { // process |