diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java index 6cff4cc61c9..f085c4c31df 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java @@ -23,8 +23,8 @@ import de.uka.ilkd.key.strategy.feature.AbstractBetaFeature.TermInfo; import de.uka.ilkd.key.strategy.feature.AppliedRuleAppsNameCache; import de.uka.ilkd.key.strategy.quantifierHeuristics.ClausesGraph; -import de.uka.ilkd.key.strategy.quantifierHeuristics.Metavariable; import de.uka.ilkd.key.strategy.quantifierHeuristics.TriggersSet; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; import org.key_project.logic.sort.Sort; import org.key_project.prover.proof.SessionCaches; diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java index d54345bd94b..89564560b0e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java @@ -72,6 +72,16 @@ public ParametricFunctionInstance getSeqGet(Sort instanceSort, TermServices serv ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); } + /** + * Whether the operator is an instance of {@code seqGet}, for any element sort. + * + * @param op an operator + * @return whether {@code op} reads a sequence element + */ + public boolean isSeqGetOp(org.key_project.logic.op.Operator op) { + return op instanceof ParametricFunctionInstance pfi && pfi.getBase() == seqGet; + } + public Function getSeqLen() { return seqLen; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java index 830a045c44b..5604666d43d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java @@ -27,7 +27,7 @@ import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.rule.inst.SVInstantiations.UpdateLabelPair; import de.uka.ilkd.key.speclang.HeapContext; -import de.uka.ilkd.key.strategy.quantifierHeuristics.Metavariable; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; import org.key_project.logic.Name; import org.key_project.logic.Namespace; 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 e82a7e11f11..e3032d6750d 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 @@ -231,7 +231,8 @@ private static NameAbstractionTable handleJava(JavaBlock jb0, JavaBlock jb1, * Moved here from {@link JavaBlock} while refactoring equalsModRenaming in {@link Term}. * As the implementation of equalsModRenaming in {@link JavaBlock} was only used in * {@link RenamingTermProperty#handleJava(JavaBlock, JavaBlock, NameAbstractionTable)} - * and the deprecated class de.uka.ilkd.key.strategy.quantifierHeuristics.EqualityConstraint, + * and the deprecated class + * de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.EqualityConstraint, * it is now only a helper method in {@link RenamingTermProperty}. * * @param jb1 the first {@link JavaBlock} diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java index c2f8d7a1794..92e3b7c5405 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.macros; import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.strategy.RuleAppCostCollector; import de.uka.ilkd.key.strategy.Strategy; @@ -34,12 +35,22 @@ public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, public > RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, G goal, MutableState mState) { - if (!isApprovedApp(app, pio, (de.uka.ilkd.key.proof.Goal) goal)) { + if (assumesMatched(app) && !isApprovedApp(app, pio, (de.uka.ilkd.key.proof.Goal) goal)) { return TopRuleAppCost.INSTANCE; } return delegate.computeCost(app, pio, goal, mState); } + /** + * Checks that the assumes clause of a taclet is empty or instantiated + * + * @param app the rule application being costed + * @return whether a taclet application has its assumes clause matched + */ + private static boolean assumesMatched(RuleApp app) { + return !(app instanceof TacletApp tacletApp) || tacletApp.assumesInstantionsComplete(); + } + @Override public void instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal, RuleAppCostCollector collector) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java index 4b6338c6e8d..96b9ad5a96e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java @@ -348,7 +348,7 @@ public ImmutableArray replace( for (int i = 0, n = vars.size(); i < n; i++) { QuantifiableVariable qv = vars.get(i); QuantifiableVariable newQv = (QuantifiableVariable) replace(qv); - result[i++] = newQv; + result[i] = newQv; if (newQv != qv) { changed = true; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java index 32d31be8906..9403d153d14 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java @@ -18,7 +18,7 @@ import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.rule.inst.SVInstantiations; -import de.uka.ilkd.key.strategy.quantifierHeuristics.Metavariable; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; import de.uka.ilkd.key.util.Debug; import org.key_project.logic.LogicServices; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java index 3a6b90860ca..6ad2fbbceb8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java @@ -17,6 +17,8 @@ import de.uka.ilkd.key.rule.UseOperationContractRule; import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.strategy.StrategyFactory; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.QuantifierTheorySupport; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.QuantifierTheorySupports; import org.key_project.logic.Name; import org.key_project.prover.engine.GoalChooserFactory; @@ -211,4 +213,13 @@ default List prepareInitConfig(InitConfig baseConfig, @Nullable Configuration additionalProfileOptions) { return Collections.emptyList(); } + + /// The theories the quantifier heuristic consults for the terms of this profile, in the order + /// it consults them. A profile over other terms returns its own. + /// + /// @param classic whether the classic trigger selection is in effect + /// @return the theories, never empty + default List getTheorySupports(boolean classic) { + return classic ? QuantifierTheorySupports.CLASSIC : QuantifierTheorySupports.JAVA_DL; + } } 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 f0094ea6a9b..709897670b1 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 @@ -234,7 +234,7 @@ protected void pushNew(Object t) { /** * the method is only still invoked to allow the - * {@link de.uka.ilkd.key.strategy.quantifierHeuristics.ConstraintAwareSyntacticalReplaceVisitor} + * {@link de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.ConstraintAwareSyntacticalReplaceVisitor} * to recursively * replace meta variables */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index 2dc7bdb0162..8543a0a52be 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -397,7 +397,7 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { if (quantifierInstantiatedEnabled()) { final TermBuffer varInst = new TermBuffer(); final Feature branchPrediction = InstantiationCostScalerFeature - .create(InstantiationCost.create(varInst, classicTriggers()), + .create(InstantiationCost.create(varInst, triggerTreatment()), allowQuantifierSplitting()); bindRuleSet(d, "gamma", @@ -406,7 +406,7 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { add(ff.quantifiedClauseSet, instQuantifiersWithQueries() ? longTermConst(0) : ff.notContainsExecutable)), - forEach(varInst, HeuristicInstantiation.forOption(classicTriggers()), + forEach(varInst, HeuristicInstantiation.forOption(triggerTreatment()), add(instantiate("t", varInst), add(branchPrediction, CostBand.DEFAULT.at(10), @@ -432,11 +432,11 @@ private void setupQuantifierInstantiationApproval(RuleSetDispatchFeature d) { final TermBuffer varInst = new TermBuffer(); bindRuleSet(d, "gamma", add(isInstantiated("t"), - not(sum(varInst, HeuristicInstantiation.forOption(classicTriggers()), + not(sum(varInst, HeuristicInstantiation.forOption(triggerTreatment()), not(eq(instOf("t"), varInst)))), InstantiationCostScalerFeature.create( - InstantiationCost.create(instOf("t"), classicTriggers()), - CostBand.DEFAULT.cost()))); + InstantiationCost.create(instOf("t"), triggerTreatment()), + longConst(0)))); final TermBuffer splitInst = new TermBuffer(); bindRuleSet(d, "triggered", @@ -628,9 +628,9 @@ private String triggersOption() { return strategyProperties.getProperty(StrategyProperties.TRIGGERS_OPTIONS_KEY); } - /** whether the classic trigger selection is in effect for this strategy */ - private boolean classicTriggers() { - return StrategyProperties.TRIGGERS_CLASSIC.equals(triggersOption()); + /** how much the quantifier heuristic is told about the theories in this strategy */ + private TriggerTreatment triggerTreatment() { + return TriggerTreatment.forOption(triggersOption()); } private boolean quantifierInstantiatedEnabled() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java index 104acbd03fe..37c61e8a4cb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java @@ -36,13 +36,13 @@ public class JFOLStrategyFactory implements StrategyFactory { might cause proof splitting."""; public static final String TOOL_TIP_TRIGGERS_BEST = - "Instantiate quantified formulas using knowledge about arrays and the heap, with the" - + " most informative ordering of the instances to try. Recommended.
" - + "Adds a small per-step cost on very large proof states."; + "" + + "Uses advanced knowledge about heap theory (in particular arrays) to find good instantiations." + + "Can deal with reads over different heaps (e.g., anon)
" + + "Slightly slower per proof step on very large proofs."; public static final String TOOL_TIP_TRIGGERS_GOOD = - "Instantiate quantified formulas using knowledge about arrays and the heap, with a" - + " lighter-weight ordering of the instances.
" - + "Close to Best, with less per-step overhead on large proof states."; + "Similar to Best but does not consider different heaps.
" + + "Slightly faster per proof step on very large proofs."; public static final String TOOL_TIP_TRIGGERS_CLASSIC = "Instantiate quantified formulas without the knowledge about arrays and the heap, and" + " without ordering the instances.
" diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java index 9e978ea3c89..c4b714c87b3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java @@ -125,4 +125,10 @@ private HeapSelectCost() {} /** {@code hide_auxiliary_eq_const}: same, for the constant-valued case. */ static final long HIDE_AUXILIARY_EQ_CONST = -500; + + /** + * {@code derive_inequality}: two objects whose reads of one field differ are different; the + * disequality feeds the assumes clauses of the select simplification rules. + */ + static final long DERIVE_INEQUALITY = -2000; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index 2a4ab73d523..9104878aae2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java @@ -8,6 +8,7 @@ import java.util.concurrent.atomic.AtomicLong; import de.uka.ilkd.key.ldt.HeapLDT; +import de.uka.ilkd.key.logic.op.Equality; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.BuiltInRule; @@ -184,6 +185,7 @@ private RuleSetDispatchFeature setupCostComputationF() { final int pullOutHeapSize = getHeapSizeBound(); bindRuleSet(d, "pull_out_heap", pullOutHeapSize <= 0 ? inftyConst() : pullOutHeap(pullOutHeapSize)); + bindRuleSet(d, "derive_inequality", longConst(DERIVE_INEQUALITY)); bindRuleSet(d, "simplify_heap_high_costs", inftyConst()); bindRuleSet(d, "javaIntegerSemantics", @@ -493,6 +495,19 @@ protected Feature setupApprovalF() { private RuleSetDispatchFeature setupApprovalDispatcher() { final RuleSetDispatchFeature d = new RuleSetDispatchFeature(); + // Only derive a disequality that is not known yet. The same disequality follows from + // every location the two objects read differently, so a duplicate-application check does + // not recognise those derivations as duplicates: their instantiations differ while their + // conclusion does not. Comparing the conclusion against the succedent does. + final TermBuffer succedentFormula = new TermBuffer(); + final TermBuffer firstObject = new TermBuffer(); + final TermBuffer secondObject = new TermBuffer(); + bindRuleSet(d, "derive_inequality", + let(firstObject, instOf("o"), let(secondObject, instOf("o2"), + sum(succedentFormula, SequentFormulasGenerator.succedent(), + not(applyTF(succedentFormula, + or(opSub(Equality.EQUALS, eq(firstObject), eq(secondObject)), + opSub(Equality.EQUALS, eq(secondObject), eq(firstObject))))))))); bindRuleSet(d, "inReachableStateImplication", NonDuplicateAppModPositionFeature.INSTANCE); bindRuleSet(d, "limitObserver", NonDuplicateAppModPositionFeature.INSTANCE); bindRuleSet(d, "partialInvAxiom", NonDuplicateAppModPositionFeature.INSTANCE); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java index 872de37dbbc..b9a45c44fc5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java @@ -89,11 +89,11 @@ public final class StrategyProperties extends Properties { /** * The quantifier instantiation treatment. {@link #TRIGGERS_BEST} and {@link #TRIGGERS_GOOD} - * both use the theory-aware trigger selection (heap and array reads); they differ in how tied - * candidates are ordered, {@code BEST} by the proving-polarity connection to the sequent, - * {@code GOOD} by generation with a lighter ordering. {@link #TRIGGERS_CLASSIC} uses the plain - * equality-and-integer trigger selection with no candidate ordering, matching the previous - * behaviour. + * both select triggers with knowledge of the heap and of array reads, and order tied + * candidates, {@code BEST} by their connection to the sequent, {@code GOOD} more cheaply. Only + * {@code BEST} matches a trigger against reads over another heap, which is how a property + * established before a method call is used after it. {@link #TRIGGERS_CLASSIC} selects with + * equality and integer knowledge only and does not order candidates. */ public static final String TRIGGERS_OPTIONS_KEY = "TRIGGERS_OPTIONS_KEY"; public static final String TRIGGERS_BEST = "TRIGGERS_BEST"; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java index 4d36ebde6a9..d75d839fc27 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java @@ -3,9 +3,13 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.JModality; import de.uka.ilkd.key.logic.op.Quantifier; import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.TheoryReasoning; import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; @@ -14,30 +18,64 @@ import org.key_project.util.collection.ImmutableMap; import org.key_project.util.collection.ImmutableSet; +/** + * Matches a trigger against a ground term of the sequent by descending both in step, binding a + * quantified variable to whatever ground subterm stands at its position. Operators and arities + * have to agree at every position above the variables, so the trigger's structure is fixed and + * only the variables are open. The trigger {@code select(heap, a, arr(i))} with quantified + * {@code i} matches the sequent term {@code select(heap, a, arr(3))} and binds {@code i} to + * {@code 3}; it does not match {@code select(heap2, a, arr(3))}, whose heap differs, nor + * {@code select(heap, b, arr(3))}. + * + * This is the weaker of the two matchings the heuristic uses. Unification (see + * {@link TwoSidedMatching}) binds metavariables on the trigger's side as well, so the trigger + * {@code select(H, a, arr(i))}, whose metavariable {@code H} stands for any heap, matches + * {@code select(heap2, a, arr(3))}, which basic matching cannot do. What unification does not + * offer is a place to intervene: it answers for the two terms at once and does not report which + * pair of subterms defeated it. Basic matching descends position by position with the ground term + * fixed, so a failing comparison stays located at the position where it failed and can be handed + * to a theory there: where {@code arr(base + i)} meets {@code arr(x)} the integer theory solves + * {@code base + i = x} for {@code i} (see {@link TheoryReasoning#solveForVariable}) and + * the match continues with {@code i = x - base}. + */ class BasicMatching { private BasicMatching() {} /** - * matching trigger to targetTerm recursively + * Matches trigger against targetTerm and its subterms, comparing + * the two structures alone. * * @param trigger a uni-trigger - * @param targetTerm a gound term - * @return all substitution found from this matching + * @param targetTerm a ground term + * @return all substitutions found */ - static ImmutableSet getSubstitutions(Term trigger, Term targetTerm) { + static ImmutableSet getSyntacticSubstitutions(Term trigger, Term targetTerm) { + return getSubstitutions(trigger, targetTerm, null); + } + + /** + * As above, and where a comparison fails the theories are asked whether they can solve it. + * + * @param trigger a uni-trigger + * @param targetTerm a ground term + * @param services the theories' operators, or null to compare the structures alone + * @return all substitutions found + */ + static ImmutableSet getSubstitutions(Term trigger, Term targetTerm, + Services services) { ImmutableSet allsubs = DefaultImmutableSet.nil(); if (targetTerm.freeVars().size() > 0 || targetTerm.op() instanceof Quantifier) { return allsubs; } - final Substitution subst = match(trigger, targetTerm); + final Substitution subst = match(trigger, targetTerm, services); if (subst != null) { allsubs = allsubs.add(subst); } final var op = targetTerm.op(); if (!(op instanceof JModality || op instanceof UpdateApplication)) { for (int i = 0; i < targetTerm.arity(); i++) { - allsubs = allsubs.union(getSubstitutions(trigger, targetTerm.sub(i))); + allsubs = allsubs.union(getSubstitutions(trigger, targetTerm.sub(i), services)); } } return allsubs; @@ -49,57 +87,125 @@ static ImmutableSet getSubstitutions(Term trigger, Term targetTerm * @return all substitution that a given pattern(ex: a term of a uniTrigger) match in the * instance. */ - private static Substitution match(Term pattern, Term instance) { - final ImmutableMap map = - matchRec(DefaultImmutableMap.nilMap(), pattern, instance); - if (map == null) { + private static Substitution match(Term pattern, Term instance, Services services) { + final Bindings bindings = + matchRec(Bindings.EMPTY, pattern, instance, services, false); + if (bindings == null) { return null; } - return new Substitution(map); + return new Substitution(bindings.variables(), bindings.solvedArrayIndex()); + } + + /** + * What a match has bound so far. Only {@code variables} is the result. A metavariable may + * occur at more than one position of a trigger and has to stand for the same term at each, + * which is what {@code metavariables} checks; it is dropped when the match ends. + * + * @param variables the instantiation of the trigger's quantified variables + * @param metavariables the terms the trigger's metavariables stand for + */ + private record Bindings(ImmutableMap variables, + ImmutableMap metavariables, boolean solvedArrayIndex) { + + static final Bindings EMPTY = new Bindings(DefaultImmutableMap.nilMap(), + DefaultImmutableMap.nilMap(), false); + + Bindings withVariable(QuantifiableVariable var, Term instance) { + final Term bound = variables.get(var); + if (bound == null) { + return new Bindings(variables.put(var, instance), metavariables, solvedArrayIndex); + } + return bound.equals(instance) ? this : null; + } + + Bindings withMetavariable(Metavariable metavariable, Term instance) { + final Term bound = metavariables.get(metavariable); + if (bound == null) { + return new Bindings(variables, metavariables.put(metavariable, instance), + solvedArrayIndex); + } + return bound.equals(instance) ? this : null; + } + + Bindings withSolution(ImmutableMap solved) { + return new Bindings(solved, metavariables, true); + } } /** * match the pattern to instance recursively. */ - private static ImmutableMap matchRec( - ImmutableMap varMap, Term pattern, Term instance) { + private static Bindings matchRec(Bindings bindings, Term pattern, Term instance, + Services services, boolean nested) { final var patternOp = pattern.op(); - if (patternOp instanceof QuantifiableVariable) { - return mapVarWithCheck(varMap, (QuantifiableVariable) patternOp, instance); + if (patternOp instanceof QuantifiableVariable var) { + return bindings.withVariable(var, instance); + } + + // A metavariable stands for any term of its sort, so comparing it as a rigid symbol fails + // against every concrete heap. Bind it like a variable instead, but only when matching for + // instantiation: trigger selection matches too, and binding there would change which + // candidates become triggers. + if (services != null && patternOp instanceof Metavariable metavariable + && pattern.sort() == instance.sort()) { + return bindings.withMetavariable(metavariable, instance); } if (patternOp != instance.op()) { - return null; + // Only below a read that has matched so far. Solving a bare array index against an + // arbitrary integer establishes nothing until the read around it is known to be the + // same. + return nested ? solveByTheory(bindings, pattern, instance, services) : null; } for (int i = 0; i < pattern.arity(); i++) { - varMap = matchRec(varMap, pattern.sub(i), instance.sub(i)); - if (varMap == null) { - return null; + final Bindings matched = + matchRec(bindings, pattern.sub(i), instance.sub(i), services, true); + if (matched == null) { + // The operators agree at the top and disagree below, which is what an array index + // written against a different offset looks like: both sides are sums, but their + // parts do not line up. Solving the two as one equation still succeeds. + return nested ? solveByTheory(bindings, pattern, instance, services) : null; } + bindings = matched; } - return varMap; + return bindings; } /** - * match a variable to a instance. + * Last resort when the structures disagree: ask the theories to solve the pattern for one of + * its variables. An array index written against an offset never matches an absolute one, so + * without this a fact about {@code base + t} cannot be used on a term about {@code x}. * - * @return true if it is a new vaiable or the instance it matched is the same as that it matched - * before. + * A pattern that holds a metavariable is not solved: the solution is built from the + * pattern's other parts, and an instance is a term of the proof, which a metavariable is not. */ - private static ImmutableMap mapVarWithCheck( - ImmutableMap varMap, QuantifiableVariable var, - Term instance) { - final Term oldTerm = varMap.get(var); - if (oldTerm == null) { - return varMap.put(var, instance); + private static Bindings solveByTheory(Bindings bindings, Term pattern, Term instance, + Services services) { + // No services means the caller asked to compare the structures alone. + if (services == null || !(pattern instanceof JTerm patternTerm) + || !(instance instanceof JTerm instanceTerm) || containsMetavariable(pattern)) { + return null; } - - if (oldTerm.equals(instance)) { - return varMap; + for (TheoryReasoning support : services.getProfile().getTheorySupports(false)) { + final ImmutableMap solved = support + .solveForVariable(patternTerm, instanceTerm, bindings.variables(), services); + if (solved != null) { + return bindings.withSolution(solved); + } } return null; } - + private static boolean containsMetavariable(Term term) { + if (term.op() instanceof Metavariable) { + return true; + } + for (int i = 0; i < term.arity(); i++) { + if (containsMetavariable(term.sub(i))) { + return true; + } + } + return false; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ClausesGraph.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ClausesGraph.java index b2f05caf939..b470ad06075 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ClausesGraph.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ClausesGraph.java @@ -18,8 +18,7 @@ /** * This class describes the relation between different clauses in a CNF. If two clauses have the - * same existential quantifiable variable, we say they are connected. And this property is - * transitive. + * same existential quantifiable variable, they are connected. Connectedness is transitive. */ public class ClausesGraph { private final ImmutableSet exVars; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Congruence.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Congruence.java index 3cfea5abd14..415148e1d66 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Congruence.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Congruence.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermFactory; import de.uka.ilkd.key.logic.op.Equality; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.TheoryReasoning; import org.key_project.util.collection.ImmutableSet; @@ -23,8 +24,8 @@ * Each merge is oriented the way the equality is written on the sequent: occurrences of the left * side rewrite to the right side. The proof search normalises sequent equalities by the rules of * the owning theory, so this direction is the theory-established one. A - * {@link QuantifierTheorySupport} can veto a rewrite that would disturb the normal forms its - * decisions depend on ({@link QuantifierTheorySupport#allowsEqualityRewrite}); then the opposite + * {@link TheoryReasoning} can veto a rewrite that would disturb the normal forms its + * decisions depend on ({@link TheoryReasoning#allowsEqualityRewrite}); then the opposite * direction is tried, and a doubly vetoed equality is left out of the congruence. * * One congruence is built per sequent in {@link Instantiation} and shared across the cost @@ -122,7 +123,7 @@ private boolean allowed(JTerm from, JTerm to) { if (to.sort() != from.sort() && !to.sort().extendsTrans(from.sort())) { return false; } - for (final QuantifierTheorySupport support : TriggersSet.THEORY_SUPPORTS) { + for (final TheoryReasoning support : services.getProfile().getTheorySupports(false)) { if (!support.allowsEqualityRewrite(from, to, services)) { return false; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityTheorySupport.java deleted file mode 100644 index 3442c475a1e..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityTheorySupport.java +++ /dev/null @@ -1,103 +0,0 @@ -/* 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.quantifierHeuristics; - -import java.util.List; - -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.op.Equality; -import de.uka.ilkd.key.logic.op.Junctor; - -import org.key_project.logic.op.Operator; -import org.key_project.logic.op.QuantifiableVariable; -import org.key_project.util.collection.ImmutableSet; - -import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; - -/** - * Support for the equality theory. - * - * Rejects the equality {@code =} as a trigger (matching on it has not been observed to help - * instantiation) and provides no derived triggers. For cost prediction it decides a literal that is - * an equality or equivalence whose two sides are equal up to renaming, and decides an arbitrary - * literal that equals an assumed one up to renaming (or contradicts it under a negation). - */ -final class EqualityTheorySupport implements QuantifierTheorySupport { - - /** - * Rejects the equality {@code =} as a trigger. - * - * @param candidate a trigger candidate that contains the quantified variables - * @param services access to the theory operators - * @return whether the candidate is rejected - */ - @Override - public boolean rejectsAsTrigger(JTerm candidate, Services services) { - return candidate.op() == Equality.EQUALS; - } - - /** - * Provides no derived triggers. - * - * @param term an accepted trigger term - * @param clauseVariables the quantified variables of the clause the trigger belongs to - * @param services access to the theory operators - * @return the empty list - */ - @Override - public List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services) { - return List.of(); - } - - /** - * Checks whether the literal is an equality or equivalence whose two sides are equal up to - * renaming. - * - * @param strippedLiteral a literal without leading negations - * @param services access to the theory operators - * @return {@code PROVED} if the two sides are equal up to renaming, otherwise {@code UNKNOWN} - */ - @Override - public LiteralDecision decideStrippedSelf(JTerm strippedLiteral, Services services) { - final Operator op = strippedLiteral.op(); - if (op == Equality.EQUALS || op == Equality.EQV) { - if (RENAMING_TERM_PROPERTY.equalsModThisProperty(strippedLiteral.sub(0), - strippedLiteral.sub(1))) { - return LiteralDecision.PROVED; - } - } - return LiteralDecision.UNKNOWN; - } - - /** - * Checks whether the literal follows from the axiom by equality up to renaming. Leading - * negations of both are tracked, so an axiom equal to the negated literal refutes it. - * - * @param literal a literal to decide - * @param axiom a literal assumed to be true - * @param services access to the theory operators - * @return {@code PROVED} if the axiom equals the literal, {@code REFUTED} if it equals its - * negation, otherwise {@code UNKNOWN} - */ - @Override - public LiteralDecision decideFromAxiom(JTerm literal, JTerm axiom, Services services) { - boolean negated = false; - JTerm pro = literal; - while (pro.op() == Junctor.NOT) { - pro = pro.sub(0); - negated = !negated; - } - JTerm ax = axiom; - while (ax.op() == Junctor.NOT) { - ax = ax.sub(0); - negated = !negated; - } - if (RENAMING_TERM_PROPERTY.equalsModThisProperty(pro, ax)) { - return negated ? LiteralDecision.REFUTED : LiteralDecision.PROVED; - } - return LiteralDecision.UNKNOWN; - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java deleted file mode 100644 index 199afb85e17..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java +++ /dev/null @@ -1,160 +0,0 @@ -/* 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.quantifierHeuristics; - -import java.util.ArrayList; -import java.util.List; - -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.transformations.pipeline.PipelineConstants; -import de.uka.ilkd.key.ldt.HeapLDT; -import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.TermBuilder; -import de.uka.ilkd.key.logic.sort.ArraySort; - -import org.key_project.logic.Name; -import org.key_project.logic.op.QuantifiableVariable; -import org.key_project.logic.sort.Sort; -import org.key_project.util.collection.ImmutableSet; - -/** - * Support for the heap theory and array reads. - * - * Rejects the bare array-index constructor {@code arr(i)} (a coordinate, not a read) and reads of - * the implicit {@code $created} field, and provides array-read triggers generalized over the heap - * so that a read written for one heap in a quantified formula matches the reads a proof produces - * over its many other heaps. - */ -final class HeapArrayTheorySupport implements QuantifierTheorySupport { - - /** - * Rejects the bare array index {@code arr(i)} and reads of the implicit created field, both of - * which flood the instantiation when matched on their own. - * - * @param candidate a trigger candidate that contains the quantified variables - * @param services access to the heap theory operators - * @return whether the candidate is rejected - */ - @Override - public boolean rejectsAsTrigger(JTerm candidate, Services services) { - final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); - // we do not want to match on expressions a.$created - if (heapLDT.isSelectOp(candidate.op()) && candidate.sub(2).op().name().toString() - .endsWith(PipelineConstants.IMPLICIT_CREATED)) { - return true; - } - // the array-index constructor arr(i) alone is a coordinate, not a read: matching on it - // instantiates with every index literal of any array on any heap. The enclosing select is - // the meaningful trigger (see the generalized variants provided below). - return candidate.op() == heapLDT.getArr(); - } - - /** - * Provides the heap-generalized array read triggers, one per array dimension of the read. - * - * @param term an accepted trigger term - * @param clauseVariables the quantified variables of the clause the trigger belongs to - * @param services access to the heap theory operators and term construction - * @return the generalized read triggers, possibly empty - */ - @Override - public List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services) { - return dimensionVariants(term, clauseVariables, services); - } - - /** - * The generalized triggers for an array read, one per array dimension it goes through. This - * is the single generalization path: for a one-dimensional read it yields one trigger, for a - * read through a multi-dimensional array one per level. - * - * Two things must be generalized. The heap, because after simplification the read occurs over - * the many heaps of a proof (store chains of symbolic execution, an anonymized loop heap), - * not only the one written in the formula; a fresh metavariable per level stands for any heap. - * And the select sorts, because a formula may read {@code x[i][i_1]} with sorts of its own - * choice (a nonNull specification types the final read as plain Object), while the ground reads - * in a sequent are built with the component sorts of {@code x}'s array type, one per dimension. - * A trigger carrying the formula's sorts never matches: parametric selects of different sorts - * are different functions. - * - * For a select chain over an array-sorted base this method therefore rebuilds the access path - * once per depth, with the component sort of the base's array type at that depth and a fresh - * heap wildcard per level: for {@code x[i][i_1]} the triggers {@code x[i]} and - * {@code x[i][i_1]}, each carrying the sorts a ground read of that depth actually has. Prefixes - * that bind only part of the clause variables enter the multi-trigger pool as usual. - * - * @param term an accepted array read trigger - * @param clauseVariables the quantified variables of the clause the trigger belongs to - * @param services access to the heap theory operators and term construction - * @return one generalized read trigger per array dimension, possibly empty - */ - private List dimensionVariants(JTerm term, - ImmutableSet clauseVariables, Services services) { - final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); - final TermBuilder tb = services.getTermBuilder(); - final List variants = new ArrayList<>(); - // decompose the select chain: walk through the object position collecting the arr - // coordinates, innermost first - final List coordinates = new ArrayList<>(); - JTerm base = term; - while (heapLDT.isSelectOp(base.op()) && base.sub(2).op() == heapLDT.getArr()) { - coordinates.add(0, base.sub(2).sub(0)); - base = base.sub(1); - } - if (coordinates.isEmpty() || !(base.sort() instanceof ArraySort)) { - return variants; - } - boolean anyVar = false; - for (final JTerm c : coordinates) { - if (!TriggerUtils.intersect(c.freeVars(), clauseVariables).isEmpty()) { - anyVar = true; - } - } - if (!anyVar) { - return variants; - } - // rebuild the path bottom-up with the array's component sorts - Sort sort = base.sort(); - JTerm read = base; - for (int depth = 0; depth < coordinates.size(); depth++) { - if (!(sort instanceof ArraySort arraySort)) { - break; - } - sort = arraySort.elementSort(); - final JTerm heapVar = - tb.var(heapWildcard(term, clauseVariables, heapLDT.targetSort(), "_d" + depth)); - final JTerm arrField = tb.func(heapLDT.getArr(), coordinates.get(depth)); - read = tb.select(sort, heapVar, read, arrField); - if (!TriggerUtils.intersect(read.freeVars(), clauseVariables).isEmpty() - && !read.equals(term)) { - variants.add(read); - } - } - return variants; - } - - /** - * A fresh heap-sorted metavariable standing for "any heap" in a generalized trigger. Its name - * is derived from the quantified variables of the read (plus a caller-chosen suffix to keep - * several wildcards of one trigger apart) rather than from creation order, so that the - * metavariable ordering (and through it the unification result and the chosen instances) does - * not depend on which goal builds its trigger set first. - * - * @param select the read the wildcard is built for - * @param clauseVariables the quantified variables of the clause the read belongs to - * @param heapSort the sort of heaps - * @param suffix keeps several wildcards of one trigger apart - * @return a fresh heap-sorted metavariable - */ - private static Metavariable heapWildcard(JTerm select, - ImmutableSet clauseVariables, Sort heapSort, String suffix) { - final StringBuilder name = new StringBuilder("heapWildcard"); - for (final QuantifiableVariable v : TriggerUtils.intersect(select.freeVars(), - clauseVariables)) { - name.append('_').append(v.name()); - } - name.append(suffix); - return new Metavariable(new Name(name.toString()), heapSort); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java index 248e9a9c49b..60ecbef3af5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java @@ -3,7 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; +import java.util.Collections; +import java.util.EnumMap; import java.util.Iterator; +import java.util.Map; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; @@ -22,14 +25,22 @@ public class HeuristicInstantiation implements TermGenerator { - private static final HeuristicInstantiation THEORY = new HeuristicInstantiation(false); - private static final HeuristicInstantiation CLASSIC = new HeuristicInstantiation(true); + /** One generator per treatment, so the option costs no allocation per instantiation. */ + private static final Map> GENERATORS; + static { + final EnumMap> generators = + new EnumMap<>(TriggerTreatment.class); + for (final TriggerTreatment t : TriggerTreatment.values()) { + generators.put(t, new HeuristicInstantiation(t)); + } + GENERATORS = Collections.unmodifiableMap(generators); + } - /** whether instances are computed with the classic trigger selection */ - private final boolean classicTriggers; + /** how much the instance computation is told about the theories */ + private final TriggerTreatment treatment; - private HeuristicInstantiation(boolean classicTriggers) { - this.classicTriggers = classicTriggers; + private HeuristicInstantiation(TriggerTreatment treatment) { + this.treatment = treatment; } /** @@ -37,11 +48,11 @@ private HeuristicInstantiation(boolean classicTriggers) { * strategy construction, like every other strategy option; reading it per generated * instance would take a synchronized settings lookup in the middle of proof search. * - * @param classicTriggers whether the classic trigger selection is in effect + * @param treatment how much the heuristic is told about the theories * @return the generator */ - public static TermGenerator forOption(boolean classicTriggers) { - return classicTriggers ? CLASSIC : THEORY; + public static TermGenerator forOption(TriggerTreatment treatment) { + return GENERATORS.get(treatment); } @Override @@ -51,7 +62,7 @@ public Iterator generate(RuleApp app, PosInOccurrence pos, Goal goal, final Term qf = pos.sequentFormula().formula(); final Instantiation ia = - Instantiation.create(qf, goal.sequent(), goal.proof().getServices(), classicTriggers); + Instantiation.create(qf, goal.sequent(), goal.proof().getServices(), treatment); final QuantifiableVariable var = qf.varsBoundHere(0).last(); assert var != null; return new HIIterator(ia.getSubstitution().iterator(), var, goal.proof().getServices()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstanceTable.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstanceTable.java new file mode 100644 index 00000000000..4f256e9a11c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstanceTable.java @@ -0,0 +1,122 @@ +/* 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.quantifierHeuristics; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; + +import org.key_project.logic.Term; + +import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; + +/** + * The candidate instances of one quantified formula on one sequent, each with its cost and its + * origin. + * + * The table is what the strategy reads: the generator iterates {@link #instances()}, and the + * cost feature, the approval check and the tie-break look instances up. A looked-up instance may + * arrive wrapped in a cast, because the generator casts a candidate whose sort does not fit the + * quantified variable; {@link #normalize} takes the wrapper off, in this one place. + * + * Instances equal up to term labels share one entry. Of several offers for one instance the + * cheapest is kept. + */ +final class InstanceTable { + + /** + * One recorded instance. + * + * @param cost the instance's predicted cost plus its origin's surcharge + * @param origin why the instance is offered + */ + record Entry(long cost, Origin origin) { + } + + private final Map entries = new LinkedHashMap<>(); + + /** + * The recorded instances bucketed by {@link Term#nameHash()}. Two terms equal up to term + * labels share that hash, so the label-insensitive duplicate check in {@link #record} + * compares only within one bucket instead of scanning every recorded instance. + */ + private final Map> byNameHash = new HashMap<>(); + + /** + * Records one offer for an instance. The first offer creates the entry; a later offer + * replaces it unless it is more expensive. + * + * @param inst the instance + * @param cost the instance's predicted cost plus its origin's surcharge + * @param origin why the instance is offered + */ + void record(Term inst, long cost, Origin origin) { + Term key = inst; + Entry old = entries.get(inst); + if (old == null) { + final List bucket = byNameHash.get(inst.nameHash()); + if (bucket != null) { + for (final Term existing : bucket) { + if (((JTerm) existing).equalsModProperty(inst, + IRRELEVANT_TERM_LABELS_PROPERTY)) { + key = existing; + old = entries.get(existing); + break; + } + } + } + if (old == null) { + byNameHash.computeIfAbsent(inst.nameHash(), h -> new ArrayList<>(2)).add(inst); + } + } + if (old == null || old.cost() >= cost) { + entries.put(key, new Entry(cost, origin)); + } + } + + /** + * The entry of an instance, or null if the instance was never offered. The query is + * normalized first, so a cast-wrapped candidate finds the entry of its argument. + * + * @param query the instance as the strategy holds it + * @param services access to the cast symbol + * @return the entry, or null + */ + Entry entryOf(Term query, Services services) { + final Entry entry = entries.get(query); + if (entry != null) { + return entry; + } + final Term normalized = normalize(query, services); + return normalized == query ? null : entries.get(normalized); + } + + /** + * The instance as this table keys it: a candidate the generator wrapped in a cast is keyed + * by the cast's argument. + * + * @param query the instance as the strategy holds it + * @param services access to the cast symbol + * @return the table's key for the instance + */ + Term normalize(Term query, Services services) { + if (query.op() instanceof ParametricFunctionInstance pfi + && pfi.getBase() == services.getJavaDLTheory().getCastSymbol(services)) { + return query.sub(0); + } + return query; + } + + /** The recorded instances, in the order they were first offered. */ + Set instances() { + return entries.keySet(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java index cdd2f5dd3f4..75057a56fc4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java @@ -3,20 +3,16 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.LinkedHashMap; import java.util.List; -import java.util.Map; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermServices; -import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; import de.uka.ilkd.key.logic.op.Quantifier; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.TriggerSupport; +import de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak.QuantifierInstantiationTieBreak; import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; @@ -31,7 +27,6 @@ import org.key_project.util.collection.ImmutableMap; import org.key_project.util.collection.ImmutableSet; -import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; class Instantiation { @@ -46,15 +41,8 @@ class Instantiation { */ private ImmutableSet assumedLiterals = DefaultImmutableSet.nil(); - /** HashMap from instance(Term) to cost Long */ - private final Map instancesWithCosts = new LinkedHashMap<>(); - /** - * The recorded instances bucketed by {@link Term#nameHash()}. Two terms equal up to term - * labels share that hash, so the label-insensitive duplicate check in - * {@link #addInstance(Substitution, long)} compares only within one bucket instead of - * scanning every recorded instance. - */ - private final Map> instancesByNameHash = new HashMap<>(); + /** The candidate instances found on the sequent, with their costs and origins. */ + private final InstanceTable instances = new InstanceTable(); /** The tie-break scorer, prepared lazily on the first tie-break request and reused. */ private QuantifierInstantiationTieBreak.Scorer scorer; @@ -71,92 +59,80 @@ class Instantiation { /** The sequent, kept for the tie-break view. */ private final Sequent sequent; + /** How much this instantiation is told about the theories. */ + private final TriggerTreatment treatment; + /** The services, kept for the tie-break view. */ private final Services services; - private Instantiation(Term allterm, Sequent seq, Services services, boolean classic) { + private Instantiation(Term allterm, Sequent seq, Services services, + TriggerTreatment treatment) { this.sequent = seq; this.services = services; firstVar = allterm.varsBoundHere(0).get(0); matrix = TriggerUtils.discardQuantifiers(allterm); /* Terms bound in every formula on goal */ - triggersSet = TriggersSet.create((JTerm) allterm, services, classic); + this.treatment = treatment; + triggersSet = TriggersSet.create((JTerm) allterm, services, treatment.isClassic()); assumedLiterals = initAssertLiterals(seq, services); congruence = new Congruence(assumedLiterals, services); assumedLiterals = normalizeAll(assumedLiterals); addInstances(sequentToTerms(seq), services); - // write-coordinate candidates are part of the theory-aware selection, dropped in classic - if (!classic) { - addStoreCoordinateInstances((JTerm) matrix, services); + if (treatment.admits(Origin.THEORY_DIRECT)) { + addTheoryInstances((JTerm) matrix, + services.getProfile().getTheorySupports(treatment.isClassic()), services); } } /** - * Heap-aware instance candidates from write coordinates: where the matrix reads an array - * through a built-up heap, {@code select(... store(h, o, arr(c), v) ..., o, arr(j))} with - * quantified index {@code j}, the written index {@code c} is a candidate for {@code j}. - * Instantiating with it lets the select collapse by the select-over-store rules, which is - * how such a quantified formula speaks about the stored value. Trigger matching cannot - * produce these candidates: the store coordinate contains no quantified variable, so no - * trigger binds {@code j} to it. The candidates go through the same cost computation as - * matched ones, so useless coordinates are excluded or ranked down as usual. + * Adds the instance candidates the theories supply for {@code term} and descends into its + * subterms. + * + * Matching binds the quantified variable to a subterm of the term it matched, so it never + * produces an instance that stands in no trigger position. A theory supplies such an instance + * directly. Which subterms yield one depends on the theory, the descent over the matrix does + * not, so every support is called on every subterm. A supplied candidate is costed like a + * matched one. + * + * The caller asks the treatment for {@link Origin#THEORY_DIRECT} before the walk starts, + * so a treatment that admits no direct instances does not pay for the descent. + * + * @param term a subterm of the matrix + * @param supports the theories to consult + * @param services access to the theories */ - private void addStoreCoordinateInstances(JTerm term, Services services) { - final var heapLDT = services.getTypeConverter().getHeapLDT(); - // isSelectOp tests the operator directly. Do not build getSelect(term.sort()): that - // constructs a select of the subterm's sort, which fails for e.g. the Null sort. - if (heapLDT.isSelectOp(term.op())) { - final JTerm field = term.sub(2); - if (field.op() == heapLDT.getArr() && field.freeVars().contains(firstVar)) { - collectWrittenIndices(term.sub(0), term.sub(1), services); - } - } - for (int i = 0; i < term.arity(); i++) { - addStoreCoordinateInstances(term.sub(i), services); - } - } - - /** Adds every ground index written on {@code obj}'s array fields in {@code heap}. */ - private void collectWrittenIndices(JTerm heap, JTerm obj, Services services) { - final var heapLDT = services.getTypeConverter().getHeapLDT(); - if (heap.sort() != heapLDT.targetSort()) { - return; - } - if (heap.op() == heapLDT.getStore()) { - final JTerm field = heap.sub(2); - if (heap.sub(1).equals(obj) && field.op() == heapLDT.getArr() - && field.freeVars().isEmpty()) { + private void addTheoryInstances(JTerm term, List supports, + Services services) { + for (final TriggerSupport support : supports) { + for (final JTerm inst : support.provideInstances(term, firstVar, services)) { final ImmutableMap varMap = - DefaultImmutableMap.nilMap() - .put(firstVar, field.sub(0)); - addInstance(new Substitution(varMap), services); + DefaultImmutableMap.nilMap().put(firstVar, inst); + record(new Substitution(varMap), Origin.THEORY_DIRECT, false, services); } } - for (int i = 0; i < heap.arity(); i++) { - collectWrittenIndices(heap.sub(i), obj, services); + for (int i = 0; i < term.arity(); i++) { + addTheoryInstances(term.sub(i), supports, services); } } - private record Cached(Proof proof, Term qf, Sequent seq, boolean classic, + private record Cached(Proof proof, Term qf, Sequent seq, TriggerTreatment treatment, Instantiation result) { } /** * Per-thread single-entry cache for {@link #create}. The parallel prover computes quantifier - * cost concurrently, so a shared static cache would hand the same {@link Instantiation} (with - * its - * mutable {@code instancesWithCosts}) to several workers and race them. ThreadLocal confines - * the - * cache -- and thereby each returned Instantiation -- to one worker, and also drops the - * cross-proof class-level lock. + * cost concurrently, so a shared cache would hand the same {@link Instantiation}, with its + * mutable instance table, to several workers at once. Confining it to one worker + * also drops the cross-proof lock the class used to take. */ private static final ThreadLocal lastCreate = new ThreadLocal<>(); - static Instantiation create(Term qf, Sequent seq, Services services, boolean classic) { + static Instantiation create(Term qf, Sequent seq, Services services, + TriggerTreatment treatment) { final Proof proof = services.getProof(); final Cached cached = lastCreate.get(); if (cached != null && qf == cached.qf() && seq == cached.seq() - && classic == cached.classic()) { + && treatment == cached.treatment()) { return cached.result(); } if (cached != null && proof != cached.proof()) { @@ -164,8 +140,8 @@ static Instantiation create(Term qf, Sequent seq, Services services, boolean cla // proof's sequent stays reachable only while this entry is in use. lastCreate.remove(); } - final Instantiation result = new Instantiation(qf, seq, services, classic); - lastCreate.set(new Cached(proof, qf, seq, classic, result)); + final Instantiation result = new Instantiation(qf, seq, services, treatment); + lastCreate.set(new Cached(proof, qf, seq, treatment, result)); return result; } @@ -179,34 +155,107 @@ private static ImmutableSet sequentToTerms(Sequent seq) { /** * For each trigger, match it against the sequent terms and store every resulting instantiation - * together with its predicted cost in {@code instancesWithCosts}. + * together with its predicted cost in the instance table. * * @param terms the sequent terms the triggers are matched against */ private void addInstances(ImmutableSet terms, Services services) { + boolean matchedByOwnTerms = false; for (final Trigger t : triggersSet.getAllTriggers()) { + if (t.isTheoryProvided()) { + continue; + } for (final Substitution sub : t.getSubstitutionsFromTerms(terms, services)) { - addInstance(sub, services); + record(sub, + sub.isSolvedByTheory() ? Origin.SOLVED_POSITION : Origin.OWN_PATTERN, + false, services); + matchedByOwnTerms = true; + } + } + for (final Trigger t : triggersSet.getAllTriggers()) { + if (!t.isTheoryProvided()) { + continue; + } + final boolean fallback = t.isFallback(); + final ImmutableSet unified = + t.getSubstitutionsFromTerms(terms, services, false); + for (final Substitution sub : unified) { + record(sub, fallback ? Origin.FALLBACK : Origin.THEORY_UNIFIED, + matchedByOwnTerms, services); + } + // The treatment is asked before the matching runs, not in record: computing matches + // no treatment admits would be wasted work. + if (treatment.admits(Origin.THEORY_MATCHED)) { + for (final Substitution sub : t.getSubstitutionsFromTerms(terms, services, true)) { + if (!unified.contains(sub)) { + record(sub, fallback ? Origin.FALLBACK : Origin.THEORY_MATCHED, + matchedByOwnTerms, services); + } + } } } } - private void addInstance(Substitution sub, Services services) { - final long cost = - PredictCostProver.computerInstanceCost(sub, (JTerm) getMatrix(), - assumedLiterals, congruence, services); - if (cost != -1) { - addInstance(sub, cost); + /** + * Records one instance candidate: drops it if the treatment does not admit its origin or + * its cost cannot be predicted, otherwise costs it with the origin's surcharge on top of its + * prediction. Only the cheapest + * offer for an instance is kept. + * + * @param sub the instantiation found + * @param origin why the instance is offered + * @param matchedByOwnTerms whether some term of the formula matched the sequent + * @param services access to the theories + */ + private void record(Substitution sub, Origin origin, boolean matchedByOwnTerms, + Services services) { + if (!treatment.admits(origin)) { + return; } + final long cost = PredictCostProver.computerInstanceCost(sub, (JTerm) getMatrix(), + assumedLiterals, congruence, services); + if (cost == -1) { + return; + } + instances.record(sub.getSubstitutedTerm(firstVar), + cost + surcharge(origin, matchedByOwnTerms), origin); } /** - * Pre-normalises the assumed literals once through the congruence, so each candidate's cost - * prediction reuses the result instead of re-normalising them. + * What an instance costs on top of its predicted cost, by its origin. + * + * A predicted cost is a product of clause sizes (see {@link PredictCostProver}), so any + * surcharge above that range puts the instance behind every unsurcharged one; the exact + * values do not matter. + * + * A solved position always costs extra: the instance is a term the matched term does not + * contain, so it is offered behind those the two terms produced by agreeing throughout. A + * theory trigger's structural match costs extra only when some term of the formula matched + * the sequent: such a match binds the trigger's metavariable to a term the trigger never + * read, so where the formula's own terms match, their instances come first, and where they + * do not, it is all there is and costs what it predicts. A fallback instance follows the + * same rule: its clause had no trigger, but another clause of the formula may have matched. * - * @param lits the assumed literals - * @return the normalised literals, or {@code lits} unchanged when the congruence is trivial + * @param origin why the instance is offered + * @param matchedByOwnTerms whether some term of the formula matched the sequent + * @return the surcharge */ + private static long surcharge(Origin origin, boolean matchedByOwnTerms) { + return switch (origin) { + case SOLVED_POSITION -> SOLVED_POSITION_SURCHARGE; + case THEORY_MATCHED, FALLBACK -> matchedByOwnTerms ? THEORY_TRIGGER_SURCHARGE : 0; + default -> 0; + }; + } + + /** Surcharge of {@link Origin#THEORY_MATCHED} instances, see {@link #surcharge}. */ + private static final long THEORY_TRIGGER_SURCHARGE = 10000L; + + /** Surcharge of {@link Origin#SOLVED_POSITION} instances, see {@link #surcharge}. */ + private static final long SOLVED_POSITION_SURCHARGE = 10000L; + + + /** Normalizes every literal by the congruence, so equal atoms coincide. */ private ImmutableSet normalizeAll(ImmutableSet lits) { if (congruence.isTrivial()) { return lits; @@ -218,46 +267,6 @@ private ImmutableSet normalizeAll(ImmutableSet lits) { return res; } - /** - * Records the instance chosen by sub for the quantified variable with its - * predicted cost, keeping the least cost when the instance is recorded already. - * - * The same instance can be found through different triggers whose matches differ only in term - * labels: one match picks the term up with an origin label, another without. Term equality is - * label sensitive, so both variants would enter the table as separate candidates, and the - * labels would decide which of the two is enumerated first. The table keeps one entry per - * instance up to term labels: a later variant merges into the entry of the first one found. - * - * @param sub the substitution providing the instance - * @param cost the predicted cost of the instance - */ - private void addInstance(Substitution sub, long cost) { - final Term inst = - sub.getSubstitutedTerm(firstVar); - Term key = inst; - Long oldCost = instancesWithCosts.get(inst); - if (oldCost == null) { - final List bucket = instancesByNameHash.get(inst.nameHash()); - if (bucket != null) { - for (final Term existing : bucket) { - if (((JTerm) existing).equalsModProperty(inst, - IRRELEVANT_TERM_LABELS_PROPERTY)) { - key = existing; - oldCost = instancesWithCosts.get(existing); - break; - } - } - } - if (oldCost == null) { - instancesByNameHash.computeIfAbsent(inst.nameHash(), h -> new ArrayList<>(2)) - .add(inst); - } - } - if (oldCost == null || oldCost >= cost) { - instancesWithCosts.put(key, cost); - } - } - /** * @param seq * @param services TODO @@ -288,26 +297,16 @@ private ImmutableSet initAssertLiterals(Sequent seq, * Try to find the cost of an instance(inst) according its quantified formula and current goal. */ static RuleAppCost computeCost(Term inst, Term form, Sequent seq, Services services, - boolean classic) { - return create(form, seq, services, classic).computeCostHelp(inst); + TriggerTreatment treatment) { + return create(form, seq, services, treatment).computeCostHelp(inst); } private RuleAppCost computeCostHelp(Term inst) { - Long cost = instancesWithCosts.get(inst); - if (cost == null && (inst.op() instanceof ParametricFunctionInstance pfi - && pfi.getBase().name().equals(JavaDLTheory.CAST_NAME))) { - cost = instancesWithCosts.get(inst.sub(0)); - } - - if (cost == null) { - // if (triggersSet) - return TopRuleAppCost.INSTANCE; - } - if (cost == -1) { + final InstanceTable.Entry entry = instances.entryOf(inst, services); + if (entry == null) { return TopRuleAppCost.INSTANCE; } - - return NumberRuleAppCost.create(cost); + return NumberRuleAppCost.create(entry.cost()); } /** @@ -320,14 +319,14 @@ private RuleAppCost computeCostHelp(Term inst) { * @param seq the sequent * @param goal the goal, for the branch history the generation signal needs * @param services access to the theory operators - * @param classic whether the classic trigger selection is active + * @param treatment how much the heuristic is told about the theories * @param strategy the tie-break strategy * @return the tie-break cost */ static RuleAppCost computeTieBreak(Term inst, Term form, Sequent seq, - Goal goal, Services services, boolean classic, + Goal goal, Services services, TriggerTreatment treatment, QuantifierInstantiationTieBreak strategy) { - return create(form, seq, services, classic).tieBreak(inst, goal, strategy); + return create(form, seq, services, treatment).tieBreak(inst, goal, strategy); } /** @@ -339,16 +338,16 @@ private RuleAppCost tieBreak(Term inst, Goal goal, QuantifierInstantiationTieBreak strategy) { if (scorer == null || scorerStrategy != strategy) { scorer = strategy.prepare(new QuantifierInstantiationTieBreak.View( - instancesWithCosts.keySet(), sequent, goal, services)); + instances.instances(), sequent, goal, services)); scorerStrategy = strategy; } - return NumberRuleAppCost.create(scorer.tieBreak(inst)); + return NumberRuleAppCost.create(scorer.tieBreak(instances.normalize(inst, services))); } /** get all instances from instancesCostCache subsCache */ ImmutableSet getSubstitution() { ImmutableSet res = DefaultImmutableSet.nil(); - for (final Term inst : instancesWithCosts.keySet()) { + for (final Term inst : instances.instances()) { res = res.add(inst); } return res; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java index d27163c8736..fabac75cfc7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java @@ -24,16 +24,16 @@ public class InstantiationCost implements Feature { final private ProjectionToTerm varInst; - /** whether the prediction runs with the classic trigger selection */ - private final boolean classicTriggers; + /** how much the prediction is told about the theories */ + private final TriggerTreatment treatment; - private InstantiationCost(ProjectionToTerm var, boolean classicTriggers) { + private InstantiationCost(ProjectionToTerm var, TriggerTreatment treatment) { varInst = var; - this.classicTriggers = classicTriggers; + this.treatment = treatment; } - public static Feature create(ProjectionToTerm varInst, boolean classicTriggers) { - return new InstantiationCost(varInst, classicTriggers); + public static Feature create(ProjectionToTerm varInst, TriggerTreatment treatment) { + return new InstantiationCost(varInst, treatment); } /** @@ -49,6 +49,6 @@ public static Feature create(ProjectionToTerm varInst, boolean classicTrig final var instance = varInst.toTerm(app, pos, jgoal, mState); return Instantiation.computeCost(instance, formula, goal.sequent(), - (Services) goal.proof().getServices(), classicTriggers); + (Services) goal.proof().getServices(), treatment); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java index 2e34d5f271c..84841f32d0b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java @@ -6,6 +6,9 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak.GenPolTieBreak; +import de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak.PolarityTieBreak; +import de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak.QuantifierInstantiationTieBreak; import org.key_project.logic.Term; import org.key_project.prover.proof.ProofGoal; @@ -66,13 +69,13 @@ public static Feature create(ProjectionToTerm varInst, String triggersOpti final de.uka.ilkd.key.proof.Goal jgoal = (de.uka.ilkd.key.proof.Goal) goal; if (strategy == null) { - // classic orders instances by their position in the sequent alone + // the classic treatment orders instances by their position in the sequent alone return NumberRuleAppCost.getZeroCost(); } final Term formula = pos.sequentFormula().formula(); final Term instance = varInst.toTerm(app, pos, jgoal, mState); return Instantiation.computeTieBreak(instance, formula, goal.sequent(), jgoal, - (Services) goal.proof().getServices(), false, strategy); + (Services) goal.proof().getServices(), TriggerTreatment.BEST, strategy); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java index 3c556d14b9c..ad55b0460ff 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java @@ -22,8 +22,9 @@ private Matching() {} * @param targetTerm a gound term * @return all substitution found from this matching */ - public static ImmutableSet basicMatching(Trigger trigger, Term targetTerm) { - return BasicMatching.getSubstitutions(trigger.getTriggerTerm(), targetTerm); + public static ImmutableSet basicMatching(Trigger trigger, Term targetTerm, + Services services) { + return BasicMatching.getSubstitutions(trigger.getTriggerTerm(), targetTerm, services); } public static ImmutableSet twoSidedMatching(UniTrigger trigger, Term targetTerm, diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java index 7dfbe159404..bdda8517dcb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java @@ -45,10 +45,16 @@ ImmutableSet elements() { @Override public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, Services services) { + return getSubstitutionsFromTerms(targetTerms, services, true); + } + + @Override + public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, + Services services, boolean basicMatching) { ImmutableList total = ImmutableList.nil(); final ImmutableSet combined = - combineElementSubstitutions(elements.iterator(), targetTerms, services); + combineElementSubstitutions(elements.iterator(), targetTerms, services, basicMatching); for (Substitution sub : combined) { if (sub.isTotalOn(clauseVariables)) { @@ -66,13 +72,13 @@ public ImmutableSet getSubstitutionsFromTerms(ImmutableSet t */ private ImmutableSet combineElementSubstitutions( Iterator remainingElements, ImmutableSet terms, - Services services) { + Services services, boolean basicMatching) { ImmutableList result = ImmutableList.nil(); if (remainingElements.hasNext()) { ImmutableSet headSubs = remainingElements.next().getSubstitutionsFromTerms(terms, services); ImmutableSet tailSubs = - combineElementSubstitutions(remainingElements, terms, services); + combineElementSubstitutions(remainingElements, terms, services, basicMatching); if (tailSubs.isEmpty()) { return headSubs; } else if (headSubs.isEmpty()) { @@ -132,6 +138,28 @@ public String toString() { return String.valueOf(elements); } + @Override + public boolean isTheoryProvided() { + for (final Trigger element : elements) { + if (element.isTheoryProvided()) { + return true; + } + } + return false; + } + + /** A multi-trigger is a fallback if one of its elements is. */ + @Override + public boolean isFallback() { + for (Trigger element : elements) { + if (element.isFallback()) { + return true; + } + } + return false; + } + + @Override public Term getTriggerTerm() { return clause; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Origin.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Origin.java new file mode 100644 index 00000000000..845d3a8e189 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Origin.java @@ -0,0 +1,43 @@ +/* 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.quantifierHeuristics; + +/** + * Why an instance is offered for a quantified formula. + * + * Every candidate instance enters the instantiation through one of the ways listed here. The + * origin decides two things: whether the current {@link TriggerTreatment} admits the instance at + * all, and what it costs on top of its predicted cost, see {@code Instantiation#surcharge}. An + * origin that reads the instance off a term the formula itself names ranks before one that does + * not. + */ +enum Origin { + + /** A term of the formula matched a sequent term structurally. */ + OWN_PATTERN, + + /** + * A term of the formula matched a sequent term except at one position, and a theory solved + * that position for the variable. The instance is a term the sequent does not contain. + */ + SOLVED_POSITION, + + /** A theory's generalized trigger unified with a sequent term. */ + THEORY_UNIFIED, + + /** + * A theory's generalized trigger matched a sequent term structurally, binding a + * metavariable to a term that does not occur in the formula. + */ + THEORY_MATCHED, + + /** A theory read the instance off the formula directly, without a trigger. */ + THEORY_DIRECT, + + /** + * A fallback trigger matched or unified. Fallback triggers exist only for a formula that no + * trigger of its own instantiates, see {@code TriggerSupport#fallbackTriggers}. + */ + FALLBACK +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java index 588fc1ae351..1883a4640ad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.Junctor; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.TheoryReasoning; import org.key_project.logic.op.Operator; import org.key_project.util.collection.DefaultImmutableSet; @@ -195,14 +196,14 @@ private JTerm provedBySelf(JTerm problem) { negated = !negated; pro = pro.sub(0); } - for (final QuantifierTheorySupport support : TriggersSet.THEORY_SUPPORTS) { - QuantifierTheorySupport.LiteralDecision decision = + for (final TheoryReasoning support : services.getProfile().getTheorySupports(false)) { + TheoryReasoning.LiteralDecision decision = support.decideStrippedSelf(pro, services); - if (decision != QuantifierTheorySupport.LiteralDecision.UNKNOWN) { + if (decision != TheoryReasoning.LiteralDecision.UNKNOWN) { if (negated) { decision = decision.negate(); } - return decision == QuantifierTheorySupport.LiteralDecision.PROVED ? trueT : falseT; + return decision == TheoryReasoning.LiteralDecision.PROVED ? trueT : falseT; } } return problem; @@ -218,11 +219,11 @@ private JTerm provedBySelf(JTerm problem) { * the problem's negation, and problem if undecided */ private JTerm provedByAnother(JTerm problem, JTerm axiom) { - for (final QuantifierTheorySupport support : TriggersSet.THEORY_SUPPORTS) { - final QuantifierTheorySupport.LiteralDecision decision = + for (final TheoryReasoning support : services.getProfile().getTheorySupports(false)) { + final TheoryReasoning.LiteralDecision decision = support.decideFromAxiom(problem, axiom, services); - if (decision != QuantifierTheorySupport.LiteralDecision.UNKNOWN) { - return decision == QuantifierTheorySupport.LiteralDecision.PROVED ? trueT : falseT; + if (decision != TheoryReasoning.LiteralDecision.UNKNOWN) { + return decision == TheoryReasoning.LiteralDecision.PROVED ? trueT : falseT; } } return problem; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ReplacerOfQuanVariablesWithMetavariables.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ReplacerOfQuanVariablesWithMetavariables.java index 81e90c39ae4..1985567b3c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ReplacerOfQuanVariablesWithMetavariables.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ReplacerOfQuanVariablesWithMetavariables.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; import org.key_project.logic.Name; import org.key_project.logic.Term; @@ -19,8 +20,7 @@ * allTerm and create constant functions for all existential variables. The variables * with new created metavariables or constant functions are store to a map mapQM. */ -@Deprecated -class ReplacerOfQuanVariablesWithMetavariables { +public class ReplacerOfQuanVariablesWithMetavariables { private ReplacerOfQuanVariablesWithMetavariables() {} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java index 1ad926b728f..035b925eee7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java @@ -31,8 +31,26 @@ public class Substitution { private final ImmutableMap varMap; + /** + * Whether a theory solved a position where the two terms disagreed to obtain this + * substitution. The instance is then a term the matched term does not contain. + */ + private final boolean solvedByTheory; + public Substitution(ImmutableMap map) { - varMap = map; + this(map, false); + } + + public Substitution(ImmutableMap map, boolean solvedByTheory) { + this.varMap = map; + this.solvedByTheory = solvedByTheory; + } + + /** + * @return whether a theory solved a disagreeing position to obtain this substitution + */ + public boolean isSolvedByTheory() { + return solvedByTheory; } public ImmutableMap getVarMap() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java index 1aab1102f3b..2cac25394fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java @@ -17,5 +17,41 @@ public interface Trigger { ImmutableSet getSubstitutionsFromTerms( ImmutableSet targetTerm, Services services); + /** + * As above, and where {@code basicMatching} is set a theory-provided trigger is matched by + * {@link BasicMatching} as well as unified. Only that matching lets a theory solve a + * array index, and only it binds a metavariable to a term the trigger never read. + * + * @param targetTerm the terms to match against + * @param services access to the theory's operators + * @param basicMatching whether a theory-provided trigger is also matched by + * {@link BasicMatching} + * @return the substitutions found + */ + default ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerm, + Services services, boolean basicMatching) { + return getSubstitutionsFromTerms(targetTerm, services); + } + Term getTriggerTerm(); + + /** + * Whether this trigger is a theory's generalization of another one rather than a term of the + * formula itself. + * + * @return whether the trigger was derived + */ + default boolean isTheoryProvided() { + return false; + } + + /** + * Whether this trigger is a theory's fallback for a clause without a covering trigger. + * Instances it yields carry the {@code FALLBACK} origin. + * + * @return whether the trigger is a fallback + */ + default boolean isFallback() { + return false; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerKind.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerKind.java new file mode 100644 index 00000000000..c272a4034e9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerKind.java @@ -0,0 +1,50 @@ +/* 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.quantifierHeuristics; + +/** + * How a uni-trigger is matched against the sequent. + * + * A trigger taken from the formula itself is matched structurally: each quantified variable is + * bound to the subterm at its position. This binds every variable the trigger carries, so it is + * only allowed when every one of them may be instantiated. A trigger that carries an existential + * variable is unified instead, which treats that variable as an unknown rather than binding it. + * A theory-derived trigger carries metavariables in place of ground subterms; unification binds + * them on any target, and structural matching is allowed in addition under the most informed + * treatment, since it instantiates from a term that does not occur in the formula. + * + * The kind is decided once, when the trigger is registered, and the matching stage chooses the + * matcher by the kind alone. + */ +enum TriggerKind { + + /** + * A term of the formula whose free variables are all universal. Matched structurally + * against ground targets, unified against quantified ones. + */ + PATTERN, + + /** + * A theory's generalization, carrying metavariables. Unified against any target, and + * additionally matched structurally against ground targets when the treatment allows it. + */ + GENERALIZED, + + /** + * A term of the formula carrying an existential variable. Unified against quantified + * targets only; ground targets yield nothing. + */ + NEEDS_UNIFY, + + /** + * A theory's generalization that also carries an existential variable. Unified against any + * target; never matched structurally. + */ + GENERALIZED_UNIFY; + + /** Whether a theory derived this trigger rather than the formula containing it. */ + boolean isTheoryProvided() { + return this == GENERALIZED || this == GENERALIZED_UNIFY; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java new file mode 100644 index 00000000000..479a5c91914 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java @@ -0,0 +1,58 @@ +/* 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.quantifierHeuristics; + +import java.util.EnumSet; +import java.util.Set; + +import de.uka.ilkd.key.strategy.StrategyProperties; + +/** + * How much the quantifier instantiation heuristic is told about the theories, as the strategy's + * trigger option selects it. + * + * A treatment is a set of admitted instance {@link Origin}s and a choice of theory supports. + * Which theories select the triggers follows {@link #isClassic()}; whether an instance found by + * some mechanism is offered at all follows {@link #admits(Origin)}. A new mechanism is one new + * origin, admitted here per treatment. + * + * The solved-position origin is admitted everywhere: solving happens inside the structural + * matching of the formula's own triggers, which every treatment runs (see + * {@code BasicMatching}). + */ +public enum TriggerTreatment { + + /** Everything the heuristic knows. */ + BEST(EnumSet.allOf(Origin.class)), + + /** The theories' trigger selection, with theory-provided triggers unified only. */ + GOOD(EnumSet.of(Origin.OWN_PATTERN, Origin.SOLVED_POSITION, Origin.THEORY_UNIFIED, + Origin.THEORY_DIRECT)), + + /** Equality and integer rejection only, and no ordering of the candidates. */ + CLASSIC(EnumSet.of(Origin.OWN_PATTERN, Origin.SOLVED_POSITION)); + + private final Set admittedOrigins; + + TriggerTreatment(Set admittedOrigins) { + this.admittedOrigins = admittedOrigins; + } + + public static TriggerTreatment forOption(String option) { + if (StrategyProperties.TRIGGERS_CLASSIC.equals(option)) { + return CLASSIC; + } + return StrategyProperties.TRIGGERS_GOOD.equals(option) ? GOOD : BEST; + } + + /** Whether only the classic supports are consulted, and candidates are left unordered. */ + public boolean isClassic() { + return this == CLASSIC; + } + + /** Whether an instance of the given origin is offered under this treatment. */ + boolean admits(Origin origin) { + return admittedOrigins.contains(origin); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerUtils.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerUtils.java index 2102c3c15c5..8c964ca87dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerUtils.java @@ -14,7 +14,7 @@ import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; -class TriggerUtils { +public class TriggerUtils { /** * remove all the quantifiable variable bounded in the top level of a given formula. diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java index 568c5438de4..622fd469195 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java @@ -4,7 +4,6 @@ package de.uka.ilkd.key.strategy.quantifierHeuristics; import java.util.ArrayList; -import java.util.HashSet; import java.util.LinkedHashMap; import java.util.LinkedHashSet; import java.util.List; @@ -16,9 +15,17 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.logic.op.*; - +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.ClauseAnalysis; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.ClauseTriggers; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.LiteralTriggers; +import de.uka.ilkd.key.strategy.quantifierHeuristics.theory.TriggerSupport; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; import org.key_project.logic.op.Operator; import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.sort.Sort; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -29,25 +36,6 @@ */ public class TriggersSet { - /** - * Per-theory support consulted for rejecting unsuitable trigger material, providing derived - * triggers, and (from {@link PredictCostProver}) deciding literals during cost prediction. - * Support for a further theory is added by extending this list. The order is significant for - * cost prediction: literals are decided by the first support that reaches a verdict, so - * equality - * is consulted before integer arithmetic, matching the original prover. - */ - static final List THEORY_SUPPORTS = - List.of(new HeapArrayTheorySupport(), new EqualityTheorySupport(), - new IntegerTheorySupport()); - - /** - * The classic trigger selection: equality and integer rejection only, without the - * symbolic-execution supports. The strategy option {@code TRIGGERS_CLASSIC} selects it. - */ - private static final List CLASSIC_SUPPORTS = - List.of(new EqualityTheorySupport(), new IntegerTheorySupport()); - /** The quantified formula in prenex CNF. */ private final JTerm allTerm; /** Whether this set was built with the classic supports; part of the cache decision. */ @@ -62,14 +50,29 @@ public class TriggersSet { /** All triggers for the formula, built from the collected ones by the constructor. */ private final ImmutableSet allTriggers; /** Maps each trigger subterm of the formula to its trigger. */ - private final Map termToTrigger = new LinkedHashMap<>(); + private final Map termToTrigger = new LinkedHashMap<>(); + /** + * The derived triggers each subterm received from the theories, by subterm. The derived + * triggers depend only on the subterm and its variables, but each provision builds them + * around fresh metavariables, so a second occurrence of the same subterm in another clause + * reuses the first occurrence's triggers instead of registering unequal copies. + */ + private final Map> derivedTriggersFor = new LinkedHashMap<>(); /** - * The subterms whose theory triggers were already provided. The derived triggers depend - * only on the subterm and its variables, but each provision builds them around fresh - * metavariables, so a second occurrence of the same subterm in another clause would - * register unequal copies of the same triggers. + * Hands the supports their metavariables, counted within this set. The set is built from the + * quantified formula alone, so the same formula always yields the same names, and no two + * derived triggers share one. See {@link TriggerSupport.MetavariableFactory}. */ - private final Set theoryTriggersProvidedFor = new HashSet<>(); + private final TriggerSupport.MetavariableFactory metavariableFactory = + new TriggerSupport.MetavariableFactory() { + private int created; + + @Override + public Metavariable fresh(Sort sort) { + return new Metavariable(new Name("unifier_derived_" + created++), sort); + } + }; + /** All universal variables of the formula. */ private final ImmutableSet uniQuantifiedVariables; /** @@ -80,12 +83,12 @@ public class TriggersSet { * The theory supports consulted for trigger rejection and provision. Under the classic trigger * selection only the classic supports (equality and integer) are kept. */ - private final List supports; + private final List supports; private TriggersSet(JTerm allTerm, Services services, boolean classic) { this.allTerm = allTerm; this.classic = classic; - this.supports = classic ? CLASSIC_SUPPORTS : THEORY_SUPPORTS; + this.supports = services.getProfile().getTheorySupports(classic); replacementWithMVs = ReplacerOfQuanVariablesWithMetavariables.createSubstitutionForVars(allTerm, services); uniQuantifiedVariables = collectUniversalVariables(allTerm); @@ -102,7 +105,7 @@ static TriggersSet create(JTerm allTerm, Services services) { } static TriggersSet create(JTerm allTerm, Services services, boolean classic) { - final Map triggerSetCache = + final Map triggerSetCache = services.getCaches().getTriggerSetCache(); allTerm = TermLabelManager.removeIrrelevantLabels(allTerm, services); TriggersSet trs; @@ -139,19 +142,50 @@ private ImmutableSet collectUniversalVariables(JTerm allte return DefaultImmutableSet.nil(); } - /** Finds the triggers in every clause of the matrix. */ + /** + * Finds the triggers in every clause of the matrix that holds the first quantified variable, + * and asks the theories for fallback triggers if none of these clauses is covered. + * + * The instantiation binds the first variable, so the formula is instantiated exactly if some + * clause holding that variable has a covering trigger. A clause without one is no gap while + * another clause covers, since every covering trigger binds the first variable. Only a + * formula where no clause covers would never be instantiated, and only for it are the + * fallbacks asked, clause by clause. The cover search runs once more per clause afterwards, + * so fallbacks that bind only some variables combine into covering multi-triggers. + */ private void initTriggers(Services services) { final QuantifiableVariable firstVariable = allTerm.varsBoundHere(0).get(0); + final List finders = new ArrayList<>(); + final List selections = new ArrayList<>(); final var clauses = TriggerUtils.iteratorByOperator(TriggerUtils.discardQuantifiers(allTerm), Junctor.AND); while (clauses.hasNext()) { final var clause = (JTerm) clauses.next(); // a trigger must contain the first variable of the quantified formula if (clause.freeVars().contains(firstVariable)) { - ClauseTriggerFinder finder = new ClauseTriggerFinder(clause); - finder.createTriggers(services); + final ClauseTriggerFinder finder = new ClauseTriggerFinder(clause); + finders.add(finder); + selections.add(finder.createTriggers(services)); + } + } + if (!anyCovered(selections)) { + for (int i = 0; i < finders.size(); i++) { + final ClauseTriggerFinder finder = finders.get(i); + finder.addFallbackTriggers(selections.get(i), services); + // A fallback binding only some of the clause's variables is an element. No clause + // had a cover before, so the search finds only covers that use a fallback. + finder.buildCoveringMultiTriggers(); + } + } + } + + private static boolean anyCovered(List selections) { + for (final ClauseTriggers selection : selections) { + if (selection.covered()) { + return true; } } + return false; } /** @@ -159,19 +193,16 @@ private void initTriggers(Services services) { * * @param trigger the trigger term * @param universalVariables the universal variables the trigger binds - * @param isUnify whether the trigger carries an existential variable and needs unification + * @param kind how the trigger is matched * @param isElement whether the trigger is an element of a multi-trigger - * @param matchByUnification whether the trigger is matched by unification even against ground - * terms * @return the uni-trigger for the term */ - private Trigger createUniTrigger(JTerm trigger, - ImmutableSet universalVariables, boolean isUnify, - boolean isElement, boolean matchByUnification) { - Trigger cached = termToTrigger.get(trigger); + private UniTrigger createUniTrigger(JTerm trigger, + ImmutableSet universalVariables, TriggerKind kind, + boolean isElement, boolean fallback) { + UniTrigger cached = termToTrigger.get(trigger); if (cached == null) { - cached = new UniTrigger(trigger, universalVariables, isUnify, isElement, - matchByUnification, this); + cached = new UniTrigger(trigger, universalVariables, kind, isElement, fallback, this); termToTrigger.put(trigger, cached); } return cached; @@ -215,61 +246,129 @@ public ClauseTriggerFinder(JTerm clause) { } + /** + * The triggers collected for the literal under search, covering ones and elements + * apart. Filled by registration and read into the literal's {@link LiteralTriggers}. + */ + private static final class Collected { + final List covering = new ArrayList<>(); + final List elements = new ArrayList<>(); + + void add(Trigger trigger, boolean isElement) { + (isElement ? elements : covering).add(trigger); + } + + LiteralTriggers forLiteral(JTerm literal) { + return new LiteralTriggers(literal, List.copyOf(covering), List.copyOf(elements)); + } + } + /** * Finds the uni-triggers and multi-trigger elements in each literal of the clause, - * registers the uni-triggers, and then builds the covering multi-triggers. + * registers the uni-triggers and builds the covering multi-triggers. * * @param services access to the theory operators and term construction + * @return what the selection found, per literal */ - public void createTriggers(Services services) { - final var literals = TriggerUtils.iteratorByOperator(clause, Junctor.OR); - while (literals.hasNext()) { - final JTerm literal = (JTerm) literals.next(); - for (JTerm term : expandIfThenElse(literal, services)) { - JTerm positive = term; - if (positive.op() == Junctor.NOT) { - positive = positive.sub(0); - } - addMaximalUniTriggers(positive, services); + public ClauseTriggers createTriggers(Services services) { + final ClauseAnalysis analysis = analyse(services); + final List perLiteral = new ArrayList<>(); + for (final JTerm literal : analysis.literals()) { + final Collected found = new Collected(); + searchTriggers(literal, null, found, services); + perLiteral.add(found.forLiteral(literal)); + } + final boolean multiCovered = buildCoveringMultiTriggers(); + return new ClauseTriggers(analysis, List.copyOf(perLiteral), multiCovered); + } + + /** + * Registers the theories' fallback triggers for this clause. Called only when no clause + * of the formula is covered, see {@link TriggersSet#initTriggers}. Which treatments act + * on the instances is decided where the instances are recorded, not here: the set is + * cached per formula and shared by the non-classic treatments. Fallback triggers are not + * part of the selection value they are asked for. + */ + private void addFallbackTriggers(ClauseTriggers selection, Services services) { + final Collected discarded = new Collected(); + for (final TriggerSupport support : supports) { + for (final JTerm fallback : support.fallbackTriggers(selection, services, + metavariableFactory)) { + registerUniTrigger(fallback, true, true, discarded); + } + } + } + + /** + * Reads the clause into the value trigger selection works on: its literals, negations + * stripped and if-then-else expanded, and its universal variables. + */ + private ClauseAnalysis analyse(Services services) { + final List literals = new ArrayList<>(); + final var disjuncts = TriggerUtils.iteratorByOperator(clause, Junctor.OR); + while (disjuncts.hasNext()) { + final JTerm disjunct = (JTerm) disjuncts.next(); + for (JTerm term : expandIfThenElse(disjunct, services)) { + literals.add(term.op() == Junctor.NOT ? term.sub(0) : term); } } - buildCoveringMultiTriggers(); + return new ClauseAnalysis(clause, clauseVariables, literals); + } + + /** + * What the search below one term produced, as the term enclosing it reads it. + */ + private enum Search { + /** + * A registered trigger below the term covers the term's universal variables. No + * enclosing term needs to become a trigger for them. + */ + SATISFIED, + /** + * No registered trigger below the term covers its universal variables. The + * enclosing term is the next candidate. + */ + OPEN } /** - * Registers the maximal uni-triggers in the term: the triggers of its subterms if any of - * them yields one, otherwise the term itself. + * Registers the maximal uni-triggers in the term: the triggers of its subterms if they + * cover the term's universal variables, otherwise the term itself. + * + * A subterm's SATISFIED counts only if the subterm carries every universal variable of + * this term. Each level checks this against its own variables, so a deep trigger + * satisfies every term above it exactly as far as the variables reach. * * @param term a subterm of a literal + * @param enclosing the term {@code term} is an argument of, null at the top of a literal + * @param found receives the triggers registered for the literal under search * @param services access to the theory operators and term construction - * @return whether a trigger was found in the term or its subterms + * @return what the search below {@code term} produced */ - private boolean addMaximalUniTriggers(JTerm term, Services services) { + private Search searchTriggers(JTerm term, JTerm enclosing, Collected found, + Services services) { if (!mightContainTriggers(term)) { - return false; + return Search.OPEN; } final ImmutableSet uniVarsInTerm = TriggerUtils.intersect(term.freeVars(), clauseVariables); - boolean foundSubtriggers = false; + boolean satisfied = false; for (int i = 0; i < term.arity(); i++) { final JTerm subTerm = term.sub(i); - final boolean found = addMaximalUniTriggers(subTerm, services); - - if (found && uniVarsInTerm.subset(subTerm.freeVars())) { - foundSubtriggers = true; + final Search below = searchTriggers(subTerm, term, found, services); + if (below == Search.SATISFIED && uniVarsInTerm.subset(subTerm.freeVars())) { + satisfied = true; } } - - // a term becomes a trigger only if none of its subterms yielded one; a subterm - // whose candidates were all rejected (not acceptable as triggers) does not count, - // so the next enclosing meaningful term gets its chance - if (!foundSubtriggers) { - return addUniTrigger(term, services); + if (satisfied) { + return Search.SATISFIED; } - - return true; + // A term becomes a trigger only if no subterm satisfies it. A subterm whose + // candidates were all forbidden does not, so the search continues with the + // enclosing term. + return registerCandidate(term, enclosing, found, services); } @SuppressWarnings("unchecked") @@ -322,7 +421,7 @@ private Set combineSubterms(JTerm originalTerm, Set[] possibleSubs /** * Check whether a given term (or a subterm of the term) might be a trigger candidate */ - private boolean mightContainTriggers(JTerm term) { + private boolean mightContainTriggers(Term term) { if (term.freeVars().isEmpty()) { return false; } @@ -335,55 +434,94 @@ private boolean mightContainTriggers(JTerm term) { } /** - * A trigger candidate is acceptable unless some theory's {@link QuantifierTheorySupport} - * rejects it as coordinate or connective material. + * The theories' combined verdict on a trigger candidate. A single {@code FORBIDDEN} + * discards the candidate; otherwise a single {@code PREFER_ENCLOSING} keeps the search + * going past it. */ - private boolean isAcceptableTrigger(JTerm term, Services services) { - for (final QuantifierTheorySupport support : supports) { - if (support.rejectsAsTrigger(term, services)) { - return false; + private TriggerSupport.CandidateVerdict verdictOn(JTerm term, JTerm enclosing, + Services services) { + TriggerSupport.CandidateVerdict combined = TriggerSupport.CandidateVerdict.ACCEPTABLE; + for (final TriggerSupport support : supports) { + switch (support.verdictOn(term, enclosing, services)) { + case FORBIDDEN: + return TriggerSupport.CandidateVerdict.FORBIDDEN; + case PREFER_ENCLOSING: + combined = TriggerSupport.CandidateVerdict.PREFER_ENCLOSING; + break; + default: + break; } } - return true; + return combined; } /** - * add a uni-trigger to triggers set or add an element of multi-triggers for this clause, - * together with the derived triggers each theory's {@link QuantifierTheorySupport} provides + * Offers one candidate to the theories and registers it as their verdict directs, + * together with the derived triggers each theory provides for an accepted one. * - * @return whether a trigger was registered for {@code term} + * @param term the candidate + * @param enclosing the term {@code term} is an argument of, null at the top of a literal + * @param found receives the triggers registered for the literal under search + * @param services access to the theory operators and term construction + * @return what the registration produced for the enclosing term */ - private boolean addUniTrigger(JTerm term, Services services) { - if (!isAcceptableTrigger(term, services)) { - return false; + private Search registerCandidate(JTerm term, JTerm enclosing, Collected found, + Services services) { + final TriggerSupport.CandidateVerdict verdict = verdictOn(term, enclosing, services); + if (verdict == TriggerSupport.CandidateVerdict.FORBIDDEN) { + return Search.OPEN; } - registerUniTrigger(term, false); + registerUniTrigger(term, false, false, found); // A theory's generalisation is a different term, not a weaker one: it can match where // the original does not and fail to match where the original does. Both are therefore // registered, so an instantiation reachable through either one stays reachable. - if (theoryTriggersProvidedFor.add(term)) { - for (final QuantifierTheorySupport support : supports) { - for (final JTerm derived : support.provideTriggers(term, clauseVariables, - services)) { - registerUniTrigger(derived, true); - } + List derived = derivedTriggersFor.get(term); + if (derived == null) { + derived = new ArrayList<>(); + for (final TriggerSupport support : supports) { + derived.addAll(support.provideTriggers(term, clauseVariables, services, + metavariableFactory)); + } + derivedTriggersFor.put(term, derived); + for (final JTerm derivedTerm : derived) { + registerUniTrigger(derivedTerm, true, false, found); + } + } else { + // The derived triggers of an earlier occurrence are registered once; this + // literal counts them as its own, classified against this clause's variables. + for (final JTerm derivedTerm : derived) { + found.add(termToTrigger.get(derivedTerm), isElement(derivedTerm)); } } - return true; + // A preferred-enclosing candidate is registered like any other, but leaves the + // search open: the read around an array index determines the accessed array and + // must become a trigger too. + return verdict == TriggerSupport.CandidateVerdict.PREFER_ENCLOSING ? Search.OPEN + : Search.SATISFIED; } - private void registerUniTrigger(JTerm term, boolean matchByUnification) { - final boolean isUnify = !term.freeVars().subset(clauseVariables); - final boolean isElement = !clauseVariables.subset(term.freeVars()); + /** Whether a trigger term binds only some of the clause's universal variables. */ + private boolean isElement(JTerm term) { + return !clauseVariables.subset(term.freeVars()); + } + + private void registerUniTrigger(JTerm term, boolean theoryProvided, boolean fallback, + Collected found) { + final boolean carriesExistential = !term.freeVars().subset(clauseVariables); + final boolean isElement = isElement(term); + final TriggerKind kind = theoryProvided + ? (carriesExistential ? TriggerKind.GENERALIZED_UNIFY : TriggerKind.GENERALIZED) + : (carriesExistential ? TriggerKind.NEEDS_UNIFY : TriggerKind.PATTERN); final ImmutableSet uniVarsInTerm = TriggerUtils.intersect(term.freeVars(), clauseVariables); - Trigger trigger = - createUniTrigger(term, uniVarsInTerm, isUnify, isElement, matchByUnification); + final UniTrigger trigger = + createUniTrigger(term, uniVarsInTerm, kind, isElement, fallback); if (isElement) { elementsOfMultiTrigger = elementsOfMultiTrigger.add(trigger); } else { collectedTriggers.add(trigger); } + found.add(trigger, isElement); } @@ -398,8 +536,11 @@ private void registerUniTrigger(JTerm term, boolean matchByUnification) { * nothing (see {@link #keepOwnedVariables}). Building all combinations of the elements * instead and keeping the covering ones yields the same instantiations, but visits 2^n * combinations, which is out of reach once a clause offers a few dozen elements. + * + * @return whether a covering multi-trigger was built */ - private void buildCoveringMultiTriggers() { + private boolean buildCoveringMultiTriggers() { + final int before = collectedTriggers.size(); final List elements = new ArrayList<>(); final List> coveredBy = new ArrayList<>(); for (final Trigger element : elementsOfMultiTrigger) { @@ -409,6 +550,8 @@ private void buildCoveringMultiTriggers() { } coverRemainingVariables(clauseVariables, DefaultImmutableSet.nil(), new ArrayList<>(), elements, coveredBy); + // every multi-trigger is new to the set, so the set grew exactly if one was built + return collectedTriggers.size() > before; } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java index 810ae65810f..b67937cdb72 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java @@ -7,6 +7,8 @@ import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.JModality; import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Constraint; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java index 765883d6510..9dce77452b3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java @@ -29,18 +29,11 @@ class UniTrigger implements Trigger { private final TriggersSet owningTriggerSet; - /** - * If {@code true} the trigger carries a non-universal (existential) variable and may therefore - * only be matched by (two-sided) unification, not by basic matching. - */ - private final boolean onlyUnify; - /** - * If {@code true} the trigger contains a metavariable in place of a ground subterm (a - * heap-generalized array read) and is matched by unification even against ground terms, so the - * metavariable can bind to any heap. Plain triggers use syntactic matching on ground terms. - */ - private final boolean matchByUnification; + /** How this trigger is matched, see {@link TriggerKind}. */ + private final TriggerKind kind; private final boolean isElementOfMultitrigger; + /** Whether this trigger is a theory's fallback for a clause without a covering trigger. */ + private final boolean fallback; // A TriggersSet is cached per proof (ServiceCaches.triggerSetCache) and thus shared across the // parallel-prover workers, so this match-result cache is hit concurrently on the cost path. The @@ -51,49 +44,101 @@ class UniTrigger implements Trigger { // run outside the lock); at worst two workers redundantly compute the same (pure) result. private final ConcurrentLruCache> matchResults = new ConcurrentLruCache<>(1000); + /** + * The results of the same matching with basic matching allowed. That matching produces + * substitutions unification alone does not, so which of the two ran is part of what was + * computed and + * has to be part of the key: sharing one cache would hand the caller whichever mode happened + * to fill the entry first. Only a generalized trigger distinguishes the two modes, see + * {@link #computeSubstitutionsForTerm}. + */ + private final ConcurrentLruCache> matchResultsByBasicMatching = + new ConcurrentLruCache<>(1000); UniTrigger(Term trigger, ImmutableSet universalVariables, - boolean onlyUnify, - boolean isElementOfMultitrigger, boolean matchByUnification, + TriggerKind kind, boolean isElementOfMultitrigger, boolean fallback, TriggersSet owningTriggerSet) { this.trigger = trigger; this.universalVariables = universalVariables; - this.onlyUnify = onlyUnify; + this.kind = kind; this.isElementOfMultitrigger = isElementOfMultitrigger; - this.matchByUnification = matchByUnification; + this.fallback = fallback; this.owningTriggerSet = owningTriggerSet; } @Override public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, Services services) { + return getSubstitutionsFromTerms(targetTerms, services, true); + } + + @Override + public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, + Services services, boolean basicMatching) { ImmutableSet allSubs = DefaultImmutableSet.nil(); for (Term target : targetTerms) { - allSubs = allSubs.union(cachedSubstitutionsForTerm(target, services)); + allSubs = allSubs.union(cachedSubstitutionsForTerm(target, services, basicMatching)); } return allSubs; } - private ImmutableSet cachedSubstitutionsForTerm(Term target, Services services) { - ImmutableSet subs = matchResults.get(target); + private ImmutableSet cachedSubstitutionsForTerm(Term target, Services services, + boolean basicMatching) { + // A plain trigger is matched basically whenever it is not unified, so the mode leaves its + // result untouched and both callers share the one cache. + final ConcurrentLruCache> cache = + basicMatching && kind.isTheoryProvided() ? matchResultsByBasicMatching : matchResults; + ImmutableSet subs = cache.get(target); if (subs == null) { - subs = computeSubstitutionsForTerm(target, services); - matchResults.put(target, subs); + subs = computeSubstitutionsForTerm(target, services, basicMatching); + cache.put(target, subs); } return subs; } - private ImmutableSet computeSubstitutionsForTerm(Term target, Services services) { - ImmutableSet subs = DefaultImmutableSet.nil(); - if (target.freeVars().size() > 0 || target.op() instanceof Quantifier - || matchByUnification) { - subs = Matching.twoSidedMatching(this, target, services); - } else if (!onlyUnify) { - subs = Matching.basicMatching(this, target); + private ImmutableSet computeSubstitutionsForTerm(Term target, + Services services, boolean basicMatching) { + final boolean groundTarget = + target.freeVars().isEmpty() && !(target.op() instanceof Quantifier); + // A quantified target is unified whatever the kind: its own variables are unknowns + // that structural matching cannot handle. + if (!groundTarget) { + return Matching.twoSidedMatching(this, target, services); } - return subs; + // Against a ground target the kind decides. Only structural matching lets a theory + // solve an array index: unification decides a pair of terms as a whole and offers no + // point at which a failing index could be solved. + switch (kind) { + case PATTERN: + return Matching.basicMatching(this, target, services); + case GENERALIZED: + ImmutableSet subs = Matching.twoSidedMatching(this, target, services); + if (basicMatching) { + final ImmutableSet basicSubs = + Matching.basicMatching(this, target, services); + if (!basicSubs.isEmpty()) { + subs = subs.union(basicSubs); + } + } + return subs; + case GENERALIZED_UNIFY: + return Matching.twoSidedMatching(this, target, services); + case NEEDS_UNIFY: + default: + return DefaultImmutableSet.nil(); + } + } + + + @Override + public boolean isTheoryProvided() { + return kind.isTheoryProvided(); } + @Override + public boolean isFallback() { + return fallback; + } @Override public Term getTriggerTerm() { @@ -132,7 +177,7 @@ public TriggersSet getTriggerSetThisBelongsTo() { */ public static boolean passedLoopTest(Term candidate, Term searchTerm) { final ImmutableSet substitutions = - BasicMatching.getSubstitutions(candidate, searchTerm); + BasicMatching.getSyntacticSubstitutions(candidate, searchTerm); for (Substitution substitution : substitutions) { if (containsCycle(substitution)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Constraint.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/Constraint.java similarity index 99% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Constraint.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/Constraint.java index 17ef7901d64..91b57c3b011 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Constraint.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/Constraint.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.constraint; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.BooleanContainer; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ConstraintAwareSyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/ConstraintAwareSyntacticalReplaceVisitor.java similarity index 97% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ConstraintAwareSyntacticalReplaceVisitor.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/ConstraintAwareSyntacticalReplaceVisitor.java index 2a16c779e73..0c85d13561a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ConstraintAwareSyntacticalReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/ConstraintAwareSyntacticalReplaceVisitor.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.constraint; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.label.TermLabelState; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/EqualityConstraint.java similarity index 99% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/EqualityConstraint.java index 6f1364e26b0..269f52f7887 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/EqualityConstraint.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.constraint; import java.util.Collections; import java.util.HashMap; @@ -38,7 +38,6 @@ * constraint would not be satisfiable (cycles, unification failed) the Constraint TOP of interface * Constraint is returned. */ -@Deprecated public class EqualityConstraint implements Constraint { /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/Metavariable.java similarity index 97% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/Metavariable.java index bded9e4f0bb..a6c0d64a647 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/constraint/Metavariable.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.constraint; import java.util.concurrent.atomic.AtomicInteger; @@ -13,7 +13,6 @@ import org.key_project.logic.TerminalSyntaxElement; import org.key_project.logic.sort.Sort; -@Deprecated public final class Metavariable extends JAbstractSortedOperator implements Comparable, TerminalSyntaxElement, Named { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/ClauseAnalysis.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/ClauseAnalysis.java new file mode 100644 index 00000000000..d55b49ee616 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/ClauseAnalysis.java @@ -0,0 +1,28 @@ +/* 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.quantifierHeuristics.theory; + +import java.util.List; + +import de.uka.ilkd.key.logic.JTerm; + +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.util.collection.ImmutableSet; + +/** + * One clause of a quantified formula, as trigger selection reads it. + * + * The clause is one conjunct of the formula's matrix. Its literals are listed with leading + * negations stripped and if-then-else terms expanded, so a consumer sees each atom once and in + * positive form. The universal variables are those of the formula that occur free in the clause; + * a trigger of the clause has to bind them. + * + * @param clause the clause as it stands in the matrix + * @param universalVariables the formula's universal variables occurring free in the clause + * @param literals the literals, negations stripped, if-then-else expanded + */ +public record ClauseAnalysis(JTerm clause, + ImmutableSet universalVariables, + List literals) { +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/ClauseTriggers.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/ClauseTriggers.java new file mode 100644 index 00000000000..4dbc69b166e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/ClauseTriggers.java @@ -0,0 +1,50 @@ +/* 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.quantifierHeuristics.theory; + +import java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.logic.JTerm; + +/** + * What trigger selection found for one clause: the triggers of each literal, and whether + * elements of several literals combined into a covering multi-trigger. + * + * A clause is covered if some literal has a covering trigger or a covering multi-trigger was + * built. Every covering trigger binds the formula's first variable, so the formula is + * instantiated exactly if some clause is covered; a formula with no covered clause is the case + * {@link TriggerSupport#fallbackTriggers} exists for. + * + * @param clause the clause as trigger selection read it + * @param literals the triggers found per literal, in the order of {@code clause.literals()} + * @param multiCovered whether a covering multi-trigger was built from the literals' elements + */ +public record ClauseTriggers(ClauseAnalysis clause, List literals, + boolean multiCovered) { + + /** Whether some literal has a covering trigger or a covering multi-trigger was built. */ + public boolean covered() { + if (multiCovered) { + return true; + } + for (final LiteralTriggers literal : literals) { + if (!literal.covering().isEmpty()) { + return true; + } + } + return false; + } + + /** The literals that yielded neither a covering trigger nor an element. */ + public List literalsWithoutTrigger() { + final List result = new ArrayList<>(); + for (final LiteralTriggers literal : literals) { + if (literal.isEmpty()) { + result.add(literal.literal()); + } + } + return result; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/EqualityTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/EqualityTheorySupport.java new file mode 100644 index 00000000000..89a351ef82b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/EqualityTheorySupport.java @@ -0,0 +1,182 @@ +/* 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.quantifierHeuristics.theory; + + +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.TermBuilder; +import de.uka.ilkd.key.logic.op.Equality; +import de.uka.ilkd.key.logic.op.Junctor; +import de.uka.ilkd.key.logic.op.LogicVariable; +import de.uka.ilkd.key.proof.OpReplacer; +import de.uka.ilkd.key.strategy.quantifierHeuristics.Substitution; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Constraint; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.EqualityConstraint; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.util.collection.DefaultImmutableMap; +import org.key_project.util.collection.ImmutableSet; + +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; + +/** + * Support for the equality theory. + * + * Forbids the equality {@code =} as a trigger (matching on it has not been observed to help + * instantiation) and provides no derived triggers. For cost prediction it decides a literal that is + * an equality or equivalence whose two sides are equal up to renaming, and decides an arbitrary + * literal that equals an assumed one up to renaming (or contradicts it under a negation). + */ +final class EqualityTheorySupport implements QuantifierTheorySupport { + + /** + * Forbids the equality {@code =} as a trigger. + * + * @param candidate a trigger candidate that contains the quantified variables + * @param enclosing the term the candidate is an argument of, null at the top of a literal + * @param services access to the theory operators + * @return the verdict + */ + @Override + public CandidateVerdict verdictOn(JTerm candidate, JTerm enclosing, Services services) { + return candidate.op() == Equality.EQUALS ? CandidateVerdict.FORBIDDEN + : CandidateVerdict.ACCEPTABLE; + } + + /** + * Provides no derived triggers. + * + * @param term an accepted trigger term + * @param clauseVariables the quantified variables of the clause the trigger belongs to + * @param services access to the theory operators + * @return the empty list + */ + @Override + public List provideTriggers(JTerm term, + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { + return List.of(); + } + + /** + * Checks whether the literal is an equality or equivalence whose two sides are equal up to + * renaming. + * + * @param strippedLiteral a literal without leading negations + * @param services access to the theory operators + * @return {@code PROVED} if the two sides are equal up to renaming, otherwise {@code UNKNOWN} + */ + @Override + public LiteralDecision decideStrippedSelf(JTerm strippedLiteral, Services services) { + final Operator op = strippedLiteral.op(); + if (op == Equality.EQUALS || op == Equality.EQV) { + if (RENAMING_TERM_PROPERTY.equalsModThisProperty(strippedLiteral.sub(0), + strippedLiteral.sub(1))) { + return LiteralDecision.PROVED; + } + } + return LiteralDecision.UNKNOWN; + } + + /** + * Checks whether the literal follows from the axiom by equality up to renaming. Leading + * negations of both are tracked, so an axiom equal to the negated literal refutes it. + * + * @param literal a literal to decide + * @param axiom a literal assumed to be true + * @param services access to the theory operators + * @return {@code PROVED} if the axiom equals the literal, {@code REFUTED} if it equals its + * negation, otherwise {@code UNKNOWN} + */ + @Override + public LiteralDecision decideFromAxiom(JTerm literal, JTerm axiom, Services services) { + boolean negated = false; + JTerm pro = literal; + while (pro.op() == Junctor.NOT) { + pro = pro.sub(0); + negated = !negated; + } + JTerm ax = axiom; + while (ax.op() == Junctor.NOT) { + ax = ax.sub(0); + negated = !negated; + } + if (RENAMING_TERM_PROPERTY.equalsModThisProperty(pro, ax)) { + return negated ? LiteralDecision.REFUTED : LiteralDecision.PROVED; + } + return LiteralDecision.UNKNOWN; + } + + @Override + public List fallbackTriggers(ClauseTriggers selection, Services services, + MetavariableFactory metavariableFactory) { + List fallbackTriggers = new ArrayList<>(); + final ClauseAnalysis clauseInfo = selection.clause(); + + final TermBuilder tb = services.getTermBuilder(); + final Map qv2mv = new LinkedHashMap<>(); + final Map mv2qv = new LinkedHashMap<>(); + for (QuantifiableVariable var : clauseInfo.clause().freeVars()) { + final Metavariable mv = metavariableFactory.fresh(var.sort()); + qv2mv.put(var, tb.var(mv)); + if (clauseInfo.universalVariables().contains(var)) { + mv2qv.put(mv, var); + } + } + final Substitution qv2mvSubst = new Substitution(DefaultImmutableMap.fromMap(qv2mv)); + final OpReplacer mv2qvReplacer = + new OpReplacer(mv2qv, services.getTermFactory()); + for (JTerm lit : clauseInfo.literals()) { + if (lit.op() == Equality.EQUALS) { + fallbackTriggers.addAll( + solveEquation(mv2qv.keySet(), qv2mvSubst, mv2qvReplacer, lit, services)); + } + } + return fallbackTriggers; + } + + /// solves equation f(u) = f(g(v)) to u = g(MV_V) + /// @param mvs set of Metavariables used to replace **universal** bound variables + /// @param qv2mv substitution of the free variables of lit by their meta variables + /// @param mv2qv OpReplacer to restore universal (not existential) bound variables + /// @param lit the JTerm representing an uncovered literal + /// @param services the Services class provides access to term construction and other services + /// @return list of solved equations that describe triggers + private List solveEquation(Set mvs, Substitution qv2mv, + OpReplacer mv2qv, JTerm lit, + Services services) { + final TermBuilder tb = services.getTermBuilder(); + final JTerm litWithMV = (JTerm) qv2mv.applyWithoutCasts(lit, services); + final Constraint c = + EqualityConstraint.BOTTOM.unify(litWithMV.sub(0), litWithMV.sub(1), services); + List solvedEquations = new ArrayList<>(); + if (c.isSatisfiable()) { + for (final Metavariable mv : mvs) { + final JTerm solution = c.getInstantiation(mv, services); + final Operator instOp = solution.op(); + if (instOp instanceof LogicVariable || + instOp instanceof Metavariable) { + // solutions that are a variable + // and contain no function symbol do not + // make useful triggers + continue; + } + final JTerm solvedEquation = mv2qv.replace(tb.equals(tb.var(mv), solution)); + solvedEquations.add(solvedEquation); + solvedEquations.add(tb.equals(solvedEquation.sub(1), solvedEquation.sub(0))); + } + } + return solvedEquations; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HandleArith.java similarity index 99% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HandleArith.java index ada457c2512..b2cc370ffc6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HandleArith.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.theory; import java.util.Map; @@ -25,7 +25,7 @@ * knowing that {@code c>=d} or {@code c<=d;} * */ -public class HandleArith { +class HandleArith { private HandleArith() {} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HeapArrayTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HeapArrayTheorySupport.java new file mode 100644 index 00000000000..e37a6509c09 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HeapArrayTheorySupport.java @@ -0,0 +1,220 @@ +/* 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.quantifierHeuristics.theory; + +import java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.HeapLDT; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.TermBuilder; +import de.uka.ilkd.key.logic.sort.ArraySort; +import de.uka.ilkd.key.strategy.quantifierHeuristics.TriggerUtils; + +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableSet; + +/** + * Support for the heap theory and array reads. + * + * Forbids the index packaging {@code arr(...)} and reads of the implicit {@code $created} + * field as triggers, derives from every accepted trigger a variant whose reads of the quantified + * variables match over any heap, so that a read written for one heap in a quantified formula + * matches the reads a proof produces over its many other heaps, and supplies the indices a formula + * writes as candidate + * instances for the index it reads. + */ +final class HeapArrayTheorySupport implements QuantifierTheorySupport { + + /** + * The trigger for an array access is the read. + * + * Around an access, three terms could trigger, and the verdicts keep them apart. The + * packaging {@code arr(...)} wraps the index expression into a Field; it discriminates + * nothing of its own, so it is never a trigger. The index expression below it can be one: + * only compound expressions reach a verdict, a bare variable is no candidate to begin + * with, and a compound expression matches only terms of its own shape. The read above + * determines the accessed array, which the index expression alone does not, so its verdict + * keeps the search going up to the select. + * + * @param candidate a trigger candidate that contains the quantified variables + * @param enclosing the term the candidate is an argument of, null at the top of a literal + * @param services access to the heap theory operators + * @return the verdict + */ + @Override + public CandidateVerdict verdictOn(JTerm candidate, JTerm enclosing, Services services) { + final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); + if (heapLDT.isSelectOp(candidate.op()) + && candidate.sub(2).op() == heapLDT.getCreated()) { + // a created read holds of every allocated object alike, so it selects nothing + return CandidateVerdict.FORBIDDEN; + } + if (candidate.op() == heapLDT.getArr()) { + // arr only packs the index expression into a Field. With a bare index it matches + // the packaging of every access on the sequent; with a compound index it adds + // no information to its argument, which receives its own verdict below. + return CandidateVerdict.FORBIDDEN; + } + if (enclosing != null && enclosing.op() == heapLDT.getArr()) { + // a compound index expression is a trigger of its own, but only the read above + // determines the accessed array, so the select must become a trigger too + return CandidateVerdict.PREFER_ENCLOSING; + } + return CandidateVerdict.ACCEPTABLE; + } + + /** + * Provides the heap-generalized variant of an accepted trigger, see {@link #freeHeaps}, and + * the inner reads of a multi-dimensional array access as triggers of their own. + * + * @param term an accepted trigger term + * @param clauseVariables the quantified variables of the clause the trigger belongs to + * @param services access to the heap theory operators and term construction + * @param metavariableFactory supplies the metavariables that stand for the heaps + * @return the generalized triggers, empty if the term contains no read + */ + @Override + public List provideTriggers(JTerm term, + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { + final List variants = new ArrayList<>(); + final JTerm generalized = + freeHeaps(term, false, clauseVariables, variants, services, metavariableFactory); + if (generalized != term) { + variants.add(generalized); + } + return variants; + } + + /** + * The array indices a store of the formula writes, as candidates for the index a quantified + * read of the same object reads. + * + * For {@code select(... store(h, o, arr(c), v) ..., o, arr(j))} the written index {@code c} + * is a candidate for the quantified {@code j}: instantiating with it collapses the select by + * the select-over-store rules. {@code c} is ground, so no trigger contains it and matching + * never produces it. + * + * @param subterm a subterm of the quantified formula's matrix + * @param variable the quantified variable an instance is sought for + * @param services access to the heap theory operators + * @return the written indices, possibly empty + */ + @Override + public List provideInstances(JTerm subterm, QuantifiableVariable variable, + Services services) { + final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); + // isSelectOp tests the operator directly. Do not build getSelect(subterm.sort()): that + // constructs a select of the subterm's sort, which fails for e.g. the Null sort. + if (!heapLDT.isSelectOp(subterm.op())) { + return List.of(); + } + final JTerm field = subterm.sub(2); + if (field.op() != heapLDT.getArr() || !field.freeVars().contains(variable)) { + return List.of(); + } + final List indices = new ArrayList<>(); + collectWrittenIndices(subterm.sub(0), subterm.sub(1), heapLDT, indices); + return indices; + } + + /** Collects every ground array index written on {@code obj}'s array fields in {@code heap}. */ + private void collectWrittenIndices(JTerm heap, JTerm obj, HeapLDT heapLDT, + List indices) { + if (heap.sort() != heapLDT.targetSort()) { + return; + } + if (heap.op() == heapLDT.getStore()) { + final JTerm field = heap.sub(2); + if (heap.sub(1).equals(obj) && field.op() == heapLDT.getArr() + && field.freeVars().isEmpty()) { + indices.add(field.sub(0)); + } + } + for (int i = 0; i < heap.arity(); i++) { + collectWrittenIndices(heap.sub(i), obj, heapLDT, indices); + } + } + + /** + * Rebuilds a term with the heap of every read that carries a clause variable replaced by a + * fresh metavariable. + * + * Such a read binds the variable to what stands at the variable's position in a read of the + * same location, and the heap the location is read over does not discriminate: after a + * method call or a loop the location is read over an anonymized heap, after an assignment + * over a store, and the quantified formula names one of them. A read whose heap is a + * metavariable matches the read over any heap. Every such read gets a metavariable of its + * own, so the reads of one trigger match over different heaps. + * + * A read without a clause variable keeps its heap. It is part of the value the trigger + * names, and a freed heap would only widen the match to values over other heaps: a guard + * {@code x < p + result[1]} would then match sums with any read of {@code result[1]}, + * binding {@code x} to terms that prove nothing. A read whose heap contains a quantified + * variable is left as it is. + * + * An array read is rebuilt with the component sort of its array. A formula may read + * {@code x[i][i_1]} with sorts of its own choice (a nonNull specification types the final + * read as plain Object), while the ground reads of a sequent carry the component sorts of + * {@code x}'s array type, and parametric selects of different sorts are different + * functions. The inner read of {@code x[i][i_1]} is added to {@code innerReads} if it + * carries a clause variable: it is a trigger of its own and enters the multi-trigger pool + * where it binds only part of the clause's variables. + * + * @param term the term to rebuild + * @param arrayOfRead whether the term is the array argument of an enclosing array read + * @param clauseVariables the quantified variables of the clause the trigger belongs to + * @param innerReads receives the rebuilt array reads that are the array of an enclosing read + * @param services access to the heap theory operators and term construction + * @param metavariableFactory supplies the metavariables that stand for the heaps + * @return the rebuilt term, or {@code term} itself if it contains no read to free + */ + private JTerm freeHeaps(JTerm term, boolean arrayOfRead, + ImmutableSet clauseVariables, List innerReads, + Services services, MetavariableFactory metavariableFactory) { + if (TriggerUtils.intersect(term.freeVars(), clauseVariables).isEmpty()) { + return term; + } + final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); + final TermBuilder tb = services.getTermBuilder(); + if (heapLDT.isSelectOp(term.op()) && term.sub(0).freeVars().isEmpty()) { + final JTerm field = freeHeaps(term.sub(2), false, clauseVariables, innerReads, + services, metavariableFactory); + final boolean arrayRead = field.op() == heapLDT.getArr(); + final JTerm object = freeHeaps(term.sub(1), arrayRead, clauseVariables, innerReads, + services, metavariableFactory); + final JTerm heap = tb.var(metavariableFactory.fresh(heapLDT.targetSort())); + final JTerm read = arrayRead && object.sort() instanceof ArraySort arraySort + ? tb.select(arraySort.elementSort(), heap, object, field) + : services.getTermFactory().createTerm(term.op(), heap, object, field); + if (arrayOfRead && arrayRead + && !TriggerUtils.intersect(read.freeVars(), clauseVariables).isEmpty()) { + innerReads.add(read); + } + return read; + } + JTerm[] subs = null; + for (int i = 0; i < term.arity(); i++) { + final JTerm sub = freeHeaps(term.sub(i), false, clauseVariables, innerReads, + services, metavariableFactory); + if (sub != term.sub(i)) { + if (subs == null) { + subs = new JTerm[term.arity()]; + for (int j = 0; j < term.arity(); j++) { + subs[j] = term.sub(j); + } + } + subs[i] = sub; + } + } + if (subs == null) { + return term; + } + return services.getTermFactory().createTerm(term.op(), new ImmutableArray<>(subs), + term.boundVars(), null); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/IntegerTheorySupport.java similarity index 50% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/IntegerTheorySupport.java index 76e6fb18dd5..497cb931c79 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/IntegerTheorySupport.java @@ -1,39 +1,49 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.theory; +import java.math.BigInteger; import java.util.List; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.ldt.IntegerLDT; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial; +import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial; +import org.key_project.logic.Term; import org.key_project.logic.op.Operator; 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; /** * Support for the integer theory. * - * Rejects the (non-strict) comparisons as triggers (matching on them has not been observed to help + * Forbids the (non-strict) comparisons as triggers (matching on them has not been observed to help * instantiation) and provides no derived triggers. For cost prediction it decides an arithmetic * comparison from itself or from an assumed comparison, through {@link HandleArith}. */ final class IntegerTheorySupport implements QuantifierTheorySupport { /** - * Rejects the non-strict comparisons {@code <=} and {@code >=} as triggers. + * Forbids the non-strict comparisons {@code <=} and {@code >=} as triggers. * * @param candidate a trigger candidate that contains the quantified variables + * @param enclosing the term the candidate is an argument of, null at the top of a literal * @param services access to the integer theory operators - * @return whether the candidate is rejected + * @return the verdict */ @Override - public boolean rejectsAsTrigger(JTerm candidate, Services services) { + public CandidateVerdict verdictOn(JTerm candidate, JTerm enclosing, Services services) { final Operator op = candidate.op(); final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); - return op == integerLDT.getLessOrEquals() || op == integerLDT.getGreaterOrEquals(); + return op == integerLDT.getLessOrEquals() || op == integerLDT.getGreaterOrEquals() + ? CandidateVerdict.FORBIDDEN + : CandidateVerdict.ACCEPTABLE; } /** @@ -46,7 +56,8 @@ public boolean rejectsAsTrigger(JTerm candidate, Services services) { */ @Override public List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services) { + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { return List.of(); } @@ -60,7 +71,7 @@ public List provideTriggers(JTerm term, @Override public LiteralDecision decideStrippedSelf(JTerm strippedLiteral, Services services) { final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); - return QuantifierTheorySupport + return TheoryReasoning .fromTruthTerm(HandleArith.provedByArith(strippedLiteral, integerLDT, services)); } @@ -76,7 +87,7 @@ public LiteralDecision decideStrippedSelf(JTerm strippedLiteral, Services servic @Override public LiteralDecision decideFromAxiom(JTerm literal, JTerm axiom, Services services) { final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); - return QuantifierTheorySupport + return TheoryReasoning .fromTruthTerm(HandleArith.provedByArith(literal, axiom, integerLDT, services)); } @@ -87,7 +98,7 @@ public LiteralDecision decideFromAxiom(JTerm literal, JTerm axiom, Services serv * place in both directions: rewriting it away collapses the structure that * {@link de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial} decomposes, and rewriting other * terms into it makes it a class representative, which the one-pass normalisation of - * {@link Congruence} does not rewrite further. Rewriting an atom to a number literal or to + * {@code Congruence} does not rewrite further. Rewriting an atom to a number literal or to * another atom stays permitted: that only identifies atoms, which the assumed equality * justifies, and can only add arithmetic decisions. * @@ -114,6 +125,82 @@ public boolean allowsEqualityRewrite(JTerm from, JTerm to, Services services) { * @param integerLDT the integer theory operators * @return whether the top operator carries polynomial structure */ + /** + * Solves {@code pattern = instance} for the single variable the pattern is affine in. + * + * A trigger array index is typically written relative to an offset, as {@code base + t}, while + * the terms a proof produces are absolute. Decomposing both sides as polynomials turns the + * match into an equation: with the pattern {@code k*t + rest} and the instance {@code s}, the + * variable is {@code (s - rest) / k}. That division has to be exact, since a non-integer + * solution cannot reproduce the instance. + * + * Instantiating a universally quantified formula with any term is sound, so a solution that + * does not reproduce the instance costs one instantiation and nothing else. + * + * Declined when the pattern is affine in more than one variable, because the equation is then + * underdetermined; when a variable sits inside a product with another atom, because that is + * not linear; and when a variable of the pattern is already bound by this match, which would + * require substituting before solving. + */ + @Override + public ImmutableMap solveForVariable(JTerm pattern, JTerm instance, + ImmutableMap varMap, Services services) { + final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); + final Sort integerSort = integerLDT.targetSort(); + // The decomposition below allocates, and matching asks after every failed comparison, so + // the cheap tests come first: only a term built by the polynomial operators can be affine. + if (pattern.sort() != integerSort || instance.sort() != integerSort + || !hasPolynomialStructure(pattern, integerLDT) + || !instance.freeVars().isEmpty() || pattern.freeVars().isEmpty()) { + return null; + } + for (final QuantifiableVariable free : pattern.freeVars()) { + if (varMap.get(free) != null) { + return null; + } + } + + final Polynomial patternPoly = Polynomial.create(pattern, services); + Polynomial rest = Polynomial.ZERO.add(patternPoly.getConstantTerm()); + Monomial linear = null; + QuantifiableVariable variable = null; + for (final Monomial part : patternPoly.getParts()) { + final ImmutableList atoms = part.getParts(); + if (atoms.stream().allMatch(a -> a.freeVars().isEmpty())) { + rest = rest.add(part); + continue; + } + if (atoms.size() != 1 || linear != null + || !(atoms.head().op() instanceof QuantifiableVariable qv)) { + return null; + } + linear = part; + variable = qv; + } + if (linear == null) { + return null; + } + + final Polynomial solution = divideExactly( + Polynomial.create(instance, services).sub(rest), linear.getCoefficient()); + return solution == null ? null : varMap.put(variable, solution.toTerm(services)); + } + + /** Divides every coefficient by the divisor, or returns null when a division is not exact. */ + private static Polynomial divideExactly(Polynomial p, BigInteger divisor) { + if (divisor.signum() == 0 || p.getConstantTerm().remainder(divisor).signum() != 0) { + return null; + } + Polynomial result = Polynomial.ZERO.add(p.getConstantTerm().divide(divisor)); + for (Monomial part : p.getParts()) { + if (part.getCoefficient().remainder(divisor).signum() != 0) { + return null; + } + result = result.add(part.setCoefficient(part.getCoefficient().divide(divisor))); + } + return result; + } + private static boolean hasPolynomialStructure(JTerm t, IntegerLDT integerLDT) { final Operator op = t.op(); return op == integerLDT.getAdd() || op == integerLDT.getMul() diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/LiteralTriggers.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/LiteralTriggers.java new file mode 100644 index 00000000000..44f97fd8d48 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/LiteralTriggers.java @@ -0,0 +1,29 @@ +/* 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.quantifierHeuristics.theory; + +import java.util.List; + +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.strategy.quantifierHeuristics.Trigger; + +/** + * The triggers that trigger selection found in one literal of a clause. + * + * A covering trigger binds every universal variable of the clause on its own. An element binds + * only some of them and becomes a trigger only together with elements of other literals, as a + * covering multi-trigger. A literal may yield both, either, or neither. + * + * @param literal the literal, negation stripped, as listed in the clause's + * {@link ClauseAnalysis} + * @param covering the triggers of the literal that bind every universal variable of the clause + * @param elements the triggers of the literal that bind only some of them + */ +public record LiteralTriggers(JTerm literal, List covering, List elements) { + + /** Whether the literal yielded neither a covering trigger nor an element. */ + public boolean isEmpty() { + return covering.isEmpty() && elements.isEmpty(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/QuantifierTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/QuantifierTheorySupport.java new file mode 100644 index 00000000000..524a7b622ad --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/QuantifierTheorySupport.java @@ -0,0 +1,15 @@ +/* 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.quantifierHeuristics.theory; + +/** + * A theory that contributes to quantifier instantiation on both counts: it selects which of its + * subterms make a trigger, and it answers the questions the heuristic asks about terms. + * + * The two halves are separate interfaces because they travel differently. A front end registers + * the theories of its own terms through {@link QuantifierTheorySupports}; one without a heap + * implements {@link TheoryReasoning} alone. + */ +public interface QuantifierTheorySupport extends TriggerSupport, TheoryReasoning { +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/QuantifierTheorySupports.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/QuantifierTheorySupports.java new file mode 100644 index 00000000000..38abae6e569 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/QuantifierTheorySupports.java @@ -0,0 +1,31 @@ +/* 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.quantifierHeuristics.theory; + +import java.util.List; + +/** + * The theories the quantifier heuristic consults, in the order it consults them. + * + * A profile hands out the lists (see {@code Profile#getTheorySupports}), so a front end whose + * terms are built from other theories registers its own instead of these. The order decides the + * outcome where two theories both answer: a literal is decided by the first that reaches a + * verdict, so equality comes before integer arithmetic, as in the original prover. + */ +public final class QuantifierTheorySupports { + + private QuantifierTheorySupports() {} + + /** Everything the heuristic knows about the terms of the Java front end. */ + public static final List JAVA_DL = + List.of(new HeapArrayTheorySupport(), new SequenceTheorySupport(), + new EqualityTheorySupport(), new IntegerTheorySupport()); + + /** + * The classic trigger selection: equality and integer rejection only, without the knowledge + * about the heap. The strategy option {@code TRIGGERS_CLASSIC} selects it. + */ + public static final List CLASSIC = + List.of(new EqualityTheorySupport(), new IntegerTheorySupport()); +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/SequenceTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/SequenceTheorySupport.java new file mode 100644 index 00000000000..1cb2c42bfee --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/SequenceTheorySupport.java @@ -0,0 +1,73 @@ +/* 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.quantifierHeuristics.theory; + +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.SeqLDT; +import de.uka.ilkd.key.logic.JTerm; + +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.util.collection.ImmutableSet; + +/** + * Support for the sequence theory: a sequence read with a compound index is registered as a + * trigger together with its index. + * + * Trigger selection registers the smallest subterm that contains the quantified variables of the + * clause. For {@code seqGet(s, k + t)} with quantified {@code t} this is the sum {@code k + t}. + * The sum matches every sum of that shape on the sequent and does not determine the sequence + * {@code s}. The read determines {@code s}. This support therefore registers the read as well. + * Matching the read against {@code seqGet(s, x)} fails at the index, and the integer theory + * solves {@code k + t = x} for {@code t} there (see {@link TheoryReasoning#solveForVariable}). + * + * Compound indices are the normal case for sequences. The rules for subsequence, concatenation + * and reversal rewrite a read into a read of the underlying sequence at {@code idx + from}, + * {@code idx - seqLen(first)} and {@code seqLen(seq) - 1 - idx}. + * + * This support provides no derived triggers and decides no literals. + */ +final class SequenceTheorySupport implements QuantifierTheorySupport { + + /** + * A candidate in the index position of a sequence read is {@code PREFER_ENCLOSING}: it + * becomes a trigger, and the search continues with the read. Every other candidate is + * {@code ACCEPTABLE}. + * + * A bare variable is never a candidate, so for a read with a variable as index the read + * itself is the smallest candidate. A candidate in the sequence position, for example a + * subsequence term, determines the sequence itself. + * + * @param candidate a trigger candidate that contains the quantified variables + * @param enclosing the term the candidate is an argument of, null at the top of a literal + * @param services access to the sequence theory operators + * @return the verdict + */ + @Override + public CandidateVerdict verdictOn(JTerm candidate, JTerm enclosing, Services services) { + final SeqLDT seqLDT = services.getTypeConverter().getSeqLDT(); + // the index is the second argument of seqGet + if (enclosing != null && seqLDT.isSeqGetOp(enclosing.op()) + && enclosing.sub(1) == candidate) { + return CandidateVerdict.PREFER_ENCLOSING; + } + return CandidateVerdict.ACCEPTABLE; + } + + /** + * Provides no derived triggers. + * + * @param term an accepted trigger term + * @param clauseVariables the quantified variables of the clause the trigger belongs to + * @param services access to the sequence theory operators + * @return the empty list + */ + @Override + public List provideTriggers(JTerm term, + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { + return List.of(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/TheoryReasoning.java similarity index 62% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/TheoryReasoning.java index 3c9a2ebe71b..3b103e3e71f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/TheoryReasoning.java @@ -1,32 +1,26 @@ /* 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.quantifierHeuristics; - -import java.util.List; +package de.uka.ilkd.key.strategy.quantifierHeuristics.theory; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.Junctor; +import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; -import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.collection.ImmutableMap; /** - * A theory's contribution to quantifier instantiation. + * A theory's own reasoning about terms and literals, as the heuristic needs it: solving an + * equation for a variable while matching, deciding a literal when a cost is predicted, and + * permitting a rewrite of the equality reasoning. * - * The instantiation heuristic needs knowledge that is specific to each theory at two points. When - * choosing triggers: what counts as coordinate or connective material rather than a meaningful - * observation (an array index, an integer comparison), and which derived triggers make an - * observation matchable against the terms a proof actually produces (a read generalized over the - * heaps of a symbolic execution). And when predicting the cost of an instantiation: whether a - * literal is proved true or false, from itself or from an assumed literal, by the theory's own - * reasoning (arithmetic comparisons, equality up to renaming). This interface isolates that - * knowledge. Registering a new support in {@link TriggersSet#THEORY_SUPPORTS} is the only change - * needed to teach the heuristic about a further theory; {@link TriggersSet} and - * {@link PredictCostProver} stay untouched. + * These questions are about terms alone. A front end whose terms are built from the same theory + * reuses an implementation unchanged, whatever the programs behind the terms are, which is not so + * for {@link TriggerSupport}. */ -interface QuantifierTheorySupport { +public interface TheoryReasoning { /** The outcome of judging a literal for cost prediction. */ enum LiteralDecision { @@ -35,7 +29,7 @@ enum LiteralDecision { /** * @return the decision for the negation of the judged literal */ - LiteralDecision negate() { + public LiteralDecision negate() { return switch (this) { case PROVED -> REFUTED; case REFUTED -> PROVED; @@ -63,26 +57,28 @@ static LiteralDecision fromTruthTerm(JTerm t) { } /** - * Whether {@code candidate} must not be used as a standalone trigger, because for this theory - * it is coordinate or connective material rather than a meaningful observation. + * Solves a trigger subterm against a ground instance when syntactic matching has failed. * - * @param candidate a subterm that contains the quantified variables and is a trigger candidate - * @param services access to the theory operators - */ - boolean rejectsAsTrigger(JTerm candidate, Services services); - - /** - * Additional triggers derived from the accepted trigger {@code term}, for example a read - * generalized so it matches across the many heaps of a proof. The returned triggers are matched - * by unification (they may contain metavariables). + * Basic matching compares the two structures, so a trigger whose array index is written + * against an offset never matches an instance written absolutely: a read of + * {@code base + t} does not match one of {@code x}, since {@code x - base} occurs nowhere in + * the proof. A theory that can invert its own index expressions solves the equation for the + * variable instead. * - * @param term an accepted trigger term - * @param clauseVariables the quantified variables of the clause the trigger belongs to - * @param services access to the theory operators - * @return derived triggers, possibly empty + * Instantiating a universally quantified formula with any term is sound, so a solution that + * turns out not to reproduce the instance costs an instantiation and nothing else. + * + * @param pattern a trigger subterm, containing at least one variable not yet bound in + * {@code varMap} + * @param instance the ground term it should match + * @param varMap the bindings established so far + * @param services access to the theory's operators + * @return the extended bindings, or null when this theory cannot solve the equation */ - List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services); + default ImmutableMap solveForVariable(JTerm pattern, JTerm instance, + ImmutableMap varMap, Services services) { + return null; + } /** * Checks whether the literal holds on its own, for cost prediction. The literal is passed @@ -111,7 +107,7 @@ default LiteralDecision decideFromAxiom(JTerm literal, JTerm axiom, Services ser } /** - * Whether the equality-based normalisation of the cost prediction (see {@link Congruence}) may + * Whether the equality-based normalisation of the cost prediction (see {@code Congruence}) may * rewrite occurrences of {@code from} to {@code to}, justified by an assumed equality between * the two. The proof search keeps the terms of a theory in a normal form of the theory's own * rules, integer terms in polynomial form for example. A theory vetoes here when the rewrite diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/TriggerSupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/TriggerSupport.java new file mode 100644 index 00000000000..7d92a33ee07 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/TriggerSupport.java @@ -0,0 +1,165 @@ +/* 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.quantifierHeuristics.theory; + +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.strategy.quantifierHeuristics.TriggersSet; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; + +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableSet; + +/** + * A theory's contribution to the choice of what a quantified formula is instantiated with. + * + * Which subterms make a usable trigger depends on the theory a term belongs to: an array index or + * an integer comparison matches everywhere and discriminates nothing, while a read determines + * which location is accessed. + * A theory also derives further triggers from an accepted one, for example a read generalized so + * it matches over the many heaps of a proof, and it names instances that no trigger reaches at + * all. + * + * This is the part of a theory's contribution that is specific to the terms a front end builds. + * A front end without a heap has nothing to contribute here and still reuses + * {@link TheoryReasoning}. + */ +public interface TriggerSupport { + + /** + * The verdict of a theory on a trigger candidate: whether the candidate becomes a trigger, + * and whether the search for triggers continues with the term enclosing it. + * + * Trigger selection traverses each literal of the quantified formula bottom-up. A candidate + * is a subterm that contains a quantified variable and is not a variable itself. For every + * candidate the verdict of every theory is determined, and the verdicts are combined as + * follows: one {@code FORBIDDEN} discards the candidate; otherwise one + * {@code PREFER_ENCLOSING} registers the candidate as a trigger and continues the search + * with the enclosing term; otherwise the candidate is registered as a trigger, and an + * enclosing term becomes a candidate only if it contains a quantified variable that the + * registered trigger does not. + */ + enum CandidateVerdict { + /** + * The candidate may become a trigger. If every theory returns {@code ACCEPTABLE}, the + * candidate is registered, and no enclosing term becomes a trigger for the variables + * the candidate binds. + */ + ACCEPTABLE, + /** + * The candidate is not a trigger, because a match of it discriminates nothing: an + * equality or a comparison {@code <=}, {@code >=} matches every literal of its shape, + * and the index packaging {@code arr(i)} of an array access matches every access. The + * search continues with the enclosing term. Where every subterm of a term is forbidden, + * the term itself is the candidate. + */ + FORBIDDEN, + /** + * The candidate is a trigger, and the term enclosing it is a candidate as well. The + * index {@code k + t} of an array access {@code a[k + t]} is such a case. The sum binds + * {@code t} but does not determine the array. The read determines the array, so both + * are registered. + */ + PREFER_ENCLOSING + } + + /** + * Returns this theory's verdict on a trigger candidate. The combination of the verdicts of + * all theories is described at {@link CandidateVerdict}. + * + * @param candidate a subterm that contains the quantified variables and is a trigger candidate + * @param enclosing the term the candidate is an argument of, null at the top of a literal + * @param services access to the theory operators + * @return the verdict + */ + CandidateVerdict verdictOn(JTerm candidate, JTerm enclosing, Services services); + + /** + * Additional triggers derived from the accepted trigger {@code term}, for example a read + * generalized so it matches across the many heaps of a proof. The returned triggers are matched + * by unification (they may contain metavariables). + * + * @param term an accepted trigger term + * @param clauseVariables the quantified variables of the clause the trigger belongs to + * @param services access to the theory operators + * @param metavariableFactory supplies the metavariables a derived trigger needs + * @return derived triggers, possibly empty + */ + List provideTriggers(JTerm term, ImmutableSet clauseVariables, + Services services, MetavariableFactory metavariableFactory); + + /** + * The fallback triggers this theory offers for a clause of a formula that no trigger + * instantiates. + * + * Some formulas yield no covering trigger in any clause: every literal holding the + * quantified variable is forbidden, and what remains binds no universal variable. Such a + * formula is never instantiated through its own terms. This method is the last resort, asked + * for each clause of such a formula and for no other, so an implementation does not compete + * with the ordinary selection and cannot lose an instantiation that exists anyway. The + * given clause is therefore uncovered itself; the value also tells, per literal, what the + * selection did find. Instances a theory reads off the formula directly, without a trigger, + * are not part of this condition: they are found later, per sequent. + * + * A returned trigger is registered as theory-provided: it is unified, and under the most + * informed treatment also matched structurally, so a metavariable in it can bind a term that + * does not occur in the formula, and a theory can solve an index below it. Instances it + * yields carry the {@code FALLBACK} origin, which only the most informed treatment admits. A + * fallback that binds only some of the clause's variables is an element, and may combine + * with other elements, the formula's own included, into a covering multi-trigger: the cover + * search runs again after the fallbacks are registered. + * + * @param selection one clause of the formula, with the triggers its literals yielded + * @param services access to the theory operators + * @param metavariableFactory supplies the metavariables a fallback trigger needs + * @return the fallback triggers, possibly empty + */ + default List fallbackTriggers(ClauseTriggers selection, Services services, + MetavariableFactory metavariableFactory) { + return List.of(); + } + + /** + * The instance candidates this theory supplies for a subterm of the quantified formula. They + * are used for the quantified variable directly, not through a trigger. + * + * Matching binds the quantified variable to a subterm of the term it matched, so it cannot + * produce an instance that occurs in no trigger position. Such an instance has to come from a + * theory instead. An array read is one case: the index a store writes is what collapses the + * read, and it is ground, so no trigger contains it. + * + * The caller descends through the matrix and passes every subterm, so an implementation + * decides on the subterm alone. A candidate is costed like a matched one. + * + * @param subterm a subterm of the quantified formula's matrix + * @param variable the quantified variable an instance is sought for + * @param services access to the theory operators + * @return the candidate instances, possibly empty + */ + default List provideInstances(JTerm subterm, QuantifiableVariable variable, + Services services) { + return List.of(); + } + + /** + * Hands out the metavariables a derived trigger puts in place of a ground subterm. + * + * The names are counted within one {@link TriggersSet}, which is built from the quantified + * formula alone, so the same formula always yields the same names and no two derived triggers + * share one. That matters because two metavariables of equal name are still distinct and are + * then ordered by a creation counter shared across the whole prover, which would make the + * order, and through it the instances chosen, depend on which goal built its trigger set + * first. A support must therefore take its metavariables from here rather than name them. + */ + interface MetavariableFactory { + /** + * @param sort the sort the metavariable stands for + * @return a metavariable distinct from every other one of its trigger set + */ + Metavariable fresh(Sort sort); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/GenPolTieBreak.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/GenPolTieBreak.java similarity index 84% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/GenPolTieBreak.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/GenPolTieBreak.java index 8c77ab1213f..96620621400 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/GenPolTieBreak.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/GenPolTieBreak.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak; import java.util.ArrayDeque; import java.util.HashMap; @@ -9,9 +9,6 @@ import java.util.Map; import java.util.TreeSet; -import de.uka.ilkd.key.ldt.JavaDLTheory; -import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; - import org.key_project.logic.Term; import org.key_project.logic.op.Function; @@ -20,9 +17,9 @@ * instance's newest skolem constant was introduced on the branch, and breaks a same-generation * tie by the proving-polarity occurrence connection of {@link PolarityOccurrenceTieBreak}. */ -final class GenPolTieBreak extends PolarityOccurrenceTieBreak { +public final class GenPolTieBreak extends PolarityOccurrenceTieBreak { - static final GenPolTieBreak INSTANCE = new GenPolTieBreak(); + public static final GenPolTieBreak INSTANCE = new GenPolTieBreak(); private GenPolTieBreak() { } @@ -43,11 +40,7 @@ public Scorer prepare(View view) { * @return the generation rank */ private static long generationValue(Map ranks, Term inst) { - Integer rank = ranks.get(inst); - if (rank == null && (inst.op() instanceof ParametricFunctionInstance pfi - && pfi.getBase().name().equals(JavaDLTheory.CAST_NAME))) { - rank = ranks.get(inst.sub(0)); - } + final Integer rank = ranks.get(inst); return rank == null ? CAP : rank; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityOccurrenceTieBreak.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityOccurrenceTieBreak.java similarity index 95% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityOccurrenceTieBreak.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityOccurrenceTieBreak.java index db8e0a073c5..703d089e795 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityOccurrenceTieBreak.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityOccurrenceTieBreak.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak; import java.util.ArrayDeque; import java.util.ArrayList; @@ -15,12 +15,10 @@ import java.util.Set; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.Equality; import de.uka.ilkd.key.logic.op.IfThenElse; import de.uka.ilkd.key.logic.op.Junctor; -import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; import de.uka.ilkd.key.logic.op.Quantifier; import de.uka.ilkd.key.proof.Proof; @@ -103,7 +101,8 @@ protected static OccData computeOccData(View view) { /** * The occurrence value of an instance with the proving-polarity boost: a formula where the * instance occurs at proving polarity counts twice, so of two equally frequent instances the - * one the proof still has to say something about comes first. A weakly connected instance gets + * one occurring in a formula that remains to be proved comes first. A weakly connected instance + * gets * a * large value, a strongly connected one a small value, bounded by {@link #CAP}. * @@ -112,13 +111,8 @@ protected static OccData computeOccData(View view) { * @return the boosted occurrence value, between 0 and {@link #CAP} */ protected static long polarityValue(OccData d, Term inst) { - Integer occ = d.occ().get(inst); - Integer pos = d.goalOcc().get(inst); - if (occ == null && (inst.op() instanceof ParametricFunctionInstance pfi - && pfi.getBase().name().equals(JavaDLTheory.CAST_NAME))) { - occ = d.occ().get(inst.sub(0)); - pos = d.goalOcc().get(inst.sub(0)); - } + final Integer occ = d.occ().get(inst); + final Integer pos = d.goalOcc().get(inst); if (occ == null) { return CAP; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityTieBreak.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityTieBreak.java similarity index 73% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityTieBreak.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityTieBreak.java index c6db279692c..6e85f35ecae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityTieBreak.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityTieBreak.java @@ -1,16 +1,16 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak; /** * Orders tied instantiation candidates by their proving-polarity connection to the sequent (see * {@link PolarityOccurrenceTieBreak#polarityValue}). The tie-break of the {@code Best} quantifier * treatment. */ -final class PolarityTieBreak extends PolarityOccurrenceTieBreak { +public final class PolarityTieBreak extends PolarityOccurrenceTieBreak { - static final PolarityTieBreak INSTANCE = new PolarityTieBreak(); + public static final PolarityTieBreak INSTANCE = new PolarityTieBreak(); private PolarityTieBreak() { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierInstantiationTieBreak.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/QuantifierInstantiationTieBreak.java similarity index 95% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierInstantiationTieBreak.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/QuantifierInstantiationTieBreak.java index e91785bf391..13336689376 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierInstantiationTieBreak.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/QuantifierInstantiationTieBreak.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak; import java.util.Collection; @@ -28,7 +28,7 @@ * {@link de.uka.ilkd.key.strategy.quantifierHeuristics.InstantiationCostScalerFeature}), so the * prediction itself is never overridden. */ -interface QuantifierInstantiationTieBreak { +public interface QuantifierInstantiationTieBreak { /** * The read-only view of a quantified formula's instantiation the tie-break reads: the candidate diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java index 54cc0fb3f4c..1cb02b44ce3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java @@ -21,11 +21,11 @@ import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.inst.SVInstantiations; -import de.uka.ilkd.key.strategy.quantifierHeuristics.Constraint; -import de.uka.ilkd.key.strategy.quantifierHeuristics.EqualityConstraint; -import de.uka.ilkd.key.strategy.quantifierHeuristics.Metavariable; import de.uka.ilkd.key.strategy.quantifierHeuristics.PredictCostProver; import de.uka.ilkd.key.strategy.quantifierHeuristics.Substitution; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Constraint; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.EqualityConstraint; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; import org.key_project.logic.Name; import org.key_project.logic.op.Function; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key index d4089afb714..b41683db336 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key @@ -534,6 +534,21 @@ \heuristics(simplify_select_elim_store) }; + \lemma + differentValuesForSameHeapAndFieldImplyDifferentObjects { + \schemaVar \term Heap h; + \schemaVar \term Object o, o2; + \schemaVar \term Field f; + \schemaVar \term beta x; + + \assumes(select(h, o, f) = x ==>) + \find(==> select(h, o2, f) = x) + + \add(==> o = o2) + + \heuristics(derive_inequality) + }; + dismissNonSelectedField { \schemaVar \term Heap h; \schemaVar \term Object o, u; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key index 23dbc2cb225..88a9c8e5946 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key @@ -278,6 +278,7 @@ hide_auxiliary_eq; hide_auxiliary_eq_const; simplify_heap_high_costs; + derive_inequality; // chrisg: pattern-based automation rules auto_induction; diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index fd1d85147d9..22c6e1a7566 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -524,6 +524,8 @@ public static ProofCollection automaticJavaDL() throws IOException { g.provable("heap/BoyerMoore/BM.count.accessible.key"); g.provable("heap/BoyerMoore/BM.count.key"); g.provable("heap/BoyerMoore/BM.monoLemma.key"); + g.provable("heap/Adjacency/project.key"); + g.provable("heap/Adjacency/distinct.key"); g = c.group("quicksort"); g.setDirectory("heap/quicksort"); @@ -905,6 +907,10 @@ public static ProofCollection automaticJavaDL() throws IOException { g.provable("standard_key/quantifiers/normalisation12.key"); g.provable("standard_key/quantifiers/normalisation13.key"); g.provable("standard_key/quantifiers/triggers0.key"); + g.provable("standard_key/quantifiers/affineArrayIndices.key"); + g.provable("standard_key/quantifiers/issue3972MVE.key"); + g.provable("standard_key/quantifiers/affineSeqIndices.key"); + g.provable("standard_key/quantifiers/affineSeqSub.key"); g = c.group("strings"); diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java index 8f635415269..2e8321e1ea8 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java +++ b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java @@ -3,16 +3,24 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; +import java.util.ArrayList; import java.util.HashSet; +import java.util.List; import java.util.Set; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.LogicVariable; +import de.uka.ilkd.key.logic.sort.ArraySort; import de.uka.ilkd.key.logic.sort.SortImpl; import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; import de.uka.ilkd.key.rule.TacletForTests; +import de.uka.ilkd.key.strategy.quantifierHeuristics.constraint.Metavariable; +import de.uka.ilkd.key.util.HelperClassForTests; import org.key_project.logic.Name; import org.key_project.logic.Namespace; @@ -380,6 +388,95 @@ public void uniTriggerPicksInnermostSubterm() { assertEquals(all.sub(0).sub(0).sub(0), triggers.iterator().next().getTriggerTerm()); // f2rr(x) } + @Test + public void sequenceReadWithCompoundIndexIsRegisteredWithItsIndex() { + // forall int t. seqGet(b, k + t) = seqGet(a, m + t): the triggers are the two + // sums and the two reads around them, see SequenceTheorySupport. + final Services services = proof.getServices(); + final TermBuilder tb = services.getTermBuilder(); + final Sort intSort = services.getTypeConverter().getIntegerLDT().targetSort(); + final Sort seqSort = services.getTypeConverter().getSeqLDT().targetSort(); + final JTerm a = tb.func(new JFunction(new Name("seq_a"), seqSort, new Sort[0])); + final JTerm b = tb.func(new JFunction(new Name("seq_b"), seqSort, new Sort[0])); + final JTerm k = tb.func(new JFunction(new Name("int_k"), intSort, new Sort[0])); + final JTerm m = tb.func(new JFunction(new Name("int_m"), intSort, new Sort[0])); + final LogicVariable t = new LogicVariable(new Name("t"), intSort); + final JTerm readB = tb.seqGet(intSort, b, tb.add(k, tb.var(t))); + final JTerm readA = tb.seqGet(intSort, a, tb.add(m, tb.var(t))); + final JTerm all = tb.all(t, tb.equals(readB, readA)); + final Set expected = Set.of(readB.sub(1), readB, readA.sub(1), readA); + final Set actual = new HashSet<>(); + for (final Trigger trigger : TriggersSet.create(all, services).getAllTriggers()) { + actual.add(trigger.getTriggerTerm()); + } + assertEquals(expected, actual); + } + + @Test + public void heapOfAReadBelowATriggerIsGeneralized() { + // forall int t. seqGet(s, idx[t]) = seqGet(u, t): the array read idx[t] is a + // trigger and, in the index position of seqGet, keeps the search going, so the sequence + // read is a trigger too. The heap support frees the heap of idx[t] in both: as the + // read's own variant and inside the sequence read, without the sequence support knowing + // about heaps. The taclet test services declare no arr function, so the services of a + // loaded problem are used. + final Services services = HelperClassForTests.createServices(); + final TermBuilder tb = services.getTermBuilder(); + final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); + final Sort intSort = services.getTypeConverter().getIntegerLDT().targetSort(); + final Sort seqSort = services.getTypeConverter().getSeqLDT().targetSort(); + final Sort intArray = ArraySort.getArraySort(intSort, services.getJavaInfo().objectSort(), + services.getJavaInfo().cloneableSort(), services.getJavaInfo().serializableSort()); + final JTerm idx = tb.func(new JFunction(new Name("arr_idx"), intArray, new Sort[0])); + final JTerm heap = + tb.func(new JFunction(new Name("heap_h"), heapLDT.targetSort(), new Sort[0])); + final JTerm s = tb.func(new JFunction(new Name("seq_s"), seqSort, new Sort[0])); + final JTerm u = tb.func(new JFunction(new Name("seq_u"), seqSort, new Sort[0])); + final LogicVariable t = new LogicVariable(new Name("t"), intSort); + final JTerm indexRead = tb.select(intSort, heap, idx, tb.arr(tb.var(t))); + final JTerm read = tb.seqGet(intSort, s, indexRead); + final JTerm all = tb.all(t, tb.equals(read, tb.seqGet(intSort, u, tb.var(t)))); + final List derived = new ArrayList<>(); + for (final Trigger trigger : TriggersSet.create(all, services).getAllTriggers()) { + if (trigger.isTheoryProvided()) { + derived.add(trigger.getTriggerTerm()); + } + } + assertEquals(2, derived.size(), "the index read and the sequence read get a variant"); + for (final Term variant : derived) { + final JTerm freedRead = (JTerm) (variant.op() == read.op() ? variant.sub(1) : variant); + assertEquals(indexRead.op(), freedRead.op()); + assertTrue(freedRead.sub(0).op() instanceof Metavariable, "its heap is free"); + assertEquals(indexRead.sub(1), freedRead.sub(1)); + assertEquals(indexRead.sub(2), freedRead.sub(2)); + } + } + + @Test + public void heapOfAGroundReadStaysInTheTrigger() { + // forall int t. seqGet(select(heap, o, f), t) = seqGet(s, t): the field read + // carries no quantified variable; it names a value of the trigger and keeps its heap, so + // no theory-provided trigger is derived. + final Services services = proof.getServices(); + final TermBuilder tb = services.getTermBuilder(); + final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); + final Sort intSort = services.getTypeConverter().getIntegerLDT().targetSort(); + final Sort seqSort = services.getTypeConverter().getSeqLDT().targetSort(); + final JTerm o = tb.func( + new JFunction(new Name("obj_o"), services.getJavaInfo().objectSort(), new Sort[0])); + final JTerm f = + tb.func(new JFunction(new Name("field_f"), heapLDT.getFieldSort(), new Sort[0])); + final JTerm heap = + tb.func(new JFunction(new Name("heap_h"), heapLDT.targetSort(), new Sort[0])); + final JTerm s = tb.func(new JFunction(new Name("seq_s"), seqSort, new Sort[0])); + final LogicVariable t = new LogicVariable(new Name("t"), intSort); + final JTerm read = tb.seqGet(intSort, tb.select(seqSort, heap, o, f), tb.var(t)); + final JTerm all = tb.all(t, tb.equals(read, tb.seqGet(intSort, s, tb.var(t)))); + for (final Trigger trigger : TriggersSet.create(all, services).getAllTriggers()) { + assertFalse(trigger.isTheoryProvided(), "no variant for a ground read"); + } + } + @Test public void fullCoverUniTriggerPreferredOverElements() { // prs(x,y) covers both clause variables -> single uni-trigger; partial pr(x) is dropped. diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArithTest.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HandleArithTest.java similarity index 98% rename from key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArithTest.java rename to key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HandleArithTest.java index 79315d794bb..63cec96df82 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArithTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/theory/HandleArithTest.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.theory; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityWalkTest.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityWalkTest.java similarity index 96% rename from key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityWalkTest.java rename to key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityWalkTest.java index 6ae08b91638..facc8aaabd1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PolarityWalkTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/tiebreak/PolarityWalkTest.java @@ -1,7 +1,7 @@ /* 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.quantifierHeuristics; +package de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; @@ -10,7 +10,7 @@ import de.uka.ilkd.key.logic.op.LogicVariable; import de.uka.ilkd.key.logic.sort.SortImpl; import de.uka.ilkd.key.rule.TacletForTests; -import de.uka.ilkd.key.strategy.quantifierHeuristics.PolarityOccurrenceTieBreak.OccInfo; +import de.uka.ilkd.key.strategy.quantifierHeuristics.tiebreak.PolarityOccurrenceTieBreak.OccInfo; import org.key_project.logic.Name; import org.key_project.logic.op.Function; diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 2dddf189f87..f6dad324aa4 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -5660,6 +5660,14 @@ diamond_split_termination { #s ... }\> (true))) +Choices: programRules:Java} +----------------------------------------------------- +== differentValuesForSameHeapAndFieldImplyDifferentObjects (differentValuesForSameHeapAndFieldImplyDifferentObjects) ========================================= +differentValuesForSameHeapAndFieldImplyDifferentObjects { +\assumes ([equals(select(h,o,f),x)]==>[]) +\find(==>equals(select(h,o2,f),x)) +\add []==>[equals(o,o2)] +\heuristics(derive_inequality) Choices: programRules:Java} ----------------------------------------------------- == disjointAllFields (disjointAllFields) ========================================= diff --git a/key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof b/key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof new file mode 100644 index 00000000000..568098806ed --- /dev/null +++ b/key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof @@ -0,0 +1,99 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 20000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + + +\proofObligation +// +{ + "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput", + "name" : "differentValuesForSameHeapAndFieldImplyDifferentObjects" +} + +\proof { +(keyLog "0" (keyUser "bubel" ) (keyVersion "05e3502a91ab2e6abbe38d72dd4c959321fc29a5")) + +(autoModeTime "37") + +(branch "dummy ID" +(rule "impRight" (formula "1")) +(rule "orRight" (formula "2")) +(rule "notRight" (formula "3")) +(rule "eqSymm" (formula "2")) +(rule "applyEq" (formula "3") (term "1,0") (ifseqformula "2")) +(rule "close" (formula "3") (ifseqformula "1")) +) +} diff --git a/key.ui/examples/heap/Adjacency/AdjacencyStore.java b/key.ui/examples/heap/Adjacency/AdjacencyStore.java new file mode 100644 index 00000000000..326b4a368ac --- /dev/null +++ b/key.ui/examples/heap/Adjacency/AdjacencyStore.java @@ -0,0 +1,53 @@ +/** + * Storing one node's neighbour list into the flat edge array of an adjacency structure. + */ +public final class AdjacencyStore { + + /*@ public normal_behavior + @ requires edges != null && list != null && edges != list; + @ requires 0 <= at && 0 <= n; + @ requires at + n <= edges.length; + @ requires n <= list.length; + @ ensures (\forall int i; 0 <= i && i < n; edges[at + i] == list[i]); + @ assignable edges[at .. at + n - 1]; + @*/ + public static void storeList(int[] edges, int at, int[] list, int n) { + int i = 0; + /*@ loop_invariant 0 <= i && i <= n; + @ loop_invariant (\forall int t; 0 <= t && t < i; edges[at + t] == list[t]); + @ assignable edges[at .. at + n - 1]; + @ decreases n - i; + @*/ + while (i < n) { + edges[at + i] = list[i]; + i++; + } + } + + /*@ public normal_behavior + @ requires edges != null && list != null && edges != list; + @ requires 0 <= at && 0 <= n; + @ requires at + n <= edges.length; + @ requires n <= list.length; + @ requires (\forall int i; 0 <= i && i < n; 0 <= list[i] && list[i] < nodeCount); + @ ensures (\forall int p; at <= p && p < at + n; + @ 0 <= edges[p] && edges[p] < nodeCount); + @ assignable edges[at .. at + n - 1]; + @*/ + public static void storeValidList(int[] edges, int at, int[] list, int n, int nodeCount) { + storeList(edges, at, list, n); + } + + /*@ public normal_behavior + @ requires edges != null && list != null && edges != list; + @ requires 0 <= at && 0 <= n; + @ requires at + n <= edges.length; + @ requires n <= list.length; + @ requires (\forall int u, v; 0 <= u && u < v && v < n; list[u] != list[v]); + @ ensures (\forall int p, q; at <= p && p < q && q < at + n; edges[p] != edges[q]); + @ assignable edges[at .. at + n - 1]; + @*/ + public static void storeDistinctList(int[] edges, int at, int[] list, int n) { + storeList(edges, at, list, n); + } +} diff --git a/key.ui/examples/heap/Adjacency/distinct.key b/key.ui/examples/heap/Adjacency/distinct.key new file mode 100644 index 00000000000..bb71d214ff0 --- /dev/null +++ b/key.ui/examples/heap/Adjacency/distinct.key @@ -0,0 +1,34 @@ +\settings { +"#Proof-Settings-Config-File +#Mon Aug 03 16:58:18 CEST 2009 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND +[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS +[DecisionProcedure]Timeout=60 +[View]ShowWholeTaclet=false +[View]MaxTooltipLines=40 +[General]DnDDirectionSensitive=true +[General]StupidMode=true +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[Strategy]Timeout=-1 +[Strategy]MaximumNumberOfAutomaticApplications=50000 +[Choice]DefaultChoices=assertions-assertions\:on, intRules-intRules\:arithmeticSemanticsIgnoringOF,initialisation-initialisation\:disableStaticInitialisation,programRules-programRules\:Java,runtimeExceptions-runtimeExceptions\:ban,JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , optimisedSelectRules-optimisedSelectRules\\:on , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off +[DecisionProcedure]ActiveRule=_noname_ +[General]UseJML=true +[View]HideClosedSubtrees=false +[View]HideIntermediateProofsteps=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +" +} + +\javaSource "."; + +\chooseContract "AdjacencyStore[AdjacencyStore::storeDistinctList([I,int,[I,int)].JML normal_behavior operation contract.0"; diff --git a/key.ui/examples/heap/Adjacency/project.key b/key.ui/examples/heap/Adjacency/project.key new file mode 100644 index 00000000000..8b2eae56536 --- /dev/null +++ b/key.ui/examples/heap/Adjacency/project.key @@ -0,0 +1,34 @@ +\settings { +"#Proof-Settings-Config-File +#Mon Aug 03 16:58:18 CEST 2009 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND +[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS +[DecisionProcedure]Timeout=60 +[View]ShowWholeTaclet=false +[View]MaxTooltipLines=40 +[General]DnDDirectionSensitive=true +[General]StupidMode=true +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[Strategy]Timeout=-1 +[Strategy]MaximumNumberOfAutomaticApplications=50000 +[Choice]DefaultChoices=assertions-assertions\:on, intRules-intRules\:arithmeticSemanticsIgnoringOF,initialisation-initialisation\:disableStaticInitialisation,programRules-programRules\:Java,runtimeExceptions-runtimeExceptions\:ban,JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , optimisedSelectRules-optimisedSelectRules\\:on , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off +[DecisionProcedure]ActiveRule=_noname_ +[General]UseJML=true +[View]HideClosedSubtrees=false +[View]HideIntermediateProofsteps=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +" +} + +\javaSource "."; + +\chooseContract "AdjacencyStore[AdjacencyStore::storeValidList([I,int,[I,int,int)].JML normal_behavior operation contract.0"; diff --git a/key.ui/examples/standard_key/quantifiers/affineArrayIndices.key b/key.ui/examples/standard_key/quantifiers/affineArrayIndices.key new file mode 100644 index 00000000000..b54f8a81319 --- /dev/null +++ b/key.ui/examples/standard_key/quantifiers/affineArrayIndices.key @@ -0,0 +1,88 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:showSatisfiability", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 10000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + +\programVariables { + int[] a; + int[] b; + int k; + int m; + int n; +} + +\problem { + \forall int t; (0 <= t & t < n -> b[k + t] = a[m + t]) + ==> \forall int x; (k <= x & x < k + n -> b[x] = a[x - k + m]) +} diff --git a/key.ui/examples/standard_key/quantifiers/affineSeqIndices.key b/key.ui/examples/standard_key/quantifiers/affineSeqIndices.key new file mode 100644 index 00000000000..fc1c507f311 --- /dev/null +++ b/key.ui/examples/standard_key/quantifiers/affineSeqIndices.key @@ -0,0 +1,88 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:showSatisfiability", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 10000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + +\programVariables { + Seq a; + Seq b; + int k; + int m; + int n; +} + +\problem { + \forall int t; (0 <= t & t < n -> seqGet(b, k + t) = seqGet(a, m + t)) + ==> \forall int x; (k <= x & x < k + n -> seqGet(b, x) = seqGet(a, x - k + m)) +} diff --git a/key.ui/examples/standard_key/quantifiers/affineSeqSub.key b/key.ui/examples/standard_key/quantifiers/affineSeqSub.key new file mode 100644 index 00000000000..5a470a3b8d8 --- /dev/null +++ b/key.ui/examples/standard_key/quantifiers/affineSeqSub.key @@ -0,0 +1,89 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:showSatisfiability", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 10000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + +\programVariables { + Seq a; + Seq b; + int k; + int m; + int n; +} + +\problem { + 0 <= n & 0 <= k & 0 <= m & k + n <= seqLen(b) & m + n <= seqLen(a), + \forall int t; (0 <= t & t < n -> seqGet(seqSub(b, k, k + n), t) = seqGet(seqSub(a, m, m + n), t)) + ==> \forall int x; (k <= x & x < k + n -> seqGet(b, x) = seqGet(a, x - k + m)) +} diff --git a/key.ui/examples/standard_key/quantifiers/issue3972MVE.key b/key.ui/examples/standard_key/quantifiers/issue3972MVE.key new file mode 100644 index 00000000000..d49d9eaa97f --- /dev/null +++ b/key.ui/examples/standard_key/quantifiers/issue3972MVE.key @@ -0,0 +1,95 @@ +// taken from Issue #3972 (https://github.com/KeYProject/key/issues/3972) +// by Mattias Ulbrich + +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:showSatisfiability", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 10000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + +\functions { + int i_0; + int v_0; +} + +\programVariables { + int[] a; +} + +\problem{ + a.length = i_0, + \forall int u; (u < v_0 & u >= 0 -> \exists int j; (j < i_0 & j >= 0 & u = a[j])) +==> + \forall int u; + (u >= 0 & u < v_0 -> \exists int j; ((j >= 0 & j < a.length & u = a[j]))) +} \ No newline at end of file