add simplification routines in the proof panel

zxcalc · Nov 10, 2023 · a3d6260 · a3d6260
1 parent 5b620f8
commit a3d6260
Show file tree

Hide file tree

Showing 3 changed files with 170 additions and 70 deletions.
diff --git a/zxlive/mainwindow.py b/zxlive/mainwindow.py
@@ -171,14 +171,6 @@ def __init__(self) -> None:
 
         self._reset_menus(False)
 
-        simplify_actions = []
-        for simp in simplifications.values():
-            simplify_actions.append(self._new_action(simp["text"], self.apply_pyzx_reduction(simp), None, simp["tool_tip"]))
-        self.simplify_menu = menu.addMenu("&Simplify")
-        for action in simplify_actions:
-            self.simplify_menu.addAction(action)
-        self.simplify_menu.menuAction().setVisible(False)
-
         graph = construct_circuit()
         self.new_graph(graph)
 
@@ -260,11 +252,9 @@ def update_tab_name(self, clean:bool) -> None:
 
     def tab_changed(self, i: int) -> None:
         if isinstance(self.active_panel, ProofPanel):
-            self.simplify_menu.menuAction().setVisible(True)
             self.proof_as_rewrite_action.setEnabled(True)
         else:
             self.proof_as_rewrite_action.setEnabled(False)
-            self.simplify_menu.menuAction().setVisible(False)
         self._undo_changed()
         self._redo_changed()
 
@@ -525,56 +515,3 @@ def proof_as_lemma(self) -> None:
         rhs_graph = self.active_panel.proof_model.graphs[-1]
         rule = CustomRule(lhs_graph, rhs_graph, name, description)
         export_rule_dialog(rule, self)
-
-    def apply_pyzx_reduction(self, reduction: SimpEntry) -> Callable[[],None]:
-        def reduce() -> None:
-            assert self.active_panel is not None and isinstance(self.active_panel, ProofPanel)
-            old_graph = self.active_panel.graph
-            new_graph = copy.deepcopy(old_graph)
-            try:
-                if reduction["in_place"]:
-                    reduction["function"](new_graph)
-                else:
-                    _new_graph = reduction["function"](new_graph)
-                    assert isinstance(_new_graph, GraphT)
-                    new_graph = _new_graph
-                cmd = AddRewriteStep(self.active_panel.graph_view, new_graph, self.active_panel.step_view, reduction["text"])
-                self.active_panel.undo_stack.push(cmd)
-            except Exception as e:
-                show_error_msg("Error", str(e))
-        return reduce
-
-
-class SimpEntry(TypedDict):
-    text: str
-    tool_tip: str
-    function: Callable[[BaseGraph], int] | Callable[[BaseGraph], None] | Callable[[BaseGraph], BaseGraph]
-    in_place: bool
-
-
-def _extract_circuit(graph: BaseGraph) -> BaseGraph:
-    graph.auto_detect_io()
-    simplify.full_reduce(graph)
-    return extract_circuit(graph).to_graph()
-
-simplifications: dict[str, SimpEntry] = {
-    'bialg_simp': {"text": "bialg_simp", "tool_tip":"bialg_simp", "function": simplify.bialg_simp, "in_place": True},
-    'spider_simp': {"text": "spider_simp", "tool_tip":"spider_simp", "function": simplify.spider_simp, "in_place": True},
-    'id_simp': {"text": "id_simp", "tool_tip":"id_simp", "function": simplify.id_simp, "in_place": True},
-    'phase_free_simp': {"text": "phase_free_simp", "tool_tip":"phase_free_simp", "function": simplify.phase_free_simp, "in_place": True},
-    'pivot_simp': {"text": "pivot_simp", "tool_tip":"pivot_simp", "function": simplify.pivot_simp, "in_place": True},
-    'pivot_gadget_simp': {"text": "pivot_gadget_simp", "tool_tip":"pivot_gadget_simp", "function": simplify.pivot_gadget_simp, "in_place": True},
-    'pivot_boundary_simp': {"text": "pivot_boundary_simp", "tool_tip":"pivot_boundary_simp", "function": simplify.pivot_boundary_simp, "in_place": True},
-    'gadget_simp': {"text": "gadget_simp", "tool_tip":"gadget_simp", "function": simplify.gadget_simp, "in_place": True},
-    'lcomp_simp': {"text": "lcomp_simp", "tool_tip":"lcomp_simp", "function": simplify.lcomp_simp, "in_place": True},
-    'clifford_simp': {"text": "clifford_simp", "tool_tip":"clifford_simp", "function": simplify.clifford_simp, "in_place": True},
-    'tcount': {"text": "tcount", "tool_tip":"tcount", "function": simplify.tcount, "in_place": True},
-    'to_gh': {"text": "to_gh", "tool_tip":"to_gh", "function": simplify.to_gh, "in_place": True},
-    'to_rg': {"text": "to_rg", "tool_tip":"to_rg", "function": simplify.to_rg, "in_place": True},
-    'full_reduce': {"text": "full_reduce", "tool_tip":"full_reduce", "function": simplify.full_reduce, "in_place": True},
-    'teleport_reduce': {"text": "teleport_reduce", "tool_tip":"teleport_reduce", "function": simplify.teleport_reduce, "in_place": True},
-    'reduce_scalar': {"text": "reduce_scalar", "tool_tip":"reduce_scalar", "function": simplify.reduce_scalar, "in_place": True},
-    'supplementarity_simp': {"text": "supplementarity_simp", "tool_tip":"supplementarity_simp", "function": simplify.supplementarity_simp, "in_place": True},
-    'to_clifford_normal_form_graph': {"text": "to_clifford_normal_form_graph", "tool_tip":"to_clifford_normal_form_graph", "function": simplify.to_clifford_normal_form_graph, "in_place": True},
-    'extract_circuit': {"text": "extract_circuit", "tool_tip":"extract_circuit", "function": _extract_circuit, "in_place": False},
-}
diff --git a/zxlive/proof_actions.py b/zxlive/proof_actions.py
@@ -3,6 +3,7 @@
 from typing import Callable, Literal, Optional, TYPE_CHECKING
 
 import pyzx
