Fix VC Function Substitution#267
Conversation
rcosta358
added
bug
bdc9dad to
2d2db90
Compare
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
There was a problem hiding this comment.
I'm fine if this works. Can you add an issue with this situation so that we know we might still need to fix it down the line?
|
Sure. |
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
There was a problem hiding this comment.
Left a couple comments. Also, it feels like we are always using .clone() is it actually needed? Also we might consider just making it immutable if we are always cloning it.
The tests seek okay Im stamping anyway
| * A substitution discovered from a function invocation equality | ||
| */ | ||
| private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement) { | ||
| private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement, |
There was a problem hiding this comment.
This could have better name since it's only for the substitution of function invocations from equalities. Think "how should I read this object". Right now is smt like "substitute at the node the invocation by the replacement because of the sourceEquality" is this the best way to read it? Does it make sense like this? Naming objects, Params, types all have a goal in API design
There was a problem hiding this comment.
The naming could be improved, even though it's a private record only within the class.
And yes, that's basically how it should be read. The sourceEquality is needed to then remove the equality from the VC.
| */ | ||
| private VCImplication removeSourceEquality(VCImplication implication, Expression sourceEquality) { | ||
| List<Expression> remaining = new ArrayList<>(implication.getRefinement().getExpression().getConjuncts()); | ||
| if (!remaining.remove(sourceEquality)) |
There was a problem hiding this comment.
What's does this if mean?
There was a problem hiding this comment.
Seeing it now, I think the if itself is not needed, since the sourceEquality will always be in the list.
| assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1", "f(y) == 1"), | ||
| step("f(x) == 0", "f(y) == 0 + 1", "0 + 1 == 1")); | ||
| assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1", "f(y) == 1"), | ||
| step("0 + 1 == 1")); |
There was a problem hiding this comment.
Why this second step? Shouldn't it be just 1 == 1 ? Probably not related to this change precisely but this step doesnt make much sense to me
There was a problem hiding this comment.
Here we are just testing the VCFunctionSubstitution, not the VCFolding.
4012d7e to
585ba2f
Compare
2 participants
Description
This PR fixes VC function substitution so function equality premises are removed after they are used to rewrite later premises or the conclusion, similarly to normal VC substitution.
Example
Related Issue
None.
Type of change
Checklist
mvn testpasses locally