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

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 chain of comparisons relates it to a value one takes, 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,50 @@ private VCImplication rebuild(VCImplication row, Iterator<List<Expression>> all,
         return result;
     }
 
+    // The constants no function or alias takes and that no chain of comparisons relates to a 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));
+        List<Expression> all = new ArrayList<>(facts);
+        all.add(expected);
+        while (all.stream().anyMatch(expression -> addComparedWithObjects(expression, objects)))
+            ;
+        Set<String> valueConstants = new HashSet<>(constants);
+        valueConstants.removeAll(objects);
+        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));
+    }
+
+    // Adds to objects the variables a comparison relates to one of them; true when it added any
+    private static boolean addComparedWithObjects(Expression expression, Set<String> objects) {
+        boolean added = false;
+        if (expression instanceof BinaryExpression binary
+                && ("==".equals(binary.getOperator()) || "!=".equals(binary.getOperator()))) {
+            List<String> compared = variablesOf(binary);
+            if (compared.stream().anyMatch(objects::contains))
+                added = objects.addAll(compared);
+        }
+        for (Expression child : expression.getChildren())
+            added |= addComparedWithObjects(child, objects);
+        return added;
+    }
+
     // 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,45 @@ 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 relevantStepLinksFactsThroughAConstantAChainOfEqualitiesRelatesToAnObject() {
+        // p == r == Photo == s == q, so the facts about q constrain tilingSet(p)
+        Var photo = new Var("Mode.Photo");
+        VCImplication implication = vc("∀p:Mode. true", "true");
+        implication.setRefinement(new Predicate(new BinaryExpression(RefinementsParser.createAST("p == r", ""), "&&",
+                new BinaryExpression(new Var("r"), "==", photo))));
+        implication.getNext()
+                .setRefinement(new Predicate(new BinaryExpression(new BinaryExpression(new Var("s"), "==", photo), "&&",
+                        RefinementsParser.createAST("s == q && startTiling(q)", ""))));
+        assertSimplificationSteps(relevantTo("tilingSet(p)"), implication,
+                step("p == r && r == Photo", "s == Photo && s == q && startTiling(q)"));
+    }
+
     @Test
     void relevantStepKeepsFactsAnUnknownFunctionTakesTheObjectOf() {
         assertSimplificationSteps(relevantTo("tilingSet(p)"), vc("compressionSet(p) && ready(p)", "startTiling(p)"),