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/term_conversion_proof_generator.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/term_conversion_proof_generator.cpp')
| -rw-r--r-- | src/expr/term_conversion_proof_generator.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 94bff5b8c..70b429510 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -94,8 +94,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f) std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node t) { // we use the existing proofs - PRefProofGenerator prg(&d_proof); - LazyCDProof pf(d_proof.getManager(), &prg); + LazyCDProof pf(d_proof.getManager(), &d_proof); NodeManager* nm = NodeManager::currentNM(); // Invariant: if visited[t] = s or rewritten[t] = s and t,s are distinct, // then pf is able to generate a proof of t=s. @@ -230,7 +229,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node t) Assert(!visited.find(t)->second.isNull()); // make the overall proof Node teq = t.eqNode(visited[t]); - return pf.mkProof(teq); + return pf.getProofFor(teq); } Node TConvProofGenerator::getRewriteStep(Node t) const |