`CliffordResynthesis` pass can create invalid circuits

[cqc-alec]

from pytket.circuit import Circuit
from pytket.passes import CliffordResynthesis
import json

with open("circ.json", "r") as f:
    circuit = Circuit.from_dict(json.load(f))

CliffordResynthesis().apply(circuit)
cmds = circuit.get_commands()
print(cmds)

generates a critical assertion error while attempting to construct the command list.
circ.json

[cqc-alec]

A much smaller example:

from pytket.circuit import Circuit
from pytket.passes import CliffordResynthesis

c = Circuit(6)
c.CZ(1, 4)
c.CZ(2, 3)
c.SWAP(3, 5)
c.CZ(1, 5)
c.SWAP(3, 5)
c.CZ(4, 5)
c.SWAP(1, 4)
c.CZ(1, 2)
c.CZ(3, 4)
c.SWAP(4, 5)
c.CZ(0, 3)
c.CZ(1, 5)
c.CZ(0, 4)

c.replace_SWAPs()
CliffordResynthesis().apply(c)
cmds = c.get_commands()
print(cmds)

generates the same assertion error.

[cqc-alec]

The implicit qubit permutation was a red herring. This even simpler example exhibits the problem:

from pytket.circuit import Circuit
from pytket.passes import CliffordResynthesis

c = Circuit(6)
c.CZ(1, 4)
c.CZ(2, 3)
c.CZ(1, 3)
c.CZ(4, 5)
c.CZ(4, 2)
c.CZ(3, 1)
c.CZ(0, 3)
c.CZ(4, 1)
c.CZ(0, 5)

CliffordResynthesis().apply(c)
cmds = c.get_commands()
print(cmds)

[cqc-alec]

There is a basic error in the logic used for CliffordResynthesis.

The logic is: first partition the circuit into convex subcircuits; then for each of those subcircuits, substitute its vertices with a resynthesised subcircuit.

"Convex" means that every path from A to B where A and B are vertices in the set contains only vertices that are in the set.

The problem is that after making the first of these substitutions, the second subcircuit may no longer be convex!

For example, consider the following (part of a) circuit:

The first convex subcircuit consists of the XXPhase(0.5) and the XXPhase(2.5); the second subcircuit consists of the XXPhase(1.5) and the YYPhase(1.5). These are disjoint convex subcircuits; however, if we were to merge the first one into a new "blob", with 3 inputs and 3 outputs, then the second one would no longer be convex because there is a path from the XXPhase(1.5) to the YPhase(1.5) passing through the blob and the YYPhase(0.5).