[SMT-LIB] prompts

[Tinelli, Cesare]

David and all,

On 27 Jun 2015, at 03:42, cok at frontiernet.net wrote:

> The SMT-LIB standard makes a distinction between the regular-output-channel and the diagnostic-output-channel. The former is supposed to contain only S-expressions in the form specified as responses to the various SMT-LIB commands. The latter can contain anything.
> What about prompts issued as part of running a solver in interactive mode?Nearly all solvers emit them on the regular-output-channel.Does the standard intend to require that prompts be issued on the diagnostic-output-channel? or is this output allowed on the regular-output-channel.
> One more thing to clarify in the standard (that I did not think of in all my reading of it before, until I encountered a solver that used stderr for prompts).

I do not recall if at some point the authors of the reference document discussed where prompts should go. The document itself does not contain enough information to respond either way. So before adding any clarification, we should probably discuss this.

My take is that regular-output-channel should contain, as you say above, only s-expressions in the form specified as responses to the various SMT-LIB commands.  Hence, the prompt should go to the diagnostic-output-channel. This would be consistent with the requirement that a solver have the same input-output behavior regardless of whether it is run in interactive or in batch mode. But I do not have a strong option here.

Any arguments on why the prompt should be sent to regular-output-channel?


Cesare


> - David
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib