TD3: non-incremental reluctant destabilization at all variables

[sim642]

This is an attempt (or two) to generalize the reluctant function return node destabilization during incremental loading to general use in TD3. This was discussed briefly during GobCon, but the draft PR is here to demonstrate exactly what was tried and where it mysteriously fails.

In the simplest (uncommented) form, this is as simple as replacing the recursive destabilize x call with solve x Widen. If the value changes, solve will do the recursive destabilize call. If it doesn't change, it won't.

This almost works on our regression suite:

• 01/37 div is unknown at an assertion.
• 22/13 was_problematic_3, 24/05 previously_problematic_c, 24/08 previously_problematic_f, 24/10 previously_problematic_h time out in 10s.

Our belief is that this is somehow due to the multiple recursive solves potentially "intersecting": side effects in solving of one destabilize and thus attempt to resolve a part of another, which then would also be destabilized and resolved differently from the direct solve call from destabilize. But this is just a hypothesis.

---

There is a commented out attempt to hopefully bypass the issue by destabilizing everything normally until certain cutoff nodes (function return nodes in this case) and then call solve only on those afterwards. But the same sort of problem can still occur between functions via side effects.

TODO

• Figure out what exactly goes wrong with the 5 regression tests.
• Come up with a solution that works?

[jerhard]

Helmut and I were discussing just now. He thought that there might be a problem with destabilize leading to calls to solve for the same unknown, if the unknown depends on itself.
His idea was to add x to the called set again before calling destabilize x, and removing it after that again.

[jerhard]

@sim642 @vesalvojdani
Did you benchmark this?

[sim642]

I think we never did because we didn't even get it to pass our tests properly, so performance wasn't the primary concern. And we haven't looked at this for a while since it's not part of #391.

[jerhard]

His idea was to add x to the called set again before calling destabilize x, and removing it after that again.

We tried this, and it fixes the termination issues, but this leads to all nodes in loops to become widening points, severely worsening the precision. An idea might be to have a separate de_called set for the destabilize; solve would then also check whether something is in de_called. But then again it's not so clear to us whether that would terminate.

[jerhard]

His idea was to add x to the called set again before calling destabilize x, and removing it after that again.

We tried this, and it fixes the termination issues, but this leads to all nodes in loops to become widening points, severely worsening the precision. An idea might be to have a separate de_called set for the destabilize; solve would then also check whether something is in de_called. But then again it's not so clear to us whether that would terminate.

I tried this now, but this does not fix the termination issues on e.g. 09/15. Unless one adds points that are in de_called and encountered in eval to the wpoint, which would defeat the purpose of having these separate sets.

[michael-schwarz]

What do we want to do with this? Any interest in fixing it up and merging or should we close this issue?

[sim642]

What do we want to do with this? Any interest in fixing it up and merging or should we close this issue?

I think there was no clear way to make this work because it drastically changes the dynamics of the solver, especially w.r.t. side effects. So I'll just close it.