fix(Dolmen): Parse triggers from formula body

[bclement-ocp]

Triggers are annotated on the body of the quantifier, but Alt-Ergo looks them up on the quantifier itself. This used to be OK, because Dolmen used to copy tags from the body to the quantifier.

Since Gbury/dolmen#207 Dolmen no longer performs this copy, which means that we now ignore triggers (or rather, we use the triggers of the parent quantifier if it exists -- which is wrong).

This patch looks for trigger on the body instead, to be compatible with future Dolmen releases.

This patch also bumps the Dolmen version for obvious reasons.

See also: #1050

[bclement-ocp]

CI is failing due to #1052

[Halbaroth]

To my understanding, root_trgs or body_trgs are disjoint? I understand you use the concatenation operator here because l @ [] and [] @ l are reduced immediately to l, but for sake of readability, I would prefer to match on the logic stored in the state of the typer as you did here:

let builtins =
  fun _st (lang : Typer.lang) ->
  match lang with
  | `Logic Alt_ergo -> ae_fpa_builtins
  | `Logic (Smtlib2 _) -> bv_builtins ++ smt_fpa_builtins
  | _ -> fun _ _ -> `Not_found

[bclement-ocp]

I was going to say that doing a concatenation this way is more robust to potential future Dolmen changes, but actually the code as written is buggy in the case of nested quantifiers in SMT (we pick up the pattern for both the outer and inner quantifier), good catch!

[bclement-ocp]

Ready for round 2 - updated to dispatch trigger parsing depending on current language. This is a bit more involved because we needed to pass through the language information to the mk_expr function.

[Halbaroth]

It seems the CI still fails even after we have merged #1052. Do you know what's happening?

[bclement-ocp]

I think either the language attribute from Dolmen is wrong, or there are certain cases where Dolmen actually stores the annotations on the body of the trigger in AE format… looking into it.

We have to check the CI.

[bclement-ocp]

It seems the CI still fails even after we have merged #1052. Do you know what's happening?

Well it looks like what is happening is that the triggers are always on the body 😅

That's what I get for not double-checking this statement from a hallway conversation with @Gbury:

In the native format, triggers are annotated on the quantifier itself

(In hindsight, the fact that some AE tests were failing with our old code was suspicious)

[bclement-ocp]

Updated the patch to only look on the body for triggers and filters as per the AE parser in Dolmen. Also added more tests to cover success and failure cases in both formats.

[Gbury]

That's what I get for not double-checking this statement from a hallway conversation with @Gbury:

In the native format, triggers are annotated on the quantifier itself

Oops, sorry about that. Maybe I should try and add some documentation about that kind of things (but the question is then: where ?).

[bclement-ocp]

That's what I get for not double-checking this statement from a hallway conversation with @Gbury:

In the native format, triggers are annotated on the quantifier itself

Oops, sorry about that. Maybe I should try and add some documentation about that kind of things (but the question is then: where ?).

No worries; I think we were both confused between what Alt-Ergo does (it did check on the quantifier) and what the Dolmen parser for Alt-Ergo does (it annotates on the body).

We could probably add a note here; the SMT-LIB triggers is documented to be on the body but not the AE trigger.

(Both are used through here which mixes all these together even though they share many of the same fields)

[Halbaroth]

Thanks for the fix and the clarification.