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

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)) {