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

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d155630e5..43328e1de 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -69,6 +69,7 @@ ProofManager::~ProofManager() {
 }
 
 ProofManager* ProofManager::currentPM() {
+  Assert(PROOF_ON(), "Cannot call ProofManager when proofs are off");
   return smt::currentProofManager();
 }
 
@@ -292,6 +293,36 @@ void ProofManager::traceUnsatCore() {
   }
 }
 
+void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) {
+  d_satProof->constructProof();
+
+  IdToSatClause used_lemmas;
+  IdToSatClause used_inputs;
+  d_satProof->collectClausesUsed(used_inputs, used_lemmas);
+
+  IdToSatClause::const_iterator it;
+
+  for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
+    std::set<Node> lemma;
+    for(unsigned i = 0; i < it->second->size(); ++i) {
+      prop::SatLiteral lit = (*(it->second))[i];
+      Node node = getCnfProof()->getAtom(lit.getSatVariable());
+      Expr atom = node.toExpr();
+      if (atom.isConst()) {
+        Assert (atom == utils::mkTrue());
+        continue;
+      }
+      lemma.insert(lit.isNegated() ? node.notNode() : node);
+    }
+
+    LemmaProofRecipe recipe = getCnfProof()->getProofRecipe(lemma);
+
+    if (recipe.simpleLemma() && recipe.getTheory() == theory) {
+      lemmas.push_back(recipe.getOriginalLemma());
+    }
+  }
+}
+
 void ProofManager::addAssertion(Expr formula) {
   Debug("proof:pm") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);