Skip to content

Commit 11be88b

Browse files
rcosta358rcosta358
committed
Simplify VCFolding
1 parent eab59f7 commit 11be88b

2 files changed

Lines changed: 55 additions & 50 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java‎

Lines changed: 27 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -18,22 +18,17 @@
1818
*/
1919
public class VCFolding {
2020

21-
/**
22-
* A folded expression and whether the fold changed the original expression
23-
*/
24-
private record Folding(Expression folded, boolean changed) {
25-
}
26-
2721
/**
2822
* Applies folding to the first foldable predicate in a VC chain
2923
*/
3024
public static VCImplication apply(VCImplication implication) {
3125
if (implication == null)
3226
return null;
3327

34-
Folding folding = fold(implication.getRefinement().getExpression());
35-
if (folding.changed()) {
36-
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folding.folded()),
28+
Expression expression = implication.getRefinement().getExpression();
29+
Expression folded = fold(expression);
30+
if (!expression.equals(folded)) {
31+
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folded),
3732
implication.getOrigin());
3833
result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
3934
return result;
@@ -51,92 +46,74 @@ public static VCImplication apply(VCImplication implication) {
5146
/**
5247
* Folds an expression
5348
*/
54-
private static Folding fold(Expression expression) {
49+
private static Expression fold(Expression expression) {
5550
if (expression instanceof BinaryExpression binary)
5651
return foldBinary(binary);
5752
if (expression instanceof UnaryExpression unary)
5853
return foldUnary(unary);
5954
if (expression instanceof Ite ite)
6055
return foldIte(ite);
61-
if (expression instanceof GroupExpression group && group.getChildren().size() == 1) {
62-
Folding child = fold(group.getExpression());
63-
return new Folding(child.folded(), true);
64-
}
65-
return new Folding(expression.clone(), false);
56+
if (expression instanceof GroupExpression group && group.getChildren().size() == 1)
57+
return fold(group.getExpression());
58+
return expression.clone();
6659
}
6760

6861
/**
6962
* Folds a binary expression and its operands
7063
*/
71-
private static Folding foldBinary(BinaryExpression binary) {
72-
Folding leftFolded = fold(binary.getFirstOperand());
73-
Folding rightFolded = fold(binary.getSecondOperand());
74-
75-
Expression leftExpression = leftFolded.folded();
76-
Expression rightExpression = rightFolded.folded();
64+
private static Expression foldBinary(BinaryExpression binary) {
65+
Expression leftExpression = fold(binary.getFirstOperand());
66+
Expression rightExpression = fold(binary.getSecondOperand());
7767
Expression left = resolvedLiteral(leftExpression);
7868
Expression right = resolvedLiteral(rightExpression);
79-
boolean childChanged = leftFolded.changed() || rightFolded.changed() || left != leftExpression
80-
|| right != rightExpression;
8169
String op = binary.getOperator();
8270

8371
Expression foldedBinary = foldLiteralBinary(left, right, op);
8472
if (foldedBinary != null)
85-
return new Folding(foldedBinary, true);
73+
return foldedBinary;
8674

8775
Expression foldedAdjacentInts = foldAdjacentInts(left, right, op);
8876
if (foldedAdjacentInts != null)
89-
return new Folding(foldedAdjacentInts, true);
77+
return foldedAdjacentInts;
9078

91-
if (childChanged)
92-
return new Folding(new BinaryExpression(left, op, right), true);
93-
return new Folding(binary.clone(), false);
79+
return new BinaryExpression(left, op, right);
9480
}
9581

9682
/**
9783
* Folds a unary expression and its operand
9884
*/
99-
private static Folding foldUnary(UnaryExpression unary) {
100-
Folding operandFolded = fold(unary.getExpression());
101-
Expression operand = operandFolded.folded();
85+
private static Expression foldUnary(UnaryExpression unary) {
86+
Expression operand = fold(unary.getExpression());
10287
String op = unary.getOp();
10388

10489
if ("!".equals(op) && operand instanceof LiteralBoolean literal)
105-
return new Folding(new LiteralBoolean(!literal.isBooleanTrue()), true);
90+
return new LiteralBoolean(!literal.isBooleanTrue());
10691

10792
if ("-".equals(op)) {
10893
if (operand instanceof LiteralInt literal)
109-
return new Folding(new LiteralInt(-literal.getValue()), true);
94+
return new LiteralInt(-literal.getValue());
11095
if (operand instanceof LiteralReal literal)
111-
return new Folding(new LiteralReal(-literal.getValue()), true);
96+
return new LiteralReal(-literal.getValue());
11297
}
11398

114-
if (operandFolded.changed())
115-
return new Folding(new UnaryExpression(op, operand), true);
116-
return new Folding(unary.clone(), false);
99+
return new UnaryExpression(op, operand);
117100
}
118101

119102
/**
120103
* Folds a conditional expression and its branches
121104
*/
122-
private static Folding foldIte(Ite ite) {
123-
Folding conditionFolded = fold(ite.getCondition());
124-
Folding thenFolded = fold(ite.getThen());
125-
Folding elseFolded = fold(ite.getElse());
126-
127-
Expression condition = conditionFolded.folded();
128-
Expression thenExpression = thenFolded.folded();
129-
Expression elseExpression = elseFolded.folded();
105+
private static Expression foldIte(Ite ite) {
106+
Expression condition = fold(ite.getCondition());
107+
Expression thenExpression = fold(ite.getThen());
108+
Expression elseExpression = fold(ite.getElse());
130109

131110
if (condition instanceof LiteralBoolean literal)
132-
return new Folding(literal.isBooleanTrue() ? thenExpression : elseExpression, true);
111+
return literal.isBooleanTrue() ? thenExpression : elseExpression;
133112

134113
if (thenExpression.equals(elseExpression))
135-
return new Folding(thenExpression, true);
114+
return thenExpression;
136115

137-
if (conditionFolded.changed() || thenFolded.changed() || elseFolded.changed())
138-
return new Folding(new Ite(condition, thenExpression, elseExpression), true);
139-
return new Folding(ite.clone(), false);
116+
return new Ite(condition, thenExpression, elseExpression);
140117
}
141118

142119
/**

‎liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,19 @@
22

33
import static liquidjava.utils.VCTestUtils.assertSimplifiedVC;
44
import static liquidjava.utils.VCTestUtils.assertVC;
5+
import static liquidjava.utils.VCTestUtils.parse;
56
import static liquidjava.utils.VCTestUtils.simplified;
67
import static liquidjava.utils.VCTestUtils.vc;
8+
import static org.junit.jupiter.api.Assertions.assertEquals;
9+
import static org.junit.jupiter.api.Assertions.assertInstanceOf;
710
import static org.junit.jupiter.api.Assertions.assertNull;
811

12+
import liquidjava.processor.SimplifiedVCImplication;
913
import liquidjava.processor.VCImplication;
1014
import liquidjava.rj_language.Predicate;
1115
import liquidjava.rj_language.ast.BinaryExpression;
1216
import liquidjava.rj_language.ast.Enum;
17+
import liquidjava.rj_language.ast.GroupExpression;
1318
import liquidjava.rj_language.ast.LiteralInt;
1419
import org.junit.jupiter.api.Test;
1520

@@ -93,6 +98,29 @@ void preservesOriginFromExistingSimplifiedImplication() {
9398
assertSimplifiedVC(result, simplified("true", "∀x:int. x + 1 + 2 > 0"));
9499
}
95100

101+
@Test
102+
void recordsOriginWhenOnlyGroupIsUnwrapped() {
103+
VCImplication implication = new VCImplication(new Predicate(new GroupExpression(parse("x > 0"))));
104+
105+
VCImplication result = VCFolding.apply(implication);
106+
107+
SimplifiedVCImplication simplified = assertInstanceOf(SimplifiedVCImplication.class, result);
108+
assertEquals("x > 0", simplified.getRefinement().toString());
109+
assertInstanceOf(GroupExpression.class, simplified.getOrigin().getRefinement().getExpression());
110+
}
111+
112+
@Test
113+
void recordsOriginWhenFoldingLaterImplication() {
114+
VCImplication implication = vc("x > 0", "1 + 2 > 0");
115+
116+
VCImplication result = VCFolding.apply(implication);
117+
118+
assertEquals("x > 0", result.getRefinement().toString());
119+
SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
120+
assertEquals("true", simplifiedNext.getRefinement().toString());
121+
assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString());
122+
}
123+
96124
private static void assertFolded(String original, String folded) {
97125
VCImplication result = VCFolding.apply(vc(original));
98126

0 commit comments

Comments
 (0)