Fix Usage Detection for Repeated Equalities

CONTRIBUTING.md

@@ -7,27 +7,40 @@ Thanks for your interest in contributing! This guide covers the essentials.
 - Java 20+
 - Maven 3.6+
 
-## Build & test
+## Build and Run
+
+To build the project, run:
 
 ```bash
-mvn clean install   # build everything
-mvn test            # run the test suite
+mvn clean install
 ```
 
-Run a single test:
+Code formatting runs automatically via `formatter-maven-plugin` during the `validate` phase.
+
+To verify a single file from the CLI, run:
 
 ```bash
-mvn -pl liquidjava-verifier -Dtest=TestExamples#testMultiplePaths test
+./liquidjava path/to/File.java
 ```
 
-Verify a single file from the CLI:
+This script recompiles `liquidjava-api` and `liquidjava-verifier` when local sources or Maven files have changed.
+
+## Testing
+
+To run all tests, run:
 
 ```bash
-./liquidjava path/to/File.java
+mvn test
 ```
 
-The launcher recompiles `liquidjava-api` and `liquidjava-verifier` only when local sources or Maven files have changed.
-Code formatting runs automatically via `formatter-maven-plugin` during the `validate` phase.
+To run specific tests, run:
+
+```bash
+mvn -pl liquidjava-verifier -Dtest=ExpressionFormatterTest test
+mvn -pl liquidjava-verifier -Dtest=ExpressionSimplifierTest test
+mvn -pl liquidjava-verifier -Dtest=RefinementsParserTest test
+mvn -pl liquidjava-verifier -Dtest=VariableResolverTest test
+```
 
 ## Release
 

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

@@ -27,7 +27,7 @@ public static Map<String, Expression> resolve(Expression exp) {
         resolveRecursive(exp, map);
 
         // remove variables that were not used in the expression
-        map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue()));
+        map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue(), true));
 
         // transitively resolve variables
         return resolveTransitive(map);
