[SMT-LIB] prompts

[Jochen Hoenicke]

Hello all,

>
> On 27 Jun 2015, at 03:42, cok at frontiernet.net wrote:
>
> > 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 think prompts are not even mentioned in the standard.  Printing them on
stdout when the solver is not used interactively would definitely be wrong
as it breaks compatibility.    A tool expecting the sexpr output that is
described in the standard would break if the solver prints prompts between
them.   I hope that the tools that print prompts on stdout check that they
are used on a tty before.  Even then it is not covered by the standard.

2015-06-28 21:17 GMT+02:00 Viktor Kuncak <viktor.kuncak at epfl.ch>:

> 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.
>

I think diagnostic output channel may be useful for debugging or to
understand why the solver finds a particular model, but it shouldn't be
parsed by a tool using the SMT solver.  Either ignore it or save it to a
log file.  With (set-option :verbosity 0) (which is even the default
according to the standard) one can disable any output on the diagnostic
channel.

Regards,
  Jochen


-- 
Jochen Hoenicke,
Email: hoenicke at informatik.uni-freiburg.de  Tel: +49 761 203 8243