diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 14:45:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-07 19:45:45 +0000 |
| commit | aa1f4021b70a1016502ead46bf68907bf092d65c (patch) | |
| tree | a0d9b352689cd27628b0be4adf1da2b297163d09 /src/expr/proof_node.cpp | |
| parent | 8838a4e8ac47f94089044e2c638376c28a0fd7cd (diff) | |
(proof-new) Proper implementation of proof node cloning (#6285)
Previously, we were traversing proof node as a tree, now we use a dag traversal.
This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat.
Diffstat (limited to 'src/expr/proof_node.cpp')
| -rw-r--r-- | src/expr/proof_node.cpp | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp index f7ad65844..9450ddc99 100644 --- a/src/expr/proof_node.cpp +++ b/src/expr/proof_node.cpp @@ -44,19 +44,6 @@ bool ProofNode::isClosed() return assumps.empty(); } -std::shared_ptr<ProofNode> ProofNode::clone() const -{ - std::vector<std::shared_ptr<ProofNode>> cchildren; - for (const std::shared_ptr<ProofNode>& cp : d_children) - { - cchildren.push_back(cp->clone()); - } - std::shared_ptr<ProofNode> thisc = - std::make_shared<ProofNode>(d_rule, cchildren, d_args); - thisc->d_proven = d_proven; - return thisc; -} - void ProofNode::setValue( PfRule id, const std::vector<std::shared_ptr<ProofNode>>& children, |