Skip to content

Commit edc6220

Browse files
rcosta358rcosta358
committed
Fix Variable Resolution & Expression Simplification
- Ignore unused variable equalities in VariableResolver, only extracts the variables actually used in the expression (excluding its own definitions) - Improves ExpressionSimplifier by collapsing duplicate conjuctions (e.g. x && x => x)
1 parent 0ab2f69 commit edc6220

File tree

4 files changed

+144
-37
lines changed

4 files changed

+144
-37
lines changed

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

Lines changed: 25 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -46,23 +46,34 @@ private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node)
4646
DerivationNode origin = node.getOrigin();
4747

4848
// binary expression with &&
49-
if (value instanceof BinaryExpression binExp) {
50-
if ("&&".equals(binExp.getOperator()) && origin instanceof BinaryDerivationNode binOrigin) {
51-
// recursively simplify children
52-
ValDerivationNode leftSimplified = simplifyDerivationTree(binOrigin.getLeft());
53-
ValDerivationNode rightSimplified = simplifyDerivationTree(binOrigin.getRight());
49+
if (value instanceof BinaryExpression binExp && "&&".equals(binExp.getOperator())) {
50+
ValDerivationNode leftSimplified;
51+
ValDerivationNode rightSimplified;
5452

55-
// check if either side is redundant
56-
if (isRedundant(leftSimplified.getValue()))
57-
return rightSimplified;
58-
if (isRedundant(rightSimplified.getValue()))
59-
return leftSimplified;
53+
// simplify children
54+
if (origin instanceof BinaryDerivationNode binOrigin) {
55+
leftSimplified = simplifyDerivationTree(binOrigin.getLeft());
56+
rightSimplified = simplifyDerivationTree(binOrigin.getRight());
57+
} else {
58+
leftSimplified = simplifyDerivationTree(new ValDerivationNode(binExp.getFirstOperand(), null));
59+
rightSimplified = simplifyDerivationTree(new ValDerivationNode(binExp.getSecondOperand(), null));
60+
}
61+
62+
// check if either side is redundant
63+
if (isRedundant(leftSimplified.getValue()))
64+
return rightSimplified;
65+
if (isRedundant(rightSimplified.getValue()))
66+
return leftSimplified;
6067

61-
// return the conjunction with simplified children
62-
Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue());
63-
DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&");
64-
return new ValDerivationNode(newValue, newOrigin);
68+
// check if children are equal (x && x => x)
69+
if (leftSimplified.getValue().toString().equals(rightSimplified.getValue().toString())) {
70+
return leftSimplified;
6571
}
72+
73+
// return the conjunction with simplified children
74+
Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue());
75+
DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&");
76+
return new ValDerivationNode(newValue, newOrigin);
6677
}
6778
// no simplification
6879
return node;

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

Lines changed: 40 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -20,35 +20,17 @@ public class VariableResolver {
2020
*/
2121
public static Map<String, Expression> resolve(Expression exp) {
2222
Map<String, Expression> map = new HashMap<>();
23+
24+
// extract variable equalities recursively
2325
resolveRecursive(exp, map);
2426

25-
// filter out variables that only appear in their own definition
26-
map.entrySet().removeIf(entry -> countOccurrences(exp, entry.getKey()) < 2);
27+
// remove variables that were not used in the expression
28+
map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey()));
2729

30+
// transitively resolve variables
2831
return resolveTransitive(map);
2932
}
3033

31-
/**
32-
* Counts occurrences of a variable in an expression
33-
*
34-
* @param exp
35-
* @param varName
36-
*
37-
* @return number of occurrences
38-
*/
39-
private static int countOccurrences(Expression exp, String varName) {
40-
if (exp instanceof Var var && var.getName().equals(varName)) {
41-
return 1;
42-
}
43-
if (exp instanceof BinaryExpression be) {
44-
return countOccurrences(be.getFirstOperand(), varName) + countOccurrences(be.getSecondOperand(), varName);
45-
}
46-
if (exp.getChildren() != null) {
47-
return exp.getChildren().stream().mapToInt(child -> countOccurrences(child, varName)).sum();
48-
}
49-
return 0;
50-
}
51-
5234
/**
5335
* Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2)
5436
*
@@ -114,4 +96,39 @@ private static Expression lookup(Expression exp, Map<String, Expression> map, Se
11496
seen.add(name);
11597
return lookup(value, map, seen);
11698
}
99+
100+
/**
101+
* Checks if a variable is used in the expression (excluding its own definitions)
102+
*
103+
* @param exp
104+
* @param name
105+
*
106+
* @return true if used, false otherwise
107+
*/
108+
private static boolean hasUsage(Expression exp, String name) {
109+
// exclude own definitions
110+
if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
111+
Expression left = binary.getFirstOperand();
112+
Expression right = binary.getSecondOperand();
113+
if (left instanceof Var v && v.getName().equals(name) && right.isLiteral())
114+
return false;
115+
if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
116+
return false;
117+
}
118+
119+
// usage found
120+
if (exp instanceof Var var && var.getName().equals(name)) {
121+
return true;
122+
}
123+
124+
// recurse children
125+
if (exp.hasChildren()) {
126+
for (Expression child : exp.getChildren())
127+
if (hasUsage(child, name))
128+
return true;
129+
}
130+
131+
// usage not found
132+
return false;
133+
}
117134
}

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

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,11 @@
22

