projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 63534a3) | patch
Distinguish name variants for types in LFSC node converter (#8624)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 18 Apr 2022 21:29:24 +0000 (16:29 -0500)
committerGitHub <noreply@github.com>
Mon, 18 Apr 2022 21:29:24 +0000 (21:29 +0000)
commit6ed000bbe930890df67da1999aa76ed0d815e850
tree0aa76f77846b2c98615718ee2fa7d54d41d22c2ctree
parent63534a395be3459444a576953da2b885cfdaf195commit | diff
Distinguish name variants for types in LFSC node converter (#8624)

This PR ensures we distinguish names for cases where types and terms are given the same name.

In particular, this generalizes the getNameForUserNameOf to work with node identifiers instead of Node, so that TypeNode can also use this method for assigning unique names.

It also adds preliminary support for uninterpreted sort constructors in the LFSC node converter.

This fixes 4 more LFSC failures on our regressions.
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_node_converter.h diff | blob | history