diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-01 09:07:34 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-01 14:07:34 +0000 |
| commit | e2675f8a1eb18be5697493d89ac97347e598c57d (patch) | |
| tree | 2435fd13dd580a4be943cd1d51823ba78877f866 /src/CMakeLists.txt | |
| parent | 971ae785a4789776e6fe36121c80b69162c2fd27 (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.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index fe9267bed..f78e951d3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -180,12 +180,16 @@ libcvc5_add_sources( proof/lfsc/lfsc_node_converter.h proof/lfsc/lfsc_post_processor.cpp proof/lfsc/lfsc_post_processor.h + proof/lfsc/lfsc_printer.cpp + proof/lfsc/lfsc_printer.h proof/lfsc/lfsc_print_channel.cpp proof/lfsc/lfsc_print_channel.h proof/lfsc/lfsc_util.cpp proof/lfsc/lfsc_util.h proof/method_id.cpp proof/method_id.h + proof/print_expr.cpp + proof/print_expr.h proof/proof.cpp proof/proof.h proof/proof_checker.cpp |