projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 079a04b) | patch
generalize handling MERGED_THROUGH_CONSTANST in EqProof conversion (#4878)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 12 Aug 2020 23:18:16 +0000 (20:18 -0300)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 23:18:16 +0000 (20:18 -0300)
commit10b5153f63a2e9a575ffe5abfad69e53ed8e3d5b
treea281c06b072211ee4004a09df90cc6a3486123betree
parent079a04b0b16f7caa31a15b97ddc9794ad0d8b862commit | diff
generalize handling MERGED_THROUGH_CONSTANST in EqProof conversion (#4878)

Now that we are using the constant folding in equality engine for more than equality it is necessary to generalize the previously-hard-coded handling of MERGED_THROUGH_CONSTANTS.
src/theory/uf/eq_proof.cpp diff | blob | history