projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 971ae78) | patch
Add the LFSC printer (#7158)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 1 Oct 2021 14:07:34 +0000 (09:07 -0500)
committerGitHub <noreply@github.com>
Fri, 1 Oct 2021 14:07:34 +0000 (14:07 +0000)
commite2675f8a1eb18be5697493d89ac97347e598c57d
tree2435fd13dd580a4be943cd1d51823ba78877f866tree
parent971ae785a4789776e6fe36121c80b69162c2fd27commit | diff
Add the LFSC printer (#7158)

This adds the LFSC printer for proof nodes. This PR has been split to not include support for DSL rewrite rules yet, or its main print method which will be added in a followup PR.

Further PRs will connect this printer as a possible output format for cvc5.
src/CMakeLists.txt diff | blob | history
src/proof/lfsc/lfsc_printer.cpp [new file with mode: 0644] blob
src/proof/lfsc/lfsc_printer.h [new file with mode: 0644] blob