33
import static org.junit.jupiter.api.Assertions.*;
44

5+
import java.util.ArrayList;
6+
57
import liquidjava.rj_language.ast.BinaryExpression;
68
import liquidjava.rj_language.ast.Expression;
9+
import liquidjava.rj_language.ast.FunctionInvocation;
710
import liquidjava.rj_language.ast.LiteralBoolean;
811
import liquidjava.rj_language.ast.LiteralInt;
912
import liquidjava.rj_language.ast.UnaryExpression;
@@ -389,6 +392,60 @@ void testTwoEqualitiesShouldNotSimplify() {
389392
assertEquals("y == 2", resultExpr.getSecondOperand().toString(), "Right operand should be y == 2");
390393
}
391394

395+
@Test
396+
void testSameVarTwiceShouldSimplifyToSingle() {
397+
// Given: x && x
398+
// Expected: x
399+
Expression varX = new Var("x");
400+
Expression fullExpression = new BinaryExpression(varX, "&&", varX);
401+
// When
402+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
403+
// Then
404+
assertNotNull(result, "Result should not be null");
405+
assertEquals("x", result.getValue().toString(),
406+
"Same variable twice should be simplified to a single variable");
407+
}
408+
409+
@Test
410+
void testSameEqualityTwiceShouldSimplifyToSingle() {
411+
// Given: x == 1 && x == 1
412+
// Expected: x == 1
413+
Expression varX = new Var("x");
414+
Expression one = new LiteralInt(1);
415+
Expression xEquals1First = new BinaryExpression(varX, "==", one);
416+
Expression xEquals1Second = new BinaryExpression(varX, "==", one);
417+
Expression fullExpression = new BinaryExpression(xEquals1First, "&&", xEquals1Second);
418+
419+
// When
420+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
421+
422+
// Then
423+
assertNotNull(result, "Result should not be null");
424+
assertEquals("x == 1", result.getValue().toString(),
425+
"Same equality twice should be simplified to a single equality");
426+
}
427+
428+
@Test
429+
void testSameExpressionTwiceShouldSimplifyToSingle() {
430+
// Given: a + b == 1 && a + b == 1
431+
// Expected: a + b == 1
432+
Expression varA = new Var("a");
433+
Expression varB = new Var("b");
434+
Expression sum = new BinaryExpression(varA, "+", varB);
435+
Expression one = new LiteralInt(1);
436+
Expression sumEquals3First = new BinaryExpression(sum, "==", one);
437+
Expression sumEquals3Second = new BinaryExpression(sum, "==", one);
438+
Expression fullExpression = new BinaryExpression(sumEquals3First, "&&", sumEquals3Second);
439+
440+
// When
441+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
442+
443+
// Then
444+
assertNotNull(result, "Result should not be null");
445+
assertEquals("a + b == 1", result.getValue().toString(),
446+
"Same expression twice should be simplified to a single equality");
447+
}
448+
392449
@Test
393450
void testCircularDependencyShouldNotSimplify() {
394451
// Given: x == y && y == x

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

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import liquidjava.rj_language.ast.LiteralInt;
1313
import liquidjava.rj_language.ast.UnaryExpression;
1414
import liquidjava.rj_language.ast.Var;
15+
import org.junit.jupiter.api.TestTemplate;
1516

1617
class VariableResolverTest {
1718

@@ -121,4 +122,25 @@ void testCircularDependency() {
121122
Map<String, Expression> result = VariableResolver.resolve(conjunction);
122123
assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings");
123124
}
125+
126+
@Test
127+
void testUnusedEqualitiesShouldBeIgnored() {
128+
// z > 0 && x == 1 && y == 2 && z == 3
129+
Expression varX = new Var("x");
130+
Expression varY = new Var("y");
131+
Expression varZ = new Var("z");
132+
Expression one = new LiteralInt(1);
133+
Expression two = new LiteralInt(2);
134+
Expression three = new LiteralInt(3);
135+
Expression zero = new LiteralInt(0);
136+
Expression zGreaterZero = new BinaryExpression(varZ, ">", zero);
137+
Expression xEquals1 = new BinaryExpression(varX, "==", one);
138+
Expression yEquals2 = new BinaryExpression(varY, "==", two);
139+
Expression zEquals3 = new BinaryExpression(varZ, "==", three);
140+
Expression conditions = new BinaryExpression(xEquals1, "&&", new BinaryExpression(yEquals2, "&&", zEquals3));
141+
Expression fullExpr = new BinaryExpression(zGreaterZero, "&&", conditions);
142+
Map<String, Expression> result = VariableResolver.resolve(fullExpr);
143+
assertEquals(1, result.size(), "Should only extract used variable z");
144+
assertEquals("3", result.get("z").toString());
145+
}
124146
}

0 commit comments

Comments
 (0)