Removal of the Triple class

KeYProject · Apr 23, 2024 · 423c10b · 423c10b
1 parent a599a6d
commit 423c10b
Show file tree

Hide file tree

Showing 33 changed files with 499 additions and 616 deletions.
diff --git a/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java b/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java
@@ -25,7 +25,6 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
-import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.sort.Sort;
@@ -87,7 +86,7 @@ protected JFunction createResultFunction(Services services, Sort sort) {
      * @return The found result {@link Term} and the conditions.
      * @throws ProofInputException Occurred Exception.
      */
-    protected List<Triple<Term, Set<Term>, Node>> computeResultsAndConditions(Services services,
+    protected List<ResultsAndCondition> computeResultsAndConditions(Services services,
             Goal goal, ProofEnvironment sideProofEnvironment, Sequent sequentToProve,
             JFunction newPredicate) throws ProofInputException {
         return SymbolicExecutionSideProofUtil.computeResultsAndConditions(services, goal.proof(),
@@ -134,4 +133,7 @@ protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Servi
     public boolean isApplicableOnSubTerms() {
         return false;
     }
+
+    public record ResultsAndCondition(Term result, Set<Term> conditions, Node node) {
+    }
 }
diff --git a/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java
@@ -3,36 +3,23 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.symbolic_execution.rule;
 
-import java.util.LinkedHashSet;
-import java.util.List;
-import java.util.Set;
-
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
-import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.TermBuilder;
-import de.uka.ilkd.key.logic.TermServices;
+import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
-import de.uka.ilkd.key.rule.BuiltInRule;
-import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
-import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.rule.RuleAbortException;
-import de.uka.ilkd.key.rule.RuleApp;
+import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
-import de.uka.ilkd.key.util.Triple;
-
+import org.jspecify.annotations.NonNull;
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.Pair;
 
-import org.jspecify.annotations.NonNull;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Set;
 
 /**
  * <p>
@@ -182,7 +169,7 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
                     .addFormula(new SequentFormula(newModalityWithUpdatesTerm), false, false)
                     .sequent();
             // Compute results and their conditions
-            List<Triple<Term, Set<Term>, Node>> conditionsAndResultsMap =
+            List<ResultsAndCondition> conditionsAndResultsMap =
                 computeResultsAndConditions(services, goal, sideProofEnv, sequentToProve,
                     newPredicate);
             // Create new single goal in which the query is replaced by the possible results
@@ -191,10 +178,10 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             resultGoal.removeFormula(pio);
             // Create results
             Set<Term> resultTerms = new LinkedHashSet<>();
-            for (Triple<Term, Set<Term>, Node> conditionsAndResult : conditionsAndResultsMap) {
-                Term conditionTerm = tb.and(conditionsAndResult.second);
-                Term resultEqualityTerm = varFirst ? tb.equals(conditionsAndResult.first, otherTerm)
-                        : tb.equals(otherTerm, conditionsAndResult.first);
+            for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
+                Term conditionTerm = tb.and(conditionsAndResult.conditions());
+                Term resultEqualityTerm = varFirst ? tb.equals(conditionsAndResult.result(), otherTerm)
+                        : tb.equals(otherTerm, conditionsAndResult.result());
                 Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, resultEqualityTerm)
                         : tb.and(conditionTerm, resultEqualityTerm);
                 resultTerms.add(resultTerm);

diff --git a/...c_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java b/...c_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java
@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.symbolic_execution.rule;
 
 import java.util.List;
-import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.PIOPathIterator;
@@ -16,7 +15,6 @@
 import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
@@ -25,7 +23,6 @@
 import de.uka.ilkd.key.rule.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
-import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.sort.Sort;
@@ -229,7 +226,7 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             sequentToProve =
                 sequentToProve.addFormula(new SequentFormula(newTerm), false, false).sequent();
             // Compute results and their conditions
-            List<Triple<Term, Set<Term>, Node>> conditionsAndResultsMap =
+            List<ResultsAndCondition> conditionsAndResultsMap =
                 computeResultsAndConditions(services, goal, sideProofEnv, sequentToProve,
                     newPredicate);
             // Create new single goal in which the query is replaced by the possible results
@@ -238,10 +235,10 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             final TermBuilder tb = services.getTermBuilder();
             resultGoal.removeFormula(pio);
             if (pio.isTopLevel() || queryConditionTerm != null) {
-                for (Triple<Term, Set<Term>, Node> conditionsAndResult : conditionsAndResultsMap) {
-                    Term conditionTerm = tb.and(conditionsAndResult.second);
-                    Term newEqualityTerm = varFirst ? tb.equals(varTerm, conditionsAndResult.first)
-                            : tb.equals(conditionsAndResult.first, varTerm);
+                for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
+                    Term conditionTerm = tb.and(conditionsAndResult.conditions());
+                    Term newEqualityTerm = varFirst ? tb.equals(varTerm, conditionsAndResult.result())
+                            : tb.equals(conditionsAndResult.result(), varTerm);
                     Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, newEqualityTerm)
                             : tb.and(conditionTerm, newEqualityTerm);
                     if (queryConditionTerm != null) {
@@ -257,11 +254,11 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
                         tb.equals(resultFunctionTerm, varTerm),
                         services),
                     pio.isInAntec(), false);
-                for (Triple<Term, Set<Term>, Node> conditionsAndResult : conditionsAndResultsMap) {
-                    Term conditionTerm = tb.and(conditionsAndResult.second);
+                for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
+                    Term conditionTerm = tb.and(conditionsAndResult.conditions());
                     Term resultTerm = tb.imp(conditionTerm,
-                        varFirst ? tb.equals(resultFunctionTerm, conditionsAndResult.first)
-                                : tb.equals(conditionsAndResult.first, resultFunctionTerm));
+                        varFirst ? tb.equals(resultFunctionTerm, conditionsAndResult.result())
+                                : tb.equals(conditionsAndResult.result(), resultFunctionTerm));
                     resultGoal.addFormula(new SequentFormula(resultTerm), true, false);
                 }
             }