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

[cok at frontiernet.net]

#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