Drop path conditions that expected does not depend on from Found

A generated boolean binder (a path condition such as #if_condition) whose
variable and refinement share no term with Expected, directly or through
other facts, and that no other row mentions, is removed as a step of the
Binder pass. The original chain the panel steps back to keeps it.

The linking helpers (factsOf, linkedTerms, termsOf, termName,
linkedToExpected) move from RefinementError to VCSimplificationUtils, so
the simplified chain, the message and the counterexample link facts the
same way.

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

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -3,7 +3,6 @@
 import java.util.ArrayList;
 import java.util.Comparator;
 import java.util.HashSet;
-import java.util.Iterator;
 import java.util.List;
 import java.util.Set;
 import java.util.stream.Collectors;
@@ -15,9 +14,6 @@
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.rj_language.ast.Expression;
-import liquidjava.rj_language.ast.FunctionInvocation;
-import liquidjava.rj_language.ast.LiteralBoolean;
-import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
@@ -27,7 +23,12 @@
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedTerms;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.termName;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf;
 
 /**
  * Error indicating that a refinement constraint either was violated or cannot be proven
@@ -72,21 +73,6 @@ private static String message(Predicate expected, VCSimplificationResult found)
                 expected.getExpression().toDisplayString());
     }
 
-    /**
-     * The facts of found linked to the terms of expected, as a conjunction, or true when there are none; found as
-     * written when every fact is linked
-     */
-    static Expression linkedToExpected(Expression found, Expression expected) {
-        List<Expression> facts = factsOf(found);
-        Set<String> linked = linkedTerms(facts, termsOf(expected));
-        List<Expression> linkedFacts = facts.stream().filter(fact -> termsOf(fact).stream().anyMatch(linked::contains))
-                .toList();
-        if (linkedFacts.size() == facts.size())
-            return found;
-        return linkedFacts.stream().reduce((first, second) -> new BinaryExpression(first, "&&", second))
-                .orElse(new LiteralBoolean(true));
-    }
-
     /** Unknown when what was found says nothing about the values the expected refinement constrains */
     private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) {
         List<String> foundVariables = found.getImplication().toPredicate().getVariableNames();
@@ -138,47 +124,6 @@ private Counterexample filterCounterexample(Counterexample counterexample) {
                 .toList());
     }
 
