Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.

4 files changed, 94 insertions, 16 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 835990613..1b4fbcc47 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -271,7 +271,7 @@ void ProofManager::traceDeps(TNode n) {
 
 void ProofManager::traceUnsatCore() {
   Assert (options::unsatCores());
-  d_satProof->constructProof();
+  constructSatProof();
   IdToSatClause used_lemmas;
   IdToSatClause used_inputs;
   d_satProof->collectClausesUsed(used_inputs,
@@ -296,11 +296,17 @@ bool ProofManager::unsatCoreAvailable() const {
   return d_satProof->derivedEmptyClause();
 }
 
+void ProofManager::constructSatProof() {
+  if (!d_satProof->proofConstructed()) {
+    d_satProof->constructProof();
+  }
+}
+
 void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) {
   Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
   Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
 
-  d_satProof->constructProof();
+  constructSatProof();
 
   IdToSatClause used_lemmas;
   IdToSatClause used_inputs;
@@ -309,24 +315,14 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod
   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);
-    }
+    std::set<Node> lemma = satClauseToNodeSet(it->second);
 
     // TODO: we should be able to drop the "haveProofRecipe" check.
     // however, there are some rewrite issues with the arith solver, resulting
     // in non-registered recipes. For now we assume no one is requesting arith lemmas.
     LemmaProofRecipe recipe;
-    if ( getCnfProof()->haveProofRecipe(lemma) )
-         recipe = getCnfProof()->getProofRecipe(lemma);
+    if (getCnfProof()->haveProofRecipe(lemma))
+      recipe = getCnfProof()->getProofRecipe(lemma);
 
     if (recipe.simpleLemma() && recipe.getTheory() == theory) {
       lemmas.push_back(recipe.getOriginalLemma());
@@ -334,6 +330,73 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod
   }
 }
 
+std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) {
+  std::set<Node> result;
+  for (unsigned i = 0; i < clause->size(); ++i) {
+    prop::SatLiteral lit = (*clause)[i];
+    Node node = getCnfProof()->getAtom(lit.getSatVariable());
+    Expr atom = node.toExpr();
+    if (atom.isConst()) {
+      Assert (atom == utils::mkTrue());
+      continue;
+    }
+    result.insert(lit.isNegated() ? node.notNode() : node);
+  }
+
+  return result;
+}
+
+Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
+  Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
+  Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
+
+  if (lemma.getKind() != kind::AND)
+    return lemma;
+
+  constructSatProof();
+
+  NodeBuilder<> builder(kind::AND);
+
+  IdToSatClause used_lemmas;
+  IdToSatClause used_inputs;
+  d_satProof->collectClausesUsed(used_inputs, used_lemmas);
+
+  IdToSatClause::const_iterator it;
+  std::set<Node>::iterator lemmaIt;
+
+  for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
+    std::set<Node> currentLemma = satClauseToNodeSet(it->second);
+
+    // TODO: we should be able to drop the "haveProofRecipe" check.
+    // however, there are some rewrite issues with the arith solver, resulting
+    // in non-registered recipes. For now we assume no one is requesting arith lemmas.
+    LemmaProofRecipe recipe;
+    if (getCnfProof()->haveProofRecipe(currentLemma))
+      recipe = getCnfProof()->getProofRecipe(currentLemma);
+
+    if (recipe.getOriginalLemma() == lemma) {
+      for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
+        builder << *lemmaIt;
+
+        // Sanity check: make sure that each conjunct really appears in the original lemma
+        bool found = false;
+        for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
+          if (lemma[i] == *lemmaIt)
+            found = true;
+        }
+        Assert(found);
+      }
+    }
+  }
+
+  Assert(builder.getNumChildren() != 0);
+
+  if (builder.getNumChildren() == 1)
+    return builder[0];
+
+  return builder;
+}
+
 void ProofManager::addAssertion(Expr formula) {
   Debug("proof:pm") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
@@ -385,6 +448,7 @@ void LFSCProof::toStream(std::ostream& out) {
 
   Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
 
+  Assert(!d_satProof->proofConstructed());
   d_satProof->constructProof();
 
   // collecting leaf clauses in resolution proof
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index b1cfc54b5..23d7d1972 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -248,6 +248,7 @@ public:
 
   bool unsatCoreAvailable() const;
   void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas);
+  Node getWeakestImplicantInUnsatCore(Node lemma);
 
   int nextId() { return d_nextId++; }
 
@@ -271,6 +272,10 @@ public:
                          ProofLetMap& letMap,
                          std::ostream& out,
                          std::ostringstream& paren);
+
+private:
+  void constructSatProof();
+  std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index c571a7b06..52e059e95 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -198,6 +198,7 @@ class TSatProof {
    */
   void constructProof(ClauseId id);
   void constructProof() { constructProof(d_emptyClauseId); }
+  bool proofConstructed() const;
   void collectClauses(ClauseId id);
   bool derivedEmptyClause() const;
   prop::SatClause* buildClause(ClauseId id);
@@ -355,7 +356,7 @@ class TSatProof {
   IdToSatClause d_seenInputs;
   IdToSatClause d_seenLemmas;
 
- private:
+   private:
   __gnu_cxx::hash_map<ClauseId, int> d_glueMap;
   struct Statistics {
     IntStat d_numLearnedClauses;
@@ -370,6 +371,7 @@ class TSatProof {
     ~Statistics();
   };
 
+  bool d_satProofConstructed;
   Statistics d_statistics;
 }; /* class TSatProof */
 
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index cd2473937..fc2bae19b 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -224,6 +224,7 @@ TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name,
       d_seenLearnt(),
       d_seenInputs(),
       d_seenLemmas(),
+      d_satProofConstructed(false),
       d_statistics(name) {
   d_proxy = new ProofProxy<Solver>(this);
 }
@@ -957,10 +958,16 @@ void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) {
 
 template <class Solver>
 void TSatProof<Solver>::constructProof(ClauseId conflict) {
+  d_satProofConstructed = true;
   collectClauses(conflict);
 }
 
 template <class Solver>
+bool TSatProof<Solver>::proofConstructed() const {
+  return d_satProofConstructed;
+}
+
+template <class Solver>
 std::string TSatProof<Solver>::clauseName(ClauseId id) {
   std::ostringstream os;
   if (isInputClause(id)) {