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

[Cesare Tinelli]

Tjark,

On 21 Apr 2016, at 9:57, Tjark Weber wrote:

> Cesare,
>
> On Sun, 2015-06-28 at 09:30 +0000, Tinelli, Cesare wrote:
>> Fair enough, in that case I would go with option (2) below.
>> I'd like to hear from more people though.
>
>>>> 1) require 'exit' to print 'success',
>>>> 2) require 'exit' not to print anything, or
>>>> 3) allow it to print 'success' without requiring it
>
> Has this question (whether solvers may/must/must not print 'success' 
> in
> response to the 'exit' command) been resolved?
>
Since we, the SMT-LIB coordinators, got no response from the community 
after the post you quote above, we have resolved it by sticking with 
option 1.

We think that the original decision is still the most reasonable: 'exit' 
is no different than the other commands. The solver should reply to it 
with 'success' right before exiting if there are no problems. If it 
*can* detect a problem, it should report it in the standard way, by 
printing an expression of the form (error <string>) on the error 
channel.

Now, if the main program (in the C sense) of the solver crashes or hangs 
or has some other problems at the process level, no error message will 
be reported by it obviously. Some errors might be reported by the 
operating system, but those are outside the scope of the SMT-LIB 
standard.

A robust solver implementation would put the bulk of the solver in a 
child process of the main program so that the main can catch some of the 
cases of erroneous termination by the subprocess and report back on with 
an (error <string>) response. But this is an architectural choice, which 
we feel is again outside the scope of the SMT-LIB standard.


Cesare


> Best,
> Tjark