Basile Clément
Basile Clément
> I will add some documentation to explain what's going on, but at least tests are OK on my machine. You marked this as ready for review but also noted...
> I can't figure out why there is a test not working on the CI that works on my side. I guess this is because the CI is slow, but...
That is an interesting point! Sounds like we indeed need to `push` and `pop` things (which we might have needed for #993 anyways -- at least we won't be able...
> After consideration, it seems my idea doesn't work in some specific cases. Are you talking about the example above with `A1`, `A2`, `A3`? It seems to me that this...
> Really? I thought the function `Satml.pop` restored the previous state of the trail? It does restore the state of the trail prior to the `push`, but prior to the...
Marking as draft for now since, while the diagnosis is correct, I am not sure the fix is the right one.
CI tests took about 2m28s (3m14s with an empty cache) vs 4m30s using setup-ocaml — almost twice faster. macOS still slow as molasses, but we gain a bit as well...
I think that this is because we never call `Uf.make` on unused symbols, and we probably don't want to do that so as to avoid overloading the data structure. Ideally...
Another thing we need to be careful about: currently we create the `Expr.t` only when the symbols are used. Changing it to creating the `Expr.t` at declaration time would have...