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 9b3d9a289019926a1fb737e5329c7b7f96b702e2..09fc5dc8b61f25d6dc88686b0c89f69292b89861 100644 (file)
--- 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 954b65bbcd26f6d04d7f951e94dffd815707cf66..b1cfc54b5561f4ff759a253b7675938128e325cd 100644 (file)
--- 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 bda8094be8fcf87bede52ced2a76acb7aecc4b3d..c571a7b06e82d0a89016a9b98f1e234142854d34 100644 (file)
--- 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 1e01e4dce8132200e9801e5b008f9e9b9e50ac20..cd24739377aa49fd1ea6a8e7606656c59c9d5ad4 100644 (file)
--- 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() ||