cqlib-core 0.1.0-beta.5

// This code is part of Cqlib.
//
// (C) Copyright China Telecom Quantum Group 2026
//
// This code is licensed under the Apache License, Version 2.0. You may
// obtain a copy of this license in the LICENSE.txt file in the root directory
// of this source tree or at http://www.apache.org/licenses/LICENSE-2.0.
//
// Any modifications or derivative works of this code must retain this
// copyright notice, and modified files need to carry a notice indicating
// that they have been altered from the originals.

// Identity transformation rules: equivalent rearrangements useful for
// topology matching, canonicalization, and gate movement.

// 1. H conjugation (H·gate·H = gate')

// H·X·H = Z
rule identity_hxh_to_z {
    match { H 0, X 0, H 0 }
    rewrite { Z 0 }
}

// H·Z·H = X
rule identity_hzh_to_x {
    match { H 0, Z 0, H 0 }
    rewrite { X 0 }
}

// H·Y·H = -Y → Y + GPhase(π)
rule identity_hyh_to_my {
    match { H 0, Y 0, H 0 }
    rewrite { Y 0, GPhase(π) }
}

// H·S·H = e^(iπ/4)·X2P
rule identity_hsh_to_sdg {
    match { H 0, S 0, H 0 }
    rewrite { X2P 0, GPhase(π/4) }
}

// H·SDG·H = e^(-iπ/4)·X2M
rule identity_hsdgh_to_s {
    match { H 0, SDG 0, H 0 }
    rewrite { X2M 0, GPhase(-π/4) }
}


// 2. S conjugation (S·gate·SDG = gate')


// S·X·SDG = Y
rule identity_sxs_to_y {
    match { S 0, X 0, SDG 0 }
    rewrite { Y 0, GPhase(π) }
}

// SDG·Y·S = X
rule identity_sdg_ys_to_x {
    match { SDG 0, Y 0, S 0 }
    rewrite { X 0, GPhase(π) }
}

// S·Z·SDG = Z (Z commutes with S)
rule identity_szs_to_z {
    match { S 0, Z 0, SDG 0 }
    rewrite { Z 0 }
}

// S·X2P·SDG = Y2M
rule identity_sx2ps_to_x2m {
    match { S 0, X2P 0, SDG 0 }
    rewrite { Y2M 0 }
}

// S·X2M·SDG = Y2P
rule identity_sx2ms_to_x2p {
    match { S 0, X2M 0, SDG 0 }
    rewrite { Y2P 0 }
}

// S·Y2P·SDG = X2P
rule identity_sy2ps_to_y2m {
    match { S 0, Y2P 0, SDG 0 }
    rewrite { X2P 0 }
}

// S·Y2M·SDG = X2M
rule identity_sy2ms_to_y2p {
    match { S 0, Y2M 0, SDG 0 }
    rewrite { X2M 0 }
}


// 3. X2P/X2M conjugation (X2P·gate·X2M = gate')

// X2P·Z·X2M = Y
rule identity_x2pzx2m_to_y {
    match { X2P 0, Z 0, X2M 0 }
    rewrite { Y 0 }
}

// X2M·Z·X2P = -Y
rule identity_x2mzx2p_to_my {
    match { X2M 0, Z 0, X2P 0 }
    rewrite { Y 0, GPhase(π) }
}

// X2P·X·X2M = X
rule identity_x2pxx2m_to_x {
    match { X2P 0, X 0, X2M 0 }
    rewrite { X 0 }
}

// X2M·Y·X2P = Z
rule identity_x2myx2p_to_z {
    match { X2M 0, Y 0, X2P 0 }
    rewrite { Z 0 }
}

// Y2P·Z·Y2M = -X
rule identity_y2pzy2m_to_mx {
    match { Y2P 0, Z 0, Y2M 0 }
    rewrite { X 0, GPhase(π) }
}

// Y2M·Z·Y2P = X
rule identity_y2mzy2p_to_x {
    match { Y2M 0, Z 0, Y2P 0 }
    rewrite { X 0 }
}

// Y2P·X·Y2M = Z
rule identity_y2pxy2m_to_z {
    match { Y2P 0, X 0, Y2M 0 }
    rewrite { Z 0 }
}

// Y2M·Y·Y2P = Y (needs verification)
rule identity_y2myy2p_to_y {
    match { Y2M 0, Y 0, Y2P 0 }
    rewrite { Y 0 }
}

// 4. CZ / CX conjugation (2-qubit Clifford)


// CZ·(X⊗I)·CZ = X⊗Z
rule identity_cz_x0_cz_to_xz {
    match { CZ 0 1, X 0, CZ 0 1 }
    rewrite { X 0, Z 1 }
}

