projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 54eac4f) | patch
Generalize congruence handling for HO in eq proofs (#6883)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 14 Jul 2021 21:35:21 +0000 (18:35 -0300)
committerGitHub <noreply@github.com>
Wed, 14 Jul 2021 21:35:21 +0000 (21:35 +0000)
commit35397d766e6cb991c0106aca56dcff865f525270
tree607a4ea156f82737263210d7d4563f1ab34bf8c6tree
parent54eac4f9781d9c07446453697128c4bd036c110dcommit | diff
Generalize congruence handling for HO in eq proofs (#6883)

Previously we were not considering proofs for HO equalities (i.e., between operators) that were transitivity chains. This commit generalizes the elaboration procedure in eq_proof to do so.
src/theory/uf/eq_proof.cpp diff | blob | history