+from pyzx import simplify, extract_circuit
 
 from PySide6.QtWidgets import QPushButton, QButtonGroup
 from PySide6.QtCore import QParallelAnimationGroup, QEasingCurve
@@ -11,6 +12,7 @@
 from .commands import AddRewriteStep
 from .common import ANIMATION_DURATION, ET, GraphT, VT
 from .custom_rule import CustomRule
+from .dialogs import show_error_msg
 
 if TYPE_CHECKING:
     from .proof_panel import ProofPanel
@@ -32,13 +34,16 @@ class ProofAction(object):
     match_type: MatchType
     tooltip: str
     copy_first: bool = field(default=False)  # Whether the graph should be copied before trying to test whether it matches. Needed if the matcher changes the graph.
+    returns_new_graph: bool = field(default=False)  # Whether the rule returns a new graph instead of returning the rewrite changes.
     button: Optional[QPushButton] = field(default=None, init=False)
 
     @classmethod
     def from_dict(cls, d: dict) -> "ProofAction":
         if 'copy_first' not in d:
             d['copy_first'] = False
-        return cls(d['text'], d['matcher'], d['rule'], d['type'], d['tooltip'], d['copy_first'])
+        if 'returns_new_graph' not in d:
+            d['returns_new_graph'] = False
+        return cls(d['text'], d['matcher'], d['rule'], d['type'], d['tooltip'], d['copy_first'], d['returns_new_graph'])
 
     def do_rewrite(self, panel: "ProofPanel") -> None:
         verts, edges = panel.parse_selection()
@@ -49,10 +54,17 @@ def do_rewrite(self, panel: "ProofPanel") -> None:
         else:
             matches = self.matcher(g, lambda e: e in edges)
 
-        etab, rem_verts, rem_edges, check_isolated_vertices = self.rule(g, matches)
-        g.remove_edges(rem_edges)
-        g.remove_vertices(rem_verts)
-        g.add_edge_table(etab)
+        try:
+            if self.returns_new_graph:
+                g = self.rule(g, matches)
+            else:
+                etab, rem_verts, rem_edges, check_isolated_vertices = self.rule(g, matches)
+                g.remove_edges(rem_edges)
+                g.remove_vertices(rem_verts)
+                g.add_edge_table(etab)
+        except Exception as e:
+            show_error_msg('Error while applying rewrite rule', str(e))
+            return
 
         cmd = AddRewriteStep(panel.graph_view, g, panel.step_view, self.name)
         anim_before = None
@@ -188,6 +200,155 @@ def update_active(self, g: GraphT, verts: list[VT], edges: list[ET]) -> None:
     }
 )
 
+always_true = lambda graph, matches: matches
+
+def apply_simplification(simplification: Callable[[GraphT], GraphT]) -> Callable[[GraphT, list], pyzx.rules.RewriteOutputType[ET,VT]]:
+    def rule(g: GraphT, matches: list) -> pyzx.rules.RewriteOutputType[ET,VT]:
+        simplification(g)
+        return ({}, [], [], True)
+    return rule
+
+def _extract_circuit(graph, matches):
+    graph.auto_detect_io()
+    simplify.full_reduce(graph)
+    return extract_circuit(graph).to_graph()
+
+simplifications: dict = {
+    'bialg_simp': {
+        "text": "bialgebra",
+        "tooltip": "bialg_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.bialg_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'spider_simp': {
+        "text": "spider fusion",
+        "tooltip": "spider_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.spider_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'id_simp': {
+        "text": "id",
+        "tooltip": "id_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.id_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'phase_free_simp': {
+        "text": "phase free",
+        "tooltip": "phase_free_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.phase_free_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'pivot_simp': {
+        "text": "pivot",
+        "tooltip": "pivot_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.pivot_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'pivot_gadget_simp': {
+        "text": "pivot gadget",
+        "tooltip": "pivot_gadget_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.pivot_gadget_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'pivot_boundary_simp': {
+        "text": "pivot boundary",
+        "tooltip": "pivot_boundary_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.pivot_boundary_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'gadget_simp': {
+        "text": "gadget",
+        "tooltip": "gadget_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.gadget_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'lcomp_simp': {
+        "text": "local complementation",
+        "tooltip": "lcomp_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.lcomp_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'clifford_simp': {
+        "text": "clifford simplification",
+        "tooltip": "clifford_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.clifford_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'tcount': {
+        "text": "tcount",
+        "tooltip": "tcount",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.tcount),
+        "type": MATCHES_VERTICES,
+        },
+    'to_gh': {
+        "text": "to green-hadamard form",
+        "tooltip": "to_gh",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.to_gh),
+        "type": MATCHES_VERTICES,
+        },
+    'to_rg': {
+        "text": "to red-green form",
+        "tooltip": "to_rg",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.to_rg),
+        "type": MATCHES_VERTICES,
+        },
+    'full_reduce': {
+        "text": "full reduce",
+        "tooltip": "full_reduce",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.full_reduce),
+        "type": MATCHES_VERTICES,
+        },
+    'teleport_reduce': {
+        "text": "teleport reduce",
+        "tooltip": "teleport_reduce",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.teleport_reduce),
+        "type": MATCHES_VERTICES,
+        },
+    'reduce_scalar': {
+        "text": "reduce scalar",
+        "tooltip": "reduce_scalar",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.reduce_scalar),
+        "type": MATCHES_VERTICES,
+        },
+    'supplementarity_simp': {
+        "text": "supplementarity",
+        "tooltip": "supplementarity_simp",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.supplementarity_simp),
+        "type": MATCHES_VERTICES,
+        },
+    'to_clifford_normal_form_graph': {
+        "text": "to clifford normal form",
+        "tooltip": "to_clifford_normal_form_graph",
+        "matcher": always_true,
+        "rule": apply_simplification(simplify.to_clifford_normal_form_graph),
+        "type": MATCHES_VERTICES,
+        },
+    'extract_circuit': {
+        "text": "circuit extraction",
+        "tooltip": "extract_circuit",
+        "matcher": always_true,
+        "rule": _extract_circuit,
+        "type": MATCHES_VERTICES,
+        "returns_new_graph": True,
+        },
+}
 
 
 spider_fuse = ProofAction.from_dict(operations['spider'])
@@ -216,4 +377,6 @@ def update_active(self, g: GraphT, verts: list[VT], edges: list[ET]) -> None:
 mult_hbox = ProofAction.from_dict(operations['mult_hbox'])
 rules_zh = ProofActionGroup("ZH rules", hbox_to_edge, fuse_hbox, mult_hbox).copy()
 
-action_groups = [rules_basic, rules_graph_theoretic, rules_zxw, rules_zh]
+simplification_actions = ProofActionGroup("Simplification routines", *[ProofAction.from_dict(s) for s in simplifications.values()]).copy()
+
+action_groups = [rules_basic, rules_graph_theoretic, rules_zxw, rules_zh, simplification_actions]
diff --git a/zxlive/proof_panel.py b/zxlive/proof_panel.py
@@ -45,7 +45,7 @@ def __init__(self, graph: GraphT, *actions: QAction) -> None:
         self.graph_view = GraphView(self.graph_scene)
         self.splitter.addWidget(self.graph_view)
         self.graph_view.set_graph(graph)
-        
+
         self.actions_bar = QTabWidget(self)
         self.layout().insertWidget(1, self.actions_bar)
         self.init_action_groups()