Fix Usage Detection for Repeated Equalities

[rcosta358]

Description

This PR fixes the VariableResolver.hasUsage so a matching equality is only excluded as a definition when it appears in a definition under a conjunction. This means that repeated equalities inside nested expressions now count as usages, allowing substitutions to propagate and simplify correctly.

Example

Before

Both x == 1 count has definitions.

x == 1 && (x == 1 ? a(y) : b(y)) // most simplified

After

The first one counts has a definition and the second one counts as an usage.

a(y) // most simplified

Related Issue

None.

Type of change

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

Checklist

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

[CatarinaGamboa]

what do you mean by "a matching equality is only excluded as a definition when it appears in a definition under a conjunction"?
It could be the opposite right (x == 1 ? a(y) : b(y)) && x == 1 and it should still simplify
I'm not sure i get the idea

[rcosta358]

Those two expressions are equivalent. It's not about the order of the conjunctions, it's about whether the equality appears as a top level conjunct or nested inside another expression.

In both examples, the outer x == 1 treated as the definition, while the x == 1 within the ite is treated as a usage.
In the previous logic both equalities would count as definitions, so x had no usages and the substitution mapping was removed.

[CatarinaGamboa]

Can we add a couple more tests to ensure similar but more complex expressions are working?
Maybe like:
mode == 2 && other == 5 && ((mode == 2 && other == 5) ? explicit(param) : start(param)) -> explicit(param)
or
"mode == 2 && other == 3 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))" -> a(p)