Remove SequentFormula class

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java

@@ -7,7 +7,6 @@
 import java.util.Arrays;
 import java.util.List;
 
-import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
@@ -22,8 +21,8 @@ public class FormulaTermLabelMerger implements TermLabelMerger {
      * {@inheritDoc}
      */
     @Override
-    public boolean mergeLabels(SequentFormula existingSF, Term existingTerm,
-            TermLabel existingLabel, SequentFormula rejectedSF, Term rejectedTerm,
+    public boolean mergeLabels(Term existingSF, Term existingTerm,
+            TermLabel existingLabel, Term rejectedSF, Term rejectedTerm,
             TermLabel rejectedLabel, List<TermLabel> mergedLabels) {
         if (existingLabel != null) {
             FormulaTermLabel fExisting = (FormulaTermLabel) existingLabel;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java

@@ -84,9 +84,9 @@ public class FormulaTermLabelRefactoring implements TermLabelRefactoring {
 
     /**
      * Key used in {@link TermLabelState} by the {@link FormulaTermLabelUpdate} to indicate that a
-     * refactoring of specified {@link SequentFormula}s ({@link RefactoringScope#SEQUENT}) is
+     * refactoring of specified {@link Term}s ({@link RefactoringScope#SEQUENT}) is
      * required, which will be performed by
-     * {@link #refactorSequentFormulas(TermLabelState, Services, Term, LabelCollection)}.
+     * {@link #refactorTerms(TermLabelState, Services, Term, LabelCollection)}.
      * <p>
      * This is for instance required if the assumes clause of a rule has a {@link FormulaTermLabel}
      * but the application does not have it. Example rules are:
@@ -95,7 +95,7 @@ public class FormulaTermLabelRefactoring implements TermLabelRefactoring {
      * </ul>
      */
     private static final String SEQUENT_FORMULA_REFACTORING_REQUIRED =
-        "sequentFormulaRefactoringRequired";
+        "TermRefactoringRequired";
 
     /**
      * {@inheritDoc}
@@ -118,7 +118,7 @@ public RefactoringScope defineRefactoringScope(TermLabelState state, Services se
             return RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS;
         } else if (isUpdateRefactoringRequired(state)) {
             return RefactoringScope.APPLICATION_BELOW_UPDATES;
-        } else if (containsSequentFormulasToRefactor(state)) {
+        } else if (containsTermsToRefactor(state)) {
             return RefactoringScope.SEQUENT;
         } else if (SyntacticalReplaceVisitor.SUBSTITUTION_WITH_LABELS_HINT.equals(hint)) {
             return RefactoringScope.APPLICATION_BELOW_UPDATES;
@@ -152,8 +152,8 @@ public void refactorLabels(TermLabelState state, Services services,
             refactorInCaseOfNewIdRequired(state, goal, term, services, labels);
         } else if (isUpdateRefactoringRequired(state)) {
             refactorBelowUpdates(applicationPosInOccurrence, term, labels);
-        } else if (containsSequentFormulasToRefactor(state)) {
-            refactorSequentFormulas(state, services, term, labels);
+        } else if (containsTermsToRefactor(state)) {
+            refactorTerms(state, services, term, labels);
         } else if (SyntacticalReplaceVisitor.SUBSTITUTION_WITH_LABELS_HINT.equals(hint)) {
             refactorSubstitution(term, tacletTerm, labels);
         }
@@ -238,18 +238,20 @@ private void refactorBelowUpdates(PosInOccurrence applicationPosInOccurrence, Te
     }
 
     /**
-     * Refactors the specified {@link SequentFormula}s.
+     * Refactors the specified {@link Term}s.
      *
      * @param state The {@link TermLabelState} of the current rule application.
      * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is
      *        applied right now.
      * @param term The {@link Term} which is now refactored.
      * @param labels The new labels the {@link Term} will have after the refactoring.
      */
-    private void refactorSequentFormulas(TermLabelState state, Services services, final Term term,
+    private void refactorTerms(TermLabelState state, Services services, final Term term,
             LabelCollection labels) {
-        Set<SequentFormula> sequentFormulas = getSequentFormulasToRefactor(state);
-        if (CollectionUtil.search(sequentFormulas, element -> element.formula() == term) != null) {
+        Set<Term> Terms = getTermsToRefactor(state);
+        if (CollectionUtil.search(Terms, element -> {
+            return element == term;
+        }) != null) {
             FormulaTermLabel termLabel = (FormulaTermLabel) term.getLabel(FormulaTermLabel.NAME);
             if (termLabel != null) {
                 labels.remove(termLabel);
@@ -373,45 +375,45 @@ public static void setParentRefactoringRequired(TermLabelState state, boolean re
     }
 
     /**
-     * Checks if {@link SequentFormula}s to refactor are specified.
+     * Checks if {@link Term}s to refactor are specified.
      *
      * @param state The {@link TermLabelState} to read from.
-     * @return {@code true} at least one {@link SequentFormula} needs to be refactored,
+     * @return {@code true} at least one {@link Term} needs to be refactored,
      *         {@code false} refactoring is not required.
      */
-    public static boolean containsSequentFormulasToRefactor(TermLabelState state) {
+    public static boolean containsTermsToRefactor(TermLabelState state) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         @SuppressWarnings("unchecked")
-        Set<SequentFormula> sfSet =
-            (Set<SequentFormula>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
+        Set<Term> sfSet =
+            (Set<Term>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
         return sfSet != null && !sfSet.isEmpty();
     }
 
     /**
-     * Returns the {@link SequentFormula}s to refactor.
+     * Returns the {@link Term}s to refactor.
      *
      * @param state The {@link TermLabelState} to read from.
-     * @return The {@link SequentFormula}s to refactor.
+     * @return The {@link Term}s to refactor.
      */
-    public static Set<SequentFormula> getSequentFormulasToRefactor(TermLabelState state) {
+    public static Set<Term> getTermsToRefactor(TermLabelState state) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         @SuppressWarnings("unchecked")
-        Set<SequentFormula> sfSet =
-            (Set<SequentFormula>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
+        Set<Term> sfSet =
+            (Set<Term>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
         return sfSet;
     }
 
     /**
-     * Adds the given {@link SequentFormula} for refactoring purpose.
+     * Adds the given {@link Term} for refactoring purpose.
      *
      * @param state The {@link TermLabelState} to modify.
-     * @param sf The {@link SequentFormula} to add.
+     * @param sf The {@link Term} to add.
      */
-    public static void addSequentFormulaToRefactor(TermLabelState state, SequentFormula sf) {
+    public static void addTermToRefactor(TermLabelState state, Term sf) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         @SuppressWarnings("unchecked")
-        Set<SequentFormula> sfSet =
-            (Set<SequentFormula>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
+        Set<Term> sfSet =
+            (Set<Term>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
         if (sfSet == null) {
             sfSet = new LinkedHashSet<>();
             labelState.put(SEQUENT_FORMULA_REFACTORING_REQUIRED, sfSet);

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java

@@ -72,11 +72,12 @@ public void updateLabels(TermLabelState state, Services services,
         }
         if (ruleApp instanceof TacletApp ta) {
             if (ta.ifInstsComplete() && ta.ifFormulaInstantiations() != null) {
-                Map<SequentFormula, FormulaTermLabel> ifLabels =
+                Map<Term, FormulaTermLabel> ifLabels =
                     new LinkedHashMap<>();
                 for (IfFormulaInstantiation ifInst : ta.ifFormulaInstantiations()) {
+                    final Term assumesFml = ifInst.getConstrainedFormula();
                     FormulaTermLabel ifLabel = StayOnFormulaTermLabelPolicy.searchFormulaTermLabel(
-                        ifInst.getConstrainedFormula().formula().getLabels());
+                        assumesFml.getLabels());
                     if (ifLabel != null) {
                         ifLabels.put(ifInst.getConstrainedFormula(), ifLabel);
                     }
@@ -85,14 +86,14 @@ public void updateLabels(TermLabelState state, Services services,
                     if (TruthValueTracingUtil.isLogicOperator(newTerm.op(), newTerm.subs())
                     // || TruthValueEvaluationUtil.isPredicate(newTermOp)
                     ) {
-                        for (Entry<SequentFormula, FormulaTermLabel> ifEntry : ifLabels
+                        for (Entry<Term, FormulaTermLabel> ifEntry : ifLabels
                                 .entrySet()) {
                             FormulaTermLabel ifLabel = ifEntry.getValue();
                             int labelSubID = FormulaTermLabel.newLabelSubID(services, ifLabel);
                             FormulaTermLabel newLabel = new FormulaTermLabel(ifLabel.getMajorId(),
                                 labelSubID, Collections.singletonList(ifLabel.getId()));
                             labels.add(newLabel);
-                            FormulaTermLabelRefactoring.addSequentFormulaToRefactor(state,
+                            FormulaTermLabelRefactoring.addTermToRefactor(state,
                                 ifEntry.getKey());
                         }
                     }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java

@@ -69,8 +69,8 @@ public TermLabel keepLabel(TermLabelState state, Services services,
                         originalLabelIds.add(mostImportantLabel.getId());
                     }
                 }
-                if (tacletHint.getSequentFormula() != null) {
-                    if (!TruthValueTracingUtil.isPredicate(tacletHint.getSequentFormula())) {
+                if (tacletHint.getTerm() != null) {
+                    if (!TruthValueTracingUtil.isPredicate(tacletHint.getTerm())) {
                         newLabelIdRequired = true;
                     }
                 } else if (tacletHint.getTerm() != null) {
@@ -164,10 +164,6 @@ public static FormulaTermLabel searchFormulaTermLabel(ImmutableArray<TermLabel>
      * @return {@code true} is top level, {@code false} is not top level.
      */
     protected boolean isTopLevel(TacletLabelHint tacletHint, Term tacletTerm) {
-        if (TacletOperation.REPLACE_TERM.equals(tacletHint.getTacletOperation())) {
-            return tacletHint.getTerm() == tacletTerm;
-        } else {
-            return tacletHint.getSequentFormula().formula() == tacletTerm;
-        }
+        return tacletHint.getTerm() == tacletTerm;
     }
 }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java

@@ -152,8 +152,8 @@ protected Set<Term> computeInitialObjectsToIgnore(boolean ignoreExceptionVariabl
             // Add initial updates which are used as backup of the heap and method arguments. They
             // are not part of the source code and should be ignored.
             Sequent sequent = getRoot().sequent();
-            for (SequentFormula sf : sequent.succedent()) {
-                Term term = sf.formula();
+            for (Term sf : sequent.succedent()) {
+                Term term = sf;
                 if (Junctor.IMP.equals(term.op())) {
                     fillInitialObjectsToIgnoreRecursively(term.sub(1), result);
                 }
@@ -434,9 +434,9 @@ protected boolean hasFreeVariables(Term term) {
     protected Set<ExtractLocationParameter> extractLocationsFromSequent(Sequent sequent,
             Set<Term> objectsToIgnore) throws ProofInputException {
         Set<ExtractLocationParameter> result = new LinkedHashSet<>();
-        for (SequentFormula sf : sequent) {
+        for (Term sf : sequent) {
             result.addAll(extractLocationsFromTerm(
-                OriginTermLabel.removeOriginLabels(sf.formula(), getServices()), objectsToIgnore));
+                OriginTermLabel.removeOriginLabels(sf, getServices()), objectsToIgnore));
         }
         return result;
     }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java

@@ -249,8 +249,8 @@ public SymbolicExecutionTreeBuilder(Proof proof, boolean mergeBranchConditions,
     protected void initMethodCallStack(final Node root, Services services) {
         // Find all modalities in the succedent
         final List<Term> modalityTerms = new LinkedList<>();
-        for (SequentFormula sequentFormula : root.sequent().succedent()) {
-            sequentFormula.formula().execPreOrder(new DefaultVisitor() {
+        for (Term succFml : root.sequent().succedent()) {
+            succFml.execPreOrder(new DefaultVisitor() {
                 @Override
                 public void visit(Term visited) {
                     if (visited.op() instanceof Modality

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java

@@ -309,7 +309,7 @@ protected ImmutableList<Term> extractInitialUpdates() {
         Sequent sequent = getRoot().sequent();
         assert sequent.antecedent().isEmpty();
         assert sequent.succedent().size() == 1;
-        Term sf = sequent.succedent().get(0).formula();
+        final Term sf = sequent.succedent().get(0);
         assert sf.op() == Junctor.IMP;
         Term modality = sf.sub(1);
         return TermBuilder.goBelowUpdates2(modality).first;
@@ -680,9 +680,9 @@ protected Set<ExtractLocationParameter> updateLocationsAccordingtoEquivalentClas
     protected Set<Term> collectObjectsFromSequent(Sequent sequent, Set<Term> objectsToIgnore)
             throws ProofInputException {
         Set<Term> result = new LinkedHashSet<>();
-        for (SequentFormula sf : sequent) {
+        for (Term sf : sequent) {
             if (SymbolicExecutionUtil.checkSkolemEquality(sf) == 0) {
-                result.addAll(collectSymbolicObjectsFromTerm(sf.formula(), objectsToIgnore));
+                result.addAll(collectSymbolicObjectsFromTerm(sf, objectsToIgnore));
             }
         }
         return result;