fix(FPA): Separate semantic triggers upon trigger construction

[bclement-ocp]

Currently, the theories are responsible for populating the semantic field of triggers when a lemma with semantic triggers is added to the theory (call to assume_th_elt).

This means that such a lemma lives for some time without semantic triggers: in particular, it is initially created using mk_forall without semantic triggers. During that call, the guard in find_particular_subst preventing the "particular substitution" optimization from triggering for lemmas with semantic trigger is ignored; which means that the "particular substitution" optimization is actually applied to lemmas with semantic triggers.

In particular, this optimization makes the lemma float_of_pos_pow_of_two in the FPA theory unsound, because it removes the check that x is actually a power of two, and causes #1111.

This patch makes the Expr module responsible for separating syntaxic and semantic triggers, rather than the theory. This ensures that a lemma with semantic triggers never appears as having no semantic triggers. In order to make sure this invariant is properly maintained, the trigger type is again made private to the Expr module. This required moving from sorting code from the Matching module to the Expr module, also ensuring that triggers are properly sorted for matching purposes at all times.

Fixes #1111