// CZ·(I⊗X)·CZ = Z⊗X
rule identity_cz_x1_cz_to_zx {
    match { CZ 0 1, X 1, CZ 0 1 }
    rewrite { Z 0, X 1 }
}

// CX·(X⊗I)·CX = X⊗X
rule identity_cx_x0_cx_to_xx {
    match { CX 0 1, X 0, CX 0 1 }
    rewrite { X 0, X 1 }
}

// CX·(I⊗Z)·CX = Z⊗Z
rule identity_cx_z1_cx_to_zz {
    match { CX 0 1, Z 1, CX 0 1 }
    rewrite { Z 0, Z 1 }
}


// 5. Gate movement through CZ/CX (partial commutation)

// S on either qubit passes through CZ
rule identity_cz_s0_to_s_cz {
    match { CZ 0 1, S 0 }
    rewrite { S 0, CZ 0 1 }
}

rule identity_cz_s1_to_s_cz {
    match { CZ 0 1, S 1 }
    rewrite { S 1, CZ 0 1 }
}


// 6. CX direction flipping


// CX 0 1 → H⊗H · CX 1 0 · H⊗H
rule identity_cx_flip {
    match { CX 0 1 }
    rewrite { H 0, H 1, CX 1 0, H 0, H 1 }
}


// 7. Other identities

// SWAP symmetry
rule identity_swap_sym {
    match { SWAP 0 1 }
    rewrite { SWAP 1 0 }
}

// CZ = H⊗H · CX(reverse) · H⊗H (alternative CZ expression)
rule identity_cz_to_hcxh {
    match { CZ 0 1 }
    rewrite { H 1, CX 0 1, H 1 }
}

// X·Z = -Y
rule identity_xz_to_y_phase {
    match { X 0, Z 0 }
    rewrite { Y 0, GPhase(π/2) }
}

// Z·X = -Y
rule identity_zx_to_y_phase {
    match { Z 0, X 0 }
    rewrite { Y 0, GPhase(-π/2) }
}

// X2P·Y2M composition
rule identity_x2p_y2m {
    match { X2P 0, Y2M 0 }
    rewrite { H 0, SDG 0, GPhase(-π/4) }
}

// Y2P·X2M composition
rule identity_y2p_x2m {
    match { Y2P 0, X2M 0 }
    rewrite { S 0, H 0, GPhase(π/4) }
}

rule compose_cx_rz_cx_to_rzz {
    match { CX 0 1, RZ(theta) 1, CX 0 1 }
    rewrite { RZZ(theta) 0 1 }
}

rule compose_cx_phase_cx_to_rzz {
    match { CX 0 1, Phase(theta) 1, CX 0 1 }
    rewrite { RZZ(theta) 0 1, GPhase(theta/2) }
}

rule compose_cz_rx_cz_to_rzx {
    match { CZ 0 1, RX(theta) 1, CZ 0 1 }
    rewrite { RZX(theta) 0 1 }
}

rule compose_cz_rx_cz_to_rzx_swapped {
    match { CZ 0 1, RX(theta) 0, CZ 0 1 }
    rewrite { RZX(theta) 1 0 }
}

rule compose_cx_cz_to_cy {
    match { CX 0 1, CZ 0 1 }
    rewrite { Phase(π/2) 0, CY 0 1 }
}

rule compose_cx_cz_to_cy_cz_swapped {
    match { CX 0 1, CZ 1 0 }
    rewrite { Phase(π/2) 0, CY 0 1 }
}

rule compose_cz_cx_to_cy {
    match { CZ 0 1, CX 0 1 }
    rewrite { Phase(-π/2) 0, CY 0 1 }
}

rule compose_cz_cx_to_cy_cz_swapped {
    match { CZ 1 0, CX 0 1 }
    rewrite { Phase(-π/2) 0, CY 0 1 }
}

rule identity_cx_to_hczh {
    match { CX 0 1 }
    rewrite { H 1, CZ 0 1, H 1 }
}

rule identity_rz_to_phase_gphase {
    match { RZ(a) 0 }
    rewrite { Phase(a) 0, GPhase(-a/2) }
}

rule identity_hx2ph_to_s {
    match { H 0, X2P 0, H 0 }
    rewrite { S 0, GPhase(-π/4) }
}

rule identity_hx2mh_to_sdg {
    match { H 0, X2M 0, H 0 }
    rewrite { SDG 0, GPhase(π/4) }
}

rule identity_hy2ph_to_y2m {
    match { H 0, Y2P 0, H 0 }
    rewrite { Y2M 0 }
}

