Andrew Reynolds a7ba49d278 Do not construct terms for print letification (#10138) ...

This modifies the smt2 printer to rely on map lookups instead of doing a deep conversion of the term-to-letify.

This makes proof printing roughly 2x faster in my initial experiments.
Update: it brings us from 4.75x -> 4.4x overhead for the overall proof toolchain.

It also corrects an issue in the LFSC signature encountered while testing, takes an optimization for the ALF printer from the dev branch, and changes the interface for let binding for convenience.

2023-12-06 16:07:26 +00:00

..

alf

Enable ALF proof printer (#10114)

2023-10-19 21:05:55 +00:00

lfsc/signatures

Do not construct terms for print letification (#10138)

2023-12-06 16:07:26 +00:00