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.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h
index e96ff5337..9c838cee7 100644
--- a/src/proof/lemma_proof.h
+++ b/src/proof/lemma_proof.h
@@ -51,6 +51,10 @@ public:
   bool wasRewritten(Node assertion) const;
   Node getExplanation(Node assertion) const;
 
+  //* Original lemma */
+  void setOriginalLemma(Node lemma);
+  Node getOriginalLemma() const;
+
   //* Proof Steps */
   void addStep(ProofStep& proofStep);
   const ProofStep* getStep(unsigned index) const;
@@ -72,6 +76,9 @@ private:
 
   //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */
   std::map<Node, Node> d_assertionToExplanation;
+
+  //* The original lemma, as asserted by the owner theory solver */
+  Node d_originalLemma;
 };
 
 } /* CVC4 namespace */