Offer a tcSmtFile option for writing typechecker SMT solver output to a file

[RyanGlScott]

There are two situations in which Cryptol can interact with an SMT solver:

1. When running the :prove command. This SMT solver is controlled by the prover option.
2. When typechecking code. This SMT solver is controlled by the tcSolver option.

With (1), one has the ability to write the SMT solver interactions to a file by enabling the smtFile option. There is no such option for (2), however, which means that the only way to record typechecker-related SMT solver interactions is to enable tcDebug and copy-paste the output that gets printed to stdout, which will look something like this:

[send->] (set-option :print-success true )
[<-recv] success
[send->] (set-option :produce-models true )
[<-recv] success
[send->] (set-option :global-decls false )
[<-recv] success
[send->] (declare-datatypes () ((InfNat (mk-infnat (value Int ) (isFin Bool ) (isErr Bool ) ) ) ) )
[<-recv] success
...

But this is not a valid SMT-LIB file, so one then has to scrub out the [send->] prefixes and remove the [<-recv] lines entirely. All told, this is quite tedious.

To avoid this tedium, Cryptol should offer a tcSmtFile option, where tcSmtFile is to tcSolver as smtFile is to prover. Moreover, it should format the typechecker-related SMT solver interactions such that it is a valid SMT-LIB file, e.g.,

[send->] (set-option :print-success true )
; success
[send->] (set-option :produce-models true )
; success
[send->] (set-option :global-decls false )
; success
[send->] (declare-datatypes () ((InfNat (mk-infnat (value Int ) (isFin Bool ) (isErr Bool ) ) ) ) )
; success
...