Skip to content

Commit a17edad

Browse files
wadoonwadoon
committed
fix double Taclet problem
1 parent af811cc commit a17edad

3 files changed

Lines changed: 45 additions & 24 deletions

File tree

‎key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -423,7 +423,8 @@ public final ProofAggregate getPO() {
423423
}
424424
proofs[i] = createProof(poNames != null ? poNames[i] : name, poTerms[i], ic);
425425
if (taclets != null) {
426-
proofs[i].getOpenGoal(proofs[i].root()).indexOfTaclets().addTaclets(taclets);
426+
var filteredTaclets = proofs[i].getInitConfig().filterTaclets(taclets);
427+
proofs[i].getOpenGoal(proofs[i].root()).indexOfTaclets().addTaclets(filteredTaclets);
427428
}
428429
}
429430

‎key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java‎

Lines changed: 43 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.proof.init;
55

6-
import java.util.*;
7-
86
import de.uka.ilkd.key.java.Services;
97
import de.uka.ilkd.key.logic.NamespaceSet;
108
import de.uka.ilkd.key.logic.op.IProgramVariable;
@@ -17,10 +15,14 @@
1715
import de.uka.ilkd.key.proof.mgt.RuleJustification;
1816
import de.uka.ilkd.key.proof.mgt.RuleJustificationByAddRules;
1917
import de.uka.ilkd.key.proof.mgt.RuleJustificationInfo;
20-
import de.uka.ilkd.key.rule.*;
18+
import de.uka.ilkd.key.rule.BuiltInRule;
19+
import de.uka.ilkd.key.rule.NoPosTacletApp;
20+
import de.uka.ilkd.key.rule.Rule;
21+
import de.uka.ilkd.key.rule.Taclet;
2122
import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder;
2223
import de.uka.ilkd.key.settings.ProofSettings;
23-
24+
import org.jspecify.annotations.NonNull;
25+
import org.jspecify.annotations.Nullable;
2426
import org.key_project.logic.Choice;
2527
import org.key_project.logic.Name;
2628
import org.key_project.logic.Namespace;
@@ -34,8 +36,7 @@
3436
import org.key_project.util.collection.ImmutableSLList;
3537
import org.key_project.util.collection.ImmutableSet;
3638

37-
import org.jspecify.annotations.NonNull;
38-
import org.jspecify.annotations.Nullable;
39+
import java.util.*;
3940

4041
/**
4142
* an instance of this class describes the initial configuration of the prover. This includes sorts,
@@ -75,10 +76,14 @@ public class InitConfig {
7576
*/
7677
private ImmutableSet<Choice> activatedChoices = DefaultImmutableSet.nil();
7778

78-
/** HashMap for quick lookups taclet name->taclet */
79+
/**
80+
* HashMap for quick lookups taclet name->taclet
81+
*/
7982
private Map<Name, Taclet> activatedTacletCache = null;
8083

81-
/** the fileRepo which is responsible for consistency between source code and proof */
84+
/**
85+
* the fileRepo which is responsible for consistency between source code and proof
86+
*/
8287
private FileRepo fileRepo;
8388

8489
// weigl this field is never set
@@ -97,7 +102,7 @@ public InitConfig(Services services) {
97102
this.services = services;
98103

99104
category2DefaultChoice = new HashMap<>(
100-
ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices());
105+
ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices());
101106
}
102107

103108

