projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8838a4e) | patch
(proof-new) Proper implementation of proof node cloning (#6285)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 7 Apr 2021 19:45:45 +0000 (14:45 -0500)
committerGitHub <noreply@github.com>
Wed, 7 Apr 2021 19:45:45 +0000 (19:45 +0000)
commitaa1f4021b70a1016502ead46bf68907bf092d65c
treea0d9b352689cd27628b0be4adf1da2b297163d09tree
parent8838a4e8ac47f94089044e2c638376c28a0fd7cdcommit | 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.
src/expr/proof_node.cpp diff | blob | history
src/expr/proof_node.h diff | blob | history
src/expr/proof_node_manager.cpp diff | blob | history
src/expr/proof_node_manager.h diff | blob | history
src/smt/proof_manager.cpp diff | blob | history
src/theory/uf/proof_equality_engine.cpp diff | blob | history