search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Sort trigger patterns before caching #1070

Closed Halbaroth closed 5 months ago

Halbaroth commented 5 months ago

As we noticed a long time ago, the Matching module of Alt-Ergo sorts patterns of multi-triggers during each iteration of the matching round. It's inefficient as the weight used for sorting doesn't change.

I thought we should perform these sorts during the generation of triggers in Expr but actually, Alt-Ergo can generate new triggers later depending on the matching configuration (see Util.matching_env).

In this PR, we perform the sorts just before caching the generated triggers in Matching.

bclement-ocp commented 5 months ago

I believe there are still places where we can create unsorted triggers, namely from backwards_triggers, forward_triggers and make itself.

I am a bit concerned about the potential for subtle bugs if unsorted triggers make their way to the matching function; I'd like to at least have a debug assertion that the triggers are sorted at that point.

Halbaroth commented 5 months ago

Good catch! I didn't notice they created new triggers!