[SMT-LIB] Response to (exit) Command?

[Tjark Weber]

Cesare,

On Sun, 2015-06-28 at 06:51 +0000, Tinelli, Cesare wrote:
> On 17 Jun 2015, at 14:19, Tjark Weber <tjark.weber at it.uu.se> wrote:
> > May (must?) a compliant solver issue a "success" response to the (exit)
> > command?
> > [...]
> > Section 4.1.2 states
> > | The value success is the default response for a successful execution
> > | of a supported command.
> > 
> > In my opinion this is ambiguous.
> 
> Why is this ambiguous? According to the reference document, the default
> response for every command is to print 'success' on successful
> execution of the command, unless the option :print-success is set to
> false. Since there is no explicit mention of a special case for 'exit',
> the default should apply to 'exit' as well. 
> 
> The real question is perhaps what it means to successfully execute
> 'exit'. In my view, it means to be able to release all resources and
> quit. So printing 'success' on the standard output would be the very
> last operation before quitting.

Being able to release all resources and quit is different from actually
releasing all resources and quitting. The (exit) command should trigger
the latter. Therefore, I think one could argue that (exit) hasn't been
successfully executed until after the solver has quit (at which point
the solver no longer can print anything).

> I can sure add a clarification now, but we could also take the opportunity to discuss explicitly first whether the standard should:
> 
> 1) require 'exit' to print 'success',
> 2) require 'exit' not to print anything, or
> 3) allow it to print 'success' without requiring it
> 
> The status quo among solvers is best reflected by option 3, but I would be against it and would settle on either 1 or 2.

I agree, and I have no strong preference between 1) and 2). As
mentioned, most solvers currently do not print success.

Best,
Tjark