diff options
author | Guy <katz911@gmail.com> | 2016-07-19 19:13:01 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-19 19:13:01 -0700 |
commit | 3e3563a1f312b024653503837a56aef10a41eb9f (patch) | |
tree | a1167a8c8d7b6b1900ea2e9e4e3fba473827b113 /src/proof/sat_proof.h | |
parent | 06d91e9121ecdadfc96d6175792992395833329f (diff) |
Allow a caller to query whether an unsat core is available or not
Diffstat (limited to 'src/proof/sat_proof.h')
-rw-r--r-- | src/proof/sat_proof.h | 1 |
1 files changed, 1 insertions, 0 deletions
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, |