projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d72a513) | patch
Fixes for LFSC printing and signatures (#8579)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 6 Apr 2022 18:43:33 +0000 (13:43 -0500)
committerGitHub <noreply@github.com>
Wed, 6 Apr 2022 18:43:33 +0000 (18:43 +0000)
commit77d0bec48a745e3c4acd65085f9c59bdfceed6c0
tree7af8c54e5438025ac359db85979be8cf4dfaf912tree
parentd72a51367e09ff34796dcdc7f86e923900804989commit | diff
Fixes for LFSC printing and signatures (#8579)

Ensures we recognize some internal FP symbols, adds a missing string operator, fixes seq.unit operator printing (required for CONG over seq.unit), fix for 0-ary tuple printing.
proofs/lfsc/signatures/theory_def.plf diff | blob | history
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_printer.cpp diff | blob | history