Make it possible to re-use a single solver connection for multiple type checker invocations

[brianhuffman]

This ticket is inspired by GaloisInc/saw-script#953. Basically, in saw we often want to parse and typecheck a large number of cryptol expressions. However, currently the typechecking API requires us to open a new solver connection every time we run the type checker, which requires starting a process, and then parsing CryptolTC.z3 and sending it to the solver. If you have to do this hundreds of times, the cost adds up.

I would like to be able to manually initialize a connection and then store the Solver handle somewhere, so I can reuse the same one for lots of different calls to the type checker.

[robdockins]

It is desirable to reduce further the number of times we fork a Z3 instance, so I'm going to reopen this issue to track the task of pushing the typechecking solver instance all the way to the top level of both the REPL and the remote Cryptol API servers.

[robdockins]

Fixed again via #1128