diff options
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 7 |
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)) { |