Performance Series 2 (5/5): Faster quantifier-instantiation heuristic, plus code cleanup (#3878)

Author: Drodt

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java

@@ -28,6 +28,22 @@ public class HandleArith {
 
     private HandleArith() {}
 
+    /** The operator of {@code t} after stripping leading negations. */
+    private static Operator strippedOp(JTerm t) {
+        Operator op = t.op();
+        while (op == Junctor.NOT) {
+            t = t.sub(0);
+            op = t.op();
+        }
+        return op;
+    }
+
+    /** Whether {@code t} (ignoring leading negations) is an integer {@code >=} or {@code <=}. */
+    private static boolean isArithComparison(JTerm t, IntegerLDT ig) {
+        final Operator op = strippedOp(t);
+        return op == ig.getGreaterOrEquals() || op == ig.getLessOrEquals();
+    }
+
     /**
      * try to prove atom by using polynomial
      *
@@ -36,6 +52,12 @@ private HandleArith() {}
      *         <code>problem</code> if it cann't be proved.
      */
     public static JTerm provedByArith(JTerm problem, Services services) {
+        final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT();
+        if (!isArithComparison(problem, integerLDT) && strippedOp(problem) != Equality.EQUALS) {
+            // neither an (in)equality nor an equality: formatArithTerm yields false and
+            // provedArithEqual returns the problem unchanged -- bail before locking the cache.
+            return problem;
+        }
         final LRUCache<JTerm, JTerm> provedByArithCache =
             services.getCaches().getProvedByArithFstCache();
         JTerm result;
@@ -47,7 +69,6 @@ public static JTerm provedByArith(JTerm problem, Services services) {
         }
 
         TermBuilder tb = services.getTermBuilder();
-        IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT();
 
         final JTerm trueT = tb.tt();
         final JTerm falseT = tb.ff();
@@ -127,6 +148,13 @@ private static JTerm provedArithEqual(JTerm problem, TermBuilder tb, Services se
      * @return trueT if true, falseT if false, and atom if can't be prove;
      */
     public static JTerm provedByArith(JTerm problem, JTerm axiom, Services services) {
+        final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT();
+        if (!isArithComparison(problem, integerLDT) || !isArithComparison(axiom, integerLDT)) {
+            // not an arithmetic implication: formatArithTerm would yield false for one side and
+            // this method returns the unproved problem -- bail before allocating the key and
+            // taking the cache lock.
+            return problem;
+        }
         final Pair<JTerm, JTerm> key = new Pair<>(problem, axiom);
         final LRUCache<Pair<JTerm, JTerm>, JTerm> provedByArithCache =
             services.getCaches().getProvedByArithSndCache();
@@ -139,7 +167,6 @@ public static JTerm provedByArith(JTerm problem, JTerm axiom, Services services)
         }
 
         final TermBuilder tb = services.getTermBuilder();
-        final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT();
         final ServiceCaches caches = services.getCaches();
 
         final JTerm cd = formatArithTerm(problem, tb, integerLDT, caches);

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java

@@ -15,101 +15,116 @@
 import org.key_project.util.collection.ImmutableMapEntry;
 import org.key_project.util.collection.ImmutableSet;
 
+/**
+ * A trigger built from several uni-trigger {@link #elements} that, taken together, bind all
+ * universal variables of a clause. A match requires matching every element and merging their
+ * substitutions into one that is consistent and total on {@link #clauseVariables}.
+ */
 class MultiTrigger implements Trigger {
 
-    private final ImmutableSet<Trigger> triggers;
+    /** The uni-trigger elements that jointly have to cover {@link #clauseVariables}. */
+    private final ImmutableSet<Trigger> elements;
 
-    private final ImmutableSet<QuantifiableVariable> qvs;
+    /** The universal variables of the clause this multi-trigger must bind. */
+    private final ImmutableSet<QuantifiableVariable> clauseVariables;
 
     private final Term clause;
 
-    MultiTrigger(ImmutableSet<Trigger> triggers, ImmutableSet<QuantifiableVariable> qvs,
+    MultiTrigger(ImmutableSet<Trigger> elements, ImmutableSet<QuantifiableVariable> clauseVariables,
             Term clause) {
-        this.triggers = triggers;
-        this.qvs = qvs;
+        this.elements = elements;
+        this.clauseVariables = clauseVariables;
         this.clause = clause;
     }
 
     @Override
     public ImmutableSet<Substitution> getSubstitutionsFromTerms(ImmutableSet<Term> targetTerms,
             Services services) {
-        ImmutableList<Substitution> res = ImmutableList.nil();
+        ImmutableList<Substitution> total = ImmutableList.nil();
 
-        ImmutableSet<Substitution> mulsubs =
-            setMultiSubstitution(triggers.iterator(), targetTerms, services);
+        final ImmutableSet<Substitution> combined =
+            combineElementSubstitutions(elements.iterator(), targetTerms, services);
 
-        for (Substitution sub : mulsubs) {
-            if (sub.isTotalOn(qvs)) {
-                res = res.prepend(sub);
+        for (Substitution sub : combined) {
+            if (sub.isTotalOn(clauseVariables)) {
+                total = total.prepend(sub);
             }
         }
 
-        return DefaultImmutableSet.fromImmutableList(res);
+        return DefaultImmutableSet.fromImmutableList(total);
     }
 
-    /** help function for getMultiSubstitution */
-    private ImmutableSet<Substitution> setMultiSubstitution(Iterator<? extends Trigger> ts,
-            ImmutableSet<Term> terms, Services services) {
-        ImmutableList<Substitution> res = ImmutableList.nil();
-        if (ts.hasNext()) {
-            ImmutableSet<Substitution> subi = ts.next().getSubstitutionsFromTerms(terms, services);
-            ImmutableSet<Substitution> nextSubs = setMultiSubstitution(ts, terms, services);
-            if (nextSubs.isEmpty()) {
-                return subi;
-            } else if (subi.isEmpty()) {
-                return nextSubs;
+    /**
+     * Matches every remaining element against the target terms and combines the per-element
+     * substitution sets by taking the cross product and merging each compatible pair (incompatible
+     * pairs are dropped). Used by {@link #getSubstitutionsFromTerms}.
+     */
+    private ImmutableSet<Substitution> combineElementSubstitutions(
+            Iterator<? extends Trigger> remainingElements, ImmutableSet<Term> terms,
+            Services services) {
+        ImmutableList<Substitution> result = ImmutableList.nil();
+        if (remainingElements.hasNext()) {
+            ImmutableSet<Substitution> headSubs =
+                remainingElements.next().getSubstitutionsFromTerms(terms, services);
+            ImmutableSet<Substitution> tailSubs =
+                combineElementSubstitutions(remainingElements, terms, services);
+            if (tailSubs.isEmpty()) {
+                return headSubs;
+            } else if (headSubs.isEmpty()) {
+                return tailSubs;
             }
-            for (Substitution sub0 : nextSubs) {
-                for (Substitution subiSub : subi) {
-                    final Substitution sub1 = unifySubstitution(sub0, subiSub);
-                    if (sub1 != null) {
-                        res = res.prepend(sub1);
+            for (Substitution tailSub : tailSubs) {
+                for (Substitution headSub : headSubs) {
+                    final Substitution merged = mergeIfCompatible(tailSub, headSub);
+                    if (merged != null) {
+                        result = result.prepend(merged);
                     }
                 }
 
             }
         }
-        return DefaultImmutableSet.fromImmutableList(res);
+        return DefaultImmutableSet.fromImmutableList(result);
     }
 
     /**
-     * unify two substitution, if same variable are bound with same term return a new substitution
-     * with all universal quantifiable variables in two substituition, otherwise return null
+     * Merges two substitutions: if they bind every shared variable to the same term, returns a new
+     * substitution containing all bindings of both; otherwise (a conflicting binding) returns
+     * {@code null}.
      */
-    private Substitution unifySubstitution(Substitution sub0, Substitution sub1) {
-        final ImmutableMap<QuantifiableVariable, Term> varMap1 = sub1.getVarMap();
-        ImmutableMap<QuantifiableVariable, Term> resMap = varMap1;
-
-        for (final ImmutableMapEntry<QuantifiableVariable, Term> en : sub0.getVarMap()) {
-            QuantifiableVariable key = en.key();
-            Term value = en.value();
-            if (varMap1.containsKey(key)) {
-                if (!(varMap1.get(key).equals(value))) {
+    private Substitution mergeIfCompatible(Substitution left, Substitution right) {
+        final ImmutableMap<QuantifiableVariable, Term> rightMap = right.getVarMap();
+        ImmutableMap<QuantifiableVariable, Term> mergedMap = rightMap;
+
+        for (final ImmutableMapEntry<QuantifiableVariable, Term> entry : left.getVarMap()) {
+            QuantifiableVariable key = entry.key();
+            Term value = entry.value();
+            if (rightMap.containsKey(key)) {
+                if (!(rightMap.get(key).equals(value))) {
                     return null;
                 }
             }
-            resMap = resMap.put(key, value);
+            mergedMap = mergedMap.put(key, value);
         }
-        return new Substitution(resMap);
+        return new Substitution(mergedMap);
     }
 
     @Override
-    public boolean equals(Object arg0) {
-        if (!(arg0 instanceof MultiTrigger a)) {
+    public boolean equals(Object other) {
+        if (!(other instanceof MultiTrigger otherTrigger)) {
             return false;
         }
 
-        return a.triggers.equals(triggers);
+        return otherTrigger.elements.equals(elements);
     }
 
     @Override
     public int hashCode() {
-        return triggers.hashCode();
+        return elements.hashCode();
     }
 
     @Override
     public String toString() {
-        return String.valueOf(triggers);
+        return String.valueOf(elements);
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java

@@ -15,6 +15,7 @@
 import org.key_project.logic.op.Function;
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.logic.sort.Sort;
+import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableMap;
 import org.key_project.util.collection.ImmutableSet;
 
@@ -94,10 +95,79 @@ private Term applySubst(QuantifiableVariable var, Term instance, Term t, TermBui
 
     /**
      * Try to apply the substitution to a term, introducing casts if necessary (may never be the
-     * case any more, XXX)
+     * case any more, XXX).
+     * <p>
+     * Fast path: all variables are substituted in a single traversal ({@link #applyGroundOnePass}).
+     * This is sound because the substitution is ground (the instances contain no free variables, so
+     * no capture can happen); shadowing of a substituted variable by a binder inside {@code t} is
+     * respected. If a cast is required (the slow, possibly dead path), it falls back to the
+     * per-variable substitution {@link #applyWithoutCastsPerVar}.
      */
     public Term applyWithoutCasts(Term t, Services services) {
         assert isGround() : "non-ground substitutions are not yet implemented: " + this;
+        final TermBuilder tb = services.getTermBuilder();
+        try {
+            return applyGroundOnePass((JTerm) t, ImmutableList.nil(), tb);
+        } catch (TermCreationException e) {
+            return applyWithoutCastsPerVar(t, services);
+        }
+    }
+
+    /**
+     * Substitute every variable of {@link #varMap} in a single traversal of {@code t}. A variable
+     * occurrence is replaced unless it is shadowed, i.e. re-bound by a binder above it (tracked in
+     * {@code boundAbove}). Subterms in which no substituted variable occurs free are returned
+     * unchanged.
+     */
+    private JTerm applyGroundOnePass(JTerm t, ImmutableList<QuantifiableVariable> boundAbove,
+            TermBuilder tb) {
+        // Variable leaves (the most common node) are handled directly, without the freeVars
+        // bookkeeping of containsSubstVar.
+        if (t.op() instanceof QuantifiableVariable qv) {
+            final Term inst = varMap.get(qv);
+            return inst != null && !boundAbove.contains(qv) ? (JTerm) inst : t;
+        }
+        if (!containsSubstVar(t)) {
+            return t;
+        }
+        final int arity = t.arity();
+        final JTerm[] newSubs = new JTerm[arity];
+        boolean changed = false;
+        for (int i = 0; i < arity; i++) {
+            final JTerm sub = t.sub(i);
+            ImmutableList<QuantifiableVariable> below = boundAbove;
+            final var boundHere = t.varsBoundHere(i);
+            for (int j = 0; j < boundHere.size(); j++) {
+                below = below.prepend(boundHere.get(j));
+            }
+            newSubs[i] = applyGroundOnePass(sub, below, tb);
+            if (newSubs[i] != sub) {
+                changed = true;
+            }
+        }
+        if (!changed) {
+            return t;
+        }
+        return tb.tf().createTerm(t.op(), newSubs, t.boundVars(), t.getLabels());
+    }
+
+    /** Whether any variable of {@link #varMap} occurs free in {@code t}. */
+    private boolean containsSubstVar(JTerm t) {
+        final ImmutableSet<QuantifiableVariable> free = t.freeVars();
+        if (free.isEmpty()) {
+            return false;
+        }
+        final Iterator<QuantifiableVariable> it = varMap.keyIterator();
+        while (it.hasNext()) {
+            if (free.contains(it.next())) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    /** Per-variable substitution (one {@link ClashFreeSubst} pass per variable), with casts. */
+    private Term applyWithoutCastsPerVar(Term t, Services services) {
         final TermBuilder tb = services.getTermBuilder();
         final Iterator<QuantifiableVariable> it = varMap.keyIterator();
         while (it.hasNext()) {

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerUtils.java

@@ -53,10 +53,9 @@ public static ImmutableSet<QuantifiableVariable> intersect(
             ImmutableSet<? extends QuantifiableVariable> set1) {
         ImmutableSet<QuantifiableVariable> res = DefaultImmutableSet.nil();
         if (!set0.isEmpty() && !set1.isEmpty()) {
-            for (QuantifiableVariable aSet0 : set0) {
-                final QuantifiableVariable el = aSet0;
-                if (set1.contains(el)) {
-                    res = res.add(el);
+            for (QuantifiableVariable element : set0) {
+                if (set1.contains(element)) {
+                    res = res.add(element);
                 }
             }
         }
@@ -69,13 +68,16 @@ public static ImmutableSet<QuantifiableVariable> intersect(
             ImmutableSet<? extends QuantifiableVariable> set2) {
 
         final int size0 = set0.size();
-        final int size1 = set0.size();
-        final int size2 = set0.size();
+        final int size1 = set1.size();
+        final int size2 = set2.size();
 
         if (size0 == 0 || size1 == 0 || size2 == 0) {
             return DefaultImmutableSet.nil();
         }
 
+        // Intersect the two smaller sets first (smaller intermediate result), leaving the largest
+        // set for the outer intersection. The three-way result is order-independent, so this only
+        // affects work, not the outcome.
         if (size0 < size2 && size1 < size2) {
             return intersect(intersect(set0, set1), set2);
         } else if (size0 < size1 && size2 < size1) {