Skip to content

Commit

Permalink
Removal of Quadruple.java
Browse files Browse the repository at this point in the history
  • Loading branch information
@wadoon
wadoon committed Apr 23, 2024
1 parent 6dee232 commit a599a6d
Show file tree
Hide file tree
Showing 5 changed files with 77 additions and 117 deletions.
44 changes: 23 additions & 21 deletions key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@
import de.uka.ilkd.key.logic.op.LocationVariable;
import de.uka.ilkd.key.rule.merge.MergeProcedure;
import de.uka.ilkd.key.rule.merge.MergeRule;
import de.uka.ilkd.key.util.Quadruple;
import de.uka.ilkd.key.util.mergerule.SymbolicExecutionState;

import org.key_project.util.collection.DefaultImmutableSet;
Expand Down Expand Up @@ -108,7 +107,7 @@ public static Term createIfThenElseTerm(final SymbolicExecutionState state1,
Term cond, ifForm, elseForm;

if (distinguishingFormula == null) {
Quadruple<Term, Term, Term, Boolean> distFormAndRightSidesForITEUpd =
DistanceFormRightSide distFormAndRightSidesForITEUpd =
createDistFormAndRightSidesForITEUpd(state1, state2, ifTerm, elseTerm, services);

cond = distFormAndRightSidesForITEUpd.first();
Expand Down Expand Up @@ -136,18 +135,18 @@ public static Term createIfThenElseTerm(final SymbolicExecutionState state1,
* the discriminating condition, the second and third elements are the respective parts for the
* if and else branch.
*
* @param v Variable to return the update for.
* @param state1 First state to evaluate.
* @param state2 Second state to evaluate.
* @param v Variable to return the update for.
* @param state1 First state to evaluate.
* @param state2 Second state to evaluate.
* @param services The services object.
* @return Input to construct an elementary update like
* <code>{ v := \if (first) \then (second) \else (third) }</code>, where first, second
* and third are the respective components of the returned triple. The fourth component
* indicates whether the path condition of the first (fourth component = false) or the
* second (fourth component = true) state was used as a basis for the condition (first
* component).
* <code>{ v := \if (first) \then (second) \else (third) }</code>, where first, second
* and third are the respective components of the returned triple. The fourth component
* indicates whether the path condition of the first (fourth component = false) or the
* second (fourth component = true) state was used as a basis for the condition (first
* component).
*/
static Quadruple<Term, Term, Term, Boolean> createDistFormAndRightSidesForITEUpd(
static DistanceFormRightSide createDistFormAndRightSidesForITEUpd(
LocationVariable v, SymbolicExecutionState state1, SymbolicExecutionState state2,
Services services) {

Expand Down Expand Up @@ -178,19 +177,19 @@ static Quadruple<Term, Term, Term, Boolean> createDistFormAndRightSidesForITEUpd
* the triple is the discriminating condition, the second and third elements are the respective
* parts for the if and else branch.
*
* @param state1 First state to evaluate.
* @param state2 Second state to evaluate.
* @param ifTerm The if term.
* @param state1 First state to evaluate.
* @param state2 Second state to evaluate.
* @param ifTerm The if term.
* @param elseTerm The else term.
* @param services The services object.
* @return Input to construct an elementary update like
* <code>{ v := \if (first) \then (second) \else (third) }</code>, where first, second
* and third are the respective components of the returned triple. The fourth component
* indicates whether the path condition of the first (fourth component = false) or the
* second (fourth component = true) state was used as a basis for the condition (first
* component).
* <code>{ v := \if (first) \then (second) \else (third) }</code>, where first, second
* and third are the respective components of the returned triple. The fourth component
* indicates whether the path condition of the first (fourth component = false) or the
* second (fourth component = true) state was used as a basis for the condition (first
* component).
*/
static Quadruple<Term, Term, Term, Boolean> createDistFormAndRightSidesForITEUpd(
static DistanceFormRightSide createDistFormAndRightSidesForITEUpd(
SymbolicExecutionState state1, SymbolicExecutionState state2, Term ifTerm,
Term elseTerm, Services services) {

Expand Down Expand Up @@ -246,7 +245,7 @@ static Quadruple<Term, Term, Term, Boolean> createDistFormAndRightSidesForITEUpd
distinguishingFormula = trySimplify(services.getProof(), distinguishingFormula, true,
SIMPLIFICATION_TIMEOUT_MS);

return new Quadruple<>(distinguishingFormula,
return new DistanceFormRightSide(distinguishingFormula,
commuteSides ? elseTerm : ifTerm, commuteSides ? ifTerm : elseTerm, commuteSides);

}
Expand All @@ -255,4 +254,7 @@ static Quadruple<Term, Term, Term, Boolean> createDistFormAndRightSidesForITEUpd
public String toString() {
return DISPLAY_NAME;
}

public record DistanceFormRightSide(Term first, Term second, Term third, boolean fourth) {
}
}
3 changes: 1 addition & 2 deletions key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeIfThenElseAntecedent.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
import de.uka.ilkd.key.logic.op.JFunction;
import de.uka.ilkd.key.rule.merge.MergeProcedure;
import de.uka.ilkd.key.rule.merge.MergeRule;
import de.uka.ilkd.key.util.Quadruple;
import de.uka.ilkd.key.util.mergerule.MergeRuleUtils;
import de.uka.ilkd.key.util.mergerule.SymbolicExecutionState;

Expand Down Expand Up @@ -103,7 +102,7 @@ private static ImmutableSet<Term> getIfThenElseConstraints(Term constrained, Ter
ImmutableSet<Term> result = DefaultImmutableSet.nil();

if (distinguishingFormula == null) {
final Quadruple<Term, Term, Term, Boolean> distFormAndRightSidesForITEUpd =
final MergeByIfThenElse.DistanceFormRightSide distFormAndRightSidesForITEUpd =
MergeByIfThenElse.createDistFormAndRightSidesForITEUpd(state1, state2, ifTerm,
elseTerm, services);

Expand Down
35 changes: 0 additions & 35 deletions key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java
View file

This file was deleted.

22 changes: 15 additions & 7 deletions keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,16 +3,15 @@
* SPDX-License-Identifier: GPL-2.0-only */
package org.key_project.slicing;

import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.util.Triple;

import java.util.Comparator;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.stream.Collectors;

import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.util.Quadruple;
import de.uka.ilkd.key.util.Triple;

/**
* Simple data object to store a mapping of rules to various counters.
*
Expand Down Expand Up @@ -83,10 +82,9 @@ public void addInitialUselessApplication(Rule rule, boolean branches) {
* @param comparator custom comparator
* @return list of rule names + counters
*/
public List<Quadruple<String, Integer, Integer, Integer>> sortBy(
Comparator<Quadruple<String, Integer, Integer, Integer>> comparator) {
public List<RuleStatisticEntry> sortBy(Comparator<RuleStatisticEntry> comparator) {
return map.entrySet().stream()
.map(entry -> new Quadruple<>(entry.getKey(), entry.getValue().first,
.map(entry -> new RuleStatisticEntry(entry.getKey(), entry.getValue().first,
entry.getValue().second, entry.getValue().third))
.sorted(comparator)
.collect(Collectors.toList());
Expand All @@ -99,4 +97,14 @@ public List<Quadruple<String, Integer, Integer, Integer>> sortBy(
public boolean branches(String rule) {
return ruleBranched.get(rule);
}

/**
* Usage statistic of a rule.
* @param ruleName
* @param numberOfApplications
* @param numberOfUselessApplications
* @param numberOfInitialUselessApplications
*/
public record RuleStatisticEntry(String ruleName, int numberOfApplications, int numberOfUselessApplications, int numberOfInitialUselessApplications) {
}
}
90 changes: 38 additions & 52 deletions keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,20 +3,19 @@
* SPDX-License-Identifier: GPL-2.0-only */
package org.key_project.slicing.ui;

import java.awt.*;
import java.awt.event.KeyAdapter;
import java.awt.event.KeyEvent;
import java.util.*;
import java.util.List;
import javax.swing.*;

import de.uka.ilkd.key.gui.MainWindow;
import de.uka.ilkd.key.gui.configuration.Config;
import de.uka.ilkd.key.util.Quadruple;

import org.key_project.slicing.RuleStatistics;
import org.key_project.slicing.RuleStatistics.RuleStatisticEntry;
import org.key_project.slicing.analysis.AnalysisResults;

import javax.swing.*;
import java.awt.*;
import java.awt.event.KeyAdapter;
import java.awt.event.KeyEvent;
import java.util.List;
import java.util.*;

/**
* Dialog that displays the results of the dependency analysis algorithm.
*
Expand Down Expand Up @@ -59,15 +58,15 @@ private void createUI(Window window) {
statisticsPane.setBackground(MainWindow.getInstance().getBackground());
statisticsPane.setSize(new Dimension(10, 360));
statisticsPane.setPreferredSize(
new Dimension(statisticsPane.getPreferredSize().width + 15, 360));
new Dimension(statisticsPane.getPreferredSize().width + 15, 360));

JScrollPane scrollPane = new JScrollPane(statisticsPane);
scrollPane.setBorder(BorderFactory.createEmptyBorder());

Font myFont = UIManager.getFont(Config.KEY_FONT_PROOF_TREE);
if (myFont != null) {
statisticsPane.putClientProperty(JEditorPane.HONOR_DISPLAY_PROPERTIES,
Boolean.TRUE);
Boolean.TRUE);
statisticsPane.setFont(myFont);
}

Expand All @@ -78,18 +77,17 @@ private void createUI(Window window) {

int w = 50
+ Math.max(
scrollPane.getPreferredSize().width,
buttonPane.getPreferredSize().width);
scrollPane.getPreferredSize().width,
buttonPane.getPreferredSize().width);
int h = scrollPane.getPreferredSize().height
+ buttonPane.getPreferredSize().height
+ 100;
setSize(w, h);

statisticsPane.setText(genTable(
statistics.sortBy(
Comparator
.comparing((Quadruple<String, Integer, Integer, Integer> it) -> it.second())
.reversed())));
statistics.sortBy(
Comparator.comparing(RuleStatisticEntry::numberOfApplications)
.reversed())));
statisticsPane.setCaretPosition(0);
setLocationRelativeTo(window);
}
Expand All @@ -111,37 +109,25 @@ private JPanel constructButtonPanel(JEditorPane statisticsPane) {
JButton sortButton1 = new JButton("Sort by name");
sortButton1.addActionListener(event -> {
statisticsPane.setText(genTable(
statistics.sortBy(Comparator.comparing(Quadruple::first))));
statistics.sortBy(Comparator.comparing(RuleStatisticEntry::ruleName))));
statisticsPane.setCaretPosition(0);
});
JButton sortButton2 = new JButton("Sort by total");
sortButton2.addActionListener(event -> {
statisticsPane.setText(genTable(
statistics.sortBy(
Comparator
.comparing(
(Quadruple<String, Integer, Integer, Integer> it) -> it.second())
.reversed())));
statistics.sortBy(Comparator.comparing(RuleStatisticEntry::numberOfApplications).reversed())));
statisticsPane.setCaretPosition(0);
});
JButton sortButton3 = new JButton("Sort by useless");
sortButton3.addActionListener(event -> {
statisticsPane.setText(genTable(
statistics.sortBy(
Comparator
.comparing(
(Quadruple<String, Integer, Integer, Integer> it) -> it.third())
.reversed())));
statistics.sortBy(Comparator.comparing(RuleStatisticEntry::numberOfUselessApplications).reversed())));
statisticsPane.setCaretPosition(0);
});
JButton sortButton4 = new JButton("Sort by initial useless");
sortButton4.addActionListener(event -> {
statisticsPane.setText(genTable(
statistics.sortBy(
Comparator
.comparing(
(Quadruple<String, Integer, Integer, Integer> it) -> it.fourth())
.reversed())));
statistics.sortBy(Comparator.comparing(RuleStatisticEntry::numberOfInitialUselessApplications).reversed())));
statisticsPane.setCaretPosition(0);
});

Expand Down Expand Up @@ -170,37 +156,37 @@ public void keyTyped(KeyEvent e) {
* @param rules statistics on rule apps (see {@link RuleStatistics})
* @return HTML
*/
private String genTable(List<Quadruple<String, Integer, Integer, Integer>> rules) {
private String genTable(List<RuleStatisticEntry> rules) {
List<String> columns = List.of("Rule name", "Total applications", "Useless applications",
"Initial useless applications");
"Initial useless applications");

List<Collection<String>> rows = new ArrayList<>();
// summary row
int uniqueRules = rules.size();
int totalSteps = rules.stream().mapToInt(Quadruple::second).sum();
int uselessSteps = rules.stream().mapToInt(Quadruple::third).sum();
int initialUseless = rules.stream().mapToInt(Quadruple::fourth).sum();
int totalSteps = rules.stream().mapToInt(RuleStatisticEntry::numberOfApplications).sum();
int uselessSteps = rules.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum();
int initialUseless = rules.stream().mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum();
rows.add(List.of(String.format("(all %d rules)", uniqueRules), Integer.toString(totalSteps),
Integer.toString(uselessSteps), Integer.toString(initialUseless)));
Integer.toString(uselessSteps), Integer.toString(initialUseless)));
// next summary row
List<Quadruple<String, Integer, Integer, Integer>> rulesBranching =
rules.stream().filter(it -> statistics.branches(it.first())).toList();
List<RuleStatisticEntry> rulesBranching =
rules.stream().filter(it -> statistics.branches(it.ruleName())).toList();
int uniqueRules2 = rulesBranching.size();
totalSteps = rulesBranching.stream().mapToInt(Quadruple::second).sum();
uselessSteps = rulesBranching.stream().mapToInt(Quadruple::third).sum();
initialUseless = rulesBranching.stream().mapToInt(Quadruple::fourth).sum();
totalSteps = rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfApplications).sum();
uselessSteps = rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum();
initialUseless = rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum();
rows.add(List.of(String.format("(%d branching rules)", uniqueRules2),
Integer.toString(totalSteps), Integer.toString(uselessSteps),
Integer.toString(initialUseless)));
Integer.toString(totalSteps), Integer.toString(uselessSteps),
Integer.toString(initialUseless)));
rules.forEach(a -> {
String name = a.first();
Integer all = a.second();
Integer useless = a.third();
Integer iua = a.fourth();
String name = a.ruleName();
Integer all = a.numberOfApplications();
Integer useless = a.numberOfUselessApplications();
Integer iua = a.numberOfInitialUselessApplications();
rows.add(List.of(name, all.toString(), useless.toString(), iua.toString()));
});

return HtmlFactory.generateTable(columns, new boolean[] { false, false, false, false },
Optional.of(new String[] { null, "right", "right", "right" }), rows, null);
return HtmlFactory.generateTable(columns, new boolean[]{false, false, false, false},
Optional.of(new String[]{null, "right", "right", "right"}), rows, null);
}
}

0 comments on commit a599a6d

Please sign in to comment.