Fix performance regression in case of many inequalities

key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java

@@ -340,6 +340,8 @@ private int hashTermHelper(Term term, ImmutableList<QuantifiableVariable> nameAb
             hashCode = 17 * hashCode + hashJavaBlock(mod);
         } else if (op instanceof ProgramVariable pv) {
             hashCode = 17 * hashCode + pv.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY);
+        } else {
+            hashCode = 17 * hashCode + op.name().hashCode();
         }
 
         return recursiveHelper(term, nameAbstractionList, hashCode);

key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java

@@ -764,11 +764,12 @@ public void printSequent(Sequent seq) {
      * @param semiseq the semisequent to be printed
      */
     public void printSemisequent(Semisequent semiseq) {
-        for (int i = 0; i < semiseq.size(); i++) {
+        int idx = semiseq.size();
+        for (SequentFormula formula : semiseq) {
             layouter.markStartSub();
-            printConstrainedFormula(semiseq.get(i));
+            printConstrainedFormula(formula);
             layouter.markEndSub();
-            if (i != semiseq.size() - 1) {
+            if (--idx != 0) {
                 layouter.print(",").brk();
             }
         }

key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java

@@ -5,7 +5,9 @@
 
 import java.util.ArrayList;
 import java.util.Iterator;
+import java.util.LinkedHashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.concurrent.atomic.AtomicLong;
 
 import de.uka.ilkd.key.java.Services;
@@ -50,6 +52,26 @@ private void addTermIndices(ImmutableList<SequentFormula> cfmas,
         }
     }
 
+    /**
+     * Create the map <code>termIndices</code> with an index for every formula of the given
+     * semisequent.
+     *
+     * @return map with an index for each formula in the semisequent
+     */
+    private ImmutableMap<SequentFormula, TermTacletAppIndex> createTermIndices(
+            ImmutableList<SequentFormula> cfmas,
+            Services services,
+            TacletIndex tacletIndex, NewRuleListener listener) {
+        final Map<SequentFormula, TermTacletAppIndex> indices = new LinkedHashMap<>();
+        for (final SequentFormula cfma : cfmas) {
+            final PosInOccurrence pos =
+                new PosInOccurrence(cfma, PosInTerm.getTopLevel(), antec);
+            indices.put(cfma, TermTacletAppIndex.create(pos, services, tacletIndex,
+                listener, ruleFilter, indexCaches));
+        }
+        return DefaultImmutableMap.fromMap(indices);
+    }
+
     /**
      * Add an index for the given formula to the map <code>termIndices</code>. An existing entry is
      * replaced with the new one. Note: destructive, use only when constructing new index
@@ -179,7 +201,8 @@ private void updateTermIndices(
         this.antec = antec;
         this.ruleFilter = ruleFilter;
         this.indexCaches = indexCaches;
-        addTermIndices((antec ? s.antecedent() : s.succedent()).asList(), services, tacletIndex,
+        this.termIndices = createTermIndices((antec ? s.antecedent() : s.succedent()).asList(),
+            services, tacletIndex,
             listener);
     }
 

key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java

@@ -211,8 +211,7 @@ public void visit(final Term p_visited) {
         if (visitedOp instanceof SchemaVariable visitedSV && visitedOp.arity() == 0
                 && svInst.isInstantiated(visitedSV)
                 && (!(visitedOp instanceof ProgramSV visitedPSV && visitedPSV.isListSV()))) {
-            final JTerm newTerm = svInst.getTermInstantiation(visitedSV,
-                svInst.getExecutionContext(), services);
+            final JTerm newTerm = svInst.getTermInstantiation(visitedSV, services);
             pushNew(newTerm);
         } else {
             // instantiation of java block

key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java

@@ -334,7 +334,7 @@ public void visit(final Term p_visited) {
                 && svInst.isInstantiated(visitedSV)
                 && (!(visitedOp instanceof ProgramSV visitedAsPSV && visitedAsPSV.isListSV()))) {
             final JTerm newTerm = toTerm(
-                svInst.getTermInstantiation(visitedSV, svInst.getExecutionContext(), services));
+                svInst.getTermInstantiation(visitedSV, services));
             final JTerm labeledTerm = TermLabelManager.label(services, termLabelState,
                 applicationPosInOccurrence, rule, ruleApp, goal, labelHint, visited, newTerm);
             pushNew(labeledTerm);

key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java

@@ -383,16 +383,15 @@ public <T> InstantiationEntry<T> getInstantiationEntry(SchemaVariable sv) {
      * @return the Object the SchemaVariable will be instantiated with, null if no instantiation is
      *         stored
      */
-    public JTerm getTermInstantiation(SchemaVariable sv, ExecutionContext ec,
-            LogicServices services) {
+    public JTerm getTermInstantiation(SchemaVariable sv, LogicServices services) {
         final Object inst = getInstantiation(sv);
         if (inst == null) {
             return null;
         } else if (inst instanceof JTerm term) {
             return term;
         } else if (inst instanceof ProgramElement) {
             return ((Services) services).getTypeConverter()
-                    .convertToLogicElement((ProgramElement) inst, ec);
+                    .convertToLogicElement((ProgramElement) inst, getExecutionContext());
         } else {
             throw CONVERT_INSTANTIATION_EXCEPTION;
         }

key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java

@@ -59,7 +59,7 @@ protected final MatchConditions addInstantiation(JTerm term, MatchResultInfo mat
         final MatchConditions matchCond = (MatchConditions) matchResultInfo;
         final SVInstantiations inst = matchCond.getInstantiations();
 
-        final JTerm t = inst.getTermInstantiation(op, inst.getExecutionContext(), services);
+        final JTerm t = inst.getTermInstantiation(op, services);
         if (t != null) {
             // An already instantiated schema variable accepts a candidate exactly when it is
             // equal to the instantiation modulo renaming. The proof-search queue relies on this:

key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/Polynomial.java

@@ -52,16 +52,11 @@ public static Polynomial create(Term polyTerm, Services services) {
         polyTerm = TermLabelManager.removeIrrelevantLabels((JTerm) polyTerm,
             services);
 
-        Polynomial res;
-        synchronized (cache) {
-            res = cache.get(polyTerm);
-        }
+        Polynomial res = cache.get(polyTerm);
 
         if (res == null) {
             res = createHelp(polyTerm, services);
-            synchronized (cache) {
-                cache.put(polyTerm, res);
-            }
+            cache.put(polyTerm, res);
         }
         return res;
     }

key.core/src/main/java/de/uka/ilkd/key/strategy/ArithTermFeatures.java

@@ -81,6 +81,7 @@ public ArithTermFeatures(IntegerLDT numbers) {
         monomialEquation = opSub(eq, add(intF, nonNegMonomial), add(intF, monomial));
         intInEquation = add(or(leqF, geqF), sub(nonNegMonomial, polynomial));
         linearInEquation = add(or(leqF, geqF), sub(linearMonomial, polynomial));
+        intRelationOp = add(or(leqF, geqF, eqF), sub(intF, intF));
         intRelation = add(or(leqF, geqF, eqF), sub(add(intF, nonNegMonomial), polynomial));
 
         notContainsProduct = rec(any(), ifZero(mulF, not(sub(not(literal), not(literal)))));
@@ -147,6 +148,7 @@ public ArithTermFeatures(IntegerLDT numbers) {
     final TermFeature monomialEquation;
     final TermFeature intInEquation;
     final TermFeature linearInEquation;
+    final TermFeature intRelationOp;
     final TermFeature intRelation;
 
     final TermFeature notContainsProduct;

key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java

@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.strategy.feature.*;
 import de.uka.ilkd.key.strategy.termProjection.*;
 import de.uka.ilkd.key.strategy.termgenerator.MultiplesModEquationsGenerator;
+import de.uka.ilkd.key.strategy.termgenerator.RelevantSequentFormulasGenerator;
 import de.uka.ilkd.key.strategy.termgenerator.RootsGenerator;
 import de.uka.ilkd.key.strategy.termgenerator.SuperTermGenerator;
 
@@ -340,9 +341,7 @@ private void setupPolySimp(RuleSetDispatchFeature d, IntegerLDT numbers) {
                 applyTF("distSummand1", tf.polynomial),
                 ifZero(applyTF("distCoeff", tf.monomial), longConst(-15),
                     applyTF("distCoeff", tf.polynomial)),
-                applyTF("distSummand0", tf.polynomial),
-
-                applyTF("distSummand1", tf.polynomial), longConst(-35)));
+                longConst(-35)));
 
         // category "direct equations"
 
@@ -754,13 +753,16 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature baseCost
          * instOf ( "multLeft" ), instOf ( "multFacLeft" ), sub ( intRel, 0 ) ) ) ) ) );
          */
 
-        final Feature totallyBounded = not(sum(intRel, SequentFormulasGenerator.sequent(),
-            not(add(applyTF(intRel, tf.intRelation), InEquationMultFeature
-                    .totallyBounded(instOf("multLeft"), instOf("multFacLeft"), sub(intRel, 0))))));
+        final Feature intRelation = applyTF(intRel, tf.intRelation);
+        final var relevantSequentFormulas =
+            RelevantSequentFormulasGenerator.sequent(tf.intRelationOp);
 
-        final Feature exactlyBounded = not(sum(intRel, SequentFormulasGenerator.sequent(),
-            not(add(applyTF(intRel, tf.intRelation), InEquationMultFeature
-                    .exactlyBounded(instOf("multLeft"), instOf("multFacLeft"), sub(intRel, 0))))));
+        final Feature totallyBounded = not(sum(intRel, relevantSequentFormulas,
+            not(add(InEquationMultFeature
+                    .totallyBounded(instOf("multLeft"), instOf("multFacLeft"), sub(intRel, 0)),
+                intRelation))));
+        final Feature exactlyBounded = new IsBoundedByInequationFeature(
+            instOf("multLeft"), instOf("multFacLeft"), tf.intRelation);
 
         // this is a bit hackish
         //
@@ -972,7 +974,7 @@ private Feature allowInEqStrengthening(TermBuffer atom, TermBuffer literal) {
     private Feature succIntEquationExists() {
         final TermBuffer succFor = new TermBuffer();
 
-        return not(sum(succFor, SequentFormulasGenerator.succedent(),
+        return not(sum(succFor, RelevantSequentFormulasGenerator.succedent(tf.intEquation),
             not(applyTF(succFor, tf.intEquation))));
     }
 

key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java

@@ -13,11 +13,11 @@
 import de.uka.ilkd.key.util.Debug;
 
 import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.indexing.FormulaTagManager;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
-import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.NumberRuleAppCost;
 import org.key_project.prover.strategy.costbased.RuleAppCost;
@@ -348,7 +348,7 @@ protected boolean assumesFormulasStillValid(Goal p_goal) {
 
         final Iterator<AssumesFormulaInstantiation> it =
             getTacletApp().assumesFormulaInstantiations().iterator();
-        final Sequent seq = p_goal.sequent();
+        final FormulaTagManager tags = p_goal.getFormulaTagManager();
 
         while (it.hasNext()) {
             final AssumesFormulaInstantiation assumesInstantiations2 = it.next();
@@ -359,8 +359,10 @@ protected boolean assumesFormulasStillValid(Goal p_goal) {
                     assumesInstantiations2);
                 throw new IllegalStateException(
                     "Unexpected assume-instantiation" + assumesInstantiations2);
-            } else if (!(assumesInst.inAntecedent() ? seq.antecedent() : seq.succedent())
-                    .contains(assumesInst.getSequentFormula())) {
+            } else if (tags.getTagForPos(assumesInst.toPosInOccurrence()) == null) {
+                // checks whether assumesInst still occurs in sequent,
+                // replaces linear lookup via Sequent#contains by
+                // hashmap lookup using the tag manager
                 return false;
             }
         }

key.core/src/main/java/de/uka/ilkd/key/strategy/feature/IsBoundedByInequationFeature.java

@@ -0,0 +1,110 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.strategy.feature;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
+
+import org.key_project.logic.Term;
+import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.sequent.Sequent;
+import org.key_project.prover.sequent.SequentFormula;
+import org.key_project.prover.strategy.costbased.MutableState;
+import org.key_project.prover.strategy.costbased.TopRuleAppCost;
+import org.key_project.prover.strategy.costbased.feature.VolatileCost;
+import org.key_project.prover.strategy.costbased.termProjection.ProjectionToTerm;
+import org.key_project.prover.strategy.costbased.termfeature.TermFeature;
+import org.key_project.util.ConcurrentLruCache;
+
+
+/**
+ * Checks whether the product of two monomials has the same variables as the left side of
+ * an inequation in the sequent. Required to bound the number of cross-multiplications.
+ */
+@VolatileCost
+public final class IsBoundedByInequationFeature extends BinaryTacletAppFeature {
+
+    private final ProjectionToTerm<Goal> mult1;
+    private final ProjectionToTerm<Goal> mult2;
+    private final TermFeature isRelation;
+
+    /**
+     * cached information about the variables occurring on the left side of an inequation
+     * The sequent is the secondary cache key to be correct when pruning.
+     */
+    private record InequationInfo(Sequent sequent, Set<Map<Term, Integer>> variables) {
+    }
+
+    private final Map<Goal, InequationInfo> relations = new ConcurrentLruCache<>(200);
+
+    /**
+     * @param mult1 the left side of the first inequation to be multiplied
+     * @param mult2 the left side of the second inequation to be multiplied
+     * @param inEquationFilter term feature describing the shape of the inequation
+     */
+    public IsBoundedByInequationFeature(ProjectionToTerm<Goal> mult1, ProjectionToTerm<Goal> mult2,
+            TermFeature inEquationFilter) {
+        this.mult1 = mult1;
+        this.mult2 = mult2;
+        this.isRelation = inEquationFilter;
+    }
+
+    @Override
+    protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
+        final Services services = goal.proof().getServices();
+        final Monomial first = Monomial.create(mult1.toTerm(app, pos, goal, mState), services);
+        final Monomial second = Monomial.create(mult2.toTerm(app, pos, goal, mState), services);
+        return getInEquations(goal, mState).contains(variables(first, second));
+    }
+
+    private Set<Map<Term, Integer>> getInEquations(Goal goal, MutableState mState) {
+        final Sequent sequent = goal.sequent();
+        final InequationInfo cached = relations.get(goal);
+        if (cached != null && cached.sequent() == sequent) {
+            return cached.variables();
+        }
+        final Services services = goal.proof().getServices();
+        final Set<Map<Term, Integer>> variables = new HashSet<>();
+        for (SequentFormula sf : sequent) {
+            final Term formula = sf.formula();
+            if (!(isRelation.compute(formula, mState, services) instanceof TopRuleAppCost)) {
+                variables.add(variables(Monomial.create(formula.sub(0), services)));
+            }
+        }
+        relations.put(goal, new InequationInfo(sequent, variables));
+        return variables;
+    }
+
+    /**
+     * @return how often each variable occurs in the monomial
+     */
+    private static Map<Term, Integer> variables(Monomial monomial) {
+        final Map<Term, Integer> counts = new HashMap<>();
+        count(monomial, counts);
+        return counts;
+    }
+
+    /**
+     * @return how often each variable occurs in the product of the two monomials
+     */
+    private static Map<Term, Integer> variables(Monomial first, Monomial second) {
+        final Map<Term, Integer> counts = new HashMap<>();
+        count(first, counts);
+        count(second, counts);
+        return counts;
+    }
+
+    private static void count(Monomial monomial, Map<Term, Integer> counts) {
+        for (Term part : monomial.getParts()) {
+            counts.merge(part, 1, Integer::sum);
+        }
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java

@@ -61,7 +61,7 @@ public boolean check(PosInOccurrence pio) {
         if (pio.posInTerm() != null) {
             final PIOPathIterator it = pio.iterator();
             while (pol != 0 && it.next() != -1) {
-                pol = checkOperator(pio.subTerm().op(), it.getChild(), pol);
+                pol = checkOperator(it.getSubTerm().op(), it.getChild(), pol);
             }
         }