Skip to content

Add diff highlighting for proof step differences in the graph view#435

Open
Kitsunp wants to merge 19 commits intozxcalc:masterfrom
Kitsunp:master
Open

Add diff highlighting for proof step differences in the graph view#435
Kitsunp wants to merge 19 commits intozxcalc:masterfrom
Kitsunp:master

Conversation

@Kitsunp
Copy link

@Kitsunp Kitsunp commented Feb 17, 2026

Addresses #190
Adds visual highlighting of vertices and edges that will change between
proof steps. When navigating to a step in proof mode, elements affected
by the next rewrite are highlighted with coloured outlines and tinted
fills, making it easy to spot the difference without manual comparison.

What it does:

  • Vertices that will be removed get a crimson outline and tinted fill
  • Vertices whose type or phase will change get an orange outline and tinted fill
  • Edges that will be removed or change type are highlighted similarly
  • Only semantically meaningful changes are shown (type, phase, structural);
    cosmetic changes like repositioning are excluded to avoid visual noise

How to test:

  1. Open a proof, apply a few rewrites
  2. Click on any step that is not the last one
  3. The nodes/edges that change in the next step should be visibly highlighted
  4. Clicking the last step clears all highlights

Files changed:

  • settings.py — diff colour scheme + toggle setting
  • settings_dialog.py — checkbox for "Highlight proof step differences"
  • vitem.py — diff highlight rendering for vertices
  • eitem.py — diff highlight rendering for edges
  • graphscene.pyhighlight_diff() and clear_diff_highlights() methods
  • proof.py — calls highlighting in move_to_step()

Leverages the existing pyzx.graph.diff.GraphDiff already used in
GraphScene.update_graph(). No new dependencies. Toggleable via Settings.

@boldar99
Copy link
Collaborator

boldar99 commented Feb 17, 2026

Hi, thanks for the PR. I have started testing it, and it seems that incorrect vertices and edges are being highlighted with simple rewrites:

Screen.Recording.2026-02-17.at.15.18.56.mov

@Kitsunp
Copy link
Author

Kitsunp commented Feb 17, 2026

Thanks for catching this @boldar99! I tracked down the root cause.
The issue is that ProofModel.get_graph() uses BaseGraph.copy() to return graphs, and .copy() renumbers vertex IDs to be consecutive (its own docstring says: "The copy will have consecutive vertex indices, even if the original graph did not"). When a rewrite removes a vertex (creating a gap in the IDs, e.g. {0, 1, 3, 4}), each call to .copy() compacts them independently — so the same logical vertex ends up with different numeric IDs in each copy. Since GraphDiff compares by vertex ID, it sees almost every vertex as "changed" even though nothing actually changed.
The fix in move_to_step():

Display graph: replaced get_graph() with copy.deepcopy() which preserves the original vertex IDs exactly (consistent with how every other graph-copy in the codebase works).
Next-step graph (for diff computation): access self.model().steps[index].graph directly instead of copying — GraphDiff only reads from it, never modifies it, so no copy is needed. This also avoids any performance concern since it's zero-cost.

image image

@boldar99
Copy link
Collaborator

Thanks for the update. It seems you have accidentally run some automated formatting on the entire codebase. Please undo this.

I have done some more testing. Fusion definitely looks a lot nicer, but it is still a bit odd. In particular, when two spiders are fused, it is the nodes and the connecting edge that should be highlighted. Same when un-fusing, then the spider that is being transformed.

Screen.Recording.2026-02-18.at.14.21.56.mov

@Kitsunp
Copy link
Author

Kitsunp commented Feb 19, 2026

image image image image @boldar99

@lia-approves
Copy link
Collaborator

lia-approves commented Feb 23, 2026

Hi @Kitsunp, in addition to the request to revert all unnecessary formatting changes to unrelated files to this issue, I tested both the fusion and the "Unfuse spider" rules in your latest commit and found the highlighting to still not be as intended. As Boldi described above:

In particular, when two spiders are fused, it is the nodes and the connecting edge that should be highlighted.

and likewise for the "Unfuse spider" rule.
Let us know if you have any questions.

@Kitsunp
Copy link
Author

Kitsunp commented Feb 23, 2026

@lia-approves Currently, the latest changes are specific to the code. I did not rewrite the format. The previous formatting correction I had made was expressed so that what is currently visible refers to the current code, and I relied on mypy for some corrections, but I will also look into the mentioned issue.

@RazinShaikh
Copy link
Collaborator

Hi @Kitsunp unfortunately there are many changes not related to the issue. For you convenience, I have highlighted some of them below.

Comment on lines 1 to 3
import pytest
# import pytest
from datetime import datetime, timedelta
from unittest.mock import Mock, patch
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why are these lines commented out?

QEasingCurve(QEasingCurve.Type.OutQuad))

return anim_before, anim_after
return anim_before, anim_after No newline at end of file
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

blank line removed here

zxlive/common.py Outdated
Comment on lines 36 to 40
if _type is bool:
val = str(val) == "True" or str(val) == "true"
if _type == int:
if _type is int:
val = int(str(val))
if _type == float:
if _type is float:
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why do you change "==" to "is"?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

all the changes in this file are not related to the diff highlighting for proof steps

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

all the changes in this file are not related to the diff highlighting for proof steps

zxlive/eitem.py Outdated

if self.refresh:
self.it.refresh()
self.it.refresh() No newline at end of file
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

new line at the end of file removed

Comment on lines 234 to 254
@staticmethod
def _phases_semantically_equal(old_phase: object, new_phase: object) -> bool:
"""Check whether two phase values represent the same rotation.

``GraphDiff`` compares phases with Python's ``!=`` operator which
is sensitive to representation: ``Fraction(1, 4) != 0.25`` is
``True`` even though both encode the same angle. This helper
converts both values to ``float`` and compares with a small
tolerance so that purely representational differences (e.g.
``Fraction`` vs ``float``) do not produce false‑positive
highlights.

For symbolic phases (``Poly`` objects or other non‑numeric types)
the function falls back to exact equality, which is the correct
behaviour since we cannot numerically evaluate free variables.
"""
try:
return abs(float(old_phase) - float(new_phase)) < 1e-12 # type: ignore[arg-type]
except (TypeError, ValueError):
# Symbolic / non-numeric phases — fall back to exact equality
return old_phase == new_phase
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this is necessary and it's best handled by PyZX rather than ZXLive. In ZXLive, we do not use float angles, they are always converted to Fractions.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

all the changes in this file are not related to the diff highlighting for proof steps

@Kitsunp
Copy link
Author

Kitsunp commented Feb 26, 2026

Thanks for the feedback @RazinShaikh, @lia-approves ! I've updated the PR with the following changes:

  1. Reverted unnecessary formatting changes: Restored the original state of unrelated files (zxlive/custom_rule.py, zxlive/edit_panel.py, zxlive/rewrite_data.py, test_update_checker.py, etc.) to keep the PR focused.
  2. Fixed Fusion/Unfusion Highlighting: I updated the logic in highlight_diff (zxlive/graphscene.py) to correctly identify and highlight the structurally affected "survivor" nodes and connecting edges during both the Fusing and Unfusing spider rules. It now limits the highlight correctly without bleeding into unaffected external neighbors.

Let me know if everything looks good now!

image image image image image

@Kitsunp Kitsunp requested a review from RazinShaikh February 27, 2026 12:24
@boldar99
Copy link
Collaborator

Hi again,

Thanks for cleaning up the rest of the project.
I have tried it and fusion and un-fusion are still not as they should be. It should only highlight the two spiders that are being fused, and the connecting edges, noting else. See the video for reference.

Screen.Recording.2026-02-27.at.17.58.16.mov

@Kitsunp
Copy link
Author

Kitsunp commented Feb 28, 2026

image image image image image @boldar99

@RazinShaikh
Copy link
Collaborator

I have not had a look at the recent changes but I wanted to suggest if you could work on making it look pretty. It should have better colours and it should look good in light mode, dark mode and all the color schemes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants