[SMT-LIB] prompts

[cok at frontiernet.net]

The argument for putting prompts on the regular output is that
most tools that have prompts do put them on stdout, I suppose either because it was not thought about or because it was simpler or to avoid problems with stdout and stderr not being flushed appropriately. It is useful to be able to use the prompt as a marker to say that all the input has been received.
I did not even think of this issue until I encountered yices-smt2 doing that and needing to accommodate it in my test suite driver.
Despite the above, I think I'm in favor of using the diagnostic output for the reasons Cesare states. It may need a bit of experimentation to be sure that the user experience from tools is OK, but I've had no problems from yices on this account.
- David
      From: "Tinelli, Cesare" <cesare-tinelli at uiowa.edu>
 To: Smt-lib <smt-lib at cs.nyu.edu> 
 Sent: Sunday, June 28, 2015 3:38 AM
 Subject: Re: [SMT-LIB] prompts
   
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



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