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/theory/theory_preprocessor.cpp | |
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/theory/theory_preprocessor.cpp')
-rw-r--r-- | src/theory/theory_preprocessor.cpp | 45 |
1 files changed, 28 insertions, 17 deletions
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index b12916b7d..328c65fcb 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -36,41 +36,52 @@ TheoryPreprocessor::~TheoryPreprocessor() {} void TheoryPreprocessor::clearCache() { d_ppCache.clear(); } -void TheoryPreprocessor::preprocess(TNode node, - preprocessing::AssertionPipeline& lemmas, - bool doTheoryPreprocess) +TrustNode TheoryPreprocessor::preprocess(TNode node, + std::vector<TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess) { // Run theory preprocessing, maybe Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node); // Remove the ITEs Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl; - lemmas.push_back(ppNode); - lemmas.updateRealAssertionsEnd(); - d_tfr.run(lemmas.ref(), lemmas.getIteSkolemMap()); - Trace("te-tform-rm") << "..done " << lemmas[0] << std::endl; + TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false); + Trace("te-tform-rm") << "..done " << ttfr.getNode() << std::endl; + Node retNode = ttfr.getNode(); if (Debug.isOn("lemma-ites")) { - Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; - Debug("lemma-ites") << " + now have the following " << lemmas.size() + Debug("lemma-ites") << "removed ITEs from lemma: " << ttfr.getNode() + << endl; + Debug("lemma-ites") << " + now have the following " << newLemmas.size() << " lemma(s):" << endl; - for (std::vector<Node>::const_iterator i = lemmas.begin(); - i != lemmas.end(); - ++i) + for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i) { - Debug("lemma-ites") << " + " << *i << endl; + Debug("lemma-ites") << " + " << newLemmas[i].getNode() << endl; } Debug("lemma-ites") << endl; } + retNode = Rewriter::rewrite(retNode); + // now, rewrite the lemmas - Node retLemma; - for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i) + for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) { - Node rewritten = Rewriter::rewrite(lemmas[i]); - lemmas.replace(i, rewritten); + // get the trust node to process + TrustNode trn = newLemmas[i]; + Assert(trn.getKind() == TrustNodeKind::LEMMA); + Node assertion = trn.getNode(); + // rewrite, which is independent of d_tpg, since additional lemmas + // are justified separately. + Node rewritten = Rewriter::rewrite(assertion); + if (assertion != rewritten) + { + // not tracking proofs, just make new + newLemmas[i] = TrustNode::mkTrustLemma(rewritten, nullptr); + } } + return TrustNode::mkTrustRewrite(node, retNode, nullptr); } struct preprocess_stack_element |