SMT2 log file for solver interaction via the API

[PhilippWendler]

It would be great if Z3 could produce a log file in the SMT2 format for usage of solver instances via the API.

Advantages of the SMT2 log compared to the current replay log would be:

• independent of API changes
• human-readable
• can be double-checked with other SMT solvers
• in my experience tends to be smaller

All other SMT solvers that we use (MathSAT5, Princess, and SMTInterpol) have this feature.

[wintersteiger]

Crucial question: do they support export of SMT2 files in incremental API scenarios (with no other SMT2 files involved)?

Z3's internal API log files are very simple, it would probably not be much effort to translate that into "readable" C programs that use the API. However, I think translating those into SMT2 files will be quite a lot of effort, as we would have to introduce stripped down versions of all SMT functions/operators, which don't produce any intermediate expressions as otherwise any search happening later will be effected.

[PhilippWendler]

Yes. We can use for example use push/pop via the API and this results in appropriate SMT2 statements in the log.

For SMTInterpol, you can see the implementation in LoggingScript (their API is just a way to use SMT2 statements via method calls instead of passing strings, so it is very easy for them).

For MathSAT5, you can for example easily try the feature out if you take their API example, add msat_set_option(cfg, "debug.api_call_trace", "1"); msat_set_option(cfg, "debug.api_call_trace_filename", "example.smt"); directly after one of the msat_create_config(); calls and build and run the example as explained at its top.
Here is the result of doing this for the trivial incremental example1 function in this program.

If you can produce C log files, that could also be nice (each of the formats has its advantages, of course, so having several of them can be nice for debugging), especially if the C program would only use the public API and thus would be independent of internal changes.
Princess for example also can produce logs as Scala programs using their API in addition to the SMT2 log.

Because I do not know the internals of Z3 I do not know how intermediate expressions would affect the search. But the SMT2 log would be valuable even if it does not guarantee that the search of the SMT solver happens exactly as it did when the API was used. This is also not guaranteed by the other SMT solvers' logs AFAIK. However, in my experience the majority of bugs in SMT solvers I encountered were reproducible with the SMT2 log. So even having an best-effort SMT2 log in addition to the replay log would be nice.

[NikolajBjorner]

done