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.

1 files changed, 5 insertions, 0 deletions

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 {