@@ -136,43 +136,35 @@ private static Expression lookup(Expression exp, Map<String, Expression> map, Se
      *
      * @param exp
      * @param name
+     * @param value
+     * @param topLevel
      *
      * @return true if used, false otherwise
      */
-    private static boolean hasUsage(Expression exp, String name, Expression value) {
-        // exclude own definitions
-        if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
+    private static boolean hasUsage(Expression exp, String name, Expression value, boolean topLevel) {
+        if (topLevel && exp instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) {
+            return hasUsage(binary.getFirstOperand(), name, value, true)
+                    || hasUsage(binary.getSecondOperand(), name, value, true);
+        }
+
+        if (topLevel && exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
             Expression left = binary.getFirstOperand();
             Expression right = binary.getSecondOperand();
-            if (left instanceof Var v && v.getName().equals(name) && right.equals(value)
-                    && (isConstant(right) || (!(right instanceof Var) && canSubstitute(v, right))))
-                return false;
-            if (left instanceof FunctionInvocation && left.toString().equals(name) && right.equals(value)
-                    && (isConstant(right) || (!(right instanceof Var) && !containsExpression(right, left))))
-                return false;
-            if (right instanceof Var v && v.getName().equals(name) && left.equals(value) && isConstant(left))
-                return false;
-            if (right instanceof FunctionInvocation && right.toString().equals(name) && left.equals(value)
-                    && isConstant(left))
+            boolean leftDefinition = name.equals(substitutionKey(left)) && right.equals(value)
+                    && (isConstant(right)
+                            || (left instanceof Var v && !(right instanceof Var) && canSubstitute(v, right))
+                            || (left instanceof FunctionInvocation && !(right instanceof Var)
+                                    && !containsExpression(right, left)));
+            boolean rightDefinition = name.equals(substitutionKey(right)) && left.equals(value) && isConstant(left);
+            if (leftDefinition || rightDefinition)
                 return false;
         }
 
-        // usage found
-        if (exp instanceof Var var && var.getName().equals(name)) {
-            return true;
-        }
-        if (exp instanceof FunctionInvocation && exp.toString().equals(name)) {
+        if (name.equals(substitutionKey(exp)))
             return true;
-        }
-
-        // recurse children
-        if (exp.hasChildren()) {
-            for (Expression child : exp.getChildren())
-                if (hasUsage(child, name, value))
-                    return true;
-        }
-
-        // usage not found
+        for (Expression child : exp.getChildren())
+            if (hasUsage(child, name, value, false))
+                return true;
         return false;
     }
 

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

@@ -658,4 +658,53 @@ void testEnumConstantsPropagateIntoTernaryCondition() {
 
         assertEquals("start(param)", result.getValue().toString());
     }
+
+    @Test
+    void testRepeatedEqualDefinitionPropagatesIntoTernaryCondition() {
+        Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expression);
+
+        assertEquals("explicit(param)", result.getValue().toString());
+    }
+
+    @Test
+    void testRepeatedEqualDefinitionsPropagateIntoCompoundTernaryCondition() {
+        Expression expression = parse(
+                "mode == 2 && other == 5 && ((mode == 2 && other == 5) ? explicit(param) : start(param))");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expression);
+
+        assertEquals("explicit(param)", result.getValue().toString());
+    }
+
+    @Test
+    void testRepeatedEqualDefinitionPropagatesWhenUsageComesFirst() {
+        Expression expression = parse("(mode == 2 ? explicit(param) : start(param)) && mode == 2");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expression);
+
+        assertEquals("explicit(param)", result.getValue().toString());
+    }
+
+    @Test
+    void testRepeatedFunctionInvocationDefinitionPropagatesIntoTernaryCondition() {
+        Expression expression = parse("modeOf(param) == 2 && (modeOf(param) == 2 ? explicit(param) : start(param))");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expression);
+
+        assertEquals("explicit(param)", result.getValue().toString());
+    }
+
+    @Test
+    void testRepeatedEqualDefinitionsPropagateIntoNestedTernaryConditions() {
+        Expression expression = parse("mode == 2 && other == 3 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expression);
+
+        assertEquals("a(p)", result.getValue().toString());
+    }
+
+    @Test
+    void testRepeatedEqualDefinitionsPropagateIntoNestedTernaryElseBranch() {
+        Expression expression = parse("mode == 2 && other == 4 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expression);
+
+        assertEquals("b(p)", result.getValue().toString());
+    }
 }

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

@@ -99,6 +99,61 @@ void testDifferentEqualityInIteConditionCountsAsUsage() {
         assertEquals("1", result.get("mode").toString());
     }
 
+    @Test
+    void testRepeatedEqualDefinitionCountsAsUsage() {
+        Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Repeated equalities should keep one definition and treat the other as usage");
+        assertEquals("2", result.get("mode").toString());
+    }
+
+    @Test
+    void testRepeatedEqualDefinitionsInCompoundIteConditionCountAsUsage() {
+        Expression expression = parse(
+                "mode == 2 && other == 5 && ((mode == 2 && other == 5) ? explicit(param) : start(param))");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(2, result.size(), "Compound ternary condition should count as a use of both variables");
+        assertEquals("2", result.get("mode").toString());
+        assertEquals("5", result.get("other").toString());
+    }
+
+    @Test
+    void testRepeatedEqualDefinitionCountsAsUsageBeforeDefinitionConjunct() {
+        Expression expression = parse("(mode == 2 ? explicit(param) : start(param)) && mode == 2");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Conjunct order should not affect repeated equality usage detection");
+        assertEquals("2", result.get("mode").toString());
+    }
+
+    @Test
+    void testRepeatedFunctionInvocationDefinitionCountsAsUsage() {
+        Expression expression = parse("modeOf(param) == 2 && (modeOf(param) == 2 ? explicit(param) : start(param))");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Function invocation definition should count repeated nested equality as usage");
+        assertEquals("2", result.get("modeOf(param)").toString());
+    }
+
+    @Test
+    void testRepeatedExpressionDefinitionCountsAsUsage() {
+        Expression expression = parse("limit == max - 1 && (limit == max - 1 ? a(p) : b(p))");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Expression definition should count repeated nested equality as usage");
+        assertEquals("max - 1", result.get("limit").toString());
+    }
+
+    @Test
+    void testRepeatedTopLevelDefinitionsOnlyDoNotCountAsUsage() {
+        Expression expression = parse("mode == 2 && mode == 2");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertTrue(result.isEmpty(), "Repeated top-level definitions alone should not count as usage");
+    }
+
     @Test
     void testReturnVariableIsNotSubstituted() {
         Expression expression = parse("x > 0 && #ret_1 == x");