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_manager.h | |
| 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_manager.h')
| -rw-r--r-- | src/expr/proof_node_manager.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 54d398545..32513cd0d 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -158,6 +158,14 @@ class ProofNodeManager bool updateNode(ProofNode* pn, ProofNode* pnr); /** Get the underlying proof checker */ ProofChecker* getChecker() const; + /** + * Clone a proof node, which creates a deep copy of pn and returns it. The + * dag structure of pn is the same as that in the returned proof node. + * + * @param pn The proof node to clone + * @return the cloned proof node. + */ + std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn); private: /** The (optional) proof checker */ |