diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-11 03:21:06 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-11 09:21:06 +0000 |
| commit | 71e843a8e9e88fc739aaa5a4a5d608004648fafa (patch) | |
| tree | 6f18912dfcb230139bbb6bdb68b38400d23d7eff /src/theory/theory_preprocessor.cpp | |
| parent | 223155cfb300458f534f4be6b88e5fdc17b0ff14 (diff) | |
(proof-new) Clean up uses of witness with skolem lemmas (#6109)
This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.
It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.
Diffstat (limited to 'src/theory/theory_preprocessor.cpp')
| -rw-r--r-- | src/theory/theory_preprocessor.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index ea4b0f82f..a9e16f48f 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -204,13 +204,14 @@ TrustNode TheoryPreprocessor::preprocessLemmaInternal( { Assert(d_lp != nullptr); // add the original proof to the lazy proof - d_lp->addLazyStep(node.getProven(), node.getGenerator()); + d_lp->addLazyStep( + node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA); // only need to do anything if lemmap changed in a non-trivial way if (!CDProof::isSame(lemmap, lemma)) { d_lp->addLazyStep(tplemma.getProven(), tplemma.getGenerator(), - PfRule::PREPROCESS_LEMMA, + PfRule::THEORY_PREPROCESS, true, "TheoryEngine::lemma_pp"); // ---------- from node -------------- from theory preprocess |