Module commutation 

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

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));

Re-exports

pub use checker::Commutation;

pub use checker::CommutationChecker;

pub use checker::CommutationConfig;

pub use checker::CommutationResult;

pub use checker::check_commutation;

pub use algebra::algebraic_commutation;

Modules

algebra

Structural algebraic commutation checks.

checker

High-level gate commutation checker.

matrix

Small local-matrix fallback for commutation checks.

rules

Rule-based commutation oracle.