Do not link Found facts through an enum constant they only compare with

An enum constant read in code is a variable named Type.CONST, so the
relevance pass linked every fact that compared a value with the same
constant. A constant is a fixed value, so such facts share no unknown;
it now links facts only when a function or alias takes it or a value
one takes is compared with it, where equal objects have equal ghost
values. A1_09 no longer shows newMode == BORDERLESS once the ternary
no longer depends on newMode.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -22,6 +22,7 @@
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.opt.NeededVariables;
+import liquidjava.rj_language.opt.VCKnownEnumValues;
 import liquidjava.rj_language.opt.VCRelevantFacts;
 import liquidjava.rj_language.opt.VCSimplification;
 import liquidjava.rj_language.opt.VCSimplificationResult;
@@ -465,8 +466,8 @@ protected void throwStateRefinementError(SourcePosition position, List<SourcePos
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
         VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected));
-        VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified,
-                new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf));
+        VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified, new VCRelevantFacts(
+                expected.getExpression(), this::ghostFunctionsOf, VCKnownEnumValues.enumConstants(foundState)));
         StateRefinementError error = new StateRefinementError(position, declarationPositions, expected, shown, map,
                 customMessage, hints, category, context,
                 e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()),

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

@@ -5,6 +5,7 @@
 
 import java.util.HashMap;
 import java.util.Map;
+import java.util.Set;
 
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
@@ -32,14 +33,25 @@ private record EnumComparison(Expression expression, String variable, String con
     }
 
     /** The enum type of each enum constant, by the name the solver translates the constant from */
