Enable mutual refinement of integer domains

[hydrogenoxide]

Motivation

The results of different analyses can be used to refine output of each other. E.g., if an interval analysis says an integer variable x is in [4, 6] and a congruence analyisis finds that x has to be congruent to 0 modulo 3, x must be 6.

Steps to fix this issue

Fix #197, [to be filled in]

Team collaborators

@Felihong, @hydrogenoxide, @MartinWehking, @nicokn

[sim642]

Besides the example of congruence domain (which doesn't yet exist) refining interval domain, there's an existing and practically-appearing refinement case with existing domains: enums domain refining interval domain. For example, the enums domain inclusion set {0, 1} should refine the interval [-2147483648,2147483647] to the interval [0, 1].

Right now the (defexc, interval, enums) tuple (Unknown int([0,7]),[0,2147483647],{0, 1}) is more precise (leq) than (Unknown int([0,7]),[-2147483648,2147483647],{0, 1}) even though according to the inclusion sets (which are more precise than the intervals, at least here) they should be equal. The above refinement would refine both intervals to [0, 1], making the tuples equal, as they should be.

[sim642]

Does the enums->interval refinement I mentioned in the above comment now exist or not? The presentation hinted at many directions been implemented and many missing, but could we have an overview somewhere?

[michael-schwarz]

Does the enums->interval refinement I mentioned in the above comment now exist or not?

It does.

The presentation hinted at many directions been implemented and many missing, but could we have an overview somewhere?

This is the current state of which refinements are implemented (solid lines) vs which are not but are at least in principle interesting (dashed lines).

The refinements where exclusion sets get more precise are dangerous, because these will lead to very big exclusion sets if done naively. The refinement of congruences based on inclusion sets is possible, but we did not find an intriguing use case for it, but it can definitely be added.