Skip to content

Commit

Permalink
Removal of the Triple class
Browse files Browse the repository at this point in the history
  • Loading branch information
wadoon committed Apr 23, 2024
1 parent f067b67 commit c691c0b
Show file tree
Hide file tree
Showing 33 changed files with 499 additions and 616 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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) {
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down Expand Up @@ -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
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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) {
Expand All @@ -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);
}
}
Expand Down
Loading

0 comments on commit c691c0b

Please sign in to comment.