-    // Conjuncts of found, also splitting negated disjunctions (!(a || b) is !a && !b) and dropping double negations, so
-    // each fact links only the terms it relates
-    private static List<Expression> factsOf(Expression expression) {
-        List<Expression> facts = new ArrayList<>();
-        if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) {
-            facts.addAll(factsOf(binary.getFirstOperand()));
-            facts.addAll(factsOf(binary.getSecondOperand()));
-        } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp())
-                && not.getExpression()instanceof BinaryExpression binary && "||".equals(binary.getOperator())) {
-            facts.addAll(factsOf(new UnaryExpression("!", binary.getFirstOperand())));
-            facts.addAll(factsOf(new UnaryExpression("!", binary.getSecondOperand())));
-        } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp())
-                && not.getExpression()instanceof UnaryExpression inner && "!".equals(inner.getOp())) {
-            facts.addAll(factsOf(inner.getExpression()));
-        } else {
-            facts.add(expression);
-        }
-        return facts;
-    }
-
-    // Terms of expected plus those of every fact sharing a term with them, directly or through other facts. The
-    // remaining facts constrain other values only, so any values satisfying them make the same counterexample
-    private static Set<String> linkedTerms(List<Expression> facts, List<String> expectedTerms) {
-        Set<String> linked = new HashSet<>(expectedTerms);
-        List<List<String>> unlinked = facts.stream().map(RefinementError::termsOf)
-                .collect(Collectors.toCollection(ArrayList::new));
-        boolean changed = true;
-        while (changed) {
-            changed = false;
-            for (Iterator<List<String>> it = unlinked.iterator(); it.hasNext();) {
-                List<String> terms = it.next();
-                if (terms.stream().anyMatch(linked::contains)) {
-                    linked.addAll(terms);
-                    it.remove();
-                    changed = true;
-                }
-            }
-        }
-        return linked;
-    }
-
     // Whether a fact of found is term == value, which the counterexample would only repeat
     private static boolean isKnown(Pair<String, String> assignment, List<Expression> facts) {
         return facts.stream()
@@ -209,32 +154,4 @@ private static int relevance(String term, List<String> expectedTerms, List<Strin
             return foundTerms.contains(term) ? 1 : 0;
         return GeneratedNames.isGenerated(term) ? 3 : 2;
     }
-
-    // Variables and ghost applications of an expression, named as in the SMT model
-    private static List<String> termsOf(Expression expression) {
-        List<String> terms = new ArrayList<>();
-        expression.getVariableNames(terms);
-        addGhostApplications(expression, terms);
-        return terms;
-    }
-
-    private static void addGhostApplications(Expression expression, List<String> terms) {
-        String term = expression instanceof FunctionInvocation ? termName(expression) : null;
-        if (term != null && !terms.contains(term))
-            terms.add(term);
-        for (Expression child : expression.getChildren())
-            addGhostApplications(child, terms);
-    }
-
-    // Name of a variable, or of a ghost application over variables, as in the SMT model; null for other expressions
-    private static String termName(Expression expression) {
-        if (expression instanceof Var var)
-            return var.getName();
-        if (expression instanceof FunctionInvocation invocation
-                && invocation.getArgs().stream().allMatch(Var.class::isInstance)) {
-            String args = invocation.getArgs().stream().map(Expression::toString).collect(Collectors.joining(", "));
-            return Utils.getSimpleName(invocation.getName()) + "(" + args + ")";
-        }
-        return null;
-    }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -1,6 +1,7 @@
 package liquidjava.diagnostics.errors;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected;
 
 import java.util.List;
 
@@ -44,7 +45,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
     // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a
     // guard on another value says nothing about the state expected needs
     private static String message(Predicate expected, VCSimplificationResult found) {
-        Expression shown = RefinementError.linkedToExpected(found.getImplication().toPredicate().getExpression(),
+        Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(),
                 expected.getExpression());
         if (!appliesGhost(shown))
             return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());

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

@@ -1,10 +1,13 @@
 package liquidjava.rj_language.opt;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedTerms;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.valueVariablesOf;
 
 import java.util.HashSet;
+import java.util.List;
 import java.util.Set;
 
 import liquidjava.processor.VCImplication;
@@ -15,7 +18,8 @@
  * Decides which binders refined only by {@code true} a simplified VC chain keeps for an error. Such a binder states no
  * fact, and a variable that another row mentions is already shown there, so its row would only read as if its value
  * were true. It is kept only when the error shows a counterexample, expected constrains the variable's value and no
- * other row mentions it: the row then shows that nothing is known about a value the error depends on
+ * other row mentions it: the row then shows that nothing is known about a value the error depends on. It also tells
+ * which binders expected does not depend on, such as path conditions over other values
  *
  * @param expectedTerms
  *            variables and ghost applications of the expected refinement
@@ -68,6 +72,35 @@ public Set<String> trueBindersToKeep(VCImplication chain) {
         return keep;
     }
 
+    /**
+     * Binders that share no term with expected, neither their variable nor a term of their refinement, directly or
+     * through other facts of the chain, and whose variable no other row mentions: expected does not depend on them.
+     * None without expected terms
+     */
+    public Set<String> unlinkedBinders(VCImplication chain) {
+        Set<String> unlinked = new HashSet<>();
+        if (expectedTerms.isEmpty())
+            return unlinked;
+        List<Expression> facts = factsOf(chain.toPredicate().getExpression());
+        Set<String> linked = linkedTerms(facts, expectedTerms);
+        for (VCImplication row = chain; row != null; row = row.getNext())
+            if (row.hasBinder() && !isLinked(row, linked) && !mentionedByOtherRows(chain, row))
+                unlinked.add(row.getName());
+        return unlinked;
+    }
+
+    private static boolean isLinked(VCImplication row, Set<String> linked) {
+        return linked.contains(row.getName())
+                || termsOf(row.getRefinement().getExpression()).stream().anyMatch(linked::contains);
+    }
+
+    private static boolean mentionedByOtherRows(VCImplication chain, VCImplication row) {
+        for (VCImplication other = chain; other != null; other = other.getNext())
+            if (other != row && containsVar(other.getRefinement().getExpression(), row.getName()))
+                return true;
+        return false;
+    }
+
     private static Set<String> primitiveBinders(VCImplication chain) {
         Set<String> primitives = new HashSet<>();
         for (VCImplication current = chain; current != null; current = current.getNext())

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

@@ -34,24 +34,25 @@ public VCBinderSimplification(NeededVariables needed) {
     @Override
     public VCImplication apply(VCImplication implication) {
         VCImplication cloned = implication.clone();
-        VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned));
+        VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned), needed.unlinkedBinders(cloned));
         return simplified == null ? cloned : simplified;
     }
 
     /**
      * Simplifies the first applicable binder in a VC chain
      */
