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, 2 insertions, 0 deletions

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 14793f380..954b65bbc 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -246,6 +246,8 @@ public:
   assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
   size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
 
+  void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas);
+
   int nextId() { return d_nextId++; }
 
   void setLogic(const LogicInfo& logic);