projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 39bd564) | patch
Eliminate match from LFSC proofs (#8090)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 23 Feb 2022 20:08:49 +0000 (14:08 -0600)
committerGitHub <noreply@github.com>
Wed, 23 Feb 2022 20:08:49 +0000 (20:08 +0000)
commit8aac6169d225233b61ac30083fbba65e9b9ed904
tree71a6085df15097b6cb88af62a913c2d126607d9dtree
parent39bd56468f08040f91ca1ed93f4741d8e76d6c38commit | diff
Eliminate match from LFSC proofs (#8090)

The smt 2.6 term match is very hard to represent in LFSC, this eliminates it in favor of the ITE term that it is syntax sugar for. Like other aspects of the LFSC conversion, this is part of the trusted core.

This avoids internal type errors in the LFSC node converter.
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_node_converter.h diff | blob | history
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history