diff options
author | Guy <katz911@gmail.com> | 2016-07-15 16:48:25 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-15 16:48:25 -0700 |
commit | 378475e685d514ec47347a9f27a2825391f9b207 (patch) | |
tree | 520757bb2da753201e7e643bc47d1a116edf0ef3 /src/proof/lemma_proof.cpp | |
parent | c0af8cf1c1e3edca35bb7ae4edf1831ebdee0abd (diff) |
The ProofManager now allows theory solvers to get their lemmas that participate in the unsat cores.
Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations
and conflict lemmas.
Diffstat (limited to 'src/proof/lemma_proof.cpp')
-rw-r--r-- | src/proof/lemma_proof.cpp | 13 |
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 */ |