Feature request: configuration option to write generated SMT commands to a file instead of being displayed on stdout

[shigoel]

For large SMT files, it would be helpful to not have a cluttered Lean Info window.

This would also allow the generated SMT file to be processed by other tools (including other solvers).

[PratherConid]

I've added auto.smt.save and auto.smt.savepath.

[shigoel]

@PratherConid Thanks for adding these options!

A follow-up request: the generated SMT files do not have the set-logic and check-sat commands. Adding those would be helpful. Thank you!

[PratherConid]

@shigoel Is the set-logic command supposed to be (set-logic ALL), or you want to specify the logic manually?

[shigoel]

Using ALL would be a safe default option, yes. If you like, you could also give an option to the user to specify their desired logic. Thanks!