ExprOptimizer: Rewrite S \in SUBSET T when it occurs in subexpressions

[lemmy]

----- MODULE ljasf -----
EXTENDS Integers

VARIABLE
    \* @type: { v: Set( { p: Set( { v: Set(Int) } ) } ) };
    m

TypeOK ==
        m \in [ v : SUBSET [ p : SUBSET [ v: SUBSET {1,2,3,4,5}] ] ]

Init ==
    m = [ v |-> {[p |-> {[v |-> {1}]} ]} ]

Next ==
    UNCHANGED m
====

input:
m["v"] ∈ SUBSET ({["p" ↦ t_5$1] : t_5$1 ∈ SUBSET ({["v" ↦ t_4$1] : t_4$1 ∈ SUBSET {1, 2, 3, 4, 5}})})

old output:
∀t_a ∈ m["v"]: ((DOMAIN t_a = {"p"}) ∧ (∀t_b ∈ t_a["p"]: ((DOMAIN t_b = {"v"}) ∧ t_b["v"] ∈ SUBSET {1, 2, 3, 4, 5})))

new output:
∀t_a ∈ m["v"]: ((DOMAIN t_a = {"p"}) ∧ (∀t_b ∈ t_a["p"]: ((DOMAIN t_b = {"v"}) ∧ (∀t_c ∈ t_b["v"]: t_c ∈ {1, 2, 3, 4, 5}))))

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality (nothing to document)
• [Entries added to ./unreleased/][changelog format] for any new functionality

[lemmy]

@konnov This is a follow-up of #2946.

Just a heads-up: GitHub automatically assigns Kukovec as the PR reviewer for me every time. I'm not sure if that's intentional.

[konnov]

This makes sense to me. Thanks for fixing this issue!

[lemmy]

Thanks for merging.