Fix Single Equality Simplification

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

@@ -15,6 +15,15 @@ public class VariableResolver {
      * Extracts variables with constant values from an expression Returns a map from variable names to their values
      */
     public static Map<String, Expression> resolve(Expression exp) {
+        // if the expression is just a single equality (not a conjunction) don't extract it
+        // this avoids creating tautologies like "1 == 1" after substitution, which are then simplified to "true"
+        if (exp instanceof BinaryExpression) {
+            BinaryExpression be = (BinaryExpression) exp;
+            if ("==".equals(be.getOperator())) {
+                return new HashMap<>();
+            }
+        }
+
         Map<String, Expression> map = new HashMap<>();
         resolveRecursive(exp, map);
         return resolveTransitive(map);

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

@@ -304,6 +304,31 @@ void testComplexArithmeticWithMultipleOperations() {
         assertDerivationEquals(expected, result, "");
     }
 
+    @Test
+    void testSingleEqualityNotSimplifiedToTrue() {
+        // Given: x == 1
+        // Expected: x == 1 (should not be simplified to "true")
+
+        Expression varX = new Var("x");
+        Expression one = new LiteralInt(1);
+        Expression xEquals1 = new BinaryExpression(varX, "==", one);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(xEquals1);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("x == 1", result.getValue().toString(),
+                "Single equality should not be simplified to a boolean literal");
+
+        // The result should be the original expression unchanged
+        assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression");
+        BinaryExpression resultExpr = (BinaryExpression) result.getValue();
+        assertEquals("==", resultExpr.getOperator(), "Operator should still be ==");
+        assertEquals("x", resultExpr.getFirstOperand().toString(), "Left operand should be x");
+        assertEquals("1", resultExpr.getSecondOperand().toString(), "Right operand should be 1");
+    }
+
     /**
      * Helper method to compare two derivation nodes recursively
      */

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

@@ -0,0 +1,110 @@
+package liquidjava.rj_language.opt;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+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.GroupExpression;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.ast.UnaryExpression;
+import liquidjava.rj_language.ast.Var;
+
+class VariableResolverTest {
+
+    @Test
+    void testSingleEqualityNotExtracted() {
+        // x == 1 should not extract because it's a single equality
+        Expression varX = new Var("x");
+        Expression one = new LiteralInt(1);
+        Expression xEquals1 = new BinaryExpression(varX, "==", one);
+        Map<String, Expression> result = VariableResolver.resolve(xEquals1);
+        assertTrue(result.isEmpty(), "Single equality should not extract variable mapping");
+    }
+
+    @Test
+    void testConjunctionExtractsVariables() {
+        // x + y && x == 1 && y == 2 should extract x -> 1, y -> 2
+        Expression varX = new Var("x");
+        Expression varY = new Var("y");
+        Expression one = new LiteralInt(1);
+        Expression two = new LiteralInt(2);
+
+        Expression xPlusY = new BinaryExpression(varX, "+", varY);
+        Expression xEquals1 = new BinaryExpression(varX, "==", one);
+        Expression yEquals2 = new BinaryExpression(varY, "==", two);
+
+        Expression conditions = new BinaryExpression(xEquals1, "&&", yEquals2);
+        Expression fullExpr = new BinaryExpression(xPlusY, "&&", conditions);
+
+        Map<String, Expression> result = VariableResolver.resolve(fullExpr);
+        assertEquals(2, result.size(), "Should extract both variables");
+        assertEquals("1", result.get("x").toString());
+        assertEquals("2", result.get("y").toString());
+    }
+
+    @Test
+    void testSingleComparisonNotExtracted() {
+        // x > 0 should not extract anything
+        Expression varX = new Var("x");
+        Expression zero = new LiteralInt(0);
+        Expression xGreaterZero = new BinaryExpression(varX, ">", zero);
+
+        Map<String, Expression> result = VariableResolver.resolve(xGreaterZero);
+        assertTrue(result.isEmpty(), "Single comparison should not extract variable mapping");
+    }
+
+    @Test
+    void testSingleArithmeticExpression() {
+        // x + 1 should not extract anything
+        Expression varX = new Var("x");
+        Expression one = new LiteralInt(1);
+        Expression xPlusOne = new BinaryExpression(varX, "+", one);
+
+        Map<String, Expression> result = VariableResolver.resolve(xPlusOne);
+        assertTrue(result.isEmpty(), "Single arithmetic expression should not extract variable mapping");
+    }
+
+    @Test
+    void testDisjunctionWithEqualities() {
+        // x == 1 || y == 2 should not extract anything
+        Expression varX = new Var("x");
+        Expression varY = new Var("y");
+        Expression one = new LiteralInt(1);
+        Expression two = new LiteralInt(2);
+
+        Expression xEquals1 = new BinaryExpression(varX, "==", one);
+        Expression yEquals2 = new BinaryExpression(varY, "==", two);
+        Expression disjunction = new BinaryExpression(xEquals1, "||", yEquals2);
+
+        Map<String, Expression> result = VariableResolver.resolve(disjunction);
+        assertTrue(result.isEmpty(), "Disjunction should not extract variable mappings");
+    }
+
+    @Test
+    void testNegatedEquality() {
+        // !(x == 1) should not extract because it's a single equality
+        Expression varX = new Var("x");
+        Expression one = new LiteralInt(1);
+        Expression xEquals1 = new BinaryExpression(varX, "==", one);
+        Expression notXEquals1 = new UnaryExpression("!", xEquals1);
+
+        Map<String, Expression> result = VariableResolver.resolve(notXEquals1);
+        assertTrue(result.isEmpty(), "Negated equality should not extract variable mapping");
+    }
+
+    @Test
+    void testGroupedEquality() {
+        // (x == 1) should not extract because it's a single equality
+        Expression varX = new Var("x");
+        Expression one = new LiteralInt(1);
+        Expression xEquals1 = new BinaryExpression(varX, "==", one);
+        Expression grouped = new GroupExpression(xEquals1);
+
+        Map<String, Expression> result = VariableResolver.resolve(grouped);
+        assertTrue(result.isEmpty(), "Grouped single equality should not extract variable mapping");
+    }
+}