Fix error handling of dolmen

[Stevendeo]

When dolmen fails, its default behavior is to call exit with a custom exit code. This MR overrides the error function of the dolmen loop so that alt-ergo keeps control over the exit code.

[bclement-ocp]

Alt-Ergo's current infrastructure for error handling is centered around the Errors module. Would it be possible to add a new DolmenError constructor to Errors.error instead, and deal with printing in the same place as for other errors?

[bclement-ocp]

BTW if the only goal is to keep control over the exit code, Dolmen provides facility to register our own exit codes (see usage in the Dolmen binary here )

[Stevendeo]

BTW if the only goal is to keep control over the exit code, Dolmen provides facility to register our own exit codes (see usage in the Dolmen binary here )

It is not only to have control over the exit code, but to have control on how alt-ergo exits. We don't want an external library to exit alt-ergo.

[Halbaroth]

Alt-Ergo's current infrastructure for error handling is centered around the Errors module. Would it be possible to add a new DolmenError constructor to Errors.error instead, and deal with printing in the same place as for other errors?

It depends if we consider the Dolmen frontend as a part of the library or a part of the binary. Currently, the situation is a mess as we have some parts of the Dolmen frontend in the binary (solving_loop manages statements as get-info, get-model, set-option, ...) and some parts in the library (mainly in d_cnf.ml, frontend.ml). I haven't decided yet which design is the best in our case, so I have no strong opinion about the location of this error.

[bclement-ocp]

Right now, the situation is that Dolmen is part of the library though :) I actually think the current situation makes sense given the infrastructure we have — D_cnf deals with parsing actual expressions while Solving_loop deals with state and solver management, which is also the separation of concerns within the legacy frontend.

Besides, Dolmen provides parsing and typechecking, which can be useful to users of the library (e.g. for parsing custom preludes or other SMT-LIB fragments), and as long as the preludes are external files, providing any meaningful FPA support in the library (e.g. #746 ) requires Dolmen (provided we keep the plan of deprecating and removing the legacy frontend).

[Halbaroth]

If @bclement-ocp agrees, we can merge it :)