Add VC Constraint Simplification

[rcosta358]

Description

This PR adds VC simplification for redundant antecedent constraints in a VCImplication chain. For any two antecedents, excluding the conclusion, if one constraint implies another, the weaker constraint is redundant.
The weaker antecedent node is removed when its binder is not used by the remaining VC.

Examples

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

is simplified to

∀x:int. x > 1 =>
∀#ret:int. #ret == x

∀x:int. x >= 0 =>
∀#fresh_1:boolean. !(x < 1) =>
∀#fresh_2:boolean. !(x < 2) =>
∀#fresh_3:boolean. !(x < 3) =>
x == 4

is simplified (in two passes) to 

∀x:int. x >= 0 =>
∀#fresh_3:boolean. !(x < 3) =>
x == 4

Related Issue

None.

Type of change

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

Checklist

• Added/updated tests
• ./mvnw -pl liquidjava-verifier 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.

[CatarinaGamboa]

You have branch conflicts. I'm still not super sure about this simplification cause the intermediate step has a meaning right that os not really accurate. Couldnt we simply mark this for removal instead of overwriting the refinement so we still remove it next turn but don't make the substitution

[rcosta358]

Agreed. I changed it so we remove the binders immediately instead of replacing their refinements with true.

[CatarinaGamboa]

Discussed offline. This is great simplification, just add the example to reduce the freshes into just one