Add More Tests

Author: rcosta358

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

@@ -115,10 +115,10 @@ private static Map<String, Expression> resolveTransitive(Map<String, Expression>
      * @return resolved expression
      */
     private static Expression lookup(Expression exp, Map<String, Expression> map, Set<String> seen) {
-        if (!(exp instanceof Var))
+        String name = substitutionKey(exp);
+        if (name == null)
             return exp;
 
-        String name = exp.toString();
         if (seen.contains(name))
             return exp; // circular reference
 

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

@@ -1158,4 +1158,38 @@ void testFunctionInvocationEqualitiesPropagateTransitively() {
 
         assertEquals("size(x3) == 0", result.getValue().toString());
     }
+
+    @Test
+    void testFunctionInvocationOnLeftBehavesLikeVariable() {
+        // Given: func(a) == func(b) && func(b) == 1
+        // Expected: func(a) == 1
+        Expression funcA = new FunctionInvocation("func", List.of(new Var("a")));
+        Expression funcB = new FunctionInvocation("func", List.of(new Var("b")));
+        Expression funcAEqualsFuncB = new BinaryExpression(funcA, "==", funcB);
+        Expression funcBEqualsOne = new BinaryExpression(funcB, "==", new LiteralInt(1));
+        Expression fullExpression = new BinaryExpression(funcAEqualsFuncB, "&&", funcBEqualsOne);
+
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        assertEquals("func(a) == 1", result.getValue().toString());
+    }
+
+    @Test
+    void testFunctionInvocationEqualitiesMixWithVariables() {
+        // Given: func(a) + x && func(a) == y && y == 1 && x == 2
+        // Expected: 3
+        Expression funcA = new FunctionInvocation("func", List.of(new Var("a")));
+        Expression x = new Var("x");
+        Expression y = new Var("y");
+        Expression addition = new BinaryExpression(funcA, "+", x);
+        Expression funcAEqualsY = new BinaryExpression(funcA, "==", y);
+        Expression yEqualsOne = new BinaryExpression(y, "==", new LiteralInt(1));
+        Expression xEqualsTwo = new BinaryExpression(x, "==", new LiteralInt(2));
+        Expression fullExpression = new BinaryExpression(addition, "&&",
+                new BinaryExpression(funcAEqualsY, "&&", new BinaryExpression(yEqualsOne, "&&", xEqualsTwo)));
+
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        assertEquals("3", result.getValue().toString());
+    }
 }

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

@@ -2,12 +2,14 @@
 
 import static org.junit.jupiter.api.Assertions.*;
 
+import java.util.List;
 import java.util.Map;
 
 import org.junit.jupiter.api.Test;
 
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.LiteralInt;
 import liquidjava.rj_language.ast.UnaryExpression;
@@ -168,4 +170,67 @@ void testFreshVariableIsNotUsedAsSubstitutionTarget() {
         Map<String, Expression> result = VariableResolver.resolve(fullExpr);
         assertTrue(result.isEmpty(), "Fresh variables should not replace another variable");
     }
+
+    @Test
+    void testFunctionInvocationEqualityExtractsFunctionKey() {
+        // size(stack) > 0 && size(stack) == 1 should extract size(stack) -> 1
+        Expression stack = new Var("stack");
+        Expression sizeStack = new FunctionInvocation("size", List.of(stack));
+        Expression sizeStackGreaterZero = new BinaryExpression(sizeStack, ">", new LiteralInt(0));
+        Expression sizeStackEqualsOne = new BinaryExpression(sizeStack, "==", new LiteralInt(1));
+        Expression fullExpr = new BinaryExpression(sizeStackGreaterZero, "&&", sizeStackEqualsOne);
+
+        Map<String, Expression> result = VariableResolver.resolve(fullExpr);
+
+        assertEquals(1, result.size(), "Should extract the function invocation as a substitution key");
+        assertEquals("1", result.get("size(stack)").toString());
+    }
+
+    @Test
+    void testLiteralOnLeftExtractsFunctionInvocationKey() {
+        // size(stack) > 0 && 1 == size(stack) should extract size(stack) -> 1
+        Expression stack = new Var("stack");
+        Expression sizeStack = new FunctionInvocation("size", List.of(stack));
+        Expression sizeStackGreaterZero = new BinaryExpression(sizeStack, ">", new LiteralInt(0));
+        Expression oneEqualsSizeStack = new BinaryExpression(new LiteralInt(1), "==", sizeStack);
+        Expression fullExpr = new BinaryExpression(sizeStackGreaterZero, "&&", oneEqualsSizeStack);
+
+        Map<String, Expression> result = VariableResolver.resolve(fullExpr);
+
+        assertEquals(1, result.size(), "Should extract function invocation equalities from either side");
+        assertEquals("1", result.get("size(stack)").toString());
+    }
+
+    @Test
+    void testFunctionInvocationEqualitiesResolveTransitively() {
+        // func(a) > 0 && func(a) == func(b) && func(b) == 1 should extract func(a) -> 1
+        Expression funcA = new FunctionInvocation("func", List.of(new Var("a")));
+        Expression funcB = new FunctionInvocation("func", List.of(new Var("b")));
+        Expression funcAGreaterZero = new BinaryExpression(funcA, ">", new LiteralInt(0));
+        Expression funcAEqualsFuncB = new BinaryExpression(funcA, "==", funcB);
+        Expression funcBEqualsOne = new BinaryExpression(funcB, "==", new LiteralInt(1));
+        Expression fullExpr = new BinaryExpression(funcAGreaterZero, "&&",
+                new BinaryExpression(funcAEqualsFuncB, "&&", funcBEqualsOne));
+
+        Map<String, Expression> result = VariableResolver.resolve(fullExpr);
+
+        assertEquals(2, result.size(), "Should keep the function invocation chain that was used");
+        assertEquals("1", result.get("func(a)").toString());
+        assertEquals("1", result.get("func(b)").toString());
+    }
+
+    @Test
+    void testUnusedFunctionInvocationEqualityIsIgnored() {
+        // x > 0 && size(stack) == 1 should not extract size(stack), because it is only defined
+        Expression x = new Var("x");
+        Expression stack = new Var("stack");
+        Expression sizeStack = new FunctionInvocation("size", List.of(stack));
+        Expression xGreaterZero = new BinaryExpression(x, ">", new LiteralInt(0));
+        Expression sizeStackEqualsOne = new BinaryExpression(sizeStack, "==", new LiteralInt(1));
+        Expression fullExpr = new BinaryExpression(xGreaterZero, "&&", sizeStackEqualsOne);
+
+        Map<String, Expression> result = VariableResolver.resolve(fullExpr);
+
+        assertTrue(result.isEmpty(), "Function invocation definitions with no usage should be ignored");
+    }
 }