Equivalence Checking Manager

This is the main class of QCEC that allows to check the equivalence of quantum circuits based on the methods proposed in [2]. It features many configuration options that orchestrate the whole procedure. This page describes all the relevant methods of the Equivalence Checking Manager.

class EquivalenceCheckingManager

Main class for orchestrating the equivalence check

Constructing an instance

The simplest way of constructing an EquivalenceCheckingManager is to just pass it the two circuits whose equivalence shall be checked.

ecm = EquivalenceCheckingManager(circ1=qc1, circ2=qc2)

This constructs the manager using all the default options. The circuits to be verified can be provided in various ways:

• Python objects:

  • qiskit.circuit.QuantumCircuit from IBM’s Qiskit (preferred)

  • QasmQobjExperiment from IBM’s Qiskit

• Files

  • OpenQASM 2.0 and (a subset of) OpenQASM 3.0 (e.g. used by IBM’s Qiskit),

  • Real (e.g. from RevLib),

  • TFC (e.g. from Reversible Logic Synthesis Benchmarks Page)

  • QC (e.g. from Feynman)

It can be further configured by passing a Configuration object to the constructor.

EquivalenceCheckingManager.__init__(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, circ1: object, circ2: object, config: mqt.qcec.pyqcec.Configuration = <mqt.qcec.pyqcec.Configuration object at 0x7efef3d35bf0>) → None

Create an equivalence checking manager for two circuits and configure it with a Configuration object.

Configuration after instantiation

In addition, the Configuration of the manager can be altered after its construction. To this end, several convenience functions are provided which allow to modify the individual options:

• Execution Options:

  These options orchestrate the run() method.

  EquivalenceCheckingManager.set_parallel(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, enable: bool = True) → None

  Set whether execution should happen in parallel.

  EquivalenceCheckingManager.set_nthreads(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, nthreads: int = 2) → None

  Set the maximum number of threads to use.

  EquivalenceCheckingManager.set_timeout(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, timeout: float = 0.0) → None

  Set a timeout (in seconds) for run().

  EquivalenceCheckingManager.set_construction_checker(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, enable: bool = False) → None

  Set whether the construction checker should be executed.

  EquivalenceCheckingManager.set_simulation_checker(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, enable: bool = True) → None

  Set whether the simulation checker should be executed.

  EquivalenceCheckingManager.set_alternating_checker(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, enable: bool = True) → None

  Set whether the alternating checker should be executed.

  EquivalenceCheckingManager.set_zx_checker(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, enable: bool = True) → None

  Set whether the ZX-calculus checker should be executed.

  EquivalenceCheckingManager.set_tolerance(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, tolerance: float = 2.2737367544323206e-13) → None

  Set the numerical tolerance of the underlying decision diagram package.

• Optimizations

  These functions allow to apply specific circuit optimizations that might not have been performed during initialization. Note that already performed optimizations cannot be reverted since they are applied at construction time.

  EquivalenceCheckingManager.fuse_single_qubit_gates(self: mqt.qcec.pyqcec.EquivalenceCheckingManager) → None

  Fuse consecutive single qubit gates.

  EquivalenceCheckingManager.reconstruct_swaps(self: mqt.qcec.pyqcec.EquivalenceCheckingManager) → None

  Try to reconstruct SWAP gates that have been decomposed or optimized away.

  EquivalenceCheckingManager.reorder_operations(self: mqt.qcec.pyqcec.EquivalenceCheckingManager) → None

  Reorder operations to establish canonical ordering.

