diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index 55a1b0ff102..7e57347e10d 100644 --- a/.git-blame-ignore-revs +++ b/.git-blame-ignore-revs @@ -4,3 +4,5 @@ b1ed8d6bc836ea40f357a839707d41fbb04ed6e2 # commit with manual formatting corrections a9fcedc6c8d96f2480549254a307b3fbe31f04bd +# formatting +f91bf7fa6d3a63720cbcfee5147a78854faa8e8a \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java b/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java index 178786cef84..9cc8fbc03a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java @@ -9,7 +9,8 @@ import java.util.Set; import de.uka.ilkd.key.logic.op.ElementaryUpdate; -import de.uka.ilkd.key.logic.op.Operator; + +import org.key_project.logic.op.Operator; /** * Collects all operators occurring in the traversed term. diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java index 6e6ffda4e91..09f232bd0c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java @@ -30,7 +30,7 @@ * @author weigl * @deprecated Use the facade new KeyIO(services).parseTerm directly */ -@Deprecated // java11:(forRemoval = true, since = "2.8.0") +@Deprecated(forRemoval = true, since = "2.8.0") public final class DefaultTermParser { /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java b/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java index 44255d8f012..94fcae3a8dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java @@ -16,7 +16,7 @@ * * @author Arne Keller */ -public class BranchLocation { +public class BranchLocation implements Comparable { /** * Branch location of the initial proof branch. */ @@ -82,6 +82,9 @@ public static BranchLocation commonPrefix(BranchLocation... locations) { * @return the remaining suffix */ public BranchLocation stripPrefix(BranchLocation prefix) { + if (prefix.size() == location.size()) { + return BranchLocation.ROOT; + } return new BranchLocation(location.stripPrefix(prefix.location)); } @@ -103,6 +106,9 @@ public BranchLocation append(Pair newBranch) { public BranchLocation removeLast() { List> list = location.toList(); list.remove(list.size() - 1); + if (list.isEmpty()) { + return BranchLocation.ROOT; + } return new BranchLocation(ImmutableList.fromList(list)); } @@ -170,4 +176,17 @@ public boolean equals(Object o) { public int hashCode() { return Objects.hash(location); } + + @Override + public int compareTo(BranchLocation other) { + if (this == other) { + return 0; + } else if (this == BranchLocation.ROOT) { + return -1; + } else if (other == BranchLocation.ROOT) { + return 1; + } else { + return location.compareTo(other.location); + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java b/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java new file mode 100644 index 00000000000..82a86b59b1c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java @@ -0,0 +1,26 @@ +/* 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.proof; + +import java.lang.ref.WeakReference; +import java.util.WeakHashMap; + +import org.key_project.logic.op.Function; + +public final class FunctionTracker { + private static final WeakHashMap> MAPPING = new WeakHashMap<>(); + + private FunctionTracker() { + + } + + public static void setIntroducedBy(Function f, Node n) { + MAPPING.put(f, new WeakReference<>(n)); + } + + public static Node getIntroducedBy(Function f) { + var x = MAPPING.get(f); + return x != null ? x.get() : null; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index b91e7f25808..2df4519234b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -30,6 +30,7 @@ import de.uka.ilkd.key.util.properties.Properties; import de.uka.ilkd.key.util.properties.Properties.Property; +import org.key_project.logic.op.Function; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -657,6 +658,9 @@ private void adaptNamespacesNewGoals(final ImmutableList goalList) { boolean first = true; for (Goal goal : goalList) { goal.node().addLocalProgVars(newProgVars); + for (Function f : newFunctions) { + FunctionTracker.setIntroducedBy(f, goal.node.parent()); + } goal.node().addLocalFunctions(newFunctions); if (first) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index aa62a4c7828..87be042fd78 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -33,7 +33,7 @@ import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; -public class Node implements Iterable { +public class Node implements Iterable, Comparable { private static final String RULE_WITHOUT_NAME = "rule without name"; private static final String RULE_APPLICATION_WITHOUT_RULE = "rule application without rule"; @@ -113,6 +113,10 @@ public class Node implements Iterable { @Nullable private Lookup userData = null; + private List group = null; + private boolean hideInProofTree = false; + private String extraNodeLabel = null; + /** * If the rule base has been extended e.g. by loading a new taclet as lemma or by applying a @@ -837,4 +841,42 @@ public int getStepIndex() { void setStepIndex(int stepIndex) { this.stepIndex = stepIndex; } + + public Node getFirstInBranch() { + Node candidate = this; + while (candidate.parent != null + && candidate.parent.getBranchLocation().equals(candidate.getBranchLocation())) { + candidate = candidate.parent; + } + return candidate; + } + + public List getGroup() { + return group; + } + + public void setGroup(List group) { + this.group = group; + } + + public String getExtraNodeLabel() { + return extraNodeLabel; + } + + public void setExtraNodeLabel(String extraNodeLabel) { + this.extraNodeLabel = extraNodeLabel; + } + + public boolean isHideInProofTree() { + return hideInProofTree; + } + + public void setHideInProofTree(boolean hideInProofTree) { + this.hideInProofTree = hideInProofTree; + } + + @Override + public int compareTo(Node node) { + return Integer.compare(this.serialNr, node.serialNr); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index 48538a003f3..a8db47e385f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -68,7 +68,7 @@ public abstract class AbstractProofReplayer { /** * The new proof. */ - private final Proof proof; + protected final Proof proof; /** * Instantiate a new replayer. @@ -93,6 +93,7 @@ protected ImmutableList reApplyRuleApp(Node node, Goal openGoal) throws IntermediateProofReplayer.BuiltInConstructionException { RuleApp ruleApp = node.getAppliedRuleApp(); ImmutableList nextGoals; + if (ruleApp.rule() instanceof BuiltInRule) { IBuiltInRuleApp builtInRuleApp = constructBuiltinApp(node, openGoal); if (!builtInRuleApp.complete()) { @@ -318,6 +319,7 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) { } if (!ourApp.complete()) { + System.out.println("incomplete!"); ourApp = ourApp.tryToInstantiate(proof.getServices()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java new file mode 100644 index 00000000000..62c3ed53725 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java @@ -0,0 +1,18 @@ +/* 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.rule; + +import de.uka.ilkd.key.logic.PosInOccurrence; + +/** + * Interface for rule applications with associated position information. + * + * @author Arne Keller + */ +public interface PosRuleApp { + /** + * @return the position the rule was applied on + */ + PosInOccurrence posInOccurrence(); +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java index 6c5d92442ad..5eecf22e2e8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java @@ -27,7 +27,7 @@ * ({@link de.uka.ilkd.key.rule.NoPosTacletApp}) is used to keep track of the (partial) * instantiation information. */ -public class PosTacletApp extends TacletApp { +public class PosTacletApp extends TacletApp implements PosRuleApp { /** * stores the information where the Taclet is to be applied. This means where the find section diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java index d930c46b70f..adda0d65ba5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.QuantifiableVariable; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.proof.Goal; @@ -23,6 +22,7 @@ import org.key_project.logic.Name; import org.key_project.logic.Named; +import org.key_project.logic.op.Operator; import org.key_project.util.EqualsModProofIrrelevancy; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -728,8 +728,8 @@ public Set collectSchemaVars() { } for (Operator op : oc.ops()) { - if (op instanceof SchemaVariable) { - result.add((SchemaVariable) op); + if (op instanceof SchemaVariable sv) { + result.add(sv); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index 207e9cf806e..a7b9f415b5f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java @@ -812,7 +812,7 @@ private TermAndBoundVarPair replaceBoundLogicVars(Term t, TermServices services) final OpCollector oc = new OpCollector(); oc.visit(t); final Set usedNames = new LinkedHashSet<>(); - for (Operator op : oc.ops()) { + for (var op : oc.ops()) { usedNames.add(op.name()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index 77a165021de..455fb6137d0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -76,6 +76,9 @@ public void addSettings(Settings settings) { settings.addPropertyChangeListener(settingsListener); if (lastReadedProperties != null) { settings.readSettings(lastReadedProperties); + } else { + // special case: no settings file present + settings.readSettings(new Properties()); } if (lastReadedConfiguration != null) { settings.readSettings(lastReadedConfiguration); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key index ca36ae77625..898e589387c 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key @@ -1806,7 +1806,7 @@ \then(aePseudoRight * aePseudoTargetFactor = aePseudoTargetRight * aePseudoLeftCoeff) \else(aePseudoTargetLeft = aePseudoTargetRight)) - \heuristics(polySimp_leftNonUnit, polySimp_applyEqPseudo, notHumanReadable, notHumanReadable) + \heuristics(polySimp_leftNonUnit, polySimp_applyEqPseudo, notHumanReadable) }; apply_eq_pseudo_leq { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 3f697ff552c..83893233ecd 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1032,7 +1032,7 @@ apply_eq_pseudo_eq { \assumes ([equals(mul(aePseudoLeft,aePseudoLeftCoeff),aePseudoRight)]==>[]) \find(equals(aePseudoTargetLeft,aePseudoTargetRight)) \sameUpdateLevel\replacewith(if-then-else(and(equals(aePseudoTargetLeft,mul(aePseudoLeft,aePseudoTargetFactor)),not(equals(aePseudoLeftCoeff,Z(0(#))))),equals(mul(aePseudoRight,aePseudoTargetFactor),mul(aePseudoTargetRight,aePseudoLeftCoeff)),equals(aePseudoTargetLeft,aePseudoTargetRight))) -\heuristics(notHumanReadable, notHumanReadable, polySimp_applyEqPseudo, polySimp_leftNonUnit) +\heuristics(notHumanReadable, polySimp_applyEqPseudo, polySimp_leftNonUnit) Choices: true} ----------------------------------------------------- == apply_eq_pseudo_geq (apply_eq_pseudo_geq) ========================================= diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java deleted file mode 100644 index cb991480cf9..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java +++ /dev/null @@ -1,70 +0,0 @@ -/* 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.gui; - -import java.awt.*; -import java.awt.event.KeyEvent; -import java.util.stream.Stream; -import javax.swing.*; - -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.gui.actions.AutoModeAction; -import de.uka.ilkd.key.gui.extension.api.TabPanel; -import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; -import de.uka.ilkd.key.gui.prooftree.ProofTreeView; - -/** - * {@link JTabbedPane} displayed in {@link MainWindow}, to the left of - * {@link de.uka.ilkd.key.gui.nodeviews.SequentView}. - * - * @author Kai Wallisch - */ -@Deprecated -public class MainWindowTabbedPane extends JTabbedPane { - private static final long serialVersionUID = 1L; - public static final float TAB_ICON_SIZE = 16f; - private final ProofTreeView proofTreeView; - - MainWindowTabbedPane(MainWindow mainWindow, KeYMediator mediator, - AutoModeAction autoModeAction) { - assert mediator != null; - assert mainWindow != null; - - proofTreeView = new ProofTreeView(mediator); - InfoView infoView = new InfoView(mainWindow, mediator); - StrategySelectionView strategySelectionView = - new StrategySelectionView(mainWindow, mediator); - GoalList openGoalsView = new GoalList(mediator); - - Stream panels = KeYGuiExtensionFacade.getAllPanels(mainWindow); - addPanel(infoView); - addPanel(strategySelectionView); - addPanel(openGoalsView); - addPanel(proofTreeView); - panels.forEach(this::addPanel); - - - // change some key mappings which collide with font settings. - getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT).getParent() - .remove(KeyStroke.getKeyStroke(KeyEvent.VK_UP, - Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); - getInputMap(JComponent.WHEN_FOCUSED).getParent().remove(KeyStroke.getKeyStroke( - KeyEvent.VK_DOWN, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask())); - setName("leftTabbed"); - } - - protected void addPanel(TabPanel p) { - addTab(p.getTitle(), p.getIcon(), p.getComponent()); - } - - protected void setEnabledForAllTabs(boolean b) { - for (int i = 0; i < getTabCount(); i++) { - getComponentAt(i).setEnabled(b); - } - } - - public ProofTreeView getProofTreeView() { - return proofTreeView; - } -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java index 2f937cdc2fa..ff83b4c1bde 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java @@ -65,7 +65,9 @@ public TreeNode[] getPath() { LinkedList path = new LinkedList<>(); TreeNode n = this; path.addFirst(n); - while ((n = n.getParent()) != null) { + // walk up the parent chain + // (robustness: do not continue indefinitely for self-parents) + while (n.getParent() != n && (n = n.getParent()) != null) { path.addFirst(n); } return path.toArray(new TreeNode[0]); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java index 0aeac640d2f..63cd2459ad1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java @@ -25,14 +25,10 @@ public GUIBranchNode(GUIProofTreeModel tree, Node subTree, Object label) { this.label = label; } + @Override public TreeNode getChildAt(int childIndex) { ensureChildrenCacheExists(); return childrenCache.get(childIndex); - /* - * int count = 0; Node n = subTree; while ( childIndex != count && n.childrenCount() == 1 ) - * { count++; n = n.child(0); } if ( childIndex == count ) { return getProofTreeModel - * ().getProofTreeNode(n); } else { return findBranch ( n.child(childIndex-count-1) ); } - */ } private void ensureChildrenCacheExists() { @@ -42,7 +38,6 @@ private void ensureChildrenCacheExists() { return; } - int count = 0; Node n = getNode(); if (n == null) { @@ -50,9 +45,12 @@ private void ensureChildrenCacheExists() { } while (true) { - childrenCache.add(count, getProofTreeModel().getProofTreeNode(n)); - count++; - final Node nextN = findChild(n); + childrenCache.add(getProofTreeModel().getProofTreeNode(n)); + Node nextN = findChild(n); + // skip nodes that are hidden in the proof tree + while (nextN != null && nextN.isHideInProofTree()) { + nextN = findChild(nextN); + } if (nextN == null) { break; } @@ -60,9 +58,9 @@ private void ensureChildrenCacheExists() { } for (int i = 0; i != n.childrenCount(); ++i) { - if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i))) { - childrenCache.add(count, findBranch(n.child(i))); - count++; + if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i)) + && !n.child(i).isHideInProofTree()) { + childrenCache.add(findBranch(n.child(i))); } } } @@ -85,6 +83,7 @@ public int getChildCount() { return childrenCache.size(); } + public TreeNode getParent() { Node self = getNode(); if (self == null) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java index 6508c75a0f3..b4e12744ecd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java @@ -487,7 +487,7 @@ public GUIAbstractTreeNode find(Node n) { public synchronized GUIAbstractTreeNode getProofTreeNode(Node n) { GUIAbstractTreeNode res = find(n); if (res == null) { - res = new GUIProofTreeNode(this, n); + res = new GUIProofTreeNode(this, n, false); proofTreeNodes.put(n, res); } return res; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java index 82d36765ae8..1215f7e5ec3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java @@ -6,6 +6,7 @@ * this class implements a TreeModel that can be displayed using the JTree class framework */ +import java.util.List; import javax.swing.tree.TreeNode; import de.uka.ilkd.key.proof.Node; @@ -17,9 +18,19 @@ class GUIProofTreeNode extends GUIAbstractTreeNode { private GUIAbstractTreeNode[] children; + private final boolean leaf; - public GUIProofTreeNode(GUIProofTreeModel tree, Node node) { + /** + * This constructor should only be called by the {@link GUIProofTreeModel}! + * Use {@link GUIProofTreeModel#getProofTreeNode(Node)} to get the nodes. + * + * @param tree the proof tree + * @param node the node + * @param leaf whether the node is a leaf + */ + GUIProofTreeNode(GUIProofTreeModel tree, Node node, boolean leaf) { super(tree, node); + this.leaf = leaf; } public TreeNode getChildAt(int childIndex) { @@ -37,6 +48,13 @@ public TreeNode getParent() { if (n == null) { return null; } + if (n.isHideInProofTree()) { + // "parent" TreeNode is another proof node + while (n.parent() != null && n.getGroup() == null) { + n = n.parent(); + } + return getProofTreeModel().getProofTreeNode(n); + } while (n.parent() != null && findChild(n.parent()) != null) { n = n.parent(); } @@ -52,6 +70,9 @@ public String toString() { // the proof tree in ProofTreeView.java Node n = getNode(); if (n != null) { + if (n.getExtraNodeLabel() != null) { + return n.serialNr() + ":" + n.getExtraNodeLabel(); + } return n.serialNr() + ":" + n.name(); } else { return "Invalid WeakReference"; @@ -66,6 +87,10 @@ public String toString() { */ private void ensureChildrenArray() { if (children == null) { + if (leaf) { + children = new GUIAbstractTreeNode[0]; + return; + } Node node = getNode(); if (node != null && node.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp ruleApp) { @@ -79,6 +104,13 @@ private void ensureChildrenArray() { } return; } + } else if (node != null && node.getGroup() != null) { + List group = node.getGroup(); + children = new GUIAbstractTreeNode[group.size() - 1]; + for (int i = 1; i < group.size(); i++) { + children[i - 1] = getProofTreeModel().getProofTreeNode(group.get(i)); + } + return; } // otherwise diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index af3bf9cbfe4..18593a8cb50 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java @@ -6,8 +6,11 @@ import java.awt.*; import java.io.File; +import java.util.ArrayList; import java.util.Arrays; +import java.util.HashMap; import java.util.List; +import java.util.Map; import javax.swing.*; import de.uka.ilkd.key.gui.KeYFileChooser; @@ -34,6 +37,8 @@ public abstract class SettingsPanel extends SimpleSettingsPanel { private static final long serialVersionUID = 3465371513326517504L; + private final Map> rows = new HashMap<>(); + protected SettingsPanel() { pCenter.setLayout(new MigLayout( // set up rows: @@ -57,7 +62,6 @@ protected SettingsPanel() { */ protected static JTextArea createInfoArea(String info) { JTextArea textArea = new JTextArea(info); - // textArea.setBackground(this.getBackground()); textArea.setEditable(false); textArea.setLineWrap(true); textArea.setWrapStyleWord(true); @@ -68,7 +72,9 @@ protected static JTextArea createInfoArea(String info) { * @param info * @param components */ - protected void addRowWithHelp(String info, JComponent... components) { + protected List addRowWithHelp(String info, JComponent... components) { + List comps = new ArrayList<>(List.of(components)); + boolean hasInfo = info != null && !info.isEmpty(); for (JComponent component : components) { component.setAlignmentX(LEFT_ALIGNMENT); @@ -83,6 +89,8 @@ protected void addRowWithHelp(String info, JComponent... components) { infoButton = new JLabel(); } pCenter.add(infoButton); + comps.add(infoButton); + return comps; } /** @@ -226,7 +234,21 @@ protected JComboBox addComboBox(String title, String info, int selectionI protected void addTitledComponent(String title, JComponent component, String helpText) { JLabel label = new JLabel(title); label.setLabelFor(component); - addRowWithHelp(helpText, label, component); + var comps = addRowWithHelp(helpText, label, component); + comps.add(label); + rows.put(title, comps); + } + + /** + * Remove a row previously added with {@link #addTitledComponent(String, JComponent, String)}. + * + * @param title title of component + */ + protected void removeTitledComponent(String title) { + for (var c : rows.get(title)) { + pCenter.remove(c); + } + rows.remove(title); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java index 02936f6fbfd..a065635f9d4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsProvider.java @@ -42,6 +42,22 @@ public interface SettingsProvider { */ JPanel getPanel(MainWindow window); + /** + * Provides the visual component for the right side. + *

