1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
// This code is part of Cqlib.
//
// (C) Copyright China Telecom Quantum Group 2025-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.
//! # Gate Commutation
//!
//! This module proves when two concrete instruction applications can be
//! exchanged by compiler passes without changing circuit semantics. A
//! successful query returns a [`Commutation`] proof, while `None` means only
//! that the available oracles could not prove commutation.
//!
//! The checker combines several conservative proof sources:
//!
//! - fast structural facts such as identity, global phase, disjoint support,
//! and identical applications;
//! - algebraic rules for diagonal gates, Pauli-axis strings, controlled-axis
//! gates, and selected symmetric two-qubit families;
//! - explicit `A; B -> B; A` rules from the compiler knowledge library;
//! - an optional small local-matrix fallback for concrete parameters.
//!
//! # Examples
//!
//! ```rust
//! use cqlib_core::circuit::{Instruction, Parameter, Qubit, StandardGate};
//! use cqlib_core::compile::commutation::{check_commutation, Commutation};
//!
//! let result = check_commutation(
//! &Instruction::Standard(StandardGate::RZ),
//! &[Qubit::new(0)],
//! &[Parameter::symbol("a")],
//! &Instruction::Standard(StandardGate::RZ),
//! &[Qubit::new(0)],
//! &[Parameter::symbol("b")],
//! );
//!
//! assert_eq!(result, Some(Commutation::Exact));
//! ```
pub use ;
pub use algebraic_commutation;