diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java index fdce3a37a67..e82a7e11f11 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java @@ -340,6 +340,8 @@ private int hashTermHelper(Term term, ImmutableList 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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 6fb286cd17b..7259ddd7a48 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/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(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java index 351047615b7..3b52de2d962 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java +++ b/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 cfmas, } } + /** + * Create the map termIndices with an index for every formula of the given + * semisequent. + * + * @return map with an index for each formula in the semisequent + */ + private ImmutableMap createTermIndices( + ImmutableList cfmas, + Services services, + TacletIndex tacletIndex, NewRuleListener listener) { + final Map 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 termIndices. 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); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java index 89bd3118b25..eb876599079 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java +++ b/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 diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java index 6c57192f287..f0094ea6a9b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java +++ b/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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java index 879d8fad9c3..bda5a01f8b1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java @@ -383,8 +383,7 @@ public InstantiationEntry 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; @@ -392,7 +391,7 @@ public JTerm getTermInstantiation(SchemaVariable sv, ExecutionContext ec, return term; } else if (inst instanceof ProgramElement) { return ((Services) services).getTypeConverter() - .convertToLogicElement((ProgramElement) inst, ec); + .convertToLogicElement((ProgramElement) inst, getExecutionContext()); } else { throw CONVERT_INSTANTIATION_EXCEPTION; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java index aa0c7b29f38..4389531bdc1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java +++ b/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: diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/Polynomial.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/Polynomial.java index 146affa7fc1..66738f546d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/Polynomial.java +++ b/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; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/ArithTermFeatures.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/ArithTermFeatures.java index 3bf7238141c..d7595cad1aa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/ArithTermFeatures.java +++ b/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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java index 4896a823ea5..5c0458c1fcb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java +++ b/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)))); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java index e7c51670ab5..5e513d296c1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java +++ b/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 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; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/IsBoundedByInequationFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/IsBoundedByInequationFeature.java new file mode 100644 index 00000000000..82e930c6f7c --- /dev/null +++ b/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 mult1; + private final ProjectionToTerm 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> variables) { + } + + private final Map 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 mult1, ProjectionToTerm 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> 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> 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 variables(Monomial monomial) { + final Map counts = new HashMap<>(); + count(monomial, counts); + return counts; + } + + /** + * @return how often each variable occurs in the product of the two monomials + */ + private static Map variables(Monomial first, Monomial second) { + final Map counts = new HashMap<>(); + count(first, counts); + count(second, counts); + return counts; + } + + private static void count(Monomial monomial, Map counts) { + for (Term part : monomial.getParts()) { + counts.merge(part, 1, Integer::sum); + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java index d8a8f4ae084..8f39d322a2a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java +++ b/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); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RelevantSequentFormulasGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RelevantSequentFormulasGenerator.java new file mode 100644 index 00000000000..4ab8a0a3575 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RelevantSequentFormulasGenerator.java @@ -0,0 +1,123 @@ +/* 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.termgenerator; + +import java.util.ArrayList; +import java.util.Iterator; +import java.util.List; +import java.util.Map; + +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.logic.Term; +import org.key_project.prover.rules.RuleApp; +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.termfeature.TermFeature; +import org.key_project.prover.strategy.costbased.termgenerator.TermGenerator; +import org.key_project.util.ConcurrentLruCache; + +/** + * Enumerates the formulas of the sequent that satisfy a term feature. + * + *

+ * A feature summing over the sequent is evaluated once per rule application candidate, while the + * formulas it is interested in change only when the sequent does. The selection is therefore kept + * per goal and reused while the goal holds the sequent it was made from: candidates of one + * round share one selection, and the sequent is walked once instead of once per candidate. + */ +@VolatileCost +public final class RelevantSequentFormulasGenerator implements TermGenerator { + + /** + * The selection of one goal, computed from and valid exactly for one sequent. + * + * @param sequent the sequent the selection was made from, compared by identity: the selection + * is a function of the sequent's formulas, so the same object carries the same + * selection. The goal's time is no substitute, since pruning rewinds it while the goal + * object lives on. + * @param formulas the formulas satisfying the feature, in sequent order + */ + private record Selection(Sequent sequent, List formulas) { + } + + /** Which formulas of the sequent to offer, before the feature selects among them. */ + private enum Part { + SEQUENT, ANTECEDENT, SUCCEDENT + } + + private final Part part; + + private final TermFeature accepted; + + /** + * Bounded and held per generator, so a selection lives no longer than the strategy of its + * proof and a pruned goal costs one recomputation rather than a leak. + */ + private final Map selections = new ConcurrentLruCache<>(200); + + private RelevantSequentFormulasGenerator(Part part, TermFeature accepted) { + this.part = part; + this.accepted = accepted; + } + + /** + * @param accepted decides which formulas are enumerated; it must be a function of the formula + * alone, since its verdict is reused for every candidate of a round + * @return the formulas of the sequent the feature accepts + */ + public static RelevantSequentFormulasGenerator sequent(TermFeature accepted) { + return new RelevantSequentFormulasGenerator(Part.SEQUENT, accepted); + } + + /** + * @param accepted decides which formulas are enumerated, see {@link #sequent} + * @return the formulas of the antecedent the feature accepts + */ + public static RelevantSequentFormulasGenerator antecedent(TermFeature accepted) { + return new RelevantSequentFormulasGenerator(Part.ANTECEDENT, accepted); + } + + /** + * @param accepted decides which formulas are enumerated, see {@link #sequent} + * @return the formulas of the succedent the feature accepts + */ + public static RelevantSequentFormulasGenerator succedent(TermFeature accepted) { + return new RelevantSequentFormulasGenerator(Part.SUCCEDENT, accepted); + } + + @Override + public Iterator generate(RuleApp app, PosInOccurrence pos, Goal goal, + MutableState mState) { + final Sequent sequent = goal.sequent(); + final Selection cached = selections.get(goal); + if (cached != null && cached.sequent() == sequent) { + return cached.formulas().iterator(); + } + final List formulas = select(goal, mState); + selections.put(goal, new Selection(sequent, formulas)); + return formulas.iterator(); + } + + private List select(Goal goal, MutableState mState) { + final var services = goal.proof().getServices(); + final List formulas = new ArrayList<>(); + final Iterable source = switch (part) { + case SEQUENT -> goal.sequent(); + case ANTECEDENT -> goal.sequent().antecedent(); + case SUCCEDENT -> goal.sequent().succedent(); + }; + for (SequentFormula sf : source) { + final Term formula = sf.formula(); + if (!(accepted.compute(formula, mState, services) instanceof TopRuleAppCost)) { + formulas.add(formula); + } + } + return formulas; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java index 501d5a3787f..9c30727d2f3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java @@ -20,6 +20,7 @@ import org.key_project.logic.op.SortedOperator; import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.PIOPathIterator; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.TopRuleAppCost; @@ -28,11 +29,13 @@ import org.key_project.prover.strategy.costbased.termgenerator.TermGenerator; import org.key_project.util.collection.ImmutableArray; -// Generates the find's ANCESTOR terms (upwards from the find position). The connectives along the -// find path are stable for a surviving application, but a generated ancestor term as a whole also -// carries the siblings of that path, which an independent rewrite can change while the find subterm -// survives. So a feature summing over these ancestors is fixed only while the find FORMULA is -// unchanged -- weakly stable, not fully stable. +/** + * Generates the terms upward a given (usually the find-)position and + * allows to iterate over those in order to check e.g. whether the + * position is below an update or quantifier. + * + * As it only looks upwards, the computed cost is weak stable + */ @WeakStableCost public abstract class SuperTermGenerator implements TermGenerator { @@ -82,16 +85,8 @@ private boolean generateFurther(Term t, MutableState mState, Services services) return !(cond.compute(t, mState, services) instanceof TopRuleAppCost); } - // same data flow as the enclosing class: ancestors of the focus position @WeakStableCost abstract static class SuperTermWithIndexGenerator extends SuperTermGenerator { - // Both are fixed at construction from the proof's services (one generator is built per - // proof and shared by all goals). They used to be lazily filled by generate(), which runs - // during proof search: under the multi-core prover several workers raced that lazy write, - // and binFunc is a freshly created operator, so a worker could read a half-initialised or - // foreign operator. Computing them once in the constructor removes the race; the value is - // unchanged, since goal.proof().getServices() is the same services the strategy was built - // with. private final Services services; private final Operator binFunc; @@ -183,28 +178,38 @@ public void validTopLevelException(Term term) } class UpwardsIterator implements Iterator { - private PosInOccurrence currentPos; + private final Term[] ancestors; + private final int[] childIndices; + private int next; private final MutableState mState; private final Services services; private UpwardsIterator(PosInOccurrence startPos, MutableState mState, Services services) { - this.currentPos = startPos; this.mState = mState; this.services = services; + final int depth = startPos.depth(); + this.ancestors = new Term[depth]; + this.childIndices = new int[depth]; + final PIOPathIterator it = startPos.iterator(); + int i = depth; + while (it.next() != -1) { + i--; + ancestors[i] = it.getSubTerm(); + childIndices[i] = it.getChild(); + } } @Override public boolean hasNext() { - return currentPos != null && !currentPos.isTopLevel(); + return next < ancestors.length; } @Override public Term next() { - final int child = currentPos.getIndex(); - currentPos = currentPos.up(); - final Term res = generateOneTerm(currentPos.subTerm(), child); + final Term res = generateOneTerm(ancestors[next], childIndices[next]); + next++; if (!generateFurther(res, mState, services)) { - currentPos = null; + next = ancestors.length; } return res; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java index d4b03156c9d..91d8140c038 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java @@ -282,7 +282,7 @@ private JTerm instantiateAndCheck(JTerm term, UpdateSV u, SchemaVariable tOrPhi, } return ((de.uka.ilkd.key.rule.MatchConditions) mc).getInstantiations() - .getTermInstantiation(result, null, TacletForTests.services()); + .getTermInstantiation(result, TacletForTests.services()); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestDropEffectlessElementary.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestDropEffectlessElementary.java index e45f58a6bb1..afb6263a706 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestDropEffectlessElementary.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestDropEffectlessElementary.java @@ -207,7 +207,7 @@ private JTerm applyDrop(JTerm term) { return term; } - return mc.getInstantiations().getTermInstantiation(result, null, TacletForTests.services()); + return mc.getInstantiations().getTermInstantiation(result, TacletForTests.services()); } } diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java index d8fb9338da3..9fbaaa01ff5 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java @@ -4,6 +4,7 @@ package org.key_project.util.collection; import java.util.Iterator; +import java.util.Map.Entry; import java.util.Objects; import org.key_project.util.Strings; @@ -26,6 +27,21 @@ public static DefaultImmutableMap nilMap() { return (DefaultImmutableMap) EMPTY_MAP; } + /** + * Creates an immutable map from the given map maintaining the order from the given {@code map} + * (if the given {@code map} supports stable ordering) + * + * @param map the map whose entries the result is to hold + * @return the persistent map holding exactly the entries of {@code map} + */ + public static ImmutableMap fromMap(java.util.Map map) { + DefaultImmutableMap result = nilMap(); + for (Entry e : map.entrySet()) { + result = new DefaultImmutableMap<>(new MapEntry<>(e.getKey(), e.getValue()), result); + } + return result; + } + /** * The map this map builds on. Lookups will also consider entries in this map if the key * does not match {@link #entry}. @@ -72,6 +88,7 @@ public ImmutableMap put(S key, T value) { return new DefaultImmutableMap<>(new MapEntry<>(key, value), this.remove(key)); } + /** * Retrieves the value mapped to key in this map. *