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

[rdelmas]

Hi,
what could be useful from a developper's perspective, would be the 
solver to tell me when it has not been able to quit gracefully so that I 
can for instance kill it using a system signal.
If the standard does not force solvers to print succces on exit I cannot 
safely assume that the lack of "success" represents failure.
In the special case of exit it would perhaps be better for the solver 
print something on *failure*.

Regards;

Le 29.06.2015 00:11, Philipp Ruemmer a écrit :
> 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
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib