projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2c9207d) | patch
[proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Sat, 24 Oct 2020 00:20:42 +0000 (21:20 -0300)
committerGitHub <noreply@github.com>
Sat, 24 Oct 2020 00:20:42 +0000 (19:20 -0500)
commit6937d6afe65ae3e51f514ca463f95faa3feda7aa
tree198d1b1f443485d75aa496da640b2f140128a443tree
parent2c9207df7bc8ce88e84ffb51cd5eed0de37283bccommit | diff
[proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)

Adding missing cases of kinds that are n-ary but whose partial applications are
not true terms in the equality engine. This in the case not only for APPLY_UF
but also for the APPLY_* kinds for datatypes.
src/theory/uf/equality_engine.cpp diff | blob | history