One Step Simplifier: optimizations and new rules

key.core/src/main/java/de/uka/ilkd/key/java/Services.java

@@ -14,6 +14,7 @@
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.util.Debug;
 import de.uka.ilkd.key.util.KeYRecoderExcHandler;
 
@@ -298,6 +299,11 @@ public void setProof(Proof p_proof) {
                 "Services are already owned by another proof:" + proof.name());
         }
         proof = p_proof;
+        // disable origin tracking if settings indicate it
+        if (!ProofIndependentSettings.DEFAULT_INSTANCE.getTermLabelSettings().getUseOriginLabels()
+                || !proof.getSettings().getTermLabelSettings().getUseOriginLabels()) {
+            profile.getTermLabelManager().disableOriginLabelRefactorings();
+        }
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/logic/PosInOccurrence.java

@@ -122,6 +122,7 @@ public int getIndex() {
         return posInTerm.getIndex();
     }
 
+    @Override
     public int hashCode() {
         return hashCode;
     }
@@ -187,6 +188,13 @@ public Term subTerm() {
         return subTermCache;
     }
 
+    /**
+     * @return whether this PiO is a valid reference
+     */
+    public boolean subTermExists() {
+        return posInTerm.existsSubTerm(sequentFormula.formula());
+    }
+
     /**
      * Ascend to the top node of the formula this object points to
      */

key.core/src/main/java/de/uka/ilkd/key/logic/PosInTerm.java

@@ -38,6 +38,22 @@ public PosInTerm(int[] path) {
         copy = false;
     }
 
+    /**
+     * Remove the first index from this position.
+     *
+     * @return position of the first subterm
+     */
+    public PosInTerm sub() {
+        if (size == 1) {
+            return PosInTerm.TOP_LEVEL;
+        }
+        int[] pathMinusHead = new int[size - 1];
+        for (int i = 1; i < size; i++) {
+            pathMinusHead[i - 1] = positions[i];
+        }
+        return new PosInTerm(pathMinusHead);
+    }
+
     /**
      * create a position from the string
      *
@@ -234,6 +250,22 @@ public Term getSubTerm(Term t) {
         return sub;
     }
 
+    /**
+     * @param t some term
+     * @return whether this position exists in that term
+     */
+    public boolean existsSubTerm(Term t) {
+        Term sub = t;
+        for (int i = 0; i < size; i++) {
+            if (positions[i] >= sub.subs().size()) {
+                return false;
+            }
+            sub = sub.sub(positions[i]);
+        }
+        return true;
+    }
+
+    @Override
     public int hashCode() {
         if (hash == (char) -1) {
             char localHash = 13;

key.core/src/main/java/de/uka/ilkd/key/logic/SequentFormula.java

@@ -50,6 +50,7 @@ public Term formula() {
     }
 
     /** equal if terms and constraints are equal */
+    @Override
     public boolean equals(Object obj) {
         if (this == obj) {
             return true;

key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java

@@ -5,6 +5,7 @@
 
 import java.util.*;
 import java.util.Map.Entry;
+import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
@@ -15,8 +16,13 @@
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
-import de.uka.ilkd.key.rule.label.*;
+import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy;
+import de.uka.ilkd.key.rule.label.OriginTermLabelRefactoring;
+import de.uka.ilkd.key.rule.label.TermLabelMerger;
+import de.uka.ilkd.key.rule.label.TermLabelPolicy;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.util.LinkedHashMap;
 import de.uka.ilkd.key.util.Pair;
 
@@ -2194,4 +2200,14 @@ protected void mergeLabels(SequentChangeInfo currentSequent, Services services,
             }
         }
     }
+
+    /**
+     * Fully disable origin tracking. This will remove the {@link OriginTermLabelRefactoring} from
+     * the manager.
+     */
+    public void disableOriginLabelRefactorings() {
+        allRulesRefactorings = ImmutableList.fromList(
+            allRulesRefactorings.stream().filter(x -> !(x instanceof OriginTermLabelRefactoring))
+                    .toList());
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/macros/SMTPreparationMacro.java

@@ -51,6 +51,11 @@ public String getCategory() {
         return "Auto Pilot";
     }
 
+    @Override
+    public String getScriptCommandName() {
+        return "smt-prepare";
+    }
+
     /**
      * Gets the description of this macro.
      * <p>

key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java

@@ -56,7 +56,7 @@ private ProofReplayer() {
     public static void run(@Nonnull Token token, CharStream input, IProofFileParser prl,
             URI source) {
         input.seek(1 + token.getStopIndex()); // ends now on \proof|
-        run(input, prl, token.getLine(), source);
+        run(input, prl, token.getLine() - 1, source);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java

@@ -12,7 +12,6 @@
 import de.uka.ilkd.key.informationflow.proof.SideProofStatistics;
 import de.uka.ilkd.key.proof.reference.ClosedBy;
 import de.uka.ilkd.key.rule.*;
-import de.uka.ilkd.key.rule.OneStepSimplifier.Protocol;
 import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp;
 import de.uka.ilkd.key.smt.SMTRuleApp;
 import de.uka.ilkd.key.util.EnhancedStringBuffer;
@@ -179,6 +178,10 @@ private void generateSummary(Proof proof) {
         summaryList.add(new Pair<>("Merge Rule apps", String.valueOf(stat.mergeRuleApps)));
         summaryList.add(new Pair<>("Total rule apps",
             EnhancedStringBuffer.format(stat.totalRuleApps).toString()));
+        if (stat.totalRuleApps > 0) {
+            String avgTime = String.valueOf((time * 1000) / stat.totalRuleApps);
+            summaryList.add(new Pair<>("Avg. time per app", avgTime + "μs"));
+        }
     }
 
 
@@ -324,10 +327,10 @@ private int interactiveRuleApps(final Node node,
          */
         private int tmpOssCaptured(final RuleApp ruleApp) {
             int tmpOssCaptured = 0;
-            final Protocol protocol =
-                ((de.uka.ilkd.key.rule.OneStepSimplifierRuleApp) ruleApp).getProtocol();
-            if (protocol != null) {
-                tmpOssCaptured = protocol.size() - 1;
+            int protocol =
+                ((de.uka.ilkd.key.rule.OneStepSimplifierRuleApp) ruleApp).getProtocolLength();
+            if (protocol != 0) {
+                tmpOssCaptured = protocol - 1;
             }
             return tmpOssCaptured;
         }