diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-08 15:59:06 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-08 21:59:06 +0000 |
| commit | 89dfd279d8786c54c35ff8f5e2802ec51a59a969 (patch) | |
| tree | c4670e40caf7b46c1d9ffd4af1dfa1c743d7c6d5 /src/proof/eager_proof_generator.cpp | |
| parent | f2fb0be98861642e0e33ff3c5dc763e8aa5fe769 (diff) | |
Add lambda lift utility (#7601)
Towards a lazy approach for handling lambdas in the higher-order extension.
Diffstat (limited to 'src/proof/eager_proof_generator.cpp')
| -rw-r--r-- | src/proof/eager_proof_generator.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/proof/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp index 2a86f982c..36ef1bf58 100644 --- a/src/proof/eager_proof_generator.cpp +++ b/src/proof/eager_proof_generator.cpp @@ -134,6 +134,18 @@ TrustNode EagerProofGenerator::mkTrustedRewrite(Node a, return TrustNode::mkTrustRewrite(a, b, this); } +TrustNode EagerProofGenerator::mkTrustedRewrite(Node a, + Node b, + PfRule id, + const std::vector<Node>& args) +{ + Node eq = a.eqNode(b); + CDProof cdp(d_pnm); + cdp.addStep(eq, id, {}, args); + std::shared_ptr<ProofNode> pf = cdp.getProofFor(eq); + return mkTrustedRewrite(a, b, pf); +} + TrustNode EagerProofGenerator::mkTrustedPropagation( Node n, Node exp, std::shared_ptr<ProofNode> pf) { |