Supporting evaluation for custom functions

[Halbaroth]

If an input file contains custom built-in functions, Dolmen's binary cannot check the model as Dolmen's evaluation function doesn't know this built-in.

For instance Alt-Ergo has a custom built-in round function which isn't a part of the SMT-LIB standard. As we discussed offline, this low-priority feature is annoying to implement.

A naive way to support this feature in AE without modifying Dolmen consists in adding definitions for these builtins in the input problem which means we have to add an option in AE to check models with Dolmen's library instead of calling the binary on the outputted model by the solver.

[Halbaroth]

After consideration, adding definitions to the input problem won't solve the issue because this definition will probably involve quantifiers and Dolmen doesn't support model checking of quantified problems.

[Gbury]

Technically, adding support for these function is quite easy (in terms of code needed for typing and evaluation). However, the main problem I see are the following:

• how to enable use of these functions: it probably need to be behind a flag at least for the CLI, and we'd need to figure out a reasonable way to do that
• what happens if/when other projects use their own custom functions ? do we add all of these custom functions to dolmen and grow the list of CLI flags to accomodate all of the expansions ?

[bclement-ocp]

Would it make sense to use dune-site's plugin mechanism for this?

Dolmen could expose a registry of builtins that plugins can register themselves into to provide the implementation of such functions. The easiest would be that the plugin also expose a name so that the builtins provided by, say, the "alt-ergo" plugin are enabled iff the command line --enable-builtins alt-ergo (maybe also DOLMEN_ENABLE_BUILTINS environment variable) is passed (and from the API there would something like BuiltinRegistry.get_builtins_for "alt-ergo").

This way, the custom functions do not live in Dolmen itself, but there could be separate packages such as dolmen-plugin-alt-ergo (which could be maintained by Alt-Ergo rather than by Dolmen) that provides the approriate builtins and are picked up by Dolmen dynamically through dune-site.

[Gbury]

(sorry for the delay) Using dune's plugin mechanism seems like a good fit for this. I won't have the time to work on that feature in the near (or medium) future, but if you're still interested, you're welcome to open a PR to add this, ^^

[bclement-ocp]

I took a quick look. It is more complicated than I expected because we also need to be able to type the builtins, which I think the right way to do would be to register typing extensions, but typing extensions can only be registered after instantiated the Dolmen_loop.Typer.Make functor has been instanciated, which is done by the binary, so the plugins would have to depend on the binary.

Alternatively, typing extensions could be moved out of the functor. This would mean that they are global rather than per-instantiation; I'd say that this is OK but will let you be the judge.

(One advantage of going global is that the extensions can be shared between multiple users of the functor; for instance for Alt-Ergo we could have a single plugin for Dolmen_loop that would provide the Alt-Ergo builtins to both Alt-Ergo and Dolmen which would be a nice user experience as users would just need to have Alt-Ergo installed to have access to the Alt-Ergo builtins in Dolmen).