diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-19 18:55:19 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-19 18:55:19 -0500 |
| commit | e8000a4693ecc1f8418c80726032ef6937e36241 (patch) | |
| tree | b6869ef2f8da60f76d6f946f38fb885f1d817d33 /src/expr/lazy_proof.cpp | |
| parent | 0f9ae462a99f04607c6406afb129fa1393f1ce33 (diff) | |
(proof-new) CDProof inherits from ProofGenerator (#4622)
This design simplifies a number of issues and makes the PRefProofGenerator class obsolete.
Diffstat (limited to 'src/expr/lazy_proof.cpp')
| -rw-r--r-- | src/expr/lazy_proof.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 400ce2cf0..3980a3cb3 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -27,12 +27,12 @@ LazyCDProof::LazyCDProof(ProofNodeManager* pnm, LazyCDProof::~LazyCDProof() {} -std::shared_ptr<ProofNode> LazyCDProof::mkProof(Node fact) +std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) { Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl; // make the proof, which should always be non-null, since we construct an // assumption in the worst case. - std::shared_ptr<ProofNode> opf = CDProof::mkProof(fact); + std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact); Assert(opf != nullptr); if (!hasGenerators()) { @@ -176,4 +176,6 @@ bool LazyCDProof::hasGenerator(Node fact) const return it != d_gens.end(); } +std::string LazyCDProof::identify() const { return "LazyCDProof"; } + } // namespace CVC4 |