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/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index c4cda4a412e..3b6dfee61c5 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 @@ -385,7 +385,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", @@ -394,7 +394,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, longConst(10), // orders candidates of one predicted-cost band by their @@ -419,10 +419,10 @@ 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()), + InstantiationCost.create(instOf("t"), triggerTreatment()), longConst(0)))); final TermBuffer splitInst = new TermBuffer(); @@ -610,9 +610,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/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index d3a856e7572..b9cae1d8584 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 @@ -9,6 +9,7 @@ import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.LocSetLDT; +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; @@ -180,6 +181,7 @@ private RuleSetDispatchFeature setupCostComputationF() { final int pullOutHeapSize = getHeapSizeBound(); bindRuleSet(d, "pull_out_heap", pullOutHeapSize <= 0 ? inftyConst() : pullOutHeap(pullOutHeapSize)); + bindRuleSet(d, "derive_inequality", longConst(-2000)); bindRuleSet(d, "simplify_heap_high_costs", inftyConst()); bindRuleSet(d, "javaIntegerSemantics", @@ -491,6 +493,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..e876d98dbae 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,6 +3,8 @@ * 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; @@ -14,30 +16,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 QuantifierTheorySupport#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 +85,112 @@ 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 says 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. - * - * @return true if it is a new vaiable or the instance it matched is the same as that it matched - * before. + * 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}. */ - 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)) { + return null; } - - if (oldTerm.equals(instance)) { - return varMap; + for (QuantifierTheorySupport support : TriggersSet.THEORY_SUPPORTS) { + final ImmutableMap solved = support + .solveForVariable(patternTerm, instanceTerm, bindings.variables(), services); + if (solved != null) { + return bindings.withSolution(solved); + } } return null; } + } 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 index 3442c475a1e..f2f54e346a8 100644 --- 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 @@ -48,7 +48,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(); } 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 index 199afb85e17..df485b4a2a6 100644 --- 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 @@ -13,7 +13,6 @@ 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; @@ -21,7 +20,7 @@ /** * 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 + * Rejects the bare array-index constructor {@code arr(i)} (an index, 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. @@ -44,12 +43,23 @@ public boolean rejectsAsTrigger(JTerm candidate, Services services) { .endsWith(PipelineConstants.IMPLICIT_CREATED)) { return true; } - // the array-index constructor arr(i) alone is a coordinate, not a read: matching on it + // the array-index constructor arr(i) alone is an index, 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(); } + /** + * An array index gives way to the read around it: alone it matches every integer term on the + * sequent, while the read says which access is meant. Both are registered, so no instantiation + * is lost. + */ + @Override + public boolean prefersEnclosingTrigger(JTerm candidate, JTerm enclosing, Services services) { + return enclosing != null + && enclosing.op() == services.getTypeConverter().getHeapLDT().getArr(); + } + /** * Provides the heap-generalized array read triggers, one per array dimension of the read. * @@ -60,8 +70,9 @@ public boolean rejectsAsTrigger(JTerm candidate, Services services) { */ @Override public List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services) { - return dimensionVariants(term, clauseVariables, services); + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { + return dimensionVariants(term, clauseVariables, services, metavariableFactory); } /** @@ -80,9 +91,11 @@ public List provideTriggers(JTerm term, * * 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. + * metavariable per level: for {@code x[i][i_1]} the triggers {@code select(H0, x, arr(i))} + * and {@code select(H1, select(H0, x, arr(i)), arr(i_1))}, whose metavariables {@code H0} and + * {@code H1} each stand for any heap, and 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 @@ -90,23 +103,24 @@ public List provideTriggers(JTerm term, * @return one generalized read trigger per array dimension, possibly empty */ private List dimensionVariants(JTerm term, - ImmutableSet clauseVariables, Services services) { + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { 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<>(); + // array indices, innermost first + final List arrayIndices = new ArrayList<>(); JTerm base = term; while (heapLDT.isSelectOp(base.op()) && base.sub(2).op() == heapLDT.getArr()) { - coordinates.add(0, base.sub(2).sub(0)); + arrayIndices.add(0, base.sub(2).sub(0)); base = base.sub(1); } - if (coordinates.isEmpty() || !(base.sort() instanceof ArraySort)) { + if (arrayIndices.isEmpty() || !(base.sort() instanceof ArraySort)) { return variants; } boolean anyVar = false; - for (final JTerm c : coordinates) { + for (final JTerm c : arrayIndices) { if (!TriggerUtils.intersect(c.freeVars(), clauseVariables).isEmpty()) { anyVar = true; } @@ -117,14 +131,13 @@ private List dimensionVariants(JTerm term, // 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++) { + for (int depth = 0; depth < arrayIndices.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)); + final JTerm heapVar = tb.var(metavariableFactory.fresh(heapLDT.targetSort())); + final JTerm arrField = tb.func(heapLDT.getArr(), arrayIndices.get(depth)); read = tb.select(sort, heapVar, read, arrField); if (!TriggerUtils.intersect(read.freeVars(), clauseVariables).isEmpty() && !read.equals(term)) { @@ -134,27 +147,5 @@ private List dimensionVariants(JTerm term, 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/Instantiation.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java index cdd2f5dd3f4..bdbf4e0927a 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 @@ -71,37 +71,40 @@ 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); + // written-array-index candidates are part of the theory-aware selection, dropped in classic + if (!treatment.isClassic()) { + addWrittenArrayIndexInstances((JTerm) matrix, 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. + * Instance candidates taken from written array indices. Where the matrix reads an array + * through a store chain, {@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. No trigger produces it, since {@code c} + * holds no quantified variable. The candidates are costed like matched ones, so useless ones + * are ranked down as usual. */ - private void addStoreCoordinateInstances(JTerm term, Services services) { + private void addWrittenArrayIndexInstances(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. @@ -112,11 +115,11 @@ private void addStoreCoordinateInstances(JTerm term, Services services) { } } for (int i = 0; i < term.arity(); i++) { - addStoreCoordinateInstances(term.sub(i), services); + addWrittenArrayIndexInstances(term.sub(i), services); } } - /** Adds every ground index written on {@code obj}'s array fields in {@code heap}. */ + /** Adds every ground array 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()) { @@ -129,7 +132,7 @@ private void collectWrittenIndices(JTerm heap, JTerm obj, Services services) { final ImmutableMap varMap = DefaultImmutableMap.nilMap() .put(firstVar, field.sub(0)); - addInstance(new Substitution(varMap), services); + addInstance(new Substitution(varMap), services, 0); } } for (int i = 0; i < heap.arity(); i++) { @@ -137,26 +140,24 @@ private void collectWrittenIndices(JTerm heap, JTerm obj, Services 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 {@code instancesWithCosts}, 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 +165,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; } @@ -184,29 +185,77 @@ private static ImmutableSet sequentToTerms(Sequent seq) { * @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); + addInstance(sub, services, + sub.isSolvedByTheory() ? SOLVED_POSITION_SURCHARGE : 0); + matchedByOwnTerms = true; + } + } + // Basic matching binds the trigger's metavariable to a term the trigger never read, so + // the instance speaks about a state the formula does not name. Where none of the formula's + // own terms match the sequent it is all there is, and costs what it predicts. Where they + // do match, it is offered behind them, so the search takes it only if nothing cheaper + // closes the goal. Only the cheapest offer for an instance is recorded. + for (final Trigger t : triggersSet.getAllTriggers()) { + if (!t.isTheoryProvided()) { + continue; + } + final ImmutableSet unified = + t.getSubstitutionsFromTerms(terms, services, false); + for (final Substitution sub : unified) { + addInstance(sub, services, 0); + } + if (treatment.allowsBasicMatchingOfTheoryTriggers()) { + final long surcharge = matchedByOwnTerms ? THEORY_TRIGGER_SURCHARGE : 0; + for (final Substitution sub : t.getSubstitutionsFromTerms(terms, services, true)) { + if (!unified.contains(sub)) { + addInstance(sub, services, surcharge); + } + } } } } - private void addInstance(Substitution sub, Services services) { - final long cost = + /** + * What an instance costs on top of its prediction when only basic matching of a + * theory-provided trigger produces it, and the formula's own terms do match the sequent. + * + * A predicted cost is a product of clause sizes (see {@link PredictCostProver}), so any + * surcharge above that range puts such instances behind the supported ones; the exact value + * does not matter. + */ + private static final long THEORY_TRIGGER_SURCHARGE = 10000L; + + /** + * What an instance costs on top of its prediction when a theory solved a disagreeing position + * to obtain it. The instance is then a term the matched term does not contain, so it is + * offered behind those the two terms produced by agreeing throughout. + */ + private static final long SOLVED_POSITION_SURCHARGE = 10000L; + + + /** + * @param sub the instantiation found + * @param services access to the theories + * @param surcharge what the instance costs on top of its prediction, zero where one of the + * formula's own terms produced it + */ + private void addInstance(Substitution sub, Services services, long surcharge) { + long cost = PredictCostProver.computerInstanceCost(sub, (JTerm) getMatrix(), assumedLiterals, congruence, services); - if (cost != -1) { - addInstance(sub, cost); + if (cost == -1) { + return; } + addInstance(sub, cost + surcharge); } - /** - * Pre-normalises the assumed literals once through the congruence, so each candidate's cost - * prediction reuses the result instead of re-normalising them. - * - * @param lits the assumed literals - * @return the normalised literals, or {@code lits} unchanged when the congruence is trivial - */ + /** Normalizes every literal by the congruence, so equal atoms coincide. */ private ImmutableSet normalizeAll(ImmutableSet lits) { if (congruence.isTrivial()) { return lits; @@ -218,19 +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); @@ -288,8 +324,8 @@ 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) { @@ -320,14 +356,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); } /** 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..29058c02d6a 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 @@ -66,13 +66,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/IntegerTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java index 76e6fb18dd5..5f5efb71fd8 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/IntegerTheorySupport.java @@ -3,14 +3,21 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; +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; /** @@ -46,7 +53,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(); } @@ -114,6 +122,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/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..cd5bc7bf694 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,16 @@ public String toString() { return String.valueOf(elements); } + @Override + public boolean isTheoryProvided() { + for (final Trigger element : elements) { + if (element.isTheoryProvided()) { + return true; + } + } + return false; + } + @Override public Term getTriggerTerm() { return clause; 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/QuantifierTheorySupport.java index 3c9a2ebe71b..3c1927d2989 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/QuantifierTheorySupport.java @@ -9,19 +9,21 @@ 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.logic.sort.Sort; +import org.key_project.util.collection.ImmutableMap; import org.key_project.util.collection.ImmutableSet; /** * A theory's contribution to quantifier instantiation. * * 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 + * choosing triggers: which subterms are unfit on their own (an array index, an integer + * comparison), and which further triggers to derive so that a read matches the terms a proof + * produces. 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. @@ -62,9 +64,51 @@ static LiteralDecision fromTruthTerm(JTerm t) { return LiteralDecision.UNKNOWN; } + /** + * Solves a trigger subterm against a ground instance when syntactic matching has failed. + * + * 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. + * + * 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 + */ + default ImmutableMap solveForVariable(JTerm pattern, JTerm instance, + ImmutableMap varMap, Services services) { + return null; + } + + /** + * Whether a candidate should give way to the term enclosing it, when that term yields a + * trigger of its own. + * + * Unlike {@link #rejectsAsTrigger}, this is a preference and not a veto. An array index + * matches every integer term on the sequent, while the read around it says which access is + * meant. Where no enclosing term yields a trigger the candidate is used anyway, since a + * clause without a trigger is never instantiated. + * + * @param candidate 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's operators + * @return whether an enclosing trigger is preferable to this candidate + */ + default boolean prefersEnclosingTrigger(JTerm candidate, JTerm enclosing, Services services) { + return false; + } + /** * 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. + * it is an array index or a connective rather than a read. * * @param candidate a subterm that contains the quantified variables and is a trigger candidate * @param services access to the theory operators @@ -79,10 +123,30 @@ static LiteralDecision fromTruthTerm(JTerm t) { * @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); + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory); + + /** + * 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); + } /** * Checks whether the literal holds on its own, for cost prediction. The literal is passed 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..1d967cf23b8 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,31 @@ 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; + } } 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..551fcc84afb --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java @@ -0,0 +1,47 @@ +/* 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 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. + */ +public enum TriggerTreatment { + + /** Everything the heuristic knows. */ + BEST, + + /** The theories' trigger selection, with theory-provided triggers unified only. */ + GOOD, + + /** Equality and integer rejection only, and no ordering of the candidates. */ + CLASSIC; + + 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 a theory-provided trigger may also be matched by {@link BasicMatching}, and not only + * unified. + * + * Basic matching binds the trigger's metavariable to a term the trigger never read, so a + * trigger written for one heap matches a read over another, and a theory can solve an array + * index along the way. It is the one part of the heuristic that instantiates from a term the + * formula does not name, so it is left to the most informed treatment. + */ + public boolean allowsBasicMatchingOfTheoryTriggers() { + return this == BEST; + } +} 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..e263cc2afa9 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 @@ -17,8 +17,10 @@ import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.logic.op.*; +import org.key_project.logic.Name; 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; @@ -70,6 +72,21 @@ public class TriggersSet { * register unequal copies of the same triggers. */ private final Set theoryTriggersProvidedFor = new HashSet<>(); + /** + * 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 QuantifierTheorySupport.MetavariableFactory}. + */ + private final QuantifierTheorySupport.MetavariableFactory metavariableFactory = + new QuantifierTheorySupport.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; /** @@ -230,7 +247,7 @@ public void createTriggers(Services services) { if (positive.op() == Junctor.NOT) { positive = positive.sub(0); } - addMaximalUniTriggers(positive, services); + addMaximalUniTriggers(positive, null, services); } } buildCoveringMultiTriggers(); @@ -244,7 +261,7 @@ public void createTriggers(Services services) { * @param services access to the theory operators and term construction * @return whether a trigger was found in the term or its subterms */ - private boolean addMaximalUniTriggers(JTerm term, Services services) { + private boolean addMaximalUniTriggers(JTerm term, JTerm enclosing, Services services) { if (!mightContainTriggers(term)) { return false; } @@ -255,7 +272,7 @@ private boolean addMaximalUniTriggers(JTerm term, Services services) { boolean foundSubtriggers = false; for (int i = 0; i < term.arity(); i++) { final JTerm subTerm = term.sub(i); - final boolean found = addMaximalUniTriggers(subTerm, services); + final boolean found = addMaximalUniTriggers(subTerm, term, services); if (found && uniVarsInTerm.subset(subTerm.freeVars())) { foundSubtriggers = true; @@ -266,7 +283,7 @@ private boolean addMaximalUniTriggers(JTerm term, Services services) { // 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); + return addUniTrigger(term, enclosing, services); } return true; @@ -336,7 +353,7 @@ private boolean mightContainTriggers(JTerm term) { /** * A trigger candidate is acceptable unless some theory's {@link QuantifierTheorySupport} - * rejects it as coordinate or connective material. + * rejects it as an array index or connective material. */ private boolean isAcceptableTrigger(JTerm term, Services services) { for (final QuantifierTheorySupport support : supports) { @@ -347,13 +364,23 @@ private boolean isAcceptableTrigger(JTerm term, Services services) { return true; } + /** Whether some theory would rather trigger on the term enclosing this one. */ + private boolean prefersEnclosing(JTerm term, JTerm enclosing, Services services) { + for (final QuantifierTheorySupport support : supports) { + if (support.prefersEnclosingTrigger(term, enclosing, services)) { + return true; + } + } + return false; + } + /** * 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 * * @return whether a trigger was registered for {@code term} */ - private boolean addUniTrigger(JTerm term, Services services) { + private boolean addUniTrigger(JTerm term, JTerm enclosing, Services services) { if (!isAcceptableTrigger(term, services)) { return false; } @@ -364,12 +391,14 @@ private boolean addUniTrigger(JTerm term, Services services) { if (theoryTriggersProvidedFor.add(term)) { for (final QuantifierTheorySupport support : supports) { for (final JTerm derived : support.provideTriggers(term, clauseVariables, - services)) { + services, metavariableFactory)) { registerUniTrigger(derived, true); } } } - return true; + // An array index is registered like any other candidate, but does not stop the + // ascent: the read around it says which access is meant and becomes a trigger too. + return !prefersEnclosing(term, enclosing, services); } private void registerUniTrigger(JTerm term, boolean matchByUnification) { 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..4051e8215b5 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 @@ -51,6 +51,16 @@ 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 tells the two apart, see + * {@link #computeSubstitutionsForTerm}. + */ + private final ConcurrentLruCache> matchResultsByBasicMatching = + new ConcurrentLruCache<>(1000); UniTrigger(Term trigger, ImmutableSet universalVariables, boolean onlyUnify, @@ -67,34 +77,60 @@ class UniTrigger implements Trigger { @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 && matchByUnification ? 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) { + private ImmutableSet computeSubstitutionsForTerm(Term target, + Services services, boolean basicMatching) { ImmutableSet subs = DefaultImmutableSet.nil(); - if (target.freeVars().size() > 0 || target.op() instanceof Quantifier - || matchByUnification) { + final boolean groundTarget = + target.freeVars().isEmpty() && !(target.op() instanceof Quantifier); + if (!groundTarget || matchByUnification) { subs = Matching.twoSidedMatching(this, target, services); - } else if (!onlyUnify) { - subs = Matching.basicMatching(this, target); + } + // Against a ground target basic matching applies as well, and only it lets a + // theory solve an array index: unification decides a pair of terms as a whole and offers no + // point at which a failing array index could be solved. + if (groundTarget && !onlyUnify && (basicMatching || !matchByUnification)) { + final ImmutableSet basicSubs = + Matching.basicMatching(this, target, services); + if (!basicSubs.isEmpty()) { + subs = subs.union(basicSubs); + } } return subs; } + @Override + public boolean isTheoryProvided() { + return matchByUnification; + } + @Override public Term getTriggerTerm() { return trigger; @@ -132,7 +168,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/resources/de/uka/ilkd/key/proof/rules/heapRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key index b27fbe81135..4a17a76e85a 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 cfd234be07b..1b3ad1c6be5 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 @@ -273,6 +273,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..6531efa1099 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"); 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";