We define a larger gate set for SQIR in ExtractionGateSet.v and for VOQC in FullGateSet.v. Both are shown below. We should unify these two gate sets for consistency. This will require updating the VOQC program representation in UnitaryListRepresentation.v to support 4- and 5-qubit gates.
In SQIR/ExtractionGateSet:
Inductive U : nat -> Set :=
| U_X : U 1
| U_H : U 1
| U_U1 : R -> U 1
| U_U2 : R -> R -> U 1
| U_U3 : R -> R -> R -> U 1
| U_CX : U 2
| U_CU1 : R -> U 2
| U_CH : U 2
| U_SWAP : U 2
| U_CCX : U 3
| U_CCU1 : R -> U 3
| U_CSWAP : U 3
| U_C3X : U 4
| U_C4X : U 5.
In VOQC/FullGateSet.v;
Inductive Full_Unitary : nat -> Set :=
| U_I : Full_Unitary 1
| U_X : Full_Unitary 1
| U_Y : Full_Unitary 1
| U_Z : Full_Unitary 1
| U_H : Full_Unitary 1
| U_S : Full_Unitary 1
| U_T : Full_Unitary 1
| U_Sdg : Full_Unitary 1
| U_Tdg : Full_Unitary 1
| U_Rx (r : R) : Full_Unitary 1
| U_Ry (r : R) : Full_Unitary 1
| U_Rz (r : R) : Full_Unitary 1
| U_Rzq (q : Q) : Full_Unitary 1
| U_U1 (r : R) : Full_Unitary 1
| U_U2 (r : R) (r : R) : Full_Unitary 1
| U_U3 (r : R) (r : R) (r : R) : Full_Unitary 1
| U_CX : Full_Unitary 2
| U_CZ : Full_Unitary 2
| U_SWAP : Full_Unitary 2
| U_CCX : Full_Unitary 3
| U_CCZ : Full_Unitary 3.
Definition U := Full_Unitary.
We define a larger gate set for SQIR in ExtractionGateSet.v and for VOQC in FullGateSet.v. Both are shown below. We should unify these two gate sets for consistency. This will require updating the VOQC program representation in UnitaryListRepresentation.v to support 4- and 5-qubit gates.
In SQIR/ExtractionGateSet:
In VOQC/FullGateSet.v;