Add VC Logical Simplification

[rcosta358]

Description

This PR adds VC logical simplification through VCImplication chains. When a refinement contains foldable logical identities, it simplifies the VC node while preserving its origin and the rest of the VC chain.

It supports the following simplifications:

• x && true → x
• x && false → false
• x || true → true
• x || false → x
• !!x → x
• p && p → p
• p || p → p
• x == x → true
• x != x → false
• x --> true → true
• false --> x → true
• true --> x → x
• x --> x → true

Example

x && true

is simplified to

x

with origin x && true

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