Status printing and models

[Halbaroth]

After testing the behavior of cvc5 and z3 and the SMTLIB specification, I noticed that we have to produce a status message (sat, unsat, unknown) before producing a model with (get-model). The information is important while checking a response for instance.

Now, let's imagine that we change the output channel for models only (with the option CLI option --model-output). Then we can loose the status of the check-sat that will be printed on the standard output. The option --model-output is not a part of the SMTLIB standard.

In the original PR of Mohamed, the status was printed twice. In my opinion, it isn't an appropriate behavior.

We can also remove the option --model-output or print the status in the model-output only if it's different from the option std_output.

[bclement-ocp]

Yes, --model-output should be removed and we should be smtlib2-compliant if/where possible.

smtlib2 has two output channels: the regular output channel and the diagnostic output channel, which defaults to stdout and stderr by default.

Alt-ergo has a bazillion output channels which don't really make sense, and some I think are never changed from their default values.

We have;

• std_output
• err_output (for errors)
• wrn_output (for warnings)
• dbg_output (for debug messages)
• mdl_output (for models)
• usc_output (for unsat cores)

We should remove all of these and only use std_output and err_output (which could be renamed to regular_output and diagnostic_output for consistency with smtlib, but stdout and stderr are fairly standard).

dbg_output and wrn_output should be replaced with err_output. mdl_output and usc_output should be replaced with std_output.

Now, and this is one of the reasons we should rename err_output to diagnostic_output, the slightly confusing thing is that smtlib errors in response to a command such as get-model should go to std_output, not err_output. This is because the user expects a reply on the regular output when calling get-model or get-unsat-core; if there is an error, it must be signaled on the channel that the user listens to!

I think that for 2.5.0 we can get away with simply removing mdl_output and using std_output instead (but let's check that the (error) responses are made on the proper channel). We can postpone cleaning up of the other channels for now; for the other channels (dbg, wrn, etc.) i think we should rather switch to an actual logging library such as Logs (but I don't think we should do this for 2.5.0; it is a wide change that would probably cause conflicts with #553 ).

By the way, what do you think about renaming the new --std-output and --err-output into --regular-output-channel and --diagnostic-output-channel for consistency with smtlib option names?

[Halbaroth]

I plan to use logs actually but for a later release. I agree to rename options and deprecated the older ones.