Make weak table more deterministic

[bclement-ocp]

Alt-ergo uses a weak hash table to store all the expressions that are created for hash consing.

Unfortunately, this means that the behavior of alt-ergo depends on the behavior of OCaml's GC: if we create term T, then forget about it, and later re-create it, the newly created term will have a different ID depending on whether the GC has run in between.

This manifests as strange bugs where simple code changes can cause issues on problems that are apparently unrelated, because they change the moment where a GC is made.

One suggestion to solve the issue is to keep all the terms in a separate array (with strong refs!), and regularly (e.g. when the number of live terms is "big enough" for some definition of "big enough" that must not be a constant value), clear the array, manually trigger a Gc.full_major () that collects all dead terms, and re-build the arrays with the remaining keys in the weak table.

This means we won't keep terms alive for longer than they need to (or at least, not too much longer), but at least we are in full control of when we allow the GC to collect the terms, and consequently we Alt-Ergo's behavior no longer depends on the GC behavior.

I tried to "deterministically reproduce the non-determinism" by forcing Gc.full_major () often (i.e. every term creation or every 10s of term creation), in the hope that it changes things up, but all I was able to do was make Alt-Ergo slow as mollasses. I plan on implementing the suggestion described above.