[Improvement]: Reduce the search space for listInhabited with large number of negative atoms

[heshanpadmasiri]

Description

Current implementation of the the listInhabited function (based on the solution to Ex6 to Castagna's paper), is constant in terms of the number of positive atoms (since we take the intersection) but super liner in terms of the negative atoms. Note in the worst case we are creating a search tree with potentially as many children as the fixed size of each negative atom (ref)

Describe your problem(s)

No response

Describe your solution(s)

In most cases this is not an issue since Ballerina don't have the difference operator to the user. But in extreme cases such as some caused by type narrowing in nBallerina we can get over 20 negative atoms ballooning the compile to hours. Two avoid Castagna points to two optimizations in Frisch's thesis section 7.3.1

1. Reorder the negative atoms such that "larger" atoms are checked first. (I couldn't find a place where a heuristic for determining the size of an atom is defined in the paper.). Idea is this should potentially allow us the prune away larger sub-trees earlier
2. Exploit the repeated sub problems (if we prove A\B is empty then A\B\C is going to be empty). I think we can do this very easily since we cache all the complicated emptiness checks.

Also note mappingInhabited also has the same problem and we many need to address it there as well

Related area

-> Compilation

Related issue(s) (optional)

No response

Suggested label(s) (optional)

No response

Suggested assignee(s) (optional)

No response

[lochana-chathura]

Closed in #42774