// 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.
// Toffoli decomposition rules.
//
// These rules own exact CCX lowering paths.
rule decompose_ccx_to_cx {
match { CCX 0 1 2 }
rewrite { H 2, CX 1 2, TDG 2, CX 0 2, T 2, CX 1 2, TDG 2, CX 0 2, T 1, T 2, H 2, CX 0 1, T 0, TDG 1, CX 0 1 }
}
rule decompose_ccx_to_cz {
match { CCX 0 1 2 }
rewrite {
CZ 1 2,
H 2, TDG 2, H 2,
CZ 0 2,
H 2, T 2, H 2,
CZ 1 2,
H 2, TDG 2, H 2,
CZ 0 2,
H 2,
T 1, T 2,
H 2, H 1,
CZ 0 1,
H 1,
T 0, TDG 1,
H 1,
CZ 0 1,
H 1
}
}
rule decompose_ccx_to_u_cx {
match { CCX 0 1 2 }
rewrite {
U(π/2, 0, π) 2,
CX 1 2,
U(0, 0, -π/4) 2,
CX 0 2,
U(0, 0, π/4) 2,
CX 1 2,
U(0, 0, π/4) 1,
U(0, 0, -π/4) 2,
CX 0 2,
CX 0 1,
U(0, 0, π/4) 0,
U(0, 0, -π/4) 1,
CX 0 1,
U(π/2, 0, -3*π/4) 2
}
}
rule decompose_ccx_to_u_cz {
match { CCX 0 1 2 }
rewrite {
U(0, π/2, -π/2) 2,
CZ 1 2,
U(π/4, π/2, -π/2) 2,
CZ 0 2,
U(π/4, -π/2, π/2) 2,
CZ 1 2,
U(π/2, 0, -3*π/4) 1,
U(π/4, π/2, -π/2) 2,
CZ 0 2,
CZ 0 1,
U(0, 0, π/4) 0,
U(π/4, π/2, -π/2) 1,
CZ 0 1,
U(π/2, 0, π) 1,
U(π/4, -π/2, π/2) 2,
GPhase(15*π/8)
}
}
rule decompose_ccx_to_rz_x2p_cx {
match { CCX 0 1 2 }
rewrite {
RZ(π/2) 2, X2P 2, RZ(π/2) 2,
CX 1 2,
RZ(-π/4) 2,
CX 0 2,
RZ(π/4) 2,
CX 1 2,
RZ(π/4) 1, RZ(-π/4) 2,
CX 0 2,
CX 0 1,
RZ(π/4) 0, RZ(-π/4) 1,
CX 0 1,
RZ(3*π/4) 2, X2P 2, RZ(π/2) 2,
GPhase(-7*π/8)
}
}
rule decompose_ccx_to_rz_x2p_x_cz {
match { CCX 0 1 2 }
rewrite {
X 1, X 2,
CZ 1 2,
RZ(-π) 1, X 1,
RZ(π/2) 2, X2P 2, RZ(π/4) 2, X2P 2,
CZ 0 2,
X2P 2, RZ(5*π/4) 2, X2P 2, RZ(π) 2,
CZ 1 2,
RZ(3*π/4) 1, X2P 1, RZ(π) 1,
X2P 2, RZ(3*π/4) 2, X2P 2, RZ(π) 2,
CZ 0 2,
CZ 0 1,
RZ(π/4) 0,
X2P 1, RZ(3*π/4) 1, X2P 1, RZ(π) 1,
CZ 0 1,
X2P 1, RZ(π/2) 1,
X2P 2, RZ(5*π/4) 2, X2P 2, RZ(π/2) 2,
GPhase(21*π/8)
}
}
rule decompose_ccx_to_rx_ry_cx {
match { CCX 0 1 2 }
rewrite {
RY(π/2) 2, RX(3*π/2) 2,
CX 1 2,
RY(π/4) 2,
CX 0 2,
RY(-π/4) 2,
CX 1 2,
RX(π/2) 1, RY(-π/4) 1,
RY(π/4) 2,
CX 0 2,
CX 0 1,
RX(π/2) 0, RY(-π/4) 0, RX(-π/2) 0,
RY(π/4) 1, RX(-π/2) 1,
CX 0 1,
RX(-π/2) 2, RY(π/2) 2, RX(-3*π/4) 2,
GPhase(π/8)
}
}
rule decompose_ccx_to_rx_ry_cz {
match { CCX 0 1 2 }
rewrite {
CZ 1 2,
RX(-π/4) 2,
CZ 0 2,
RX(π/4) 2,
CZ 1 2,
RY(π/2) 1, RX(-3*π/4) 1, RX(-π/4) 2,
CZ 0 2,
CZ 0 1,
RX(π/2) 0, RY(-π/4) 0, RX(-π/2) 0,
RX(-π/4) 1,
CZ 0 1,
RY(π/2) 1, RX(π) 1, RX(π/4) 2,
GPhase(π/8)
}
}
rule decompose_ccx_to_rx_ry_rxx {
match { CCX 0 1 2 }
rewrite {
RY(π/2) 0, RY(π/2) 1, RY(π/2) 2, RX(π) 2,
RXX(π/2) 1 2,
RX(-π/2) 1, RY(π/4) 2, RX(-π/2) 2,
RXX(π/2) 0 2,
RX(-π/2) 0, RY(-π/4) 2, RX(-π/2) 2,
RXX(π/2) 1 2,
RX(π/4) 1, RY(π/4) 2, RX(-π/2) 2,
RXX(π/2) 0 2,
RX(1.131679298895586) 0,
RXX(-π/4) 0 1,
RX(-1.917077462293033) 0, RY(-π/2) 0,
RX(-π/2) 1, RY(-π/2) 1,
RX(-π/2) 2, RY(π/2) 2, RX(-3*π/4) 2,
GPhase(9*π/8)
}
}
rule decompose_ccx_to_rx_ry_rzz {
match { CCX 0 1 2 }
rewrite {
RX(π) 1, RY(π/2) 2, RX(π) 2,
RZZ(π/4) 1 2,
RY(-π/2) 1, RX(π/4) 1,
RZZ(π/2) 0 1,
RX(π/2) 0, RY(π/2) 0, RX(-π/2) 0,
RX(-π/2) 1,
RX(-π/2) 2, RY(π/4) 2, RX(-π/2) 2,
RZZ(π/4) 1 2,
RY(-π/2) 1, RX(π/4) 1,
RZZ(π/2) 0 1,
RX(π/2) 0, RY(π/2) 0, RX(π/2) 0,
RY(π/2) 1, RX(π/2) 1,
RX(-π/2) 2, RY(π/4) 2, RX(-π/2) 2,
RZZ(π/4) 0 2,
RX(π/2) 0, RY(π/4) 0, RX(π/2) 0,
RY(π/2) 2, RX(-3*π/4) 2,
GPhase(5*π/8)
}
}
rule decompose_ccx_to_rz_x2p_x_rzz {
match { CCX 0 1 2 }
rewrite {
X 1,
RZ(π/2) 2, X2P 2, RZ(π/2) 2,
RZZ(π/4) 1 2,
RZ(π/4) 1, X2P 1, RZ(-π/2) 1,
RZZ(-π/2) 0 1,
RZ(π/2) 0, X2P 1, RZ(-π) 1,
X 2, RZ(-π/4) 2,
RZZ(π/4) 1 2,
RZ(π/4) 1, X2P 1, RZ(-π/2) 1,
RZZ(-π/2) 0 1,
RZ(π/2) 0, X 0,
RZ(-π) 1, X2P 1, RZ(π/2) 1,
X 2, RZ(-π/4) 2,
RZZ(π/4) 0 2,
RZ(-π/4) 0, X 0,
RZ(3*π/4) 2, X2P 2, RZ(π/2) 2,
GPhase(π/8)
}
}
rule decompose_h_ccx_h_to_rz_x2p_cz {
match { H 2, CCX 0 1 2, H 2 }
rewrite {
RZ(-π/2) 2, X2P 2,
CZ 1 2,
RZ(-π/4) 1, X2P 2, RZ(π/4) 2, X2P 2,
CZ 0 2,
X2P 2, RZ(5*π/4) 2, X2P 2, RZ(π) 2,
CZ 1 2,
X2P 1, RZ(π) 1,
X2P 2, RZ(3*π/4) 2, X2P 2, RZ(π) 2,
CZ 0 2,
CZ 0 1,
RZ(π/4) 0,
X2P 1, RZ(3*π/4) 1, X2P 1, RZ(π) 1,
CZ 0 1,
X2P 1, RZ(π/2) 1,
X2P 2, RZ(3*π/4) 2,
GPhase(21*π/8)
}
}
rule decompose_h_ccx_h_to_rz_cx {
match { H 2, CCX 0 1 2, H 2 }
rewrite {
CX 1 2, RZ(-π/4) 2,
CX 0 2, RZ(π/4) 2,
CX 1 2, RZ(π/4) 1, RZ(-π/4) 2,
CX 0 2,
CX 0 1, RZ(π/4) 0, RZ(-π/4) 1,
CX 0 1, RZ(π/4) 2,
GPhase(π/8)
}
}
rule decompose_h_ccx_h_to_rx_ry_rzz {
match { H 2, CCX 0 1 2, H 2 }
rewrite {
RX(π) 1,
RZZ(π/4) 1 2,
RY(-π/2) 1, RX(π/4) 1,
RZZ(π/2) 0 1,
RX(π/2) 0, RY(π/2) 0, RX(-π/2) 0,
RX(-π/2) 1,
RX(-π/2) 2, RY(π/4) 2, RX(-π/2) 2,
RZZ(π/4) 1 2,
RY(-π/2) 1, RX(π/4) 1,
RZZ(π/2) 0 1,
RX(π/2) 0, RY(π/2) 0, RX(π/2) 0,
RY(π/2) 1, RX(π/2) 1,
RX(-π/2) 2, RY(π/4) 2, RX(-π/2) 2,
RZZ(π/4) 0 2,
RX(π/2) 0, RY(π/4) 0, RX(π/2) 0,
RX(-π/2) 2, RY(π/4) 2, RX(π/2) 2,
GPhase(5*π/8)
}
}
rule decompose_ccx_to_rz_x2p_rzx {
match { CCX 0 1 2 }
rewrite {
RZ(π/2) 2, X2P 2, RZ(π/2) 2,
RZ(π/2) 1, X2P 2, RZX(-π/2) 1 2, RZ(-π/4) 2,
RZ(π/2) 0, X2P 2, RZX(-π/2) 0 2, RZ(π/4) 2,
RZ(π/2) 1, X2P 2, RZX(-π/2) 1 2, RZ(π/4) 1, RZ(-π/4) 2,
RZ(π/2) 0, X2P 2, RZX(-π/2) 0 2,
RZ(π/2) 0, X2P 1, RZX(-π/2) 0 1,
RZ(π/4) 0, RZ(-π/4) 1,
RZ(π/2) 0, X2P 1, RZX(-π/2) 0 1,
RZ(3*π/4) 2, X2P 2, RZ(π/2) 2,
GPhase(5*π/8)
}
}