• Application Options

  These options describe the Application Scheme that is used for the individual equivalence checkers (based on decision diagrams). The scheme can either be set collectively for all checkers at once or individually.

  EquivalenceCheckingManager.set_application_scheme(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, scheme: mqt.qcec.pyqcec.ApplicationScheme = 'proportional') → None

  Set the Application Scheme that is used for all checkers (based on decision diagrams).

  EquivalenceCheckingManager.set_construction_application_scheme(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, scheme: mqt.qcec.pyqcec.ApplicationScheme = 'proportional') → None

  Set the Application Scheme that is used for the construction checker.

  EquivalenceCheckingManager.set_simulation_application_scheme(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, scheme: mqt.qcec.pyqcec.ApplicationScheme = 'proportional') → None

  Set the Application Scheme that is used for the simulation checker.

  EquivalenceCheckingManager.set_alternating_application_scheme(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, scheme: mqt.qcec.pyqcec.ApplicationScheme = 'proportional') → None

  Set the Application Scheme that is used for the alternating checker.

  The Gate Cost application scheme can be configured with a profile that specifies the cost of gates. Again, this can be set collectively for all checkers or individually.

  EquivalenceCheckingManager.set_gate_cost_profile(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, profile: str = '') → None

  Set the profile used in the Gate Cost application scheme for all checkers (based on decision diagrams).

  EquivalenceCheckingManager.set_construction_gate_cost_profile(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, profile: str = '') → None

  Set the profile used in the Gate Cost application scheme for the construction checker.

  EquivalenceCheckingManager.set_simulation_gate_cost_profile(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, profile: str = '') → None

  Set the profile used in the Gate Cost application scheme for the simulation checker.

  EquivalenceCheckingManager.set_alternating_gate_cost_profile(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, profile: str = '') → None

  Set the profile used in the Gate Cost application scheme for the alternating checker.

• Functionality Options

  These options influence all checkers that consider the whole functionality of a circuit.

  EquivalenceCheckingManager.set_trace_threshold(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, threshold: float = 1e-08) → None

  Set the trace threshold used for comparing two unitaries or functionality matrices.

• Simulation Options

  These options influence the simulation checker.

  EquivalenceCheckingManager.set_fidelity_threshold(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, threshold: float = 1e-08) → None

  Set the fidelity threshold used for comparing two states or state vectors.

  EquivalenceCheckingManager.set_max_sims(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, sims: int = 16) → None

  Set the maximum number of simulations to be started for the simulation checker.

  EquivalenceCheckingManager.set_state_type(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, state_type: mqt.qcec.pyqcec.StateType = 'computational_basis') → None

  Set the type of states used for the simulations in the simulation checker.

  EquivalenceCheckingManager.set_seed(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, seed: int = 0) → None

  Set the seed for the state generator in the simulation checker.

  EquivalenceCheckingManager.store_cex_input(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, enable: bool = False) → None

  Set whether to store the input state if a counterexample is obtained.

  EquivalenceCheckingManager.store_cex_output(self: mqt.qcec.pyqcec.EquivalenceCheckingManager, enable: bool = False) → None

  Set whether to store the output states if a counterexample is obtained.

Running the equivalence check

Once the manager has been constructed and (optionally) configured, the equivalence check can be started by calling run().

EquivalenceCheckingManager.run(self: mqt.qcec.pyqcec.EquivalenceCheckingManager) → None

Execute the equivalence check as configured.

Obtaining the results

After the run has completed, several results can be obtained:

• The final result of the equivalence check.

  EquivalenceCheckingManager.equivalence(self: mqt.qcec.pyqcec.EquivalenceCheckingManager) → mqt.qcec.pyqcec.EquivalenceCriterion

  Returns the EquivalenceCriterion that has been determined as the result of the equivalence check.

• The EquivalenceCheckingManager.Results object that also contains statistics such as runtime and performed simulations.

  EquivalenceCheckingManager.get_results(self: mqt.qcec.pyqcec.EquivalenceCheckingManager) → mqt.qcec.pyqcec.EquivalenceCheckingManager.Results

  Returns the EquivalenceCheckingManager.Results of the equivalence check including statistics.

• A JSON-style dictionary containing all available information.

  Results.json(self: mqt.qcec.pyqcec.EquivalenceCheckingManager.Results) → json

  Returns a JSON-style dictionary of the results.