projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bd184f9) | patch
(proof-new) Improve robustness of CONG rule (#4882)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Aug 2020 21:34:47 +0000 (16:34 -0500)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 21:34:47 +0000 (18:34 -0300)
commit85a8dfddd887a041f397d1ff2c3a6c34900c5775
tree81344647d0ac9c61040dfa3954c8200c8efbf561tree
parentbd184f9813a91d8f60eb0521893a5154b9f92357commit | diff
(proof-new) Improve robustness of CONG rule (#4882)

This makes it so that the explicit Kind is wrapped in a Node as an argument to the CONG proof rule. This allows us to distinguish applications with the same parameterized operator but different kinds (e.g. APPLY_SELECTOR vs APPLY_SELECTOR_TOTAL).
src/expr/proof_rule.h diff | blob | history
src/theory/uf/proof_checker.cpp diff | blob | history