Removal of Triple, and Quadruple (#3529)

KeYProject · Dec 5, 2024 · 0ae2058 · 0ae2058
2 parents 9ef68b3 + 7c41529
commit 0ae2058
Show file tree

Hide file tree

Showing 45 changed files with 574 additions and 586 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
@@ -6,7 +6,6 @@
 import java.util.Deque;
 import java.util.LinkedList;
 import java.util.List;
-import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.ldt.JavaDLTheory;
@@ -18,14 +17,12 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.JFunction;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
 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 +84,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 +131,5 @@ protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Servi
     public boolean isApplicableOnSubTerms() {
         return false;
     }
+
 }
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
@@ -8,24 +8,13 @@
 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.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableArray;
@@ -181,7 +170,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
                     .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
@@ -190,10 +179,11 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
             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;
@@ -228,7 +225,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
             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
@@ -237,10 +234,11 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
             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) {
@@ -256,11 +254,11 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
                         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);
                 }
             }

diff --git a/..._execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ResultsAndCondition.java b/..._execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ResultsAndCondition.java
@@ -0,0 +1,19 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.symbolic_execution.rule;
+
+import java.util.Set;
+
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.proof.Node;
+
+/**
+ * The return value of a side proof.
+ *
+ * @param result     a term representing the result (first formula of succedent)
+ * @param conditions formulas of the antecedent
+ * @param node       the final node of the side proof
+ */
+public record ResultsAndCondition(Term result, Set<Term> conditions, Node node) {
+}
diff --git a/...src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java b/...src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java
@@ -32,9 +32,9 @@
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile;
 import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile;
+import de.uka.ilkd.key.symbolic_execution.rule.ResultsAndCondition;
 import de.uka.ilkd.key.util.ProofStarter;
 import de.uka.ilkd.key.util.SideProofUtil;