-    private final Map<String, String> enumTypes = new HashMap<>();
+    private final Map<String, String> enumTypes;
 
     public VCKnownEnumValues(VCImplication implication) {
+        this.enumTypes = enumTypesOf(implication);
+    }
+
+    /** The names the constants of the enum types of the chain's binders are translated from, which denote values */
+    public static Set<String> enumConstants(VCImplication implication) {
+        return enumTypesOf(implication).keySet();
+    }
+
+    private static Map<String, String> enumTypesOf(VCImplication implication) {
+        Map<String, String> enumTypes = new HashMap<>();
         for (VCImplication row = implication; row != null; row = row.getNext())
             if (row.getType() != null && row.getType().getDeclaration()instanceof CtEnum<?> enumDecl)
                 for (CtEnumValue<?> value : enumDecl.getEnumValues())
                     enumTypes.put(String.format(Formats.ENUM, enumDecl.getSimpleName(), value.getSimpleName()),
                             enumDecl.getQualifiedName());
+        return enumTypes;
     }
 
     /**

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

@@ -15,6 +15,7 @@
 
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.AliasInvocation;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.FunctionInvocation;
@@ -27,22 +28,28 @@
  * value it constrains. Different ghost functions, or the same one over different objects, are different solver terms,
  * so facts that share no symbol with expected, directly or through other facts, are independent of it and are left out.
  * An object whose value a fact constrains, such as {@code x == y}, or that an alias or unknown function takes, is one
- * symbol with all its ghost functions, so its facts are never split. Nothing changes when every fact or none is
- * relevant
+ * symbol with all its ghost functions, so its facts are never split. A constant, such as an enum constant read in code,
+ * is a fixed value, so facts that only compare values with it share no symbol through it; it stays one when a function
+ * or alias takes it or a value one takes is compared with it, as equal objects have equal ghost values. Nothing changes
+ * when every fact or none is relevant
  */
 public class VCRelevantFacts implements VCSimplificationPass {
 
     private final Expression expected;
     private final Function<String, Set<String>> ghostFunctionsOf;
+    private final Set<String> constants;
 
     /**
      * @param ghostFunctionsOf
      *            the ghost functions an invocation name stands for: a state's state set function, or the ghost itself;
      *            none for any other name
+     * @param constants
+     *            the variable names that denote constants, such as enum constants
      */
-    public VCRelevantFacts(Expression expected, Function<String, Set<String>> ghostFunctionsOf) {
+    public VCRelevantFacts(Expression expected, Function<String, Set<String>> ghostFunctionsOf, Set<String> constants) {
         this.expected = expected;
         this.ghostFunctionsOf = ghostFunctionsOf;
+        this.constants = constants;
     }
 
     @Override
@@ -60,8 +67,10 @@ public VCImplication apply(VCImplication implication) {
         addSymbols(expected, new HashMap<>(), values);
         allFacts.forEach(fact -> addSymbols(fact, new HashMap<>(), values));
 
-        Set<String> linked = symbolsOf(expected, values);
-        List<Set<String>> unlinked = new ArrayList<>(allFacts.stream().map(fact -> symbolsOf(fact, values)).toList());
+        Set<String> valueConstants = valueConstants(expected, allFacts);
+        Set<String> linked = symbolsOf(expected, values, valueConstants);
+        List<Set<String>> unlinked = new ArrayList<>(
+                allFacts.stream().map(fact -> symbolsOf(fact, values, valueConstants)).toList());
         boolean changed = true;
         while (changed) {
             changed = false;
@@ -75,8 +84,11 @@ public VCImplication apply(VCImplication implication) {
             }
         }
 
-        List<List<Expression>> kept = rowFacts.stream().map(facts -> facts.stream()
-                .filter(fact -> symbolsOf(fact, values).stream().anyMatch(linked::contains)).toList()).toList();
+        List<List<Expression>> kept = rowFacts.stream()
+                .map(facts -> facts.stream()
+                        .filter(fact -> symbolsOf(fact, values, valueConstants).stream().anyMatch(linked::contains))
+                        .toList())
+                .toList();
         int relevant = kept.stream().mapToInt(List::size).sum();
         if (relevant == 0 || relevant == allFacts.size())
             return implication;
@@ -99,13 +111,45 @@ private VCImplication rebuild(VCImplication row, Iterator<List<Expression>> all,
         return result;
     }
 
+    // The constants no function or alias takes and that are compared with no value one takes
+    private Set<String> valueConstants(Expression expected, List<Expression> facts) {
+        Set<String> objects = new HashSet<>();
+        addArguments(expected, objects);
+        facts.forEach(fact -> addArguments(fact, objects));
+        Set<String> valueConstants = new HashSet<>(constants);
+        valueConstants.removeAll(objects);
+        removeComparedWithObjects(expected, objects, valueConstants);
+        facts.forEach(fact -> removeComparedWithObjects(fact, objects, valueConstants));
+        return valueConstants;
+    }
+
+    private static void addArguments(Expression expression, Set<String> objects) {
+        if (expression instanceof FunctionInvocation invocation)
+            invocation.getArgs().forEach(argument -> objects.addAll(variablesOf(argument)));
+        else if (expression instanceof AliasInvocation alias)
+            alias.getArgs().forEach(argument -> objects.addAll(variablesOf(argument)));
+        expression.getChildren().forEach(child -> addArguments(child, objects));
+    }
+
+    private static void removeComparedWithObjects(Expression expression, Set<String> objects,
+            Set<String> valueConstants) {
+        if (expression instanceof BinaryExpression binary
+                && ("==".equals(binary.getOperator()) || "!=".equals(binary.getOperator()))) {
+            List<String> compared = variablesOf(binary);
+            if (compared.stream().anyMatch(objects::contains))
+                valueConstants.removeAll(compared);
+        }
+        expression.getChildren().forEach(child -> removeComparedWithObjects(child, objects, valueConstants));
+    }
+
     // The symbols an expression constrains: f(x) for a ghost function over an object, or the object itself when values
-    // has it, and the variables whose value it constrains
-    private Set<String> symbolsOf(Expression expression, Set<String> values) {
+    // has it, and the variables whose value it constrains, except the value constants
+    private Set<String> symbolsOf(Expression expression, Set<String> values, Set<String> valueConstants) {
         Map<String, String> applications = new HashMap<>();
         Set<String> symbols = new HashSet<>();
         addSymbols(expression, applications, symbols);
         applications.forEach((application, object) -> symbols.add(values.contains(object) ? object : application));
+        symbols.removeAll(valueConstants);
         return symbols;
     }
 

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

@@ -9,7 +9,12 @@
 import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.Test;
 
+import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.Context;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.TestUtils;
 
@@ -190,7 +195,7 @@ private static VCRelevantFacts relevantTo(String expected) {
         Map<String, String> stateSets = Map.of("startTiling", "state1", "tilingSet", "state1", "state1", "state1",
                 "compressionSet", "state2", "state2", "state2");
         return new VCRelevantFacts(RefinementsParser.createAST(expected, ""),
-                name -> stateSets.containsKey(name) ? Set.of(stateSets.get(name)) : Set.of());
+                name -> stateSets.containsKey(name) ? Set.of(stateSets.get(name)) : Set.of(), Set.of("Mode.Photo"));
     }
 
     @Test
@@ -200,6 +205,31 @@ void relevantStepKeepsEveryStateSetOfAnObjectComparedAsAValue() {
                 step("compressionSet(q) && startTiling(p)", "p == q"));
     }
 
+    @Test
+    void relevantStepDoesNotLinkFactsThroughAConstant() {
+        // code reads an enum constant as a variable named after it
+        Var photo = new Var("Mode.Photo");
+        VCImplication implication = vc("∀n:Mode. true", "true");
+        implication.setRefinement(new Predicate(new BinaryExpression(new Var("n"), "==", photo)));
+        implication.getNext()
+                .setRefinement(new Predicate(new Ite(new BinaryExpression(new Var("m"), "==", photo),
+                        RefinementsParser.createAST("startTiling(p)", ""),
+                        RefinementsParser.createAST("compressionSet(p)", ""))));
+        assertSimplificationSteps(relevantTo("tilingSet(p)"), implication,
+                step("m == Photo ? startTiling(p) : compressionSet(p)"));
+    }
+
+    @Test
+    void relevantStepLinksFactsThroughAConstantAnObjectEquals() {
+        Var photo = new Var("Mode.Photo");
+        VCImplication implication = vc("∀p:Mode. true", "true");
+        implication.setRefinement(new Predicate(new BinaryExpression(new Var("p"), "==", photo)));
+        implication.getNext().setRefinement(new Predicate(
+                new BinaryExpression(RefinementsParser.createAST("startTiling(q)", ""), "&&", new Var("ready"))));
+        implication.getNext().getRefinement().getExpression().getChildren().get(0).setChild(0, photo);
+        assertSimplificationSteps(relevantTo("tilingSet(p)"), implication, step("p == Photo", "startTiling(Photo)"));
+    }
+
     @Test
     void relevantStepKeepsFactsAnUnknownFunctionTakesTheObjectOf() {
         assertSimplificationSteps(relevantTo("tilingSet(p)"), vc("compressionSet(p) && ready(p)", "startTiling(p)"),