@@ -106,7 +111,6 @@ public InitConfig(Services services) {
106111
// -------------------------------------------------------------------------
107112

108113

109-
110114
// -------------------------------------------------------------------------
111115
// public interface
112116
// -------------------------------------------------------------------------
@@ -151,7 +155,7 @@ public void addCategory2DefaultChoices(@NonNull Map<String, String> init) {
151155
// FIXME weigl: I do not understand why the default choices are back progragated!
152156
// For me this is a design flaw.
153157
Map<String, String> clone =
154-
new HashMap<>(category2DefaultChoice);
158+
new HashMap<>(category2DefaultChoice);
155159
ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(clone);
156160
// invalidate active taclet cache
157161
activatedTacletCache = null;
@@ -182,7 +186,7 @@ public HashMap<Taclet, TacletBuilder<? extends Taclet>> getTaclet2Builder() {
182186
*/
183187
public void setActivatedChoices(ImmutableSet<Choice> activatedChoices) {
184188
category2DefaultChoice =
185-
ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices();
189+
ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices();
186190

187191
HashMap<String, String> c2DC = new HashMap<>(category2DefaultChoice);
188192
for (final Choice c : activatedChoices) {
@@ -198,7 +202,7 @@ public void setActivatedChoices(ImmutableSet<Choice> activatedChoices) {
198202
}
199203
this.activatedChoices = activatedChoices
200204
.union(
201-
DefaultImmutableSet.fromImmutableList(category2DefaultChoiceList));
205+
DefaultImmutableSet.fromImmutableList(category2DefaultChoiceList));
202206

203207
// invalidate active taclet cache
204208
activatedTacletCache = null;
@@ -255,7 +259,7 @@ private void fillActiveTacletCache() {
255259
if (activatedTacletCache != null) {
256260
return;
257261
}
258-
final LinkedHashMap<Name, Taclet> tacletCache = new LinkedHashMap<>();
262+
final Map<Name, Taclet> tacletCache = new TreeMap<>();
259263
var choices = Collections.unmodifiableSet(activatedChoices.toSet());
260264
for (Taclet t : taclets) {
261265
TacletBuilder<? extends Taclet> b = taclet2Builder.get(t);
@@ -266,6 +270,9 @@ private void fillActiveTacletCache() {
266270
}
267271

268272
if (t != null) {
273+
if (tacletCache.containsKey(t.name())) {
274+
throw new IllegalArgumentException();
275+
}
269276
tacletCache.put(t.name(), t);
270277
}
271278
}
@@ -293,7 +300,7 @@ public void registerRule(Rule r, RuleJustification j) {
293300
}
294301

295302
public void registerRuleIntroducedAtNode(RuleApp r, Node node,
296-
boolean isAxiom) {
303+
boolean isAxiom) {
297304
justifInfo.addJustification(r.rule(), new RuleJustificationByAddRules(node, isAxiom));
298305
}
299306

@@ -431,7 +438,7 @@ public InitConfig copyWithServices(Services services) {
431438
ic.setActivatedChoices(activatedChoices);
432439
ic.category2DefaultChoice = new HashMap<>(category2DefaultChoice);
433440
ic.setTaclet2Builder(
434-
(HashMap<Taclet, TacletBuilder<? extends Taclet>>) taclet2Builder.clone());
441+
(HashMap<Taclet, TacletBuilder<? extends Taclet>>) taclet2Builder.clone());
435442
ic.taclets = taclets;
436443
ic.originalKeYFileName = originalKeYFileName;
437444
ic.header = header;
@@ -441,11 +448,10 @@ public InitConfig copyWithServices(Services services) {
441448
}
442449

443450

444-
445451
@Override
446452
public String toString() {
447453
return "Namespaces:" + namespaces() + "\n" + "Services:" + services + "\n" + "Taclets:"
448-
+ getTaclets() + "\n" + "Built-In:" + builtInRules() + "\n";
454+
+ getTaclets() + "\n" + "Built-In:" + builtInRules() + "\n";
449455
}
450456

451457
public FileRepo getFileRepo() {
@@ -459,10 +465,10 @@ public void setFileRepo(FileRepo fileRepo) {
459465
/// Enforce the given choice. Remove choices of the same category from the current set.
460466
public void activateChoice(Choice choice) {
461467
setActivatedChoices(
462-
getActivatedChoices()
463-
.stream().filter(it -> choice.category().equals(it.category()))
464-
.collect(ImmutableSet.collector())
465-
.add(choice));
468+
getActivatedChoices()
469+
.stream().filter(it -> choice.category().equals(it.category()))
470+
.collect(ImmutableSet.collector())
471+
.add(choice));
466472
}
467473

468474
/// returns the user-given declarations used during loading
@@ -474,4 +480,19 @@ public void activateChoice(Choice choice) {
474480
public void setHeader(KeyAst.@Nullable Declarations header) {
475481
this.header = header;
476482
}
483+
484+
public Collection<NoPosTacletApp> filterTaclets(ImmutableSet<NoPosTacletApp> taclets) {
485+
var result = new HashMap<Name, NoPosTacletApp>();
486+
var choices = Collections.unmodifiableSet(activatedChoices.toSet());
487+
for (var app : taclets) {
488+
var t = app.taclet();
489+
if (t.getChoices().eval(choices)) {
490+
if (result.containsKey(t.name())) {
491+
throw new IllegalArgumentException("Duplicate choice: " + t.name() + " by PO");
492+
}
493+
result.put(t.name(), app);
494+
}
495+
}
496+
return result.values();
497+
}
477498
}

‎key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,6 @@ protected void applyAddrule(ImmutableList<? extends org.key_project.prover.rules
168168
for (var tacletToAdd : rules) {
169169
final Node n = goal.node();
170170
String name = tacletToAdd.name() + AUTO_NAME + n.getUniqueTacletId();
171-
System.out.println(name);
172171
tacletToAdd = tacletToAdd.setName(name);
173172

174173

0 commit comments

Comments
 (0)