Skip to content

Commit 423c10b

Browse files
wadoonwadoon
committed
Removal of the Triple class
1 parent a599a6d commit 423c10b

File tree

33 files changed

+499
-616
lines changed

33 files changed

+499
-616
lines changed

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@
2525
import de.uka.ilkd.key.rule.BuiltInRule;
2626
import de.uka.ilkd.key.strategy.StrategyProperties;
2727
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
28-
import de.uka.ilkd.key.util.Triple;
2928

3029
import org.key_project.logic.Name;
3130
import org.key_project.logic.sort.Sort;
@@ -87,7 +86,7 @@ protected JFunction createResultFunction(Services services, Sort sort) {
8786
* @return The found result {@link Term} and the conditions.
8887
* @throws ProofInputException Occurred Exception.
8988
*/
90-
protected List<Triple<Term, Set<Term>, Node>> computeResultsAndConditions(Services services,
89+
protected List<ResultsAndCondition> computeResultsAndConditions(Services services,
9190
Goal goal, ProofEnvironment sideProofEnvironment, Sequent sequentToProve,
9291
JFunction newPredicate) throws ProofInputException {
9392
return SymbolicExecutionSideProofUtil.computeResultsAndConditions(services, goal.proof(),
@@ -134,4 +133,7 @@ protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Servi
134133
public boolean isApplicableOnSubTerms() {
135134
return false;
136135
}
136+
137+
public record ResultsAndCondition(Term result, Set<Term> conditions, Node node) {
138+
}
137139
}

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java‎

Lines changed: 11 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -3,36 +3,23 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.symbolic_execution.rule;
55

6-
import java.util.LinkedHashSet;
7-
import java.util.List;
8-
import java.util.Set;
9-
106
import de.uka.ilkd.key.java.Services;
11-
import de.uka.ilkd.key.logic.PosInOccurrence;
12-
import de.uka.ilkd.key.logic.Sequent;
13-
import de.uka.ilkd.key.logic.SequentFormula;
14-
import de.uka.ilkd.key.logic.Term;
15-
import de.uka.ilkd.key.logic.TermBuilder;
16-
import de.uka.ilkd.key.logic.TermServices;
7+
import de.uka.ilkd.key.logic.*;
178
import de.uka.ilkd.key.logic.op.*;
189
import de.uka.ilkd.key.proof.Goal;
19-
import de.uka.ilkd.key.proof.Node;
2010
import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
21-
import de.uka.ilkd.key.rule.BuiltInRule;
22-
import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
23-
import de.uka.ilkd.key.rule.IBuiltInRuleApp;
24-
import de.uka.ilkd.key.rule.RuleAbortException;
25-
import de.uka.ilkd.key.rule.RuleApp;
11+
import de.uka.ilkd.key.rule.*;
2612
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
2713
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
28-
import de.uka.ilkd.key.util.Triple;
29-
14+
import org.jspecify.annotations.NonNull;
3015
import org.key_project.logic.Name;
3116
import org.key_project.util.collection.ImmutableArray;
3217
import org.key_project.util.collection.ImmutableList;
3318
import org.key_project.util.collection.Pair;
3419

35-
import org.jspecify.annotations.NonNull;
20+
import java.util.LinkedHashSet;
21+
import java.util.List;
22+
import java.util.Set;
3623

3724
/**
3825
* <p>
@@ -182,7 +169,7 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
182169
.addFormula(new SequentFormula(newModalityWithUpdatesTerm), false, false)
183170
.sequent();
184171
// Compute results and their conditions
185-
List<Triple<Term, Set<Term>, Node>> conditionsAndResultsMap =
172+
List<ResultsAndCondition> conditionsAndResultsMap =
186173
computeResultsAndConditions(services, goal, sideProofEnv, sequentToProve,
187174
newPredicate);
188175
// 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)
191178
resultGoal.removeFormula(pio);
192179
// Create results
193180
Set<Term> resultTerms = new LinkedHashSet<>();
194-
for (Triple<Term, Set<Term>, Node> conditionsAndResult : conditionsAndResultsMap) {
195-
Term conditionTerm = tb.and(conditionsAndResult.second);
196-
Term resultEqualityTerm = varFirst ? tb.equals(conditionsAndResult.first, otherTerm)
197-
: tb.equals(otherTerm, conditionsAndResult.first);
181+
for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
182+
Term conditionTerm = tb.and(conditionsAndResult.conditions());
183+
Term resultEqualityTerm = varFirst ? tb.equals(conditionsAndResult.result(), otherTerm)
184+
: tb.equals(otherTerm, conditionsAndResult.result());
198185
Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, resultEqualityTerm)
199186
: tb.and(conditionTerm, resultEqualityTerm);
200187
resultTerms.add(resultTerm);

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java‎

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
package de.uka.ilkd.key.symbolic_execution.rule;
55

66
import java.util.List;
7-
import java.util.Set;
87

98
import de.uka.ilkd.key.java.Services;
109
import de.uka.ilkd.key.logic.PIOPathIterator;
@@ -16,7 +15,6 @@
1615
import de.uka.ilkd.key.logic.TermServices;
1716
import de.uka.ilkd.key.logic.op.*;
1817
import de.uka.ilkd.key.proof.Goal;
19-
import de.uka.ilkd.key.proof.Node;
2018
import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
2119
import de.uka.ilkd.key.rule.BuiltInRule;
2220
import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
@@ -25,7 +23,6 @@
2523
import de.uka.ilkd.key.rule.RuleAbortException;
2624
import de.uka.ilkd.key.rule.RuleApp;
2725
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
28-
import de.uka.ilkd.key.util.Triple;
2926

3027
import org.key_project.logic.Name;
3128
import org.key_project.logic.sort.Sort;
@@ -229,7 +226,7 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
229226
sequentToProve =
230227
sequentToProve.addFormula(new SequentFormula(newTerm), false, false).sequent();
231228
// Compute results and their conditions
232-
List<Triple<Term, Set<Term>, Node>> conditionsAndResultsMap =
229+
List<ResultsAndCondition> conditionsAndResultsMap =
233230
computeResultsAndConditions(services, goal, sideProofEnv, sequentToProve,
234231
newPredicate);
235232
// 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)
238235
final TermBuilder tb = services.getTermBuilder();
239236
resultGoal.removeFormula(pio);
240237
if (pio.isTopLevel() || queryConditionTerm != null) {
241-
for (Triple<Term, Set<Term>, Node> conditionsAndResult : conditionsAndResultsMap) {
242-
Term conditionTerm = tb.and(conditionsAndResult.second);
243-
Term newEqualityTerm = varFirst ? tb.equals(varTerm, conditionsAndResult.first)
244-
: tb.equals(conditionsAndResult.first, varTerm);
238+
for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
239+
Term conditionTerm = tb.and(conditionsAndResult.conditions());
240+
Term newEqualityTerm = varFirst ? tb.equals(varTerm, conditionsAndResult.result())
241+
: tb.equals(conditionsAndResult.result(), varTerm);
245242
Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, newEqualityTerm)
246243
: tb.and(conditionTerm, newEqualityTerm);
247244
if (queryConditionTerm != null) {
@@ -257,11 +254,11 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
257254
tb.equals(resultFunctionTerm, varTerm),
258255
services),
259256
pio.isInAntec(), false);
260-
for (Triple<Term, Set<Term>, Node> conditionsAndResult : conditionsAndResultsMap) {
261-
Term conditionTerm = tb.and(conditionsAndResult.second);
257+
for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) {
258+
Term conditionTerm = tb.and(conditionsAndResult.conditions());
262259
Term resultTerm = tb.imp(conditionTerm,
263-
varFirst ? tb.equals(resultFunctionTerm, conditionsAndResult.first)
264-
: tb.equals(conditionsAndResult.first, resultFunctionTerm));
260+
varFirst ? tb.equals(resultFunctionTerm, conditionsAndResult.result())
261+
: tb.equals(conditionsAndResult.result(), resultFunctionTerm));
265262
resultGoal.addFormula(new SequentFormula(resultTerm), true, false);
266263
}
267264
}

0 commit comments

Comments
 (0)