[SMT-LIB] prompts

[Viktor Kuncak]

In my group several of us believe we should only have (or care about) one
input and one output channel. Basically, we believe we should not have
prompts as separate from the standard. If something is important enough
information for the user, it is likely important enough for some form of
automated interaction as well, and should become part of the specified
interface.

Of course, solver output, just like solver input, should support a notion
of comments, which can contain additional information for the user.

Speaking of that, I would also say that SMT-LIB should also support
multi-line nested comments (in input and output).

Best regards
  Viktor

On Sun, Jun 28, 2015 at 8:01 AM cok at frontiernet.net <cok at frontiernet.net>
wrote:

> 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
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>