+ * This panel will be wrapped inside a {@link JScrollPane}. + *

+ * You are allowed to reuse the return component. But then you should update the components, + * e.g. text field, during handling of the call. + * + * @param window non-null reference + * @param settingsDialog the settings dialog + * @return + */ + default JComponent getPanel(MainWindow window, JDialog settingsDialog) { + return getPanel(window); + } + /** * Tree children of your settings dialog. *

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java new file mode 100644 index 00000000000..b8b06d9034a --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/FormDialog.java @@ -0,0 +1,126 @@ +/* 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.gui.utilities; + +import java.awt.*; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.function.Consumer; +import java.util.function.Function; +import javax.swing.*; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Simple and generic input form dialog. Supports {@link JTextField} and {@link JTextArea} as + * fields. + * + * @author Arne Keller + */ +public class FormDialog extends JDialog { + private static final Logger LOGGER = LoggerFactory.getLogger(FormDialog.class); + + /** + * Construct and show a new form. + * + * @param owner parent dialog + * @param title title of the form + * @param comps components of the dialog: (name, input element) + * @param validate validation function (return a non-null string if there is an error) + * @param onSubmit callback for submit action + * @param onCancel callback for cancel action + */ + public FormDialog(JDialog owner, String title, List comps, + Function, String> validate, + Consumer> onSubmit, Runnable onCancel) { + super(owner); + + setTitle(title); + setModal(true); + setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE); + + JPanel mainPane = new JPanel(); + mainPane.setLayout(new GridBagLayout()); + + var c = new GridBagConstraints(); + c.insets.bottom = 10; + c.insets.top = 10; + c.insets.left = 10; + c.insets.right = 10; + c.gridy = 1; + c.anchor = GridBagConstraints.WEST; + + for (var comp : comps) { + c.gridx = 1; + mainPane.add(new JLabel(comp.name), c.clone()); + c.gridx = 2; + c.fill = GridBagConstraints.HORIZONTAL; + mainPane.add(comp.element, c.clone()); + + c.gridy++; + } + + var submit = new JButton("Submit"); + submit.addActionListener(e -> { + try { + Map data = new HashMap<>(); + for (var comp : comps) { + data.put(comp.name, extractValue(comp.element)); + } + var error = validate.apply(data); + if (error != null) { + JOptionPane.showMessageDialog(this, error, "Validation error", + JOptionPane.ERROR_MESSAGE); + return; + } + onSubmit.accept(data); + dispose(); + } catch (Exception err) { + LOGGER.error("submit action failed ", err); + } + }); + + var cancel = new JButton("Cancel"); + cancel.addActionListener(e -> { + onCancel.run(); + dispose(); + }); + + JPanel buttonPane = new JPanel(); + buttonPane.setLayout(new FlowLayout(FlowLayout.RIGHT, 5, 5)); + buttonPane.add(submit); + buttonPane.add(cancel); + + c.gridx = 2; + c.insets = new Insets(5, 5, 5, 5); + mainPane.add(buttonPane, c); + + setContentPane(mainPane); + pack(); + setLocationRelativeTo(owner); + setVisible(true); + } + + /** + * An input element with a name to show in the form dialog. + * The element has to be a {@link JTextArea} or {@link JTextField}! + * + * @param name the name + * @param element the element + */ + public record NamedInputElement(String name, JComponent element) { + } + + private static String extractValue(JComponent comp) { + if (comp instanceof JTextArea textArea) { + return textArea.getText(); + } else if (comp instanceof JTextField textField) { + return textField.getText(); + } else { + throw new IllegalStateException("FormDialog used with incorrect component"); + } + } +} diff --git a/key.util/src/main/java/org/key_project/util/collection/Pair.java b/key.util/src/main/java/de/uka/ilkd/key/util/Pair.java similarity index 85% rename from key.util/src/main/java/org/key_project/util/collection/Pair.java rename to key.util/src/main/java/de/uka/ilkd/key/util/Pair.java index 56cb9295521..6357f3a6233 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Pair.java +++ b/key.util/src/main/java/de/uka/ilkd/key/util/Pair.java @@ -14,7 +14,7 @@ * @param type of first element * @param type of second element */ -public class Pair { +public class Pair implements Comparable> { /** * First element. */ @@ -97,4 +97,18 @@ public static Set getSecondSet(Collection> pairs) { } return res; } + + @Override + public int compareTo(Pair other) { + if (this == other) { + return 0; + } + var a = (Comparable) this.first; + var b = (Comparable) this.second; + var value = a.compareTo(other.first); + if (value != 0) { + return value; + } + return b.compareTo(other.second); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java b/key.util/src/main/java/de/uka/ilkd/key/util/Quadruple.java similarity index 100% rename from key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java rename to key.util/src/main/java/de/uka/ilkd/key/util/Quadruple.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/Triple.java b/key.util/src/main/java/de/uka/ilkd/key/util/Triple.java similarity index 100% rename from key.core/src/main/java/de/uka/ilkd/key/util/Triple.java rename to key.util/src/main/java/de/uka/ilkd/key/util/Triple.java diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java b/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java index aeecc7916dc..76f54f48108 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java @@ -9,33 +9,33 @@ * * @author Arne Keller */ -public class DefaultEdge implements GraphEdge { +public class DefaultEdge implements GraphEdge { /** * Source node of this edge. */ - private Object source; + private V source; /** * Target node of this edge. */ - private Object target; + private V target; @Override - public Object getSource() { + public V getSource() { return source; } @Override - public void setSource(Object source) { + public void setSource(V source) { this.source = source; } @Override - public Object getTarget() { + public V getTarget() { return target; } @Override - public void setTarget(Object target) { + public void setTarget(V target) { this.target = target; } } diff --git a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java index 3f48bef5442..306d5c2e629 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java +++ b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java @@ -17,7 +17,7 @@ * @param edge type * @author Arne Keller */ -public class DirectedGraph implements Graph { +public class DirectedGraph> implements Graph { /** * Set of vertices in this graph. */ @@ -130,4 +130,21 @@ public void removeEdge(E e) { incomingEdges.get(e.getTarget()).remove(e); edges.remove(e); } + + /** + * Create a copy of this graph. A new set of vertices and edges is created, + * but the vertex and edge objects are shared. + * + * @return copy of this graph + */ + public DirectedGraph copy() { + DirectedGraph graph = new DirectedGraph<>(); + for (V v : vertices) { + graph.addVertex(v); + } + for (E e : edges) { + graph.addEdge((V) e.getSource(), (V) e.getTarget(), e); + } + return graph; + } } diff --git a/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java b/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java index 55f8ed3268f..72e7358aa00 100644 --- a/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java +++ b/key.util/src/main/java/org/key_project/util/collection/GraphEdge.java @@ -8,28 +8,28 @@ * * @author Arne Keller */ -public interface GraphEdge { +public interface GraphEdge { /** * @return where this edge starts */ - Object getSource(); + V getSource(); /** * @return where this edge goes to */ - Object getTarget(); + V getTarget(); /** * Specify the source of this edge. * * @param source source node */ - void setSource(Object source); + void setSource(V source); /** * Specify the target of this edge. * * @param target target node */ - void setTarget(Object target); + void setTarget(V target); } diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index 6fd1ec96f77..9a5207ee93a 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -15,7 +15,8 @@ /** * List interface to be implemented by non-destructive lists */ -public interface ImmutableList extends Iterable, java.io.Serializable { +public interface ImmutableList + extends Iterable, java.io.Serializable, Comparable> { /** * Returns a Collector that accumulates the input elements into a new ImmutableList. @@ -355,8 +356,43 @@ default T last() { return remainder.head(); } + @Override + default int compareTo(ImmutableList other) { + if (this.isEmpty() && other.isEmpty()) { + return 0; + } else if (this.isEmpty()) { + return -1; + } else if (other.isEmpty()) { + return 1; + } else if (this.head().getClass() != other.head().getClass()) { + throw new IllegalStateException( + "tried to compare lists with elements of different classes"); + } else if (!(this.head() instanceof Comparable)) { + throw new IllegalStateException("tried to compare list with incomparable elements"); + } else { + var l1 = this; + var l2 = other; + while (true) { + if (l1.isEmpty()) { + return -1; + } else if (l2.isEmpty()) { + return 1; + } + var a = (Comparable) l1.head(); + var b = (T) l2.head(); + var value = a.compareTo(b); + if (value != 0) { + return value; + } + l1 = l1.tail(); + l2 = l2.tail(); + } + } + } + /** * Get the n-th element of this list. + * Time complexity: Θ(n). * * @param idx the 0-based index of the element * @return the element at index idx. @@ -366,5 +402,4 @@ default T last() { default T get(int idx) { return take(idx).head(); } - } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java index 539693f3e25..9188bab22d6 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyNodeData.java @@ -40,7 +40,7 @@ public class DependencyNodeData { public DependencyNodeData(List> inputs, List outputs, String label) { this.inputs = Collections.unmodifiableList(inputs); - this.outputs = Collections.unmodifiableList(outputs); + this.outputs = outputs; this.label = label; } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index 1e629f71944..1f78a2580e6 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -11,10 +11,13 @@ import java.util.WeakHashMap; import java.util.stream.Stream; +import de.uka.ilkd.key.logic.OpCollector; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.PosInTerm; import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.proof.BranchLocation; +import de.uka.ilkd.key.proof.FunctionTracker; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -32,7 +35,9 @@ import de.uka.ilkd.key.rule.RuleAppUtil; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.rule.inst.InstantiationEntry; +import org.key_project.logic.op.Function; import org.key_project.slicing.analysis.AnalysisResults; import org.key_project.slicing.analysis.DependencyAnalyzer; import org.key_project.slicing.graph.AddedRule; @@ -170,6 +175,39 @@ private List> inputsOfNode(Node n, Set } } + // determine for each instantiated schema variable which node first introduced that variable + if (ruleApp instanceof TacletApp t) { + var it = t.instantiations().pairIterator(); + while (it.hasNext()) { + var x = it.next(); + InstantiationEntry y = x.value(); + Object z = y.getInstantiation(); + if (z instanceof Term term) { + z = term.op(); + } + if (z instanceof Function finalZ) { + // skip if z is contained in any of the other inputs + if (input.stream().anyMatch(form -> { + var graphNode = form.first; + if (graphNode instanceof TrackedFormula tf) { + OpCollector op = new OpCollector(); + tf.formula.formula().execPreOrder(op); + return op.contains(finalZ); + } + return false; + })) { + continue; + } + + var a = FunctionTracker.getIntroducedBy(((Function) z)); + if (a != null && a != n) { + input.add(new Pair<>( + graph.getFunctionNode(finalZ, a.getBranchLocation()), false)); + } + } + } + } + return input; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java new file mode 100644 index 00000000000..c9736169979 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroup.java @@ -0,0 +1,114 @@ +/* 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 org.key_project.slicing; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.List; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.PosRuleApp; +import de.uka.ilkd.key.rule.Rule; +import de.uka.ilkd.key.rule.RuleApp; +import de.uka.ilkd.key.rule.Taclet; + +import org.key_project.slicing.graph.DependencyGraph; + +/** + * Proof step regrouping functionality. + * + * @author Arne Keller + */ +public final class ProofRegroup { + private ProofRegroup() { + + } + + public static void regroupProof(Proof proof, DependencyGraph graph) { + /* + * alpha, delta + * negationNormalForm, conjNormalForm + * polySimp_*, inEqSimp_*, simplify_literals + * + * simplify_enlarging, simplify, simplify_select + */ + var groups = ProofRegroupSettingsProvider.getSettings().getGroups(); + Deque q = new ArrayDeque<>(); + q.add(proof.root()); + while (!q.isEmpty()) { + Node n = q.pop(); + if (n.childrenCount() == 0) { + continue; + } + RuleApp r = n.getAppliedRuleApp(); + if (r == null) { + continue; + } + Rule rule = r.rule(); + if (rule instanceof Taclet taclet) { + var ruleSets = taclet.getRuleSets(); + String matchingGroup = null; + for (var name : ruleSets) { + for (String i : groups.keySet()) { + if (groups.get(i).contains(name.toString())) { + matchingGroup = i; + break; + } + } + } + if (matchingGroup != null) { + List group = new ArrayList<>(); + group.add(n); + while (true) { + if (n.childrenCount() != 1) { + break; + } + var n2 = n.child(0); + var r2 = n2.getAppliedRuleApp(); + var rule2 = r2.rule(); + if (r2 instanceof PosRuleApp p2 && rule2 instanceof Taclet) { + var graphNode = graph.getGraphNode(proof, n2.getBranchLocation(), + p2.posInOccurrence()); + Node finalN = n; + if (graph.edgesProducing(graphNode) + .noneMatch(a -> a.getProofStep() == finalN)) { + break; + } + var ruleSets2 = ((Taclet) rule2).getRuleSets(); + var found = false; + for (var name : ruleSets2) { + if (groups.get(matchingGroup).contains(name.toString())) { + found = true; + break; + } + } + if (!found) { + break; + } + group.add(n2); + n = n2; + } else { + break; + } + } + if (group.size() > 1) { + group.get(0).setGroup(group); + group.get(0).setExtraNodeLabel(matchingGroup); + for (int i = 1; i < group.size(); i++) { + group.get(i).setHideInProofTree(true); + } + } + } + } + for (int i = 0; i < n.childrenCount(); i++) { + q.add(n.child(i)); + } + } + // make sure the changed structure is visible + MainWindow.getInstance().getProofTreeView().getDelegateModel().updateTree(null); + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java new file mode 100644 index 00000000000..50eb418fbf9 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettings.java @@ -0,0 +1,100 @@ +/* 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 org.key_project.slicing; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; +import de.uka.ilkd.key.settings.Configuration; + +public class ProofRegroupSettings extends AbstractPropertiesSettings { + private static final String CATEGORY = "ProofRegrouping"; + private static final List DEFAULT_GROUPS = List.of("Propositional expansion", + "Negation/conjunctive normal form", "Polynomial/inequation normal form", "Simplification"); + + private final List> groups = new ArrayList<>(); + + public ProofRegroupSettings() { + super(CATEGORY); + } + + @Override + public void readSettings(Configuration configuration) { + var cat = configuration.getSection(category); + if (cat != null) { + for (var entry : cat.getEntries()) { + var groupName = entry.getKey(); + var v = entry.getValue(); + var prop = createStringProperty(groupName, ""); + prop.set((String) v); + groups.add(prop); + } + } + if (groups.isEmpty()) { + addGroup(DEFAULT_GROUPS.get(0), List.of("alpha", "delta")); + addGroup(DEFAULT_GROUPS.get(1), + List.of("negationNormalForm", "conjNormalForm")); + addGroup(DEFAULT_GROUPS.get(2), + List.of("polySimp_expand", "polySimp_normalise", "polySimp_newSym", + "polySimp_pullOutGcd", "polySimp_applyEq", "polySimp_applyEqRigid", + "polySimp_directEquations", "polySimp_applyEqPseudo", + "inEqSimp_forNormalisation", "inEqSimp_directInEquations", + "inEqSimp_propagation", + "inEqSimp_nonLin", "inEqSimp_signCases", + "inEqSimp_expand", "inEqSimp_saturate", + "inEqSimp_pullOutGcd", "inEqSimp_special_nonLin", + "simplify_literals")); + addGroup(DEFAULT_GROUPS.get(3), + List.of("simplify", "simplify_select", "simplify_enlarging")); + } + } + + public void addGroup(String name, List ruleSets) { + groups.add(createStringProperty(name, String.join(",", ruleSets))); + } + + public void updateGroup(String name, List ruleSets) { + for (var prop : groups) { + if (prop.getKey().equals(name)) { + prop.set(String.join(",", ruleSets)); + } + } + } + + public Map> getGroups() { + Map> m = new HashMap<>(); + for (var pe : groups) { + var name = pe.getKey(); + m.put(name, List.of(pe.get().split(","))); + } + return m; + } + + public Map> getUserGroups() { + Map> m = new HashMap<>(); + for (var pe : groups) { + var name = pe.getKey(); + if (DEFAULT_GROUPS.contains(name)) { + continue; + } + m.put(name, List.of(pe.get().split(","))); + } + return m; + } + + public void removeGroup(String name) { + PropertyEntry toRemove = null; + for (var pe : groups) { + if (pe.getKey().equals(name)) { + toRemove = pe; + break; + } + } + groups.remove(toRemove); + propertyEntries.remove(toRemove); + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java new file mode 100644 index 00000000000..3209c2a98ca --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofRegroupSettingsProvider.java @@ -0,0 +1,168 @@ +/* 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 org.key_project.slicing; + + +import java.util.ArrayList; +import java.util.List; +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.settings.SettingsPanel; +import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.gui.utilities.FormDialog; +import de.uka.ilkd.key.settings.ProofIndependentSettings; + +import org.key_project.util.collection.Pair; + +import net.miginfocom.layout.CC; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Settings for the proof slicing extension. + * + * @author Arne Keller + */ +public class ProofRegroupSettingsProvider extends SettingsPanel implements SettingsProvider { + private static final Logger LOGGER = + LoggerFactory.getLogger(ProofRegroupSettingsProvider.class); + + /** + * Singleton instance of the settings. + */ + private static final ProofRegroupSettings SETTINGS = new ProofRegroupSettings(); + + /** + * Text for introductory explanation + */ + private static final String INTRO_LABEL = "Adjust heuristics groups here."; + + /** + * The configured groups: name -> text area with heuristic names. + */ + private final List> groups = new ArrayList<>(); + + /** + * Construct a new settings provider. + */ + public ProofRegroupSettingsProvider() { + setHeaderText("Proof Regrouping Options"); + } + + @Override + public String getDescription() { + return "Proof Regrouping"; + } + + /** + * @return the settings managed by this provider + */ + public static ProofRegroupSettings getSettings() { + ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(SETTINGS); + return SETTINGS; + } + + @Override + public JPanel getPanel(MainWindow window) { + return getPanel(window, null); + } + + @Override + public JPanel getPanel(MainWindow window, JDialog dialog) { + ProofRegroupSettings ss = getSettings(); + + pCenter.removeAll(); + pCenter.add(new JLabel(INTRO_LABEL), new CC().span().alignX("left")); + + for (var e : ss.getGroups().entrySet()) { + var ta = + addTextArea(e.getKey(), String.join("\n", e.getValue()), null, emptyValidator()); + groups.add(new Pair<>(e.getKey(), ta)); + } + + setupAddAndRemoveButtons(dialog, ss); + + return this; + } + + private void setupAddAndRemoveButtons(JDialog dialog, ProofRegroupSettings ss) { + // remove any previously added buttons + for (int i = 0; i < pCenter.getComponentCount(); i++) { + if (pCenter.getComponent(i) instanceof JButton) { + pCenter.remove(i); + i--; + } + } + + var addNew = new JButton("Add new group"); + addNew.addActionListener(e -> { + try { + new FormDialog(dialog, "Add new group", + List.of(new FormDialog.NamedInputElement("Name", new JTextField()), + new FormDialog.NamedInputElement("Heuristics", new JTextArea())), + data -> { + var name = data.get("Name"); + if (ss.getGroups().containsKey(name)) { + return "Group name already in use!"; + } + return null; + }, + data -> { + var name = data.get("Name"); + var content = data.get("Heuristics"); + var ta = + addTextArea(name, "", null, emptyValidator()); + ta.setText(content); + groups.add(new Pair<>(name, ta)); + ss.addGroup(name, List.of(ta.getText().split("\n"))); + + setupAddAndRemoveButtons(dialog, ss); + dialog.validate(); + dialog.repaint(); + }, () -> { + // ignore cancel + }); + } catch (Exception err) { + err.printStackTrace(); + } + }); + pCenter.add(addNew, "wrap"); + for (var group : ss.getUserGroups().keySet()) { + var remove = new JButton("Remove " + group); + remove.addActionListener(e -> { + try { + ss.removeGroup(group); + for (var groupPair : groups) { + if (groupPair.first.equals(group)) { + removeTitledComponent(groupPair.first); + groups.remove(groupPair); + setupAddAndRemoveButtons(dialog, ss); + dialog.validate(); + dialog.repaint(); + break; + } + } + } catch (Exception error) { + LOGGER.error("failed to remove group", error); + } + }); + pCenter.add(remove, "wrap"); + } + } + + @Override + public void applySettings(MainWindow window) { + ProofRegroupSettings ss = getSettings(); + for (Pair ta : groups) { + ss.updateGroup(ta.first, List.of(ta.second.getText().split("\n"))); + } + } + + + @Override + public int getPriorityOfSettings() { + return 10000; + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java new file mode 100644 index 00000000000..2bc52cda589 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ProofReorder.java @@ -0,0 +1,188 @@ +/* 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 org.key_project.slicing; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.*; +import java.util.stream.Collectors; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.PosInTerm; +import de.uka.ilkd.key.proof.BranchLocation; +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.io.*; + +import org.key_project.slicing.graph.AnnotatedEdge; +import org.key_project.slicing.graph.DependencyGraph; +import org.key_project.slicing.graph.GraphNode; +import org.key_project.slicing.graph.PseudoInput; + +/** + * Proof reordering functionality. + * + * @author Arne Keller + */ +public final class ProofReorder { + private ProofReorder() { + + } + + public static void reorderProof(Proof proof, DependencyGraph depGraph) + throws IOException, ProofInputException, ProblemLoaderException, + IntermediateProofReplayer.BuiltInConstructionException { + depGraph.ensureProofIsTracked(proof); + MainWindow.getInstance().getMediator().stopInterface(true); + + SortedMap> steps = new TreeMap<>(); + + Set done = new HashSet<>(); + + Deque todo = new ArrayDeque<>(); + todo.add(new BranchTodo(BranchLocation.ROOT, proof.root())); + while (!todo.isEmpty()) { + var t = todo.pop(); + var loc = t.location; + var root = t.rootNode; + if (done.contains(loc)) { + continue; + } + done.add(loc); + System.out.println("doing branch " + loc); + + // q: the list of dependency graph nodes "currently available" for proof steps + Deque q = new ArrayDeque<>(); + for (int i = 1; i <= root.sequent().size(); i++) { + var node = depGraph.getGraphNode(proof, loc, + PosInOccurrence.findInSequent(root.sequent(), i, PosInTerm.getTopLevel())); + q.addLast(node); + } + List newOrder = new ArrayList<>(); + Set newOrderSorted = new HashSet<>(); + + // First, get all nodes that do not directly connect to the dependency graph of the + // previous branch. These are taclets that do not have any formulas as direct inputs, + // e.g. sign_case_distinction. + // However, if one of these nodes splits the proof, it will be done last. + Node finalNode = null; + Node toCheck = root; + while (toCheck.getBranchLocation() == loc) { + DependencyNodeData data = toCheck.lookup(DependencyNodeData.class); + if (data == null) { + break; // closed goal + } + if (data.inputs.size() == 1 && data.inputs.get(0).first instanceof PseudoInput) { + if (toCheck.childrenCount() > 1) { + finalNode = toCheck; + break; + } + // Do this one first. + newOrder.add(toCheck); + } + toCheck = toCheck.child(0); + } + + while (!q.isEmpty()) { + var nextNode = q.pop(); + depGraph.outgoingEdgesOf(nextNode).forEach(node -> { + var newLoc = node.getBranchLocation(); + if (!newLoc.equals(loc)) { + /* + * if (!todo.containsKey(newLoc) && !done.contains(newLoc)) { + * System.out.println("adding branch " + newLoc); + * todo.put(newLoc, node.getFirstInBranch()); + * } + */ + return; + } + + if (newOrderSorted.contains(node)) { + return; + } + // check that all inputs are available + if (!depGraph.inputsOf(node) + .allMatch(otherNode -> depGraph.edgesProducing(otherNode) + .allMatch(edge -> newOrderSorted.contains(edge.getProofStep()) + || !edge.getProofStep().getBranchLocation() + .equals(loc)))) { + q.addLast(nextNode); + return; + } + // check that all consumed inputs were already used by all other steps + if (!depGraph.inputsConsumedBy(node) + .allMatch( + input -> depGraph.edgesUsing(input).map(AnnotatedEdge::getProofStep) + .allMatch(x -> node == x || newOrderSorted.contains(x) + || !x.getBranchLocation().equals(loc)))) { + q.addLast(nextNode); + return; + } + newOrder.add(node); + newOrderSorted.add(node); + + var outputs = depGraph.outputsOf(node).collect(Collectors.toList()); + Collections.reverse(outputs); + outputs.forEach(q::addFirst); + }); + } + // add the next branches to the queue + for (int i = 0; i < newOrder.size(); i++) { + if (newOrder.get(i).childrenCount() != 1 + || newOrder.get(i).child(0).childrenCount() == 0) { + var last = newOrder.remove(i); + var c = last.childrenCount(); + c--; + while (c >= 0) { + todo.addFirst( + new BranchTodo(last.child(c).getBranchLocation(), last.child(c))); + c--; + } + newOrder.add(last); + break; + } + } + if (finalNode != null) { + newOrder.add(finalNode); + } + steps.put(loc, newOrder); + } + + ProblemLoaderControl control = new DefaultUserInterfaceControl(); + Path tmpFile = Files.createTempFile("proof", ".proof"); + ProofSaver.saveProofObligationToFile(tmpFile.toFile(), proof); + + String bootClassPath = proof.getEnv().getJavaModel().getBootClassPath(); + AbstractProblemLoader problemLoader = new SingleThreadProblemLoader( + tmpFile.toFile(), + proof.getEnv().getJavaModel().getClassPathEntries(), + bootClassPath != null ? new File(bootClassPath) : null, + null, + proof.getEnv().getInitConfigForEnvironment().getProfile(), + false, + control, false, null); + problemLoader.load(); + // Files.delete(tmpFile); + Proof newProof = problemLoader.getProof(); + new ReorderingReplayer(proof, newProof, steps).copy(); + ProofSaver.saveToFile(tmpFile.toFile(), newProof); + KeYMediator mediator = MainWindow.getInstance().getMediator(); + mediator.startInterface(true); + + ProblemLoader problemLoader2 = + mediator.getUI().getProblemLoader(tmpFile.toFile(), null, null, null, mediator); + // user already knows about any warnings + problemLoader2.setIgnoreWarnings(true); + problemLoader2.runAsynchronously(); + } + + private record BranchTodo(BranchLocation location, Node rootNode) { + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java new file mode 100644 index 00000000000..bfa1e8a4cab --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/RegroupExtension.java @@ -0,0 +1,155 @@ +/* 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 org.key_project.slicing; + +import java.util.ArrayList; +import java.util.List; +import javax.swing.*; + +import de.uka.ilkd.key.control.InteractionListener; +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.IssueDialog; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.macros.ProofMacro; +import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; +import de.uka.ilkd.key.rule.BuiltInRule; +import de.uka.ilkd.key.rule.IBuiltInRuleApp; +import de.uka.ilkd.key.rule.RuleApp; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Proof regrouping and reordering extension. + * + * @author Arne Keller + */ +@KeYGuiExtension.Info(name = "Reordering and regrouping", + description = "Author: Arne Keller ", + experimental = false, + optional = true, + priority = 9001) +public class RegroupExtension implements KeYGuiExtension, + KeYGuiExtension.Startup, KeYGuiExtension.Settings, + KeYGuiExtension.Toolbar, InteractionListener { + private static final Logger LOGGER = LoggerFactory.getLogger(RegroupExtension.class); + + @Override + public JToolBar getToolbar(MainWindow mainWindow) { + JToolBar bar = new JToolBar(); + JButton b = new JButton(); + b.setText("Reorder"); + b.addActionListener(e -> { + KeYMediator m = MainWindow.getInstance().getMediator(); + Proof p = m.getSelectedProof(); + if (!p.closed()) { + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Cannot reorder incomplete proof", "Error", JOptionPane.ERROR_MESSAGE); + return; + } + try { + var depTracker = m.getSelectedProof().lookup(DependencyTracker.class); + if (depTracker == null) { + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Cannot reorder proof without dependency tracker", "Error", + JOptionPane.ERROR_MESSAGE); + return; + } + var depGraph = depTracker.getDependencyGraph(); + ProofReorder.reorderProof(m.getSelectedProof(), depGraph); + } catch (Exception exc) { + LOGGER.error("failed to reorder proof ", exc); + MainWindow.getInstance().getMediator().startInterface(true); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); + } + }); + bar.add(b); + JButton b2 = new JButton(); + b2.setText("Regroup"); + b2.addActionListener(e -> { + KeYMediator m = MainWindow.getInstance().getMediator(); + try { + var depTracker = m.getSelectedProof().lookup(DependencyTracker.class); + if (depTracker == null) { + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Cannot regroup proof without dependency tracker", "Error", + JOptionPane.ERROR_MESSAGE); + return; + } + var depGraph = depTracker.getDependencyGraph(); + ProofRegroup.regroupProof(m.getSelectedProof(), depGraph); + } catch (Exception exc) { + LOGGER.error("", exc); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); + } + }); + bar.add(b2); + return bar; + } + + @Override + public SettingsProvider getSettings() { + return new ProofRegroupSettingsProvider(); + } + + @Override + public void init(MainWindow window, KeYMediator mediator) { + mediator.getUI().getProofControl().addInteractionListener(this); + } + + @Override + public void runPrune(Node node) { + if (node.isHideInProofTree()) { + // Perhaps there are some nodes below the prune target in this group. + // These should be removed from the proof tree view. + var groupNode = node.parent(); + while (groupNode.getGroup() == null) { + var prev = groupNode; + groupNode = groupNode.parent(); + // robustness: no infinite loop + // (should never happen anyhow) + if (prev == groupNode) { + return; + } + } + var groupNodes = groupNode.getGroup(); + var removedAfter = groupNodes.indexOf(node); + groupNode.setGroup(new ArrayList<>(groupNodes.subList(0, removedAfter + 1))); + } + } + + @Override + public void settingChanged(Proof proof, de.uka.ilkd.key.settings.Settings settings, + SettingType type, String message) { + + } + + @Override + public void runMacro(Node node, ProofMacro macro, PosInOccurrence posInOcc, + ProofMacroFinishedInfo info) { + + } + + @Override + public void runBuiltInRule(Node node, IBuiltInRuleApp app, BuiltInRule rule, + PosInOccurrence pos, boolean forced) { + + } + + @Override + public void runAutoMode(List initialGoals, Proof proof, ApplyStrategyInfo info) { + + } + + @Override + public void runRule(Node goal, RuleApp app) { + + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java new file mode 100644 index 00000000000..fc0a0cbd1e4 --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ReorderingReplayer.java @@ -0,0 +1,64 @@ +/* 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 org.key_project.slicing; + +import java.util.*; + +import de.uka.ilkd.key.proof.BranchLocation; +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.io.*; +import de.uka.ilkd.key.proof.replay.AbstractProofReplayer; +import de.uka.ilkd.key.rule.OneStepSimplifier; + +import org.key_project.util.collection.ImmutableList; + +/** + * Replayer that will reorder a proof based on the provided sorting of the steps. + * + * @author Arne Keller + */ +public class ReorderingReplayer extends AbstractProofReplayer { + + private final SortedMap> steps; + + public ReorderingReplayer(Proof originalProof, Proof proof, + SortedMap> steps) { + super(originalProof, proof); + this.steps = steps; + } + + public void copy() + throws IntermediateProofReplayer.BuiltInConstructionException { + OneStepSimplifier.refreshOSS(proof); + Deque nodeQueue = new ArrayDeque<>(); + Deque queue = new ArrayDeque<>(); + queue.add(proof.getOpenGoal(proof.root())); + + for (Map.Entry> e : steps.entrySet()) { + nodeQueue.addAll(e.getValue()); + } + + while (!nodeQueue.isEmpty() && !queue.isEmpty()) { + Node nextNode = nodeQueue.pop(); + Goal nextGoal = queue.pop(); + // skip nextNode if it is a closed goal + if (nextNode.getAppliedRuleApp() == null) { + continue; + } + proof.getServices().getNameRecorder().setProposals( + nextNode.getNameRecorder().getProposals()); + ImmutableList newGoals = reApplyRuleApp(nextNode, nextGoal); + List sortedGoals = newGoals.toList(); + Collections.reverse(sortedGoals); + for (Goal g : newGoals) { + if (g.node().isClosed()) { + continue; + } + queue.addFirst(g); + } + } + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 13b32c6c07f..c81a6dd3e51 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -115,7 +115,7 @@ public List getContextActions(@NonNull KeYMediator mediator, } @Override - public void selectedProofChanged(KeYSelectionEvent e) { + public void selectedProofChanged(KeYSelectionEvent e) { createTrackerForProof(e.getSource().getSelectedProof()); } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java index 0b1b1f08388..25fad7413b3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java @@ -12,7 +12,7 @@ * * @author Arne Keller */ -public class AnnotatedEdge extends DefaultEdge { +public class AnnotatedEdge extends DefaultEdge { /** * The node that added this edge to the dependency graph. */ diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 02f109322a2..a884a6f6bc1 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -9,13 +9,16 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.proof.BranchLocation; +import de.uka.ilkd.key.proof.FunctionTracker; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.util.Triple; +import org.key_project.logic.op.Function; import org.key_project.slicing.DependencyNodeData; import org.key_project.slicing.DependencyTracker; import org.key_project.util.EqualsModProofIrrelevancy; +import org.key_project.util.collection.DirectedGraph; import org.key_project.util.collection.Pair; import org.slf4j.Logger; @@ -48,6 +51,9 @@ public class DependencyGraph { */ private final Map> edgeDataReversed = new IdentityHashMap<>(); + /** + * Create a new empty dependency graph. + */ public DependencyGraph() { graph = new EquivalenceDirectedGraph(); } @@ -364,6 +370,52 @@ public GraphNode getGraphNode(Proof proof, BranchLocation locationGuess, PosInOc return null; } + /** + * Get the graph node for a given function and branch location. + * If the function is not registered in the graph yet, a new graph node is created. + * The function has to be a skolem constant! + * + * @param function function + * @param loc branch location + * @return graph node representing the function + */ + public TrackedFunction getFunctionNode(Function function, BranchLocation loc) { + TrackedFunction candidate = new TrackedFunction(function, loc); + if (graph.containsVertex(candidate)) { + return candidate; + } + graph.addVertex(candidate); + var edges = edgeDataReversed.get(FunctionTracker.getIntroducedBy(function)); + var sourcesDone = new HashSet<>(); + Collection newEdges = new ArrayList<>(); + for (var x : edges) { + GraphNode g = x.getSource(); + if (sourcesDone.contains(g)) { + continue; + } + sourcesDone.add(g); + AnnotatedEdge e = new AnnotatedEdge(FunctionTracker.getIntroducedBy(function), false); + graph.addEdge(g, candidate, e); + newEdges.add(e); + } + edgeDataReversed.get(FunctionTracker.getIntroducedBy(function)).addAll(newEdges); + DependencyNodeData n = + FunctionTracker.getIntroducedBy(function).lookup(DependencyNodeData.class); + if (n != null) { + n.outputs.add(candidate); + } + return candidate; + } + + /** + * Get a copy of the internal graph. + * + * @return internal graph data + */ + public DirectedGraph getInternalGraph() { + return graph.copy(); + } + /** * Remove all nodes B with degree 2: * A → B → C diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java index f7e6e99fc18..3867fdf19fe 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java @@ -17,6 +17,7 @@ import org.key_project.slicing.DependencyNodeData; import org.key_project.slicing.analysis.AnalysisResults; +import org.key_project.util.collection.DirectedGraph; import org.key_project.util.collection.Pair; /** @@ -36,6 +37,51 @@ public final class DotExporter { private DotExporter() { } + /** + * Convert the given dependency graph into a text representation (DOT format). + * If analysis results are given, useless nodes and edges are marked in red. + * If abbreviateFormulas is true, node labels are shortened. + * + * @param graph dependency graph to show + * @return string representing the dependency graph + */ + public static String exportDot2(DirectedGraph graph) { + StringBuilder buf = new StringBuilder(); + buf.append("digraph {\n"); + // expected direction in output rendering is reverse internal order + buf.append("edge [dir=\"back\"];\n"); + + for (AnnotatedEdge in : graph.edgeSet()) { + var src = in.getSource(); + var dst = in.getTarget(); + String inString = src.toString(false, false); + String outString = dst.toString(false, false); + var label = in.getProofStep().lookup(DependencyNodeData.class).label; + buf + .append('"') + .append(inString) + .append("\" -> \"") + .append(outString) + .append("\" [label=\"") + .append(label) + .append("\"]\n"); + // make sure the formulas are drawn with the correct shape + String shape = SHAPES.get(src.getClass()); + if (shape != null) { + buf.append('"').append(inString).append("\" [shape=\"").append(shape) + .append("\"]\n"); + } + shape = SHAPES.get(dst.getClass()); + if (shape != null) { + buf.append('"').append(outString).append("\" [shape=\"").append(shape) + .append("\"]\n"); + } + } + + buf.append('}'); + return buf.toString(); + } + /** * Convert the given dependency graph into a text representation (DOT format). * If analysis results are given, useless nodes and edges are marked in red. diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java new file mode 100644 index 00000000000..2cfaadc34ec --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFunction.java @@ -0,0 +1,58 @@ +/* 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 org.key_project.slicing.graph; + +import java.util.Objects; + +import de.uka.ilkd.key.proof.BranchLocation; + +import org.key_project.logic.op.Function; + +/** + * A skolem constant tracked in the dependency graph. + * + * @author Arne Keller + */ +public class TrackedFunction extends GraphNode { + private final Function function; + + public TrackedFunction(Function f, BranchLocation loc) { + super(loc); + + this.function = f; + } + + @Override + public GraphNode popLastBranchID() { + return new TrackedFunction(function, getBranchLocation().removeLast()); + } + + @Override + public String toString(boolean abbreviated, boolean omitBranch) { + return "variable " + function.toString(); + } + + public Function getFunction() { + return function; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + + TrackedFunction that = (TrackedFunction) o; + + return Objects.equals(function, that.function); + } + + @Override + public int hashCode() { + return function != null ? function.hashCode() : 0; + } +} diff --git a/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension index 154d90dcbdf..49e7314e4b6 100644 --- a/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ b/keyext.slicing/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -1 +1,2 @@ -org.key_project.slicing.SlicingExtension \ No newline at end of file +org.key_project.slicing.SlicingExtension +org.key_project.slicing.RegroupExtension diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/FunctionTrackerTest.java b/keyext.slicing/src/test/java/org/key_project/slicing/FunctionTrackerTest.java new file mode 100644 index 00000000000..3e329adb59f --- /dev/null +++ b/keyext.slicing/src/test/java/org/key_project/slicing/FunctionTrackerTest.java @@ -0,0 +1,34 @@ +/* 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 org.key_project.slicing; + +import java.io.File; +import java.util.Collection; + +import de.uka.ilkd.key.control.KeYEnvironment; + +import org.key_project.slicing.graph.AnnotatedEdge; +import org.key_project.slicing.graph.TrackedFunction; +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +public class FunctionTrackerTest { + public static final File TEST_CASES_DIRECTORY = FindResources.getTestCasesDirectory(); + + @Test + void tracksSkolemConstantCorrectly() throws Exception { + var file = new File(TEST_CASES_DIRECTORY, "testFunctionTracker.proof"); + var env = KeYEnvironment.load(file); + var proof = env.getLoadedProof(); + var tracker = new DependencyTracker(proof); + var depGraph = tracker.getDependencyGraph(); + Collection edges = depGraph.edgesOf(proof.findAny(x -> x.serialNr() == 4)); + assertEquals(2, edges.size()); + var edge = edges.stream().findFirst().get(); + assertInstanceOf(TrackedFunction.class, edge.getSource()); + } +} diff --git a/keyext.slicing/src/test/resources/testcase/testFunctionTracker.proof b/keyext.slicing/src/test/resources/testcase/testFunctionTracker.proof new file mode 100644 index 00000000000..70ce899f1e8 --- /dev/null +++ b/keyext.slicing/src/test/resources/testcase/testFunctionTracker.proof @@ -0,0 +1,143 @@ +\profile "Java Profile"; + +\settings // Proof-Settings-Config-File +{ + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "floatRules" : "floatRules:assumeStrictfp", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "wdChecks" : "wdChecks:off", + "wdOperator" : "wdOperator:L" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "JavaCardDLStrategy", + "MaximumNumberOfAutomaticApplications" : 7000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED", + "DEP_OPTIONS_KEY" : "DEP_ON", + "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_ON", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } + } + +\functions { + int b; +} +\problem { + \exists int c; (c = Z(5(#)) & lt(c, b)) + & \exists int c; (c = Z(7(#)) & gt(c, b)) + & \exists int c; c = Z(0(#)) +-> b = Z(6(#)) +} + +\proof { +(keyLog "0" (keyUser "arne" ) (keyVersion "bd6f1082c56a8177268809c89ccd4d7a7a8628d2")) + +(autoModeTime "78") + +(branch "dummy ID" +(rule "impRight" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "exLeft" (formula "3") (inst "sk=c_0") (userinteraction)) +(rule "sign_case_distinction" (inst "signCasesLeft=c_0") (userinteraction)) +(branch "c_0 is negative" + (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "4") (userinteraction)) + (rule "leq_literals" (formula "1") (userinteraction)) + (rule "closeFalse" (formula "1") (userinteraction)) +) +(branch "c_0 is zero" + (rule "exLeft" (formula "1") (inst "sk=c_1")) + (rule "andLeft" (formula "1")) + (rule "exLeft" (formula "3") (inst "sk=c_2")) + (rule "andLeft" (formula "3")) + (rule "inEqSimp_ltToLeq" (formula "2")) + (rule "polySimp_mulComm0" (formula "2") (term "1,0,0")) + (rule "inEqSimp_gtToGeq" (formula "4")) + (rule "polySimp_mulComm0" (formula "4") (term "1,0,0")) + (rule "applyEqRigid" (formula "2") (term "1,0") (ifseqformula "1")) + (rule "polySimp_addComm1" (formula "2") (term "0")) + (rule "add_literals" (formula "2") (term "0,0")) + (rule "applyEq" (formula "4") (term "1,0") (ifseqformula "3")) + (rule "polySimp_addComm1" (formula "4") (term "0")) + (rule "add_literals" (formula "4") (term "0,0")) + (rule "inEqSimp_sepNegMonomial0" (formula "2")) + (rule "polySimp_mulLiterals" (formula "2") (term "0")) + (rule "polySimp_elimOne" (formula "2") (term "0")) + (rule "inEqSimp_sepNegMonomial1" (formula "4")) + (rule "polySimp_mulLiterals" (formula "4") (term "0")) + (rule "polySimp_elimOne" (formula "4") (term "0")) + (rule "inEqSimp_strengthen0" (formula "4") (ifseqformula "6")) + (rule "add_literals" (formula "4") (term "1")) + (rule "inEqSimp_contradEq3" (formula "6") (ifseqformula "4")) + (rule "mul_literals" (formula "6") (term "1,0,0")) + (rule "add_literals" (formula "6") (term "0,0")) + (rule "qeq_literals" (formula "6") (term "0")) + (builtin "One Step Simplification" (formula "6")) + (rule "false_right" (formula "6")) + (rule "inEqSimp_contradInEq1" (formula "4") (ifseqformula "2")) + (rule "qeq_literals" (formula "4") (term "0")) + (builtin "One Step Simplification" (formula "4")) + (rule "closeFalse" (formula "4")) +) +(branch "c_0 is positive" + (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "4") (userinteraction)) + (rule "qeq_literals" (formula "1") (userinteraction)) + (rule "closeFalse" (formula "1") (userinteraction)) +) +) +}