Add VC Folding Simplification

[rcosta358]

Description

This PR adds VC simplification for foldable expressions through VCImplication chains. When a refinement contains constant arithmetic, boolean expressions, conditionals, adjacent integer constants, or resolved enum literals, it folds the VC node while preserving its origin and the rest of the VC chain.

It also adds focused unit tests for both the VC folding alone and the VC simplification with both the substitution and folding.

Example

1 + 2 > 0

is simplified to

3 > 0

with origin 1 + 2 > 0

and then simplified to

true

with origin 3 > 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]

It could be cool to have like implication.fold() and have that method call the VCFolding. In terms of API thats a bit more ergonomic since the user doenst need to know that there is another class resposible for the folding itself

[rcosta358]

Maybe just implication.simplify() to call VCSimplification.simplifyToFixedPoint?

[CatarinaGamboa]

So with this architecture, each VCImplication only has one origin->simplification right?
Its not possible for one VCImplication to formulate 2 "independent" simplifications for different parts of the expression like you had planned before.
Like

           VC: forall x: x == 3 -> forall y: y == 4 -> x < y
            // there are 2 independent simplifcations possible
VC: forall y: y == 4 -> 3 < y      e      forall x: x == 3 -> x < 4
           // but just one outcome for each of the next ones
                             3 < 4
                              true

If you want to keep this structure, I think this architecture does not work 😕
Nevertheless, this current option works for me if you want to leave that for a followup but it might require some more deep changes

[rcosta358]

Yes, you are correct, but I think we should keep this approach because it stays consistent with the VCSubstitution, and even though it can be a bit more verbose than the previous one, each simplification step is atomic and easier to debug.