summaryrefslogtreecommitdiff
path: root/src/proof/lemma_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/lemma_proof.cpp')
-rw-r--r--src/proof/lemma_proof.cpp13
1 files changed, 13 insertions, 0 deletions
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp
index a12a516cf..3a962f987 100644
--- a/src/proof/lemma_proof.cpp
+++ b/src/proof/lemma_proof.cpp
@@ -65,6 +65,10 @@ void LemmaProofRecipe::dump(const char *tag) const {
Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl;
}
+ if (d_originalLemma != Node()) {
+ Debug(tag) << std::endl << "Original lemma: " << d_originalLemma << std::endl << std::endl;
+ }
+
unsigned count = 1;
Debug(tag) << "Base assertions:" << std::endl;
for (std::set<Node>::iterator baseIt = d_baseAssertions.begin();
@@ -190,4 +194,13 @@ unsigned LemmaProofRecipe::getNumSteps() const {
return d_proofSteps.size();
}
+void LemmaProofRecipe::setOriginalLemma(Node lemma) {
+ d_originalLemma = lemma;
+}
+
+Node LemmaProofRecipe::getOriginalLemma() const {
+ return d_originalLemma;
+}
+
+
} /* namespace CVC4 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback