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 | |
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')
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/passes/theory_preprocess.cpp | 43 |
2 files changed, 37 insertions, 12 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 diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index e888e7a2b..6c751f864 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -29,17 +29,44 @@ TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "theory-preprocess"){}; PreprocessingPassResult TheoryPreprocess::applyInternal( - AssertionPipeline* assertionsToPreprocess) + AssertionPipeline* assertions) { - TheoryEngine* te = d_preprocContext->getTheoryEngine(); - for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + + IteSkolemMap& imap = assertions->getIteSkolemMap(); + PropEngine* propEngine = d_preprocContext->getPropEngine(); + // Remove all of the ITE occurrences and normalize + for (unsigned i = 0, size = assertions->size(); i < size; ++i) { - TNode a = (*assertionsToPreprocess)[i]; - Assert(Rewriter::rewrite(a) == a); - assertionsToPreprocess->replaceTrusted(i, te->preprocess(a)); - a = (*assertionsToPreprocess)[i]; - Assert(Rewriter::rewrite(a) == a); + Node assertion = (*assertions)[i]; + std::vector<theory::TrustNode> newAsserts; + std::vector<Node> newSkolems; + TrustNode trn = + propEngine->preprocess(assertion, newAsserts, newSkolems, true); + if (!trn.isNull()) + { + // process + assertions->replaceTrusted(i, trn); + // rewritten assertion has a dependence on the node (old pf architecture) + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(trn.getNode(), assertion); + } + } + Assert(newSkolems.size() == newAsserts.size()); + for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) + { + imap[newSkolems[j]] = assertions->size(); + assertions->pushBackTrusted(newAsserts[j]); + // new assertions have a dependence on the node (old pf architecture) + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), + assertion); + } + } } + return PreprocessingPassResult::NO_CONFLICT; } |