diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-27 15:33:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-27 13:33:12 -0700 |
commit | b90cfb462bde3e75c07bb14e2393ee8e4b4f4d42 (patch) | |
tree | 4e7f89713008787557ae1293c6d0149e185c9b66 /src/preprocessing | |
parent | faa97a6f1ee19760dfb0a79ad18c53afdff6b09a (diff) |
(proof-new) Proof production for term formula removal (#4687)
This adds proof support in the term formula removal pass.
It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index f021fff28..2cc244a34 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -34,9 +34,23 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) { d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + IteSkolemMap& imap = assertions->getIteSkolemMap(); // Remove all of the ITE occurrences and normalize - d_preprocContext->getIteRemover()->run( - assertions->ref(), assertions->getIteSkolemMap(), true); + for (unsigned i = 0, size = assertions->size(); i < size; ++i) + { + std::vector<theory::TrustNode> newAsserts; + std::vector<Node> newSkolems; + TrustNode trn = d_preprocContext->getIteRemover()->run( + (*assertions)[i], newAsserts, newSkolems, true); + // process + assertions->replace(i, trn.getNode()); + Assert(newSkolems.size() == newAsserts.size()); + for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) + { + imap[newSkolems[j]] = assertions->size(); + assertions->ref().push_back(newAsserts[j].getNode()); + } + } for (unsigned i = 0, size = assertions->size(); i < size; ++i) { assertions->replace(i, Rewriter::rewrite((*assertions)[i])); |