Add VC Constraint Simplification

[rcosta358]

Description

This PR adds VC simplification for antecedent constraints implied by stronger later antecedents in a VCImplication chain, replacing redundant binder constraints with true.

Example

∀x:int. x > 0 =>
∀#fresh:boolean. x > 1 =>
∀#ret:int. #ret == x

is simplified to

∀x:int. true =>
∀#fresh:boolean. x > 1 =>
∀#ret:int. #ret == x

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]

Why substitute by "true"? I don't think this is a good idea cause true is usually "we don't know anything about this", so I would say either remove it completely or leave the "x > 0".
This might also bring a question of how we should present the path variables (freshed from ifs) cause this only makes sense because we know that that is true right? But how we write it seems it is just another variable

[rcosta358]

We substitute by true and then it is removed in the next pass by the binder simplification.
I see this as "this information is not needed" rather than "we don't know anything about this".

Removing it right away is possible, but it would basically repeat the same logic from the VCBinderSimplification. That's why I decided to leave that to that pass.