rule identity_hy2mh_to_y2p {
    match { H 0, Y2M 0, H 0 }
    rewrite { Y2P 0 }
}

rule identity_sysdg_to_x {
    match { S 0, Y 0, SDG 0 }
    rewrite { X 0 }
}

rule identity_sdg_xs_to_y {
    match { SDG 0, X 0, S 0 }
    rewrite { Y 0 }
}

rule identity_xy_to_z_phase {
    match { X 0, Y 0 }
    rewrite { Z 0, GPhase(-π/2) }
}

rule identity_yx_to_z_phase {
    match { Y 0, X 0 }
    rewrite { Z 0, GPhase(π/2) }
}

rule identity_yz_to_x_phase {
    match { Y 0, Z 0 }
    rewrite { X 0, GPhase(-π/2) }
}

rule identity_zy_to_x_phase {
    match { Z 0, Y 0 }
    rewrite { X 0, GPhase(π/2) }
}

rule identity_hth_to_rx {
    match { H 0, T 0, H 0 }
    rewrite { RX(π/4) 0, GPhase(π/8) }
}

rule identity_htdgh_to_rx {
    match { H 0, TDG 0, H 0 }
    rewrite { RX(-π/4) 0, GPhase(-π/8) }
}

rule compose_cx_bridge_4cx {
    match { CX 0 1, CX 1 2, CX 0 1, CX 1 2 }
    rewrite { CX 0 2 }
}

rule compose_cx_bridge_4cx_rev {
    match { CX 1 2, CX 0 1, CX 1 2, CX 0 1 }
    rewrite { CX 0 2 }
}

rule compose_swap_cx_bridge {
    match { SWAP 0 1, CX 1 2, SWAP 0 1 }
    rewrite { CX 0 2 }
}

rule compose_swap_cx_bridge_far {
    match { SWAP 0 1, CX 0 2, SWAP 0 1 }
    rewrite { CX 1 2 }
}

rule compose_swap_cz_bridge {
    match { SWAP 0 1, CZ 1 2, SWAP 0 1 }
    rewrite { CZ 0 2 }
}

rule compose_swap_swap_swap {
    match { SWAP 0 1, SWAP 0 2, SWAP 0 1 }
    rewrite { SWAP 1 2 }
}

rule compose_cx3_to_swap {
    match { CX 0 1, CX 1 0, CX 0 1 }
    rewrite { SWAP 0 1 }
}

rule compose_cx3_to_swap_rev {
    match { CX 1 0, CX 0 1, CX 1 0 }
    rewrite { SWAP 0 1 }
}

rule compose_swap_cx_swap_to_cx_flip {
    match { SWAP 0 1, CX 0 1, SWAP 0 1 }
    rewrite { CX 1 0 }
}

rule compose_swap_cz_swap_to_cz {
    match { SWAP 0 1, CZ 0 1, SWAP 0 1 }
    rewrite { CZ 0 1 }
}

rule compose_swap_crz_swap {
    match { SWAP 0 1, CRZ(a) 0 1, SWAP 0 1 }
    rewrite { CRZ(a) 1 0 }
}

rule compose_swap_crx_swap {
    match { SWAP 0 1, CRX(a) 0 1, SWAP 0 1 }
    rewrite { CRX(a) 1 0 }
}

rule compose_hh_cx_hh_to_cx_flip {
    match { H 0, H 1, CX 0 1, H 0, H 1 }
    rewrite { CX 1 0 }
}

rule compose_h1_cz_h1_to_cx {
    match { H 1, CZ 0 1, H 1 }
    rewrite { CX 0 1 }
}

rule compose_h0_cz_h0_to_cx_flip {
    match { H 0, CZ 0 1, H 0 }
    rewrite { CX 1 0 }
}

rule compose_h0_cx_h0_to_cz {
    match { H 0, CX 1 0, H 0 }
    rewrite { CZ 0 1 }
}

rule compose_h1_cx_h1_to_cz {
    match { H 1, CX 0 1, H 1 }
    rewrite { CZ 0 1 }
}

rule compose_y2m_cz_y2p_to_cx {
    match { Y2M 1, CZ 0 1, Y2P 1 }
    rewrite { CX 0 1 }
}

rule compose_y2p_cz_y2m_to_z_cx {
    match { Y2P 1, CZ 0 1, Y2M 1 }
    rewrite { Z 0, CX 0 1 }
}

rule compose_x2p_cz_x2m_to_cy {
    match { X2P 1, CZ 0 1, X2M 1 }
    rewrite { CY 0 1 }
}

