Remove SVSubstitute

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java

@@ -32,6 +32,7 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import org.key_project.logic.SyntaxElement;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
@@ -76,7 +77,7 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
      * A {@link Map} mapping from relevant variables for the condition to their runtime equivalent
      * in KeY
      */
-    private Map<SVSubstitute, SVSubstitute> variableNamingMap;
+    private Map<SyntaxElement, SyntaxElement> variableNamingMap;
 
     /**
      * The list of parameter variables of the method that contains the associated breakpoint
@@ -162,14 +163,14 @@ private void putValuesFromGlobalVars(ProgramVariable varForCondition, Node node,
      *
      * @return the cloned map
      */
-    private Map<SVSubstitute, SVSubstitute> getOldMap() {
-        Map<SVSubstitute, SVSubstitute> oldMap = new HashMap<>();
-        for (Entry<SVSubstitute, SVSubstitute> svSubstituteSVSubstituteEntry : getVariableNamingMap()
+    private Map<SyntaxElement, SyntaxElement> getOldMap() {
+        Map<SyntaxElement, SyntaxElement> oldMap = new HashMap<>();
+        for (Entry<SyntaxElement, SyntaxElement> svSubstituteSVSubstituteEntry : getVariableNamingMap()
                 .entrySet()) {
             Entry<?, ?> oldEntry = svSubstituteSVSubstituteEntry;
-            if (oldEntry.getKey() instanceof SVSubstitute
-                    && oldEntry.getValue() instanceof SVSubstitute) {
-                oldMap.put((SVSubstitute) oldEntry.getKey(), (SVSubstitute) oldEntry.getValue());
+            if (oldEntry.getKey() instanceof SyntaxElement
+                    && oldEntry.getValue() instanceof SyntaxElement) {
+                oldMap.put((SyntaxElement) oldEntry.getKey(), (SyntaxElement) oldEntry.getValue());
             }
         }
         return oldMap;
@@ -200,7 +201,7 @@ private void freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScop
      * @param oldMap the oldMap variableNamings
      */
     private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope,
-            Map<SVSubstitute, SVSubstitute> oldMap, RuleApp ruleApp) {
+            Map<SyntaxElement, SyntaxElement> oldMap, RuleApp ruleApp) {
         // look for renamings KeY did
         boolean found = false;
         // get current renaming tables
@@ -215,7 +216,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
                         .getHashMap().entrySet()) {
                     Entry<?, ?> entry = value;
                     if (entry.getKey() instanceof LocationVariable
-                            && entry.getValue() instanceof SVSubstitute) {
+                            && entry.getValue() instanceof SyntaxElement) {
                         if ((VariableNamer.getBasename(((LocationVariable) entry.getKey()).name()))
                                 .equals(varForCondition.name())
                                 && ((LocationVariable) entry.getKey()).name().toString()
@@ -229,7 +230,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
                             // add new value
                             toKeep.add((LocationVariable) entry.getValue());
                             getVariableNamingMap().put(varForCondition,
-                                (SVSubstitute) entry.getValue());
+                                (SyntaxElement) entry.getValue());
                             found = true;
                             break;
                         } else if (inScope && ((LocationVariable) entry.getKey()).name()
@@ -242,7 +243,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
                             // add new value
                             toKeep.add((LocationVariable) entry.getValue());
                             getVariableNamingMap().put(varForCondition,
-                                (SVSubstitute) entry.getValue());
+                                (SyntaxElement) entry.getValue());
                             found = true;
                             break;
                         }
@@ -263,7 +264,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
     protected void refreshVarMaps(RuleApp ruleApp, Node node) {
         boolean inScope = isInScope(node);
         // collect old values
-        Map<SVSubstitute, SVSubstitute> oldMap = getOldMap();
+        Map<SyntaxElement, SyntaxElement> oldMap = getOldMap();
         // put values into map which have to be replaced
         for (ProgramVariable varForCondition : getVarsForCondition()) {
             // put global variables only done when a variable is instantiated by
@@ -498,14 +499,14 @@ public Set<LocationVariable> getToKeep() {
     /**
      * @return the variableNamingMap
      */
-    public Map<SVSubstitute, SVSubstitute> getVariableNamingMap() {
+    public Map<SyntaxElement, SyntaxElement> getVariableNamingMap() {
         return variableNamingMap;
     }
 
     /**
      * @param variableNamingMap the variableNamingMap to set
      */
-    public void setVariableNamingMap(Map<SVSubstitute, SVSubstitute> variableNamingMap) {
+    public void setVariableNamingMap(Map<SyntaxElement, SyntaxElement> variableNamingMap) {
         this.variableNamingMap = variableNamingMap;
     }
 

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

@@ -5,7 +5,6 @@
 
 import de.uka.ilkd.key.rule.MatchConditions;
 
-import org.key_project.logic.SyntaxElement;
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 

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

@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.java;
 
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
 
 import org.key_project.logic.SyntaxElement;
 
@@ -14,7 +13,7 @@
  * to achieve an immutable structure
  */
 
-public interface SourceElement extends SVSubstitute, SyntaxElement {
+public interface SourceElement extends SyntaxElement {
 
 
     /**

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

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java;
 
-import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.TerminalSyntaxElement;
 
 /**

key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java

@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.java.declaration;
 
 import de.uka.ilkd.key.java.JavaProgramElement;
-import de.uka.ilkd.key.java.TerminalProgramElement;
 import de.uka.ilkd.key.java.visitor.Visitor;
 
 import org.key_project.logic.SyntaxElement;

key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java

@@ -5,7 +5,6 @@
 
 import de.uka.ilkd.key.java.declaration.Modifier;
 
-import org.key_project.logic.TerminalSyntaxElement;
 import org.key_project.util.ExtList;
 
 /**

key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java

@@ -5,7 +5,6 @@
 
 import de.uka.ilkd.key.java.LoopInitializer;
 import de.uka.ilkd.key.java.NonTerminalProgramElement;
-import de.uka.ilkd.key.java.TerminalProgramElement;
 
 import org.key_project.util.collection.ImmutableArray;
 

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

@@ -17,6 +17,7 @@
 import de.uka.ilkd.key.java.statement.ILoopInit;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
+
 import org.key_project.logic.SyntaxElement;
 
 /**
@@ -31,5 +32,5 @@ public interface ProgramConstruct extends Expression, Statement, ILoopInit, IFor
     SyntaxElement getChild(int n);
 
     @Override
-    int getChildCount() ;
+    int getChildCount();
 }

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

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.op.Operator;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.Visitor;
@@ -43,7 +42,7 @@
  * supported: {@link Term#execPostOrder(Visitor)} and {@link Term#execPreOrder(Visitor)}.
  */
 public interface Term
-        extends SVSubstitute, Sorted, TermEqualsModProperty, org.key_project.logic.Term {
+        extends Sorted, TermEqualsModProperty, org.key_project.logic.Term {
     @Override
     Operator op();
 

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

@@ -152,7 +152,7 @@
  * @see TermLabelManager
  */
 // spotless:on
-public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove*/ TerminalSyntaxElement {
+public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove */ TerminalSyntaxElement {
 
     /**
      * Retrieves the i-th parameter object of this term label.

key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java

@@ -125,7 +125,7 @@ public String toString() {
         return super.toString();
     }
 
-    public static class JavaModalityKind extends Kind implements SVSubstitute {
+    public static class JavaModalityKind extends Kind {
         private static final Map<String, JavaModalityKind> kinds = new HashMap<>();
         /**
          * The diamond operator of dynamic logic. A formula <alpha;>Phi can be read as after

key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java

@@ -13,7 +13,7 @@
  * etc. have to implement this interface.
  */
 public interface Operator
-        extends org.key_project.logic.op.Operator, SVSubstitute, EqualsModProofIrrelevancy {
+        extends org.key_project.logic.op.Operator, EqualsModProofIrrelevancy {
 
     /**
      * comparator to compare operators; for modalities only their kind is compared

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java

@@ -23,7 +23,6 @@
 
 import org.key_project.logic.Name;
 import org.key_project.logic.SyntaxElement;
-import org.key_project.logic.TerminalSyntaxElement;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 
@@ -34,7 +33,8 @@
  * Objects of this class are schema variables matching program constructs within modal operators.
  * The particular construct being matched is determined by the ProgramSVSort of the schema variable.
  */
-public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator , SyntaxElement {
+public final class ProgramSV extends OperatorSV
+        implements ProgramConstruct, UpdateableOperator, SyntaxElement {
     public static final Logger LOGGER = LoggerFactory.getLogger(ProgramSV.class);
 
     private static final ProgramList EMPTY_LIST_INSTANTIATION =

key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java

@@ -5,7 +5,6 @@
 
 import java.util.WeakHashMap;
 
-import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.TerminalSyntaxElement;
 
 public class Qualifier<T> implements TerminalSyntaxElement {

key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java

@@ -6,13 +6,15 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
+
 import org.key_project.logic.TerminalSyntaxElement;
 
 /**
  * TermTransformer perform complex term transformation which cannot be (efficiently or at all)
  * described by taclets.
  */
-public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator, /*TODO: check*/ TerminalSyntaxElement {
+public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator,
+        /* TODO: check */ TerminalSyntaxElement {
 
     /**
      * initiates term transformation of <tt>term</tt>. Note the top level operator of of parameter

key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java

@@ -12,7 +12,8 @@
 /**
  * Schema variable that is instantiated with logical variables.
  */
-public final class VariableSV extends OperatorSV implements QuantifiableVariable, TerminalSyntaxElement {
+public final class VariableSV extends OperatorSV
+        implements QuantifiableVariable, TerminalSyntaxElement {
 
     /**
      * Creates a new SchemaVariable that is used as placeholder for bound(quantified) variables.

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

@@ -10,9 +10,9 @@
 import de.uka.ilkd.key.logic.TermFactory;
 import de.uka.ilkd.key.logic.op.Operator;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
 import de.uka.ilkd.key.util.InfFlowSpec;
 
+import org.key_project.logic.SyntaxElement;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
@@ -36,7 +36,7 @@ public class OpReplacer {
     /**
      * The replacement map.
      */
-    private final ReplacementMap<? extends SVSubstitute, ? extends SVSubstitute> map;
+    private final ReplacementMap<? extends SyntaxElement, ? extends SyntaxElement> map;
 
     /**
      * <p>
@@ -53,7 +53,7 @@ public class OpReplacer {
      *        with
      * @param tf a term factory.
      */
-    public OpReplacer(Map<? extends SVSubstitute, ? extends SVSubstitute> map, TermFactory tf) {
+    public OpReplacer(Map<? extends SyntaxElement, ? extends SyntaxElement> map, TermFactory tf) {
         this(map, tf, null);
     }
 
@@ -65,12 +65,12 @@ public OpReplacer(Map<? extends SVSubstitute, ? extends SVSubstitute> map, TermF
      * @param tf a term factory.
      * @param proof the currently loaded proof
      */
-    public OpReplacer(Map<? extends SVSubstitute, ? extends SVSubstitute> map, TermFactory tf,
+    public OpReplacer(Map<? extends SyntaxElement, ? extends SyntaxElement> map, TermFactory tf,
             Proof proof) {
         assert map != null;
 
         this.map = map instanceof ReplacementMap
-                ? (ReplacementMap<? extends SVSubstitute, ? extends SVSubstitute>) map
+                ? (ReplacementMap<? extends SyntaxElement, ? extends SyntaxElement>) map
                 : ReplacementMap.create(tf, proof, map);
 
         this.tf = tf;
@@ -234,7 +234,7 @@ public Term replace(Term term) {
             return newTerm;
         }
 
-        for (SVSubstitute svs : map.keySet()) {
+        for (SyntaxElement svs : map.keySet()) {
             if (term.equalsModProperty(svs, TERM_LABELS_PROPERTY)) {
                 return (Term) map.get(svs);
             }

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

@@ -11,11 +11,12 @@
 import de.uka.ilkd.key.logic.TermFactory;
 import de.uka.ilkd.key.logic.label.OriginTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelManager;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
 import de.uka.ilkd.key.settings.ProofSettings;
 import de.uka.ilkd.key.settings.TermLabelSettings;
 import de.uka.ilkd.key.util.LinkedHashMap;
 
+import org.key_project.logic.SyntaxElement;
+
 /**
  * A map to be used in an {@link OpReplacer}. It maps operators that should be replaced to their
  * replacements.
@@ -25,7 +26,7 @@
  * @param <S> the type of the elements to replace.
  * @param <T> the type of the replacements.
  */
-public interface ReplacementMap<S extends SVSubstitute, T> extends Map<S, T> {
+public interface ReplacementMap<S extends SyntaxElement, T> extends Map<S, T> {
 
     /**
      * Creates a new replacement map.
@@ -36,7 +37,7 @@ public interface ReplacementMap<S extends SVSubstitute, T> extends Map<S, T> {
      * @param proof the currently loaded proof, or {@code null} if no proof is loaded.
      * @return a new replacement map.
      */
-    static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
+    static <S extends SyntaxElement, T> ReplacementMap<S, T> create(TermFactory tf,
             Proof proof) {
         var noIrrelevantTermLabelsMap = proof == null
                 ? ProofSettings.DEFAULT_SETTINGS.getTermLabelSettings().getUseOriginLabels()
@@ -58,7 +59,7 @@ static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
      * @param initialMappings a map whose mapping should be added to the new replacement map.
      * @return a new replacement map.
      */
-    static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
+    static <S extends SyntaxElement, T> ReplacementMap<S, T> create(TermFactory tf,
             Proof proof, Map<S, T> initialMappings) {
         ReplacementMap<S, T> result = create(tf, proof);
         result.putAll(initialMappings);
@@ -77,7 +78,7 @@ static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
      * @param <S> the type of the operators to replace.
      * @param <T> the type of the replacements.
      */
-    class DefaultReplacementMap<S extends SVSubstitute, T> extends LinkedHashMap<S, T>
+    class DefaultReplacementMap<S extends SyntaxElement, T> extends LinkedHashMap<S, T>
             implements ReplacementMap<S, T> {
         private static final long serialVersionUID = 6223486569442129676L;
     }
@@ -98,7 +99,7 @@ class DefaultReplacementMap<S extends SVSubstitute, T> extends LinkedHashMap<S,
      *
      * @see OriginTermLabel
      */
-    class NoIrrelevantLabelsReplacementMap<S extends SVSubstitute, T>
+    class NoIrrelevantLabelsReplacementMap<S extends SyntaxElement, T>
             implements ReplacementMap<S, T> {
 
         /**