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/theory/eager_proof_generator.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/theory/eager_proof_generator.h')
| -rw-r--r-- | src/theory/eager_proof_generator.h | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 9a00f3612..226750a91 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -86,7 +86,9 @@ class EagerProofGenerator : public ProofGenerator NodeProofNodeMap; public: - EagerProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr); + EagerProofGenerator(ProofNodeManager* pnm, + context::Context* c = nullptr, + std::string name = "EagerProofGenerator"); ~EagerProofGenerator() {} /** Get the proof for formula f. */ std::shared_ptr<ProofNode> getProofFor(Node f) override; @@ -152,7 +154,7 @@ class EagerProofGenerator : public ProofGenerator TrustNode mkTrustNodeSplit(Node f); //--------------------------------------- end common proofs /** identify */ - std::string identify() const override { return "EagerProofGenerator"; } + std::string identify() const override; protected: /** Set that pf is the proof for conflict conf */ @@ -163,6 +165,8 @@ class EagerProofGenerator : public ProofGenerator void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf); /** The proof node manager */ ProofNodeManager* d_pnm; + /** Name identifier */ + std::string d_name; /** A dummy context used by this class if none is provided */ context::Context d_context; /** |