projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 895bf22) | patch
Use raw symbols in proofs (#8550)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 4 Apr 2022 17:41:40 +0000 (12:41 -0500)
committerGitHub <noreply@github.com>
Mon, 4 Apr 2022 17:41:40 +0000 (17:41 +0000)
commitf1559c05eb317a591bb18a832d0e87078d85218b
tree5f60ec0e448c3fc8cf9a98a9cb68dea4ee2e1081tree
parent895bf2273d3e9baa89d4a6de174e7789f2ab71afcommit | diff
Use raw symbols in proofs (#8550)

This ensures we don't quote symbols that should not be quoted, fixing two issues:
(1) Proofs in the internal calculus don't convert `:args` to `|:args|`.
(2) LFSC identifiers for terms are not quoted based on SMT-LIB restrictions.

Work towards https://github.com/cvc5/cvc5-projects/issues/466, quoted TypeNode names still need to be addressed.
src/expr/node_manager_template.cpp diff | blob | history
src/expr/node_manager_template.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_node_converter.h diff | blob | history
src/proof/lfsc/lfsc_printer.cpp diff | blob | history
src/proof/proof_node_to_sexpr.cpp diff | blob | history
src/theory/builtin/kinds diff | blob | history