From: Guy <katz911@gmail.com>
Date: Fri, 15 Jul 2016 23:48:25 +0000 (-0700)
Subject: The ProofManager now allows theory solvers to get their lemmas that participate in... 
X-Git-Tag: cvc5-1.0.0~6040^2~46
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=378475e685d514ec47347a9f27a2825391f9b207;p=cvc5.git

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.
---

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 */
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 */
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);
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);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 913a6800b..b4c6c97cd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -91,6 +91,8 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
       Node emptyNode;
       LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode);
 
+      proofRecipe->setOriginalLemma(lemma);
+
       Node rewritten;
       if (lemma.getKind() == kind::OR) {
         for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
@@ -156,7 +158,7 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
 void TheoryEngine::finishInit() {
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
-  
+
   //initialize the model
   if( d_logicInfo.isQuantified() ) {
     d_curr_model = d_quantEngine->getModel();