Teach online what4 backend about smtFile option

[RyanGlScott]

This passes the value of smtFile to each call to startSolverProcess in the online what4 backend, thereby fixing #1475. After this patch, the test case in #1475 now produces an .smt2 file, as expected.

[RyanGlScott]

Hm. I opted to copy the existing code that writes to smtFile when using w4-offline. However, one thing that I didn't realize is that this code always prints a message saying "Writing to SMT-Lib file ...", even if smtFile isn't explicitly set. This is what is causing the various test suite failures, as many more tests are now printing out "Writing to SMT-Lib file ..." than before.

Any objections if I change the code such that this "Writing to SMT-Lib file ..." message is only printed if smtFile is explicitly set?

[yav]

LGTM

[yav]

I think a more traditional name for these are "callbacks" rather than "continuations"?

[RyanGlScott]

@yav, do you have an opinion on #1476 (comment)?

[yav]

Yes, I thin we should only print the message when we were explicitly asked to save the file

[RyanGlScott]

Looking at this more closely, the way I am going about this is entirely wrong. The behavior of {sbv,w4}-offline is to always print out the SMT-LIB2 term, regardless of whether you are using stdout or an smtFile. As a result, I really shouldn't be copying the code that implements w4-offline, as that's meant for a different purpose.

Luckily, there is a much simpler way to solve this issue: we are currently calling startSolverProcess (which initiates an online what4 solver connection) like so:

cryptol/src/Cryptol/Symbolic/What4.hs

Line 504 in 8cca245

(W4.startSolverProcess fs Nothing (w4 sym))

That Nothing (of type Maybe Handle) indicates that the output will not be duplicated to any file handle. All we have to do to fix the issue at hand is obtain pcSmtFile's Handle and pass it there. I've pushed a change which does this, and now all of the test cases pass once more.

This is now ready for another round of review.