summaryrefslogtreecommitdiff
path: root/src/expr/buffered_proof_generator.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/buffered_proof_generator.h')
-rw-r--r--src/expr/buffered_proof_generator.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index 81e2667bf..89e8b196d 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -48,6 +48,8 @@ class BufferedProofGenerator : public ProofGenerator
CDPOverwrite opolicy = CDPOverwrite::NEVER);
/** Get proof for. It is robust to (dis)equality symmetry. */
std::shared_ptr<ProofNode> getProofFor(Node f) override;
+ /** Whether a step has been registered for f. */
+ bool hasProofFor(Node f) override;
/** identify */
std::string identify() const override { return "BufferedProofGenerator"; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback