fix double Taclet problem

Author: wadoon

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

@@ -423,7 +423,9 @@ public final ProofAggregate getPO() {
             }
             proofs[i] = createProof(poNames != null ? poNames[i] : name, poTerms[i], ic);
             if (taclets != null) {
-                proofs[i].getOpenGoal(proofs[i].root()).indexOfTaclets().addTaclets(taclets);
+                var filteredTaclets = proofs[i].getInitConfig().filterTaclets(taclets);
+                proofs[i].getOpenGoal(proofs[i].root()).indexOfTaclets()
+                        .addTaclets(filteredTaclets);
             }
         }
 

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

@@ -17,7 +17,10 @@
 import de.uka.ilkd.key.proof.mgt.RuleJustification;
 import de.uka.ilkd.key.proof.mgt.RuleJustificationByAddRules;
 import de.uka.ilkd.key.proof.mgt.RuleJustificationInfo;
-import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.rule.BuiltInRule;
+import de.uka.ilkd.key.rule.NoPosTacletApp;
+import de.uka.ilkd.key.rule.Rule;
+import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder;
 import de.uka.ilkd.key.settings.ProofSettings;
 
@@ -75,10 +78,14 @@ public class InitConfig {
      */
     private ImmutableSet<Choice> activatedChoices = DefaultImmutableSet.nil();
 
-    /** HashMap for quick lookups taclet name->taclet */
+    /**
+     * HashMap for quick lookups taclet name->taclet
+     */
     private Map<Name, Taclet> activatedTacletCache = null;
 
-    /** the fileRepo which is responsible for consistency between source code and proof */
+    /**
+     * the fileRepo which is responsible for consistency between source code and proof
+     */
     private FileRepo fileRepo;
 
     // weigl this field is never set
@@ -106,7 +113,6 @@ public InitConfig(Services services) {
     // -------------------------------------------------------------------------
 
 
-
     // -------------------------------------------------------------------------
     // public interface
     // -------------------------------------------------------------------------
@@ -255,7 +261,7 @@ private void fillActiveTacletCache() {
         if (activatedTacletCache != null) {
             return;
         }
-        final LinkedHashMap<Name, Taclet> tacletCache = new LinkedHashMap<>();
+        final Map<Name, Taclet> tacletCache = new TreeMap<>();
         var choices = Collections.unmodifiableSet(activatedChoices.toSet());
         for (Taclet t : taclets) {
             TacletBuilder<? extends Taclet> b = taclet2Builder.get(t);
@@ -266,6 +272,9 @@ private void fillActiveTacletCache() {
                 }
 
                 if (t != null) {
+                    if (tacletCache.containsKey(t.name())) {
+                        throw new IllegalArgumentException();
+                    }
                     tacletCache.put(t.name(), t);
                 }
             }
@@ -441,7 +450,6 @@ public InitConfig copyWithServices(Services services) {
     }
 
 
-
     @Override
     public String toString() {
         return "Namespaces:" + namespaces() + "\n" + "Services:" + services + "\n" + "Taclets:"
@@ -474,4 +482,19 @@ public void activateChoice(Choice choice) {
     public void setHeader(KeyAst.@Nullable Declarations header) {
         this.header = header;
     }
+
+    public Collection<NoPosTacletApp> filterTaclets(ImmutableSet<NoPosTacletApp> taclets) {
+        var result = new HashMap<Name, NoPosTacletApp>();
+        var choices = Collections.unmodifiableSet(activatedChoices.toSet());
+        for (var app : taclets) {
+            var t = app.taclet();
+            if (t.getChoices().eval(choices)) {
+                if (result.containsKey(t.name())) {
+                    throw new IllegalArgumentException("Duplicate choice: " + t.name() + " by PO");
+                }
+                result.put(t.name(), app);
+            }
+        }
+        return result.values();
+    }
 }

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

@@ -168,7 +168,6 @@ protected void applyAddrule(ImmutableList<? extends org.key_project.prover.rules
         for (var tacletToAdd : rules) {
             final Node n = goal.node();
             String name = tacletToAdd.name() + AUTO_NAME + n.getUniqueTacletId();
-            System.out.println(name);
             tacletToAdd = tacletToAdd.setName(name);