refactor(opam_solver): incremental at-most groups

[art-w]

In preparation for the on-demand loading of opam packages by the opam_solver, this refactoring introduces a small abstraction At_most_group to represent a (growing) set of SAT variables of which at most n may be true (e.g. for conflict classes with n=1 or in the future for minimizing avoid-version).

Currently we don't make use of the fact that those groups may grow as every constraint is preloaded ahead of time (so we only seal those groups once before the SAT solver starts, just like before). With on-demand parsing of opam files however, we'll have to handle the incremental discovery of additional elements bounded by these at-most-size groups.

Growing a group incrementally is possible (e.g. from [y;z] to [x;y;z]) because the new constraint at_most n [x;y;z] is strictly stronger than the previous one at_most n [y;z] (we could even get rid of the old clause, but currently this removal operation is not available nor critical for performances).

It's possible to merge this PR before or after the incremental SAT clauses (#16303), although it's not that useful atm (it's just easier to review as an independent refactoring).

[Alizter]

No behaviour changes from what I can tell.