diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 14:48:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-12 14:48:31 -0500 |
| commit | 2174ab36023326cd998565bbf35d31c38bc10594 (patch) | |
| tree | a61a1cb1cc00faa1339adf315fd4037b0ca08b1a /src/expr/lazy_proof.h | |
| parent | 27413a45e28001f6155d529a59d679556cdc011e (diff) | |
(proof-new) Improve interfaces to proof generators (#4803)
This includes configurable naming and a caching policy for term conversion proof generator.
Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.
Diffstat (limited to 'src/expr/lazy_proof.h')
| -rw-r--r-- | src/expr/lazy_proof.h | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 1f68a3ccb..4368cbb85 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -45,7 +45,8 @@ class LazyCDProof : public CDProof */ LazyCDProof(ProofNodeManager* pnm, ProofGenerator* dpg = nullptr, - context::Context* c = nullptr); + context::Context* c = nullptr, + std::string name = "LazyCDProof"); ~LazyCDProof(); /** * Get lazy proof for fact, or nullptr if it does not exist. This may @@ -66,6 +67,9 @@ class LazyCDProof : public CDProof * * @param expected The fact that can be proven. * @param pg The generator that can proof expected. + * @param isClosed Whether to expect that pg can provide a closed proof for + * this fact. + * @param ctx The context we are in (for debugging). * @param forceOverwrite If this flag is true, then this call overwrites * an existing proof generator provided for expected, if one was provided * via a previous call to addLazyStep in the current context. @@ -76,6 +80,8 @@ class LazyCDProof : public CDProof */ void addLazyStep(Node expected, ProofGenerator* pg, + bool isClosed = true, + const char* ctx = "LazyCDProof::addLazyStep", bool forceOverwrite = false, PfRule trustId = PfRule::ASSUME); /** @@ -85,8 +91,6 @@ class LazyCDProof : public CDProof bool hasGenerators() const; /** Does the given fact have an explicitly provided generator? */ bool hasGenerator(Node fact) const; - /** identify */ - std::string identify() const override; protected: typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction> |