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

[Philipp Ruemmer]

Hi all,

for reasons of consistency, I would also prefer #1.

A related hypothetical question is whether the SMT-LIB standard, at some 
point in the far future, might define proper cases in which 'exit' can 
fail. For instance, a unix shell (or at least bash) sometimes refuses to 
exit with the explanation that there are still stopped jobs around; at 
the moment something like this does not exist in SMT-LIB of course, but 
it's not impossible to imagine similar scenarios in SMT-LIB.

Philipp

On 06/28/2015 01:49 PM, cok at frontiernet.net wrote:
> #3 is not a good idea, except as a transition, because a tool that is interacting with the solver does not know whether to expect a "success" response or not. Granted it is handleable, but more of a nuisance.
> I'd prefer #1, for consistency. I'm having a hard time imagining what internal processing would prevent a solver from printing to the output channel just before closing that channel (if it is not stdout) and terminating. I'm not too concerned about tools that fail in some respect after printing success and before aborting. I could live with #2.
>
> Note that a quick check of cvc4, z3, yices2 in interactive mode shows that those three anyway all implement #1 - printing success, if :print-success is true.
> By the way, I'm cleaning up, for public sharing, a compliance test suite that I have used for jSMTLIB - as well as migrating it to V2.5/6. It identifies differences such as this, and many others...
>
> - David
>
>        From: Florian Schanda <florian.schanda at altran.com>
>   To: smt-lib at cs.nyu.edu
> Cc: "Tinelli, Cesare" <cesare-tinelli at uiowa.edu>
>   Sent: Sunday, June 28, 2015 6:13 AM
>   Subject: Re: [SMT-LIB] Response to (exit) Command?
>     
> On Sunday 28 Jun 2015 07:51:08 Tinelli, Cesare wrote:
>> 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
> As a user, I think (2) would be what I expect.
>
>      Florian
>
>
> _______________________________________________
> 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