rule compose_cx_rx_cx_to_rxx {
    match { CX 0 1, RX(a) 0, CX 0 1 }
    rewrite { RXX(a) 0 1 }
}

rule move_x_ctrl_cx {
    match { X 0, CX 0 1 }
    rewrite { CX 0 1, X 0, X 1 }
}

rule move_z_tgt_cx {
    match { Z 1, CX 0 1 }
    rewrite { CX 0 1, Z 0, Z 1 }
}

rule move_y_ctrl_cx {
    match { Y 0, CX 0 1 }
    rewrite { CX 0 1, Y 0, X 1 }
}

rule move_x0_cz {
    match { X 0, CZ 0 1 }
    rewrite { CZ 0 1, X 0, Z 1 }
}

rule move_x1_cz {
    match { X 1, CZ 0 1 }
    rewrite { CZ 0 1, Z 0, X 1 }
}

// Shortening identities, in circuit execution order; preserve scalar phases.
rule identity_rz_xy_absorb {
    match { RZ(a) 0, XY(b) 0 }
    rewrite { XY(b - a/2) 0 }
}

rule identity_xy_rz_absorb {
    match { XY(b) 0, RZ(a) 0 }
    rewrite { XY(b + a/2) 0 }
}

rule compose_rz_xy2p_rz {
    match { RZ(a) 0, XY2P(b) 0, RZ(c) 0 }
    rewrite { XY2P(b - a) 0, RZ(a + c) 0 }
}

rule compose_rz_xy2p_rz_cancel {
    match { RZ(a) 0, XY2P(b) 0, RZ(c) 0 }
    require { a + c == 0 mod 4*π }
    rewrite { XY2P(b - a) 0 }
}

rule compose_rz_xy2p_rz_global_phase {
    match { RZ(a) 0, XY2P(b) 0, RZ(c) 0 }
    require { a + c == 2*π mod 4*π }
    rewrite { XY2P(b - a) 0, GPhase(π) }
}

rule compose_rz_xy2m_rz {
    match { RZ(a) 0, XY2M(b) 0, RZ(c) 0 }
    rewrite { XY2M(b - a) 0, RZ(a + c) 0 }
}

rule compose_rz_xy2m_rz_cancel {
    match { RZ(a) 0, XY2M(b) 0, RZ(c) 0 }
    require { a + c == 0 mod 4*π }
    rewrite { XY2M(b - a) 0 }
}

rule compose_rz_xy2m_rz_global_phase {
    match { RZ(a) 0, XY2M(b) 0, RZ(c) 0 }
    require { a + c == 2*π mod 4*π }
    rewrite { XY2M(b - a) 0, GPhase(π) }
}

rule compose_rz_rxy_rz {
    match { RZ(a) 0, RXY(theta, b) 0, RZ(c) 0 }
    rewrite { RXY(theta, b - a) 0, RZ(a + c) 0 }
}

rule compose_rz_rxy_rz_cancel {
    match { RZ(a) 0, RXY(theta, b) 0, RZ(c) 0 }
    require { a + c == 0 mod 4*π }
    rewrite { RXY(theta, b - a) 0 }
}

rule compose_rz_rxy_rz_global_phase {
    match { RZ(a) 0, RXY(theta, b) 0, RZ(c) 0 }
    require { a + c == 2*π mod 4*π }
    rewrite { RXY(theta, b - a) 0, GPhase(π) }
}

rule compose_x2p_rz_x2m {
    match { X2P 0, RZ(a) 0, X2M 0 }
    rewrite { RY(a) 0 }
}

rule compose_x2m_rz_x2p {
    match { X2M 0, RZ(a) 0, X2P 0 }
    rewrite { RY(-a) 0 }
}

rule compose_y2m_rz_y2p {
    match { Y2M 0, RZ(a) 0, Y2P 0 }
    rewrite { RX(a) 0 }
}

rule compose_y2p_rz_y2m {
    match { Y2P 0, RZ(a) 0, Y2M 0 }
    rewrite { RX(-a) 0 }
}

rule identity_x2p_rz_pi_echo {
    match { X2P 0, RZ(a) 0, X2P 0 }
    require { a == π mod 2*π }
    rewrite { RZ(a) 0 }
}

rule identity_x2m_rz_pi_echo {
    match { X2M 0, RZ(a) 0, X2M 0 }
    require { a == π mod 2*π }
    rewrite { RZ(a) 0 }
}

rule identity_y2p_rz_pi_echo {
    match { Y2P 0, RZ(a) 0, Y2P 0 }
    require { a == π mod 2*π }
    rewrite { RZ(a) 0 }
}

