projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 912ada0) | patch
(proof-new) Refactoring cyclic checks (#5291)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 19 Oct 2020 00:58:50 +0000 (19:58 -0500)
committerGitHub <noreply@github.com>
Mon, 19 Oct 2020 00:58:50 +0000 (19:58 -0500)
commit94e3d9a0c2a51fbfd44516113527f34ed2c13e44
treefc3b5fbac632c53b83f3d103f2a653cbf41d48eatree
parent912ada0fb5368f3420b455b8bc76e88db164c37ccommit | diff
(proof-new) Refactoring cyclic checks (#5291)

This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true.

It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.
src/expr/proof_node_algorithm.cpp diff | blob | history
src/expr/proof_node_algorithm.h diff | blob | history
src/expr/proof_node_manager.cpp diff | blob | history
src/expr/proof_node_to_sexpr.cpp diff | blob | history