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

[Tinelli, Cesare]

Hi Tjark and all,

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?
> 
> Figure 3.10 in the SMT-LIB Standard is inconclusive, as the script
> contains a previous "(set-option :print-success false)" 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.

As always though nothing is written in stone here. If there are strong arguments for exempting 'exit' from printing success we could adjust the standard accordingly. 


> Arguably, when the (exit) command has
> been successfully executed (and not just parsed), the solver is no
> longer able to respond at all.
> 
> It is perhaps unsurprising then that different SMT solvers currently
> show different behavior. (veriT seems to print "success", while most if
> not all other solvers don't.)
> 
> I would suggest to add a clarifying remark or footnote to the Standard,
> perhaps in Section 4.2.1, that details which behavior(s) are required
> or permitted here.
> 
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.

Any opinions?


Cesare


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