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.cpp | |
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.cpp')
-rw-r--r-- | src/theory/eager_proof_generator.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index 9c25fb3e4..09f02708b 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -20,8 +20,9 @@ namespace CVC4 { namespace theory { EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, - context::Context* c) - : d_pnm(pnm), d_proofs(c == nullptr ? &d_context : c) + context::Context* c, + std::string name) + : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c) { } @@ -97,8 +98,7 @@ TrustNode EagerProofGenerator::mkTrustNode(Node n, const std::vector<Node>& args, bool isConflict) { - std::vector<std::shared_ptr<ProofNode>> children; - std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, children, args, n); + std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, n); return mkTrustNode(n, pf, isConflict); } @@ -117,9 +117,10 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) { // make the lemma Node lem = f.orNode(f.notNode()); - std::vector<Node> args; - return mkTrustNode(lem, PfRule::SPLIT, args, false); + return mkTrustNode(lem, PfRule::SPLIT, {f}, false); } +std::string EagerProofGenerator::identify() const { return d_name; } + } // namespace theory } // namespace CVC4 |