Skip to content

Commit f5aaf6f

Browse files
committed
Track Simplification Pass Names
1 parent c643a39 commit f5aaf6f

3 files changed

Lines changed: 21 additions & 4 deletions

File tree

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,6 @@ public static VCSimplificationResult simplifyOnce(VCSimplificationResult implica
5050
VCImplication simplified = pass.apply(implication.getImplication());
5151
if (implication.getImplication().equals(simplified))
5252
return implication;
53-
return new VCSimplificationResult(simplified, implication);
53+
return new VCSimplificationResult(simplified, implication, pass.getName());
5454
}
5555
}

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationPass.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,10 @@
77
*/
88
public interface VCSimplificationPass {
99
VCImplication apply(VCImplication implication);
10+
11+
default String getName() {
12+
String className = getClass().getSimpleName();
13+
String name = className.startsWith("VC") ? className.substring(2) : className;
14+
return name.replaceAll("(?<=[a-z0-9])(?=[A-Z])", " ");
15+
}
1016
}

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,18 @@ public final class VCSimplificationResult {
1111

1212
private final VCImplication implication;
1313
private final VCSimplificationResult origin;
14+
private final String simplification;
1415

1516
public VCSimplificationResult(VCImplication implication) {
16-
this(implication, null);
17+
this.implication = Objects.requireNonNull(implication).clone();
18+
this.origin = null;
19+
this.simplification = null;
1720
}
1821

19-
public VCSimplificationResult(VCImplication implication, VCSimplificationResult origin) {
22+
public VCSimplificationResult(VCImplication implication, VCSimplificationResult origin, String simplification) {
2023
this.implication = Objects.requireNonNull(implication).clone();
21-
this.origin = origin;
24+
this.origin = Objects.requireNonNull(origin);
25+
this.simplification = Objects.requireNonNull(simplification);
2226
}
2327

2428
/**
@@ -35,6 +39,13 @@ public VCSimplificationResult getOrigin() {
3539
return origin;
3640
}
3741

42+
/**
43+
* Returns the name of the simplification pass that produced this result or null for the original VC chain
44+
*/
45+
public String getSimplification() {
46+
return simplification;
47+
}
48+
3849
@Override
3950
public String toString() {
4051
if (origin == null)

0 commit comments

Comments
 (0)