-    private VCImplication simplify(VCImplication implication, Set<String> keptTrueBinders) {
+    private VCImplication simplify(VCImplication implication, Set<String> keptTrueBinders,
+            Set<String> unlinkedBinders) {
         if (implication == null)
             return null;
 
         if (isFalseBinder(implication))
             return collapseFalseBinder(implication);
 
-        if (isRemovableBinder(implication, keptTrueBinders))
+        if (isRemovableBinder(implication, keptTrueBinders, unlinkedBinders))
             return removeBinder(implication);
 
-        VCImplication next = simplify(implication.getNext(), keptTrueBinders);
+        VCImplication next = simplify(implication.getNext(), keptTrueBinders, unlinkedBinders);
         if (next == null)
             return null;
 
@@ -87,29 +88,39 @@ private VCImplication removeBinder(VCImplication implication) {
     /**
      * Checks whether a binder can be removed without changing the VC conclusion or hiding what explains the error. A
      * binder refined only by true states no fact, so it is removed even when a later implication uses its variable,
-     * unless the error needs it
+     * unless the error needs it. A generated path condition that expected does not depend on is removed too
      */
-    private boolean isRemovableBinder(VCImplication implication, Set<String> keptTrueBinders) {
+    private boolean isRemovableBinder(VCImplication implication, Set<String> keptTrueBinders,
+            Set<String> unlinkedBinders) {
         if (!implication.hasBinder())
             return false;
 
         if (isTrueBinder(implication))
             return !keptTrueBinders.contains(implication.getName());
+        if (isGeneratedBooleanBinder(implication) && unlinkedBinders.contains(implication.getName()))
+            return true;
         return !containsVar(implication.getNext(), implication.getName()) && isUnusedFreshPathBinder(implication);
     }
 
     /**
      * Checks for a generated boolean path binder refined exactly by itself
      */
     private boolean isUnusedFreshPathBinder(VCImplication implication) {
-        if (!implication.hasNext() || !GeneratedNames.isGenerated(implication.getName())
-                || !"boolean".equals(implication.getType().getQualifiedName()))
+        if (!implication.hasNext() || !isGeneratedBooleanBinder(implication))
             return false;
 
         return implication.getRefinement().getExpression()instanceof Var var
                 && implication.getName().equals(var.getName());
     }
 
+    /**
+     * Checks for a binder of a generated boolean, such as a path condition
+     */
+    private boolean isGeneratedBooleanBinder(VCImplication implication) {
+        return GeneratedNames.isGenerated(implication.getName())
+                && "boolean".equals(implication.getType().getQualifiedName());
+    }
+
     /**
      * Replaces a false binder implication with true
      */