From: Guy <katz911@gmail.com>
Date: Wed, 20 Jul 2016 02:13:01 +0000 (-0700)
Subject: Allow a caller to query whether an unsat core is available or not
X-Git-Tag: cvc5-1.0.0~6040^2~42
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3e3563a1f312b024653503837a56aef10a41eb9f;p=cvc5.git

Allow a caller to query whether an unsat core is available or not
---

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 9b3d9a289..09fc5dc8b 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -292,8 +292,13 @@ void ProofManager::traceUnsatCore() {
   }
 }
 
+bool ProofManager::unsatCoreAvailable() const {
+  return d_satProof->derivedEmptyClause();
+}
+
 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();
 
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 954b65bbc..b1cfc54b5 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -246,6 +246,7 @@ public:
   assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
   size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
 
+  bool unsatCoreAvailable() const;
   void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas);
 
   int nextId() { return d_nextId++; }
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index bda8094be..c571a7b06 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -199,6 +199,7 @@ class TSatProof {
   void constructProof(ClauseId id);
   void constructProof() { constructProof(d_emptyClauseId); }
   void collectClauses(ClauseId id);
+  bool derivedEmptyClause() const;
   prop::SatClause* buildClause(ClauseId id);
 
   virtual void printResolution(ClauseId id, std::ostream& out,
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 1e01e4dce..cd2473937 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -997,6 +997,11 @@ prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) {
   return clause;
 }
 
+template <class Solver>
+bool TSatProof<Solver>::derivedEmptyClause() const {
+  return hasResolutionChain(d_emptyClauseId);
+}
+
 template <class Solver>
 void TSatProof<Solver>::collectClauses(ClauseId id) {
   if (d_seenInputs.find(id) != d_seenInputs.end() ||