cut and check support in Dolmen frontend

[bclement-ocp]

The cut and check primitives are not supported with the Dolmen frontend. Part of the reason is that Dolmen does not type cut and check.

$ cat check_cut.ae
goal g_check : check (true = false) -> true = false
goal g_cut : cut (true = false) -> true = false
$ alt-ergo check_cut.ae
File "check_cut.ae", line 1, characters 23-35: I don't know (0.0036) (2 steps) (goal check_1)
File "check_cut.ae", line 1, characters 16-52: I don't know (0.0041) (2 steps) (goal g_check)
File "check_cut.ae", line 2, characters 19-31: I don't know (0.0041) (2 steps) (goal cut_1)
File "check_cut.ae", line 2, characters 14-48: Valid (0.0041) (0 steps) (goal g_cut)
$ alt-ergo --frontend dolmen check_cut.ae
File "check_cut.ae", line 1, character 15-35:
1 | goal g_check : check (true = false) -> true = false
                   ^^^^^^^^^^^^^^^^^^^^
Error The following Dolmen builtin is currently not handled during typing
      `check`. Please report upstream

See also Gbury/dolmen#178

[bclement-ocp]

After discussing with @Gbury we can deal with this in Alt-Ergo proper for now. This would require adding support in the "additional builtins" in d_cnf.

Note that:

• This is a rarely used feature. We could just have our own error message more appropriate for Alt-Ergo (although I just realized I don't think we have access to the location in the additional builtins)
• If we do want to support it in Alt-Ergo, this is a bit annoying because now D_cnf.make must be able to return multiple goals, not just one (same as what happens in the old typechecker). The current architecture assumes that D_cnf returns a single goal.

[Halbaroth]

In my opinion we should deprecate this feature as we can reproduce this behaviour using the SMT-LIB language. We can deprecate the feature with the legacy frontend in 2.6.0 and make clear we don't plan on supporting these keywords in the new frontend for the native language.

[bclement-ocp]

I tried to make a proper warning for this but it seems like it is blocked on Gbury/dolmen#218 — we don't have a clean way of of pre-empting the message from Dolmen that mentions "Dolmen" (which we would want to avoid).