-import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableArray;
@@ -169,7 +169,8 @@ public static List<Pair<Term, Node>> computeResults(Services services, Proof pro
      * @return The found result {@link Term} and the conditions.
      * @throws ProofInputException Occurred Exception.
      */
-    public static List<Triple<Term, Set<Term>, Node>> computeResultsAndConditions(Services services,
+    public static List<ResultsAndCondition> computeResultsAndConditions(
+            Services services,
             Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve,
             Operator operator, String description, String methodTreatment, String loopTreatment,
             String queryTreatment, String splittingOption, boolean addNamesToServices)
@@ -182,8 +183,7 @@ public static List<Triple<Term, Set<Term>, Node>> computeResultsAndConditions(Se
             Set<Operator> relevantThingsInSequentToProve =
                 extractRelevantThings(info.getProof().getServices(), sequentToProve);
             // Extract results and conditions from side proof
-            List<Triple<Term, Set<Term>, Node>> conditionsAndResultsMap =
-                new LinkedList<>();
+            List<ResultsAndCondition> conditionsAndResultsMap = new LinkedList<>();
             for (Goal resultGoal : info.getProof().openGoals()) {
                 if (SymbolicExecutionUtil.hasApplicableRules(resultGoal)) {
                     throw new IllegalStateException("Not all applicable rules are applied.");
@@ -245,8 +245,8 @@ public static List<Triple<Term, Set<Term>, Node>> computeResultsAndConditions(Se
                 if (result == null) {
                     result = services.getTermBuilder().ff();
                 }
-                conditionsAndResultsMap.add(
-                    new Triple<>(result, resultConditions, resultGoal.node()));
+                conditionsAndResultsMap
+                        .add(new ResultsAndCondition(result, resultConditions, resultGoal.node()));
             }
             return conditionsAndResultsMap;
         } finally {
@@ -303,14 +303,11 @@ public static void addNewNamesToNamespace(Services services, Term term) {
         final Namespace<JFunction> functions = services.getNamespaces().functions();
         final Namespace<IProgramVariable> progVars = services.getNamespaces().programVariables();
         // LogicVariables are always local bound
-        term.execPreOrder(new DefaultVisitor() {
-            @Override
-            public void visit(Term visited) {
-                if (visited.op() instanceof JFunction) {
-                    functions.add((JFunction) visited.op());
-                } else if (visited.op() instanceof IProgramVariable) {
-                    progVars.add((IProgramVariable) visited.op());
-                }
+        term.execPreOrder((DefaultVisitor) visited -> {
+            if (visited.op() instanceof JFunction) {
+                functions.add((JFunction) visited.op());
+            } else if (visited.op() instanceof IProgramVariable) {
+                progVars.add((IProgramVariable) visited.op());
             }
         });
     }
@@ -385,12 +382,9 @@ public static Set<Operator> extractRelevantThings(final Services services,
             Sequent sequentToProve) {
         final Set<Operator> result = new HashSet<>();
         for (SequentFormula sf : sequentToProve) {
-            sf.formula().execPreOrder(new DefaultVisitor() {
-                @Override
-                public void visit(Term visited) {
-                    if (isRelevantThing(services, visited)) {
-                        result.add(visited.op());
-                    }
+            sf.formula().execPreOrder((DefaultVisitor) visited -> {
+                if (isRelevantThing(services, visited)) {
+                    result.add(visited.op());
                 }
             });
         }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
@@ -10,7 +10,7 @@
 
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.parser.Location;
+import de.uka.ilkd.key.nparser.ProofScriptEntry;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
@@ -21,7 +21,7 @@
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
 
-import org.key_project.util.collection.Pair;
+import org.jspecify.annotations.Nullable;
 
 /**
  * Instances of this class are used to collect and access all relevant information for verification
@@ -48,7 +48,7 @@ public class KeYEnvironment<U extends UserInterfaceControl> {
     /**
      * An optional field denoting a script contained in the proof file.
      */
-    private final Pair<String, Location> proofScript;
+    private final @Nullable ProofScriptEntry proofScript;
 
     /**
      * Indicates that this {@link KeYEnvironment} is disposed.
@@ -77,7 +77,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) {
      * @param initConfig The loaded project.
      */
     public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof,
-            Pair<String, Location> proofScript, ReplayResult replayResult) {
+            @Nullable ProofScriptEntry proofScript, ReplayResult replayResult) {
         this.ui = ui;
         this.initConfig = initConfig;
         this.loadedProof = loadedProof;
@@ -317,7 +317,7 @@ public boolean isDisposed() {
         return disposed;
     }
 
-    public Pair<String, Location> getProofScript() {
+    public @Nullable ProofScriptEntry getProofScript() {
         return proofScript;
     }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java
@@ -3,9 +3,11 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.nparser;
 
+import java.net.URI;
 import java.net.URL;
 import java.util.List;
 
+import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.nparser.builder.BuilderHelpers;
 import de.uka.ilkd.key.nparser.builder.ChoiceFinder;
 import de.uka.ilkd.key.nparser.builder.FindProblemInformation;
@@ -15,7 +17,6 @@
 import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.settings.ProofSettings;
 import de.uka.ilkd.key.speclang.njml.JmlParser;
-import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.util.java.StringUtil;
 
@@ -84,12 +85,24 @@ public static class File extends KeyAst<KeYParser.FileContext> {
             return settings;
         }
 
-        public @Nullable Triple<String, Integer, Integer> findProofScript() {
+        /**
+         * Returns the a {@link ProofScriptEntry} from the underlying AST if an {@code \proofscript}
+         * entry is present.
+         * The {@code url} is used as the source of input and might be later used for error message,
+         * or including
+         * other files.
+         *
+         * @param url location pointing to the source of the AST
+         * @return a {@link ProofScriptEntry} if {@code \proofscript} is present
+         */
+        public @Nullable ProofScriptEntry findProofScript(URI url) {
             if (ctx.problem() != null && ctx.problem().proofScript() != null) {
                 KeYParser.ProofScriptContext pctx = ctx.problem().proofScript();
+                Location location = new Location(url,
+                    Position.newOneBased(pctx.ps.getLine(), pctx.ps.getCharPositionInLine()));
+
                 String text = pctx.ps.getText();
-                return new Triple<>(StringUtil.trim(text, '"'), pctx.ps.getLine(),
-                    pctx.ps.getCharPositionInLine());
+                return new ProofScriptEntry(StringUtil.trim(text, '"'), location);
             }
             return null;
         }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofScriptEntry.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofScriptEntry.java
@@ -0,0 +1,19 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.nparser;
+
+import de.uka.ilkd.key.parser.Location;
+
+import org.jspecify.annotations.NonNull;
+
+/**
+ * This struct encapsulate the information of a proofscript found in key files.
+ *
+ * @param script the content of the script
+ * @param location location of the content
+ * @author Alexander Weigl
+ * @version 1 (23.04.24)
+ */
+public record ProofScriptEntry(@NonNull String script, @NonNull Location location) {
+}