rule identity_y2m_rz_pi_echo {
    match { Y2M 0, RZ(a) 0, Y2M 0 }
    require { a == π mod 2*π }
    rewrite { RZ(a) 0 }
}

rule identity_xy2p_rz_pi_echo {
    match { XY2P(phi) 0, RZ(a) 0, XY2P(phi) 0 }
    require { a == π mod 2*π }
    rewrite { RZ(a) 0 }
}

rule identity_xy2m_rz_pi_echo {
    match { XY2M(phi) 0, RZ(a) 0, XY2M(phi) 0 }
    require { a == π mod 2*π }
    rewrite { RZ(a) 0 }
}

// CZ conjugation of pi pulses removes both entanglers; include native RZ targets.
rule identity_cz_y0_cz {
    match { CZ 0 1, Y 0, CZ 0 1 }
    rewrite { Y 0, Z 1 }
}

rule identity_cz_y0_cz_to_rz {
    match { CZ 0 1, Y 0, CZ 0 1 }
    rewrite { Y 0, RZ(π) 1, GPhase(π/2) }
}

rule identity_cz_y0_cz_swapped {
    match { CZ 0 1, Y 0, CZ 1 0 }
    rewrite { Y 0, Z 1 }
}

rule identity_cz_y0_cz_to_rz_swapped {
    match { CZ 0 1, Y 0, CZ 1 0 }
    rewrite { Y 0, RZ(π) 1, GPhase(π/2) }
}

rule identity_cz_y1_cz {
    match { CZ 0 1, Y 1, CZ 0 1 }
    rewrite { Y 1, Z 0 }
}

rule identity_cz_y1_cz_to_rz {
    match { CZ 0 1, Y 1, CZ 0 1 }
    rewrite { Y 1, RZ(π) 0, GPhase(π/2) }
}

rule identity_cz_y1_cz_swapped {
    match { CZ 0 1, Y 1, CZ 1 0 }
    rewrite { Y 1, Z 0 }
}

rule identity_cz_y1_cz_to_rz_swapped {
    match { CZ 0 1, Y 1, CZ 1 0 }
    rewrite { Y 1, RZ(π) 0, GPhase(π/2) }
}

rule identity_cz_xy0_cz {
    match { CZ 0 1, XY(phi) 0, CZ 0 1 }
    rewrite { XY(phi) 0, Z 1 }
}

rule identity_cz_xy0_cz_to_rz {
    match { CZ 0 1, XY(phi) 0, CZ 0 1 }
    rewrite { XY(phi) 0, RZ(π) 1, GPhase(π/2) }
}

rule identity_cz_xy0_cz_swapped {
    match { CZ 0 1, XY(phi) 0, CZ 1 0 }
    rewrite { XY(phi) 0, Z 1 }
}

rule identity_cz_xy0_cz_to_rz_swapped {
    match { CZ 0 1, XY(phi) 0, CZ 1 0 }
    rewrite { XY(phi) 0, RZ(π) 1, GPhase(π/2) }
}

rule identity_cz_xy1_cz {
    match { CZ 0 1, XY(phi) 1, CZ 0 1 }
    rewrite { XY(phi) 1, Z 0 }
}

rule identity_cz_xy1_cz_to_rz {
    match { CZ 0 1, XY(phi) 1, CZ 0 1 }
    rewrite { XY(phi) 1, RZ(π) 0, GPhase(π/2) }
}

rule identity_cz_xy1_cz_swapped {
    match { CZ 0 1, XY(phi) 1, CZ 1 0 }
    rewrite { XY(phi) 1, Z 0 }
}

rule identity_cz_xy1_cz_to_rz_swapped {
    match { CZ 0 1, XY(phi) 1, CZ 1 0 }
    rewrite { XY(phi) 1, RZ(π) 0, GPhase(π/2) }
}

// Also accept Z after the central RZ(pi) has been specialized.
rule identity_x2p_z_echo {
    match { X2P 0, Z 0, X2P 0 }
    rewrite { Z 0 }
}

rule identity_x2m_z_echo {
    match { X2M 0, Z 0, X2M 0 }
    rewrite { Z 0 }
}

rule identity_y2p_z_echo {
    match { Y2P 0, Z 0, Y2P 0 }
    rewrite { Z 0 }
}

rule identity_y2m_z_echo {
    match { Y2M 0, Z 0, Y2M 0 }
    rewrite { Z 0 }
}

rule identity_xy2p_z_echo {
    match { XY2P(phi) 0, Z 0, XY2P(phi) 0 }
    rewrite { Z 0 }
}

rule identity_xy2m_z_echo {
    match { XY2M(phi) 0, Z 0, XY2M(phi) 0 }
    rewrite { Z 0 }
}