No shortcut for narrow and meet in HConsed when int refinement is active

[michael-schwarz]

As @sim642 noted in #1005, int domain refinement (which we do not only after transformers, but also after meet and narrow), breaks the assumption that x op x =x for narrow and meet.

This disables the shortcut in HConsed for narrow and meet whenever an int refinement is active, and its precondition is not met. It should not be too expensive, as a local boolean to cache this information is introduced.

Closes #1005.

(#1005 also mentions a different but related issue that refinement could be applied more often still, but I think this we can save for a separate PR, this PR fixes the immediate issue and makes refinement usable together with hash consing).

[sim642]

This essentially just ignores the issue in the int domains (specifically the reduced product of them) instead of fixing it. I don't think this is the right solution because it still violates the narrowing property $a \sqcap b \sqsubseteq a \mathbin{\Delta} b \sqsubseteq a$. If $a = b$, then this reduces to $a \sqsubseteq a \mathbin{\Delta} a \sqsubseteq a$, which implies $a \mathbin{\Delta} a = a$. The TD3 paper makes this assumption, so we can't just gloss over this.

Before this, HConsed presented to TD3 a narrowing which obeys this property. It only failed the additional verification for suddenly becoming more precise. After this, the narrow presented to TD3 fails this property, so TD3 might no longer behave as it's supposed to.

What it essentially means is that a stable sequence might become unstable out of nowhere, instead of remaining ultimately stable. Therefore, the TD3 termination proof falls apart.

[michael-schwarz]

Ok, we can argue that this should not close the issue then, and the issue should be renamed ("invalid narrowing in the presence of refinement" or something).

However, I still think it is an improvement: The main thing this currently does is make the behavior consistent between having hash-consing on or off. Hash-consing should be a performance optimization only, there should not be any difference observable between the case where it is enabled or disabled. This conflates issues unnecessarily.

The point where your concern applies is immediately when we define the meet and narrow to refine, violating the properties you described above. Hashconsing accidentally fixing that again is not really the way to go.

Edit: Might also be interesting to see to what extent it is relevant that the concretizations remain the same in both cases.

[michael-schwarz]

Relevant paper by Cortesi: https://www.dsi.unive.it/~cortesi/paperi/CL_2011.pdf

[sim642]

Actually, narrow not being idempotent might not be a problem for termination in practice. It might be in the proof but in practice we don't check if the sequence is ultimately stable. We only check if it's stable for one iteration and end narrowing there. Unlike widening, it's perfectly fine to end narrowing at any point. It doesn't even have to reach one step stability. We can just get a less precise result maybe.

That narrowing property is just what implies that one step stability means ultimate stability.

[michael-schwarz]

Merging this as per discussion at the GobCon yesterday.

[sim642]

It should not be too expensive, as a local boolean to cache this information is introduced.

This is immediately evaluated though, not a ResettableLazy/ref. A properly dynamic value already exists as IntDomain.get_refinement, so we should just reuse that.

[michael-schwarz]

This module is constructed dynamically though, so it is not really a problem here.