Distinguish Definitions from Usages in Variable Resolver

[rcosta358]

Description

This PR fixes a problem in the simplification where value propagation could be skipped for expressions like x == 1 && x == 2. The resolver treated any equality involving x and a literal as the definition of x, even when only one of those equalities was the actual definition being propagated.

Now the resolver tracks the value that defined the substitution and uses it to distinguish the defining equality from later usages. For a direct contradiction like x == 1 && x == 2, either value can be picked for propagation: both expose the contradiction and fold to false.

Example

Before

mode⁷⁰ == 1 &&
(mode⁷⁰ == 2 ? compressionExplicit(param⁷¹) : startCompression(param⁷¹)) &&
state1(param⁷¹) == state1(param⁶⁹) &&
startTiling(param⁶⁹) &&
startCompression(param⁶⁹)

After

startCompression(param⁷¹) &&
state1(param⁷¹) == state1(param⁶⁹) &&
startTiling(param⁶⁹) &&
startCompression(param⁶⁹)

Related Issue

None.

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added/updated tests in ExpressionSimplifierTest and VariableResolverTest
• mvn test passes locally
• Updated docs/README if behavior or API changed

[CatarinaGamboa]

Awesome! We still need something similar now to deal with final fields/enums right?

[rcosta358]

Yeah we need to handle enums in the simplification process.
Will do it in a separate PR.