diff options
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 5 |
1 files changed, 5 insertions, 0 deletions
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 @@ -998,6 +998,11 @@ prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) { } 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() || d_seenLemmas.find(id) != d_seenLemmas.end() || |