Add VC Arithmetic Simplification

[rcosta358]

Description

This PR adds VC simplification for arithmetic identity expressions through VCImplication chains for when operands are not constants. When a refinement contains simplifiable arithmetic such as neutral elements, zero multiplication, double negation, negated operands, or guarded division/modulo identities, it simplifies the VC node while preserving its origin and the rest of the VC chain.

This new simplification pass is done after substitution and folding, with the following simplifications:

• x + 0 → x
• 0 + x → x
• x - 0 → x
• 0 - x → -x
• x + (-x) → 0
• (-x) + x → 0
• x - x → 0
• -(-x) → x
• x + (-y) → x - y
• x - (-y) → x + y
• x * 1 → x
• 1 * x → x
• x * 0 → 0
• 0 * x → 0
• x / 1 → x
• 0 / x → 0 (if x != 0)
• x / x → 1 (if x != 0)
• x % 1 → 0
• x % x → 0 (if x != 0)

Example

x * 1 > 0

is simplified to

x > 0

with origin x * 1 > 0

Related Issue

None.

Type of change

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

Checklist

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

[CatarinaGamboa]

lgtm