dReal/dReach exit codes

[shmarovfedor]

I just checked the exit codes in dReal/dReach and I found out that dReal returns 1 (EXIT_FAILURE) in case of abnormal termination and 0 (EXIT_SUCCESS) otherwise. dReach always returns 0 (even in case of failure).

I thought that it would be very useful to specify several exit codes in dReach/dReal corresponding to the appropriate computation results. I talked to @pzuliani and he suggested using codes 51 (sat) and 52 (unsat) as they are not reserved.

That would be very helpful to the developers who want to call dReal/dReach from their applications and just check for sat or unsat. Checking the exit code would be much easier than finding a correct output file and reading the result from there.

[soonhokong]

I see. I still think that we need to respect the Unix tradition where normal program termination should return 0.

However, we can provide a command-line option for this feature. I'll implement this soon, just give us a good name for this option :-)

[shmarovfedor]

We were thinking that --exit_code would be the option for this purpose. I think it should work for both dReach and dReal. The exit codes are 51 if sat and 52 if unsat

Also we found out that dReach does not check whether dReal terminated correctly. Hence, dReach calls dReal up to -k times even if dReal failed on the previous calls and returns 0 regardless.

[pzuliani]

@soonhokong: for ProbReach we need a reliable way to run multiple instances of dReach on a multicore system, so it would be great if you could implement --exit_code.

Then we could use these macros to read the actual code https://www.gnu.org/software/libc/manual/html_node/Process-Completion-Status.html

[soonhokong]

OK. I'll implement it.

[pzuliani]

Perfect - thank you!

[soonhokong]

@pzuliani and @shmarovfedor, can you use a script something like https://gist.github.com/soonhokong/0fe364a343694c788e05 instead?

Usage:

./exit_code_wrapper.sh ~/work/dReal/bin/dReal ~/work/dReal/src/tests/nra/03.smt2 --visualize

An .smt2 file can have multiple check commands and we can have a different sat/unsat result for each of check command. I know what you want is to grab the result of last 'check' and return the exit code accordingly, but it requires some changes in the codebase and I think it's cleaner if you can use the script.

[pzuliani]

Oh, I see your point - many thanks. Btw, are the check commands processed FIFO?

I think ProbReach is currently getting the result using something like the script.

[soonhokong]

Oh, I see your point - many thanks. Btw, are the check commands processed FIFO?

Yes.

I think ProbReach is currently getting the result using something like the script.

I see.

[pzuliani]

Actually, we only need dReach to return the code. Fedor has added a -z dReach option to return the 51/52 exit code. Could you have a look at the change and possibly merge it?

That way we wouldn't need to parse the dReach command line, deal with output files, etc - it'd be an easier, plug and play integration with ProbReach. Thanks ...

[soonhokong]

OK, please ask him to submit a pull-request, I'll review and merge it.

[shmarovfedor]

Just did. Thanks Soonho

[soonhokong]

merged.

[pzuliani]

Many thanks Soonho!