Add LFSC node converter (#6944)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 2 Sep 2021 22:32:49 +0000 (17:32 -0500)
committerGitHub <noreply@github.com>
Thu, 2 Sep 2021 22:32:49 +0000 (22:32 +0000)
commitbc008131991c13bb635c9351942e1ef3f7e6f49b
tree9c6612afecaa54dd46d9c5e7b7fcffc80cbc40ac
parente2994ed485c941c669787ce38876e2478dba28d0
Add LFSC node converter (#6944)

This utility converts from terms used in the internal calculus to terms that capture how they should be printed in LFSC.
src/CMakeLists.txt
src/expr/nary_term_util.h
src/proof/lfsc/lfsc_node_converter.cpp [new file with mode: 0644]
src/proof/lfsc/lfsc_node_converter.h [new file with mode: 0644]