diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 92a11a26..23d785b8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -199,8 +199,9 @@ jobs: if: fromJSON(needs.change-detection.outputs.run-python-tests) uses: munich-quantum-toolkit/workflows/.github/workflows/reusable-python-linter.yml@d6314c45667c131055a0389afc110e8dedc6da3f # v1.17.11 with: - enable-ty: true + check-stubs: true enable-mypy: false + enable-ty: true build-sdist: name: 🚀 CD diff --git a/.license-tools-config.json b/.license-tools-config.json index 16db5d7e..2a72a12e 100644 --- a/.license-tools-config.json +++ b/.license-tools-config.json @@ -34,6 +34,7 @@ ".*\\.profile", "uv\\.lock", "py\\.typed", - ".*build.*" + ".*build.*", + "qcec_patterns.txt" ] } diff --git a/CHANGELOG.md b/CHANGELOG.md index 5218233c..c0a3a092 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,7 @@ This project adheres to [Semantic Versioning], with the exception that minor rel ### Changed +- ♻️ Auto-generate `pyqcec.pyi` via `nanobind.stubgen` ([#831]) ([**@denialhaag**]) - 🔧 Replace `mypy` with `ty` ([#775], [#825]) ([**@denialhaag**]) ## [3.4.0] - 2026-01-13 @@ -124,6 +125,7 @@ _📚 Refer to the [GitHub Release Notes] for previous changelogs._ +[#831]: https://github.com/munich-quantum-toolkit/qcec/pull/831 [#825]: https://github.com/munich-quantum-toolkit/qcec/pull/825 [#817]: https://github.com/munich-quantum-toolkit/qcec/pull/817 [#796]: https://github.com/munich-quantum-toolkit/qcec/pull/796 diff --git a/UPGRADING.md b/UPGRADING.md index 63f01909..84b33d69 100644 --- a/UPGRADING.md +++ b/UPGRADING.md @@ -4,6 +4,8 @@ This document describes breaking changes and how to upgrade. For a complete list ## [Unreleased] +To comply with established guidelines for attribute names, `mqt.qcec.pyqcec.StateType.random_1Q_basis` has been renamed to `random_1q_basis`. + ## [3.4.0] ### Python wheels diff --git a/bindings/application_scheme.cpp b/bindings/application_scheme.cpp deleted file mode 100644 index 2715a736..00000000 --- a/bindings/application_scheme.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/* - * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM - * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH - * All rights reserved. - * - * SPDX-License-Identifier: MIT - * - * Licensed under the MIT License - */ - -#include "checker/dd/applicationscheme/ApplicationScheme.hpp" - -#include - -namespace ec { - -namespace nb = nanobind; -using namespace nb::literals; - -// NOLINTNEXTLINE(misc-use-internal-linkage) -void registerApplicationSchema(const nb::module_& m) { - nb::enum_(m, "ApplicationScheme", nb::is_arithmetic()) - .value("sequential", ApplicationSchemeType::Sequential) - .value("reference", ApplicationSchemeType::Sequential) - .value("one_to_one", ApplicationSchemeType::OneToOne) - .value("naive", ApplicationSchemeType::OneToOne) - .value("lookahead", ApplicationSchemeType::Lookahead) - .value( - "gate_cost", ApplicationSchemeType::GateCost, - "Each gate of the first circuit is associated with a corresponding " - "cost according to some cost function *f(...)*. Whenever a gate *g* " - "from the first circuit is applied *f(g)* gates are applied from the " - "second circuit. Referred to as *compilation_flow* in " - ":cite:p:`burgholzer2020verifyingResultsIBM`.") - .value("compilation_flow", ApplicationSchemeType::GateCost) - .value("proportional", ApplicationSchemeType::Proportional); -} - -} // namespace ec diff --git a/bindings/bindings.cpp b/bindings/bindings.cpp index bfb2ff78..c04d1bad 100644 --- a/bindings/bindings.cpp +++ b/bindings/bindings.cpp @@ -16,7 +16,7 @@ namespace nb = nanobind; using namespace nb::literals; // forward declarations -void registerApplicationSchema(const nb::module_& m); +void registerApplicationScheme(const nb::module_& m); void registerConfiguration(const nb::module_& m); void registerEquivalenceCheckingManager(const nb::module_& m); void registerEquivalenceCriterion(const nb::module_& m); @@ -24,7 +24,7 @@ void registerStateType(const nb::module_& m); // NOLINTNEXTLINE(performance-unnecessary-value-param) NB_MODULE(MQT_QCEC_MODULE_NAME, m) { - registerApplicationSchema(m); + registerApplicationScheme(m); registerConfiguration(m); registerEquivalenceCheckingManager(m); registerEquivalenceCriterion(m); diff --git a/bindings/configuration.cpp b/bindings/configuration.cpp deleted file mode 100644 index 1f99f173..00000000 --- a/bindings/configuration.cpp +++ /dev/null @@ -1,120 +0,0 @@ -/* - * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM - * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH - * All rights reserved. - * - * SPDX-License-Identifier: MIT - * - * Licensed under the MIT License - */ - -#include "Configuration.hpp" - -#include -#include // NOLINT(misc-include-cleaner) - -namespace ec { - -namespace nb = nanobind; -using namespace nb::literals; - -// NOLINTNEXTLINE(misc-use-internal-linkage) -void registerConfiguration(const nb::module_& m) { - // Class definitions - auto configuration = nb::class_(m, "Configuration"); - auto execution = - nb::class_(configuration, "Execution"); - auto optimizations = - nb::class_(configuration, "Optimizations"); - auto application = - nb::class_(configuration, "Application"); - auto functionality = - nb::class_(configuration, "Functionality"); - auto simulation = - nb::class_(configuration, "Simulation"); - auto parameterized = - nb::class_(configuration, "Parameterized"); - - // Configuration - configuration.def(nb::init<>()) - .def_rw("execution", &Configuration::execution) - .def_rw("optimizations", &Configuration::optimizations) - .def_rw("application", &Configuration::application) - .def_rw("functionality", &Configuration::functionality) - .def_rw("simulation", &Configuration::simulation) - .def_rw("parameterized", &Configuration::parameterized) - .def("json", - [](const Configuration& config) { - const nb::module_ json = nb::module_::import_("json"); - const nb::object loads = json.attr("loads"); - return loads(config.json().dump()); - }) - .def("__repr__", &Configuration::toString); - - // execution options - execution.def(nb::init<>()) - .def_rw("parallel", &Configuration::Execution::parallel) - .def_rw("nthreads", &Configuration::Execution::nthreads) - .def_rw("timeout", &Configuration::Execution::timeout) - .def_rw("run_construction_checker", - &Configuration::Execution::runConstructionChecker) - .def_rw("run_simulation_checker", - &Configuration::Execution::runSimulationChecker) - .def_rw("run_alternating_checker", - &Configuration::Execution::runAlternatingChecker) - .def_rw("run_zx_checker", &Configuration::Execution::runZXChecker) - .def_rw("numerical_tolerance", - &Configuration::Execution::numericalTolerance) - .def_rw("set_all_ancillae_garbage", - &Configuration::Execution::setAllAncillaeGarbage); - - // optimization options - optimizations.def(nb::init<>()) - .def_rw("fuse_single_qubit_gates", - &Configuration::Optimizations::fuseSingleQubitGates) - .def_rw("reconstruct_swaps", - &Configuration::Optimizations::reconstructSWAPs) - .def_rw("remove_diagonal_gates_before_measure", - &Configuration::Optimizations::removeDiagonalGatesBeforeMeasure) - .def_rw("transform_dynamic_circuit", - &Configuration::Optimizations::transformDynamicCircuit) - .def_rw("reorder_operations", - &Configuration::Optimizations::reorderOperations) - .def_rw("backpropagate_output_permutation", - &Configuration::Optimizations::backpropagateOutputPermutation) - .def_rw("elide_permutations", - &Configuration::Optimizations::elidePermutations); - - // application options - application.def(nb::init<>()) - .def_rw("construction_scheme", - &Configuration::Application::constructionScheme) - .def_rw("simulation_scheme", - &Configuration::Application::simulationScheme) - .def_rw("alternating_scheme", - &Configuration::Application::alternatingScheme) - .def_rw("profile", &Configuration::Application::profile); - - // functionality options - functionality.def(nb::init<>()) - .def_rw("trace_threshold", &Configuration::Functionality::traceThreshold) - .def_rw("check_partial_equivalence", - &Configuration::Functionality::checkPartialEquivalence); - - // simulation options - simulation.def(nb::init<>()) - .def_rw("fidelity_threshold", - &Configuration::Simulation::fidelityThreshold) - .def_rw("max_sims", &Configuration::Simulation::maxSims) - .def_rw("state_type", &Configuration::Simulation::stateType) - .def_rw("seed", &Configuration::Simulation::seed); - - // parameterized options - parameterized.def(nb::init<>()) - .def_rw("parameterized_tolerance", - &Configuration::Parameterized::parameterizedTol) - .def_rw("additional_instantiations", - &Configuration::Parameterized::nAdditionalInstantiations); -} - -} // namespace ec diff --git a/bindings/equivalence_checking_manager.cpp b/bindings/equivalence_checking_manager.cpp deleted file mode 100644 index b189f6a1..00000000 --- a/bindings/equivalence_checking_manager.cpp +++ /dev/null @@ -1,120 +0,0 @@ -/* - * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM - * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH - * All rights reserved. - * - * SPDX-License-Identifier: MIT - * - * Licensed under the MIT License - */ - -#include "Configuration.hpp" -#include "EquivalenceCheckingManager.hpp" -#include "EquivalenceCriterion.hpp" -#include "ir/QuantumComputation.hpp" - -#include -#include // NOLINT(misc-include-cleaner) -#include // NOLINT(misc-include-cleaner) -#include - -namespace ec { - -namespace nb = nanobind; -using namespace nb::literals; - -// NOLINTNEXTLINE(misc-use-internal-linkage) -void registerEquivalenceCheckingManager(const nb::module_& m) { - // Class definitions - auto ecm = - nb::class_(m, "EquivalenceCheckingManager"); - auto results = - nb::class_(ecm, "Results"); - - // Constructors - ecm.def(nb::init(), - "circ1"_a, "circ2"_a, "config"_a = Configuration()); - - // Access to circuits - ecm.def_prop_ro("qc1", &EquivalenceCheckingManager::getFirstCircuit, - nb::rv_policy::reference_internal); - ecm.def_prop_ro("qc2", &EquivalenceCheckingManager::getSecondCircuit, - nb::rv_policy::reference_internal); - - // Access to configuration - ecm.def_prop_rw( - "configuration", &EquivalenceCheckingManager::getConfiguration, - [](EquivalenceCheckingManager& manager, const Configuration& config) { - manager.getConfiguration() = config; - }, - nb::rv_policy::reference_internal); - - // Run - ecm.def("run", &EquivalenceCheckingManager::run); - - // Results - ecm.def_prop_ro("results", &EquivalenceCheckingManager::getResults, - nb::rv_policy::reference_internal); - ecm.def_prop_ro("equivalence", &EquivalenceCheckingManager::equivalence); - - // Convenience functions - // Execution - ecm.def("disable_all_checkers", - &EquivalenceCheckingManager::disableAllCheckers) - // Application - .def("set_application_scheme", - &EquivalenceCheckingManager::setApplicationScheme, - "scheme"_a = "proportional") - .def("set_gate_cost_profile", - &EquivalenceCheckingManager::setGateCostProfile, "profile"_a = "") - .def("__repr__", [](const EquivalenceCheckingManager& manager) { - return ""; - }); - - // EquivalenceCheckingManager::Results bindings - results.def(nb::init<>()) - .def_rw("preprocessing_time", - &EquivalenceCheckingManager::Results::preprocessingTime) - .def_rw("check_time", &EquivalenceCheckingManager::Results::checkTime) - .def_rw("equivalence", &EquivalenceCheckingManager::Results::equivalence) - .def_rw("started_simulations", - &EquivalenceCheckingManager::Results::startedSimulations) - .def_rw("performed_simulations", - &EquivalenceCheckingManager::Results::performedSimulations) - .def_rw("cex_input", &EquivalenceCheckingManager::Results::cexInput) - .def_rw("cex_output1", &EquivalenceCheckingManager::Results::cexOutput1) - .def_rw("cex_output2", &EquivalenceCheckingManager::Results::cexOutput2) - .def_rw("performed_instantiations", - &EquivalenceCheckingManager::Results::performedInstantiations) - .def_prop_rw( - "checker_results", - [](const EquivalenceCheckingManager::Results& results) { - const nb::module_ json = nb::module_::import_("json"); - const nb::object loads = json.attr("loads"); - return loads(results.checkerResults.dump()); - }, - [](EquivalenceCheckingManager::Results& results, - const nb::dict& value) { - const nb::module_ json = nb::module_::import_("json"); - const nb::object dumps = json.attr("dumps"); - const auto jsonString = nb::cast(dumps(value)); - results.checkerResults = nlohmann::json::parse(jsonString); - }) - .def("considered_equivalent", - &EquivalenceCheckingManager::Results::consideredEquivalent) - .def("json", - [](const EquivalenceCheckingManager::Results& results) { - const nb::module_ json = nb::module_::import_("json"); - const nb::object loads = json.attr("loads"); - return loads(results.json().dump()); - }) - .def("__str__", &EquivalenceCheckingManager::Results::toString) - .def("__repr__", [](const EquivalenceCheckingManager::Results& res) { - return ""; - }); -} - -} // namespace ec diff --git a/bindings/equivalence_criterion.cpp b/bindings/equivalence_criterion.cpp deleted file mode 100644 index 19acc29a..00000000 --- a/bindings/equivalence_criterion.cpp +++ /dev/null @@ -1,36 +0,0 @@ -/* - * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM - * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH - * All rights reserved. - * - * SPDX-License-Identifier: MIT - * - * Licensed under the MIT License - */ - -#include "EquivalenceCriterion.hpp" - -#include - -namespace ec { - -namespace nb = nanobind; -using namespace nb::literals; - -// NOLINTNEXTLINE(misc-use-internal-linkage) -void registerEquivalenceCriterion(const nb::module_& m) { - nb::enum_(m, "EquivalenceCriterion", - nb::is_arithmetic()) - .value("no_information", EquivalenceCriterion::NoInformation) - .value("not_equivalent", EquivalenceCriterion::NotEquivalent) - .value("equivalent", EquivalenceCriterion::Equivalent) - .value("equivalent_up_to_phase", - EquivalenceCriterion::EquivalentUpToPhase) - .value("equivalent_up_to_global_phase", - EquivalenceCriterion::EquivalentUpToGlobalPhase) - .value("probably_equivalent", EquivalenceCriterion::ProbablyEquivalent) - .value("probably_not_equivalent", - EquivalenceCriterion::ProbablyNotEquivalent); -} - -} // namespace ec diff --git a/bindings/qcec_patterns.txt b/bindings/qcec_patterns.txt new file mode 100644 index 00000000..55bcfafb --- /dev/null +++ b/bindings/qcec_patterns.txt @@ -0,0 +1,3 @@ +_hashable_values_: + +_unhashable_values_map_: diff --git a/bindings/register_application_scheme.cpp b/bindings/register_application_scheme.cpp new file mode 100644 index 00000000..21bb092f --- /dev/null +++ b/bindings/register_application_scheme.cpp @@ -0,0 +1,70 @@ +/* + * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM + * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH + * All rights reserved. + * + * SPDX-License-Identifier: MIT + * + * Licensed under the MIT License + */ + +#include "checker/dd/applicationscheme/ApplicationScheme.hpp" + +#include + +namespace ec { + +namespace nb = nanobind; +using namespace nb::literals; + +// NOLINTNEXTLINE(misc-use-internal-linkage) +void registerApplicationScheme(const nb::module_& m) { + nb::enum_( + m, "ApplicationScheme", nb::is_arithmetic(), + R"pb(Describes the order in which the individual operations of both circuits are applied during the equivalence check. + +In case of the alternating equivalence checker, this is the key component to allow the intermediate decision diagrams to remain close to the identity (as proposed in :cite:p:`burgholzer2021advanced`). +See :doc:`/compilation_flow_verification` for more information on the dedicated application scheme for verifying compilation flow results (as proposed in :cite:p:`burgholzer2020verifyingResultsIBM`). + +In case of the other checkers, which consider both circuits individually, using a non-sequential application scheme can significantly boost the operation caching performance in the underlying decision diagram package.)pb") + + .value( + "sequential", ApplicationSchemeType::Sequential, + R"pb(Applies all gates from the first circuit, before proceeding with the second circuit. + +Referred to as *"reference"* in :cite:p:`burgholzer2021advanced`.)pb") + + .value("reference", ApplicationSchemeType::Sequential, + R"pb(Alias for :attr:`~ApplicationScheme.sequential`.)pb") + + .value( + "one_to_one", ApplicationSchemeType::OneToOne, + R"pb(Alternates between applications from the first and the second circuit. + +Referred to as *"naive"* in :cite:p:`burgholzer2021advanced`.)pb") + + .value("naive", ApplicationSchemeType::OneToOne, + R"pb(Alias for :attr:`~ApplicationScheme.one_to_one`.)pb") + + .value( + "lookahead", ApplicationSchemeType::Lookahead, + R"pb(Looks whether an application from the first circuit or the second circuit yields the smaller decision diagram. + +Only works for the alternating equivalence checker.)pb") + + .value( + "gate_cost", ApplicationSchemeType::GateCost, + R"pb(Each gate of the first circuit is associated with a corresponding cost according to some cost function *f(...)*. +Whenever a gate *g* from the first circuit is applied *f(g)* gates are applied from the second circuit. + +Referred to as *"compilation_flow"* in :cite:p:`burgholzer2020verifyingResultsIBM`.)pb") + + .value("compilation_flow", ApplicationSchemeType::GateCost, + R"pb(Alias for :attr:`~ApplicationScheme.gate_cost`.)pb") + + .value( + "proportional", ApplicationSchemeType::Proportional, + R"pb(Alternates between applications from the first and the second circuit, but applies the gates in proportion to the number of gates in each circuit.)pb"); +} + +} // namespace ec diff --git a/bindings/register_configuration.cpp b/bindings/register_configuration.cpp new file mode 100644 index 00000000..9223baa3 --- /dev/null +++ b/bindings/register_configuration.cpp @@ -0,0 +1,299 @@ +/* + * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM + * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH + * All rights reserved. + * + * SPDX-License-Identifier: MIT + * + * Licensed under the MIT License + */ + +#include "Configuration.hpp" + +#include +#include // NOLINT(misc-include-cleaner) + +namespace ec { + +namespace nb = nanobind; +using namespace nb::literals; + +// NOLINTNEXTLINE(misc-use-internal-linkage) +void registerConfiguration(const nb::module_& m) { + // Class definitions + auto configuration = nb::class_( + m, "Configuration", R"pb(Provides all the means to configure QCEC. + +All options are split into the following categories: + +- :class:`.Execution` +- :class:`.Optimizations` +- :class:`.Application` +- :class:`.Functionality` +- :class:`.Simulation` +- :class:`.Parameterized` + +All options can be passed to the :func:`.verify` and :func:`.verify_compilation` functions as keyword arguments. +There, they are incorporated into the :class:`.Configuration` using the :func:`~.configuration.augment_config_from_kwargs` function.)pb"); + + auto execution = nb::class_( + configuration, "Execution", + R"pb(Options that orchestrate the :meth:`~.EquivalenceCheckingManager.run` method.)pb"); + + auto optimizations = nb::class_( + configuration, "Optimizations", + R"pb(Options that influence which circuit optimizations are applied during pre-processing.)pb"); + + auto application = nb::class_( + configuration, "Application", + R"pb(Options describing the :class:`.ApplicationScheme` used for the individual equivalence checkers.)pb"); + + auto functionality = nb::class_( + configuration, "Functionality", + R"pb(Options for all checkers that consider the whole functionality of a circuit.)pb"); + + auto simulation = nb::class_( + configuration, "Simulation", + R"pb(Options that influence the simulation checker.)pb"); + + auto parameterized = nb::class_( + configuration, "Parameterized", + R"pb(Options that influence the equivalence checking scheme for parameterized circuits.)pb"); + + // Configuration + configuration.def(nb::init<>(), "Initializes the configuration.") + .def_rw("execution", &Configuration::execution) + .def_rw("optimizations", &Configuration::optimizations) + .def_rw("application", &Configuration::application) + .def_rw("functionality", &Configuration::functionality) + .def_rw("simulation", &Configuration::simulation) + .def_rw("parameterized", &Configuration::parameterized) + .def( + "json", + [](const Configuration& config) { + const auto json = nb::module_::import_("json"); + const auto loads = json.attr("loads"); + const auto dict = loads(config.json().dump()); + return nb::cast>(dict); + }, + R"pb(Returns a JSON-style dictionary of the configuration.)pb") + .def("__repr__", &Configuration::toString); + + // execution options + execution.def(nb::init<>()) + .def_rw( + "parallel", &Configuration::Execution::parallel, + R"pb(Set whether execution should happen in parallel. Defaults to :code:`True`.)pb") + + .def_rw( + "nthreads", &Configuration::Execution::nthreads, + R"pb(Set the maximum number of threads to use. Defaults to the maximum number of available threads reported by the OS.)pb") + + .def_rw( + "timeout", &Configuration::Execution::timeout, + R"pb(Set a timeout for :meth:`~.EquivalenceCheckingManager.run` (in seconds). + +Defaults to :code:`0.`, which means no timeout. + +.. note:: + + Timeouts in QCEC work by checking an atomic flag in between the application of gates (for DD-based checkers) or rewrite rules (for the ZX-based checkers). + Unfortunately, this means that an operation needs to be fully applied before a timeout can set in. + If a certain operation during the equivalence check takes a very long time (e.g., because the DD is becoming very large), the timeout will not be triggered until that operation is finished. + Thus, it is possible that the timeout is not triggered at the expected time, and it might seem like the timeout is being ignored. + + Unfortunately, there is no clean way to kill a thread without letting it finish its computation. + That's something that could be made possible by switching from multi-threading to multi-processing, but the overhead of processes versus threads is huge on certain platforms and that would not be a good trade-off. + In addition, more fine-grained abortion checks would significantly decrease the overall performance due to all the branching that would be necessary. + + Consequently, timeouts in QCEC are a best-effort feature, and they should not be relied upon to always work as expected. + From experience, they tend to work reliably well for the ZX-based checkers, but they are less reliable for the DD-based checkers.)pb") + .def_rw("run_construction_checker", + &Configuration::Execution::runConstructionChecker, + R"pb(Set whether the construction checker should be executed. + +Defaults to :code:`False` since the alternating checker is to be preferred in most cases.)pb") + + .def_rw("run_simulation_checker", + &Configuration::Execution::runSimulationChecker, + R"pb(Set whether the simulation checker should be executed. + +Defaults to :code:`True` since simulations can quickly show the non-equivalence of circuits in many cases.)pb") + + .def_rw("run_alternating_checker", + &Configuration::Execution::runAlternatingChecker, + R"pb(Set whether the alternating checker should be executed. + +Defaults to :code:`True` since staying close to the identity can quickly show the equivalence of circuits in many cases.)pb") + + .def_rw("run_zx_checker", &Configuration::Execution::runZXChecker, + R"pb(Set whether the ZX-calculus checker should be executed. + +Defaults to :code:`True` but arbitrary multi-controlled operations are only partially supported.)pb") + + .def_rw( + "numerical_tolerance", &Configuration::Execution::numericalTolerance, + R"pb(Set the numerical tolerance of the underlying decision diagram package. + +Defaults to :code:`2e-13` and should only be changed by users who know what they are doing.)pb") + + .def_rw("set_all_ancillae_garbage", + &Configuration::Execution::setAllAncillaeGarbage, + R"pb(Set whether all ancillae should be treated as garbage qubits. + +Defaults to :code:`False` but the ZX-calculus checker will not be able to handle circuits with non-garbage ancillae.)pb"); + + // optimization options + optimizations.def(nb::init<>()) + .def_rw( + "fuse_single_qubit_gates", + &Configuration::Optimizations::fuseSingleQubitGates, + R"pb(Fuse consecutive single-qubit gates by grouping them together. + +Defaults to :code:`True` as this typically increases the performance of the subsequent equivalence check.)pb") + + .def_rw( + "reconstruct_swaps", &Configuration::Optimizations::reconstructSWAPs, + R"pb(Try to reconstruct SWAP gates that have been decomposed (into a sequence of 3 CNOT gates) or optimized away (as a consequence of a SWAP preceded or followed by a CNOT on the same qubits). + + Defaults to :code:`True` since this reconstruction enables the efficient tracking of logical to physical qubit permutations throughout circuits that have been mapped to a target architecture.)pb") + + .def_rw("remove_diagonal_gates_before_measure", + &Configuration::Optimizations::removeDiagonalGatesBeforeMeasure, + R"pb(Remove any diagonal gates at the end of the circuit. + +This might be desirable since any diagonal gate in front of a measurement does not influence the probabilities of the respective states. + +Defaults to :code:`False` since, in general, circuits differing by diagonal gates at the end should still be considered non-equivalent.)pb") + + .def_rw( + "transform_dynamic_circuit", + &Configuration::Optimizations::transformDynamicCircuit, + R"pb(Circuits containing dynamic circuit primitives such as mid-circuit measurements, resets, or classically-controlled operations cannot be verified in a straight-forward fashion due to the non-unitary nature of these primitives, which is why this setting defaults to :code:`False`. + +By enabling this optimization, any dynamic circuit is first transformed to a circuit without non-unitary primitives by, first, substituting qubit resets with new qubits and, then, applying the deferred measurement principle to defer measurements to the end.)pb") + + .def_rw( + "reorder_operations", + &Configuration::Optimizations::reorderOperations, + R"pb(The operations of a circuit are stored in a sequential container. + +This introduces some dependencies in the order of operations that are not naturally present in the quantum circuit. +As a consequence, two quantum circuits that contain exactly the same operations, list their operations in different ways, also apply there operations in a different order. +This optimization pass established a canonical ordering of operations by, first, constructing a directed, acyclic graph for the operations and, then, traversing it in a breadth-first fashion. + +Defaults to :code:`True`.)pb") + + .def_rw( + "backpropagate_output_permutation", + &Configuration::Optimizations::backpropagateOutputPermutation, + R"pb(Backpropagate the output permutation to the input permutation. + +Defaults to :code:`False` since this might mess up the initially given input permutation. +Can be helpful for dynamic quantum circuits that have been transformed to a static circuit by enabling the :attr:`~.Configuration.Optimizations.transform_dynamic_circuit` optimization.)pb") + + .def_rw( + "elide_permutations", + &Configuration::Optimizations::elidePermutations, + R"pb(Elide permutations from the circuit by permuting the qubits in the circuit and eliminating SWAP gates from the circuits. + +Defaults to :code:`True` as this typically boosts performance.)pb"); + + // application options + application.def(nb::init<>()) + .def_rw( + "construction_scheme", + &Configuration::Application::constructionScheme, + R"pb(The :class:`.ApplicationScheme` used for the construction checker.)pb") + + .def_rw( + "simulation_scheme", &Configuration::Application::simulationScheme, + R"pb(The :class:`.ApplicationScheme` used for the simulation checker.)pb") + + .def_rw( + "alternating_scheme", &Configuration::Application::alternatingScheme, + R"pb(The :class:`.ApplicationScheme` used for the alternating checker.)pb") + + .def_rw( + "profile", &Configuration::Application::profile, + R"pb(The :attr:`Gate Cost <.ApplicationScheme.gate_cost>` application scheme can be configured with a profile that specifies the cost of gates. + +This profile can be set via a file constructed like a lookup table. +Every line :code:` ` specifies the cost for a given gate type and with a certain number of controls, e.g., :code:`X 0 1` denotes that a single-qubit X gate has a cost of :code:`1`, while :code:`X 2 15` denotes that a Toffoli gate has a cost of :code:`15`.)pb"); + + // functionality options + functionality.def(nb::init<>()) + .def_rw( + "trace_threshold", &Configuration::Functionality::traceThreshold, + R"pb(While decision diagrams are canonical in theory, i.e., equivalent circuits produce equivalent decision diagrams, numerical inaccuracies and approximations can harm this property. + +This can result in a scenario where two decision diagrams are really close to one another, but cannot be identified as such by standard methods (i.e., comparing their root pointers). +Instead, for two decision diagrams :code:`U` and :code:`U'` representing the functionalities of two circuits :code:`G` and :code:`G'`, the trace of the product of one decision diagram with the inverse of the other can be computed and compared to the trace of the identity. + +Alternatively, it can be checked, whether :code:`U*U`^-1` is \"close enough\" to the identity by recursively checking that each decision diagram node is close enough to the identity structure (i.e., the first and last successor have weights close to one, while the second and third successor have weights close to zero). +Whenever any decision diagram node differs from this structure by more than the configured threshold, the circuits are concluded to be non-equivalent. + +Defaults to :code:`1e-8`.)pb") + + .def_rw( + "check_partial_equivalence", + &Configuration::Functionality::checkPartialEquivalence, + R"pb(Two circuits are partially equivalent if, for each possible initial input state, they have the same probability for each measurement outcome. + +If set to :code:`True`, a check for partial equivalence will be performed and the contributions of garbage qubits to the circuit are ignored. +If set to :code:`False`, the checker will output 'not equivalent' for circuits that are partially equivalent but not totally equivalent. +In particular, garbage qubits will be treated as if they were measured qubits. + +Defaults to :code:`False`.)pb"); + + // simulation options + simulation.def(nb::init<>()) + .def_rw( + "fidelity_threshold", &Configuration::Simulation::fidelityThreshold, + R"pb(Similar to :attr:`~.Configuration.Functionality.trace_threshold`, this setting is here to tackle numerical inaccuracies in the simulation checker. + +Instead of computing a trace, the fidelity between the states resulting from the simulation is computed. +Whenever the fidelity differs from :code:`1.` by more than the configured threshold, the circuits are concluded to be non-equivalent. + +Defaults to :code:`1e-8`.)pb") + + .def_rw( + "max_sims", &Configuration::Simulation::maxSims, + R"pb(The maximum number of simulations to be started for the simulation checker. + +In practice, just a couple of simulations suffice in most cases to detect a potential non-equivalence. +Either defaults to :code:`16` or the maximum number of available threads minus 2, whichever is more.)pb") + + .def_rw( + "state_type", &Configuration::Simulation::stateType, + R"pb(The :class:`type of states <.StateType>` used for the simulations in the simulation checker. + +Defaults to :attr:`.StateType.computational_basis`.)pb") + + .def_rw("seed", &Configuration::Simulation::seed, + R"pb(The seed used in the quantum state generator. + +Defaults to :code:`0`, which means that the seed is chosen non-deterministically for each program run.)pb"); + + // parameterized options + parameterized.def(nb::init<>()) + .def_rw( + "parameterized_tolerance", + &Configuration::Parameterized::parameterizedTol, + R"pb(Set threshold below which instantiated parameters shall be considered zero. + +Defaults to :code:`1e-12`.)pb") + + .def_rw( + "additional_instantiations", + &Configuration::Parameterized::nAdditionalInstantiations, + R"pb(Number of instantiations shall be performed in addition to the default ones. + +For parameterized circuits that cannot be shown to be equivalent by the ZX checker the circuits are instantiated with concrete values for parameters and subsequently checked with QCEC's default schemes. +The first instantiation tries to set as many gate parameters to 0. +The last instantiations initializes the parameters with random values to guarantee completeness of the equivalence check. +Because random instantiation is costly, additional instantiations can be performed that lead to simpler equivalence checking instances as the random instantiation. +This option changes how many of those additional checks are performed.)pb"); +} + +} // namespace ec diff --git a/bindings/register_equivalence_checking_manager.cpp b/bindings/register_equivalence_checking_manager.cpp new file mode 100644 index 00000000..ce254d9a --- /dev/null +++ b/bindings/register_equivalence_checking_manager.cpp @@ -0,0 +1,187 @@ +/* + * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM + * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH + * All rights reserved. + * + * SPDX-License-Identifier: MIT + * + * Licensed under the MIT License + */ + +#include "Configuration.hpp" +#include "EquivalenceCheckingManager.hpp" +#include "EquivalenceCriterion.hpp" +#include "checker/dd/applicationscheme/ApplicationScheme.hpp" +#include "ir/QuantumComputation.hpp" + +#include +#include // NOLINT(misc-include-cleaner) +#include // NOLINT(misc-include-cleaner) +#include // NOLINT(misc-include-cleaner) +#include + +namespace ec { + +namespace nb = nanobind; +using namespace nb::literals; + +// NOLINTNEXTLINE(misc-use-internal-linkage) +void registerEquivalenceCheckingManager(const nb::module_& m) { + nb::module_::import_("mqt.core.dd"); + + // Class definitions + auto ecm = nb::class_( + m, "EquivalenceCheckingManager", R"pb(The main class of QCEC. + +Allows checking the equivalence of quantum circuits based on the methods proposed in :cite:p:`burgholzer2021advanced`. +It features many configuration options that orchestrate the procedure.)pb"); + + auto results = nb::class_( + ecm, "Results", + R"pb(Captures the main results and statistics from :meth:`~.EquivalenceCheckingManager.run`.)pb"); + + // Constructors + ecm.def( + nb::init(), + "circ1"_a, "circ2"_a, "config"_a = Configuration(), + R"pb(Create an equivalence checking manager for two circuits and configure it with a :class:`.Configuration` object.)pb"); + + // Access to circuits + ecm.def_prop_ro("qc1", &EquivalenceCheckingManager::getFirstCircuit, + nb::rv_policy::reference_internal, + R"pb(The first circuit to be checked.)pb"); + ecm.def_prop_ro("qc2", &EquivalenceCheckingManager::getSecondCircuit, + nb::rv_policy::reference_internal, + R"pb(The second circuit to be checked.)pb"); + + // Access to configuration + ecm.def_prop_rw( + "configuration", &EquivalenceCheckingManager::getConfiguration, + [](EquivalenceCheckingManager& manager, const Configuration& config) { + manager.getConfiguration() = config; + }, + nb::rv_policy::reference_internal, + R"pb(The configuration of the equivalence checking manager.)pb"); + + // Run + ecm.def("run", &EquivalenceCheckingManager::run, + R"pb(Execute the equivalence check as configured.)pb"); + + // Results + ecm.def_prop_ro("results", &EquivalenceCheckingManager::getResults, + nb::rv_policy::reference_internal, + R"pb(The results of the equivalence check.)pb"); + + ecm.def_prop_ro( + "equivalence", &EquivalenceCheckingManager::equivalence, + R"pb(The :class:`.EquivalenceCriterion` determined as the result of the equivalence check.)pb"); + + // Convenience functions + // Execution + ecm.def("disable_all_checkers", + &EquivalenceCheckingManager::disableAllCheckers, + R"pb(Disable all equivalence checkers.)pb") + + // Application + .def( + "set_application_scheme", + &EquivalenceCheckingManager::setApplicationScheme, + "scheme"_a = ApplicationSchemeType::Proportional, + R"pb(Set the :class:`.ApplicationScheme` used for all checkers (based on decision diagrams). + +Args: + scheme: The application scheme. Defaults to :attr:`.ApplicationScheme.proportional`.)pb") + + .def( + "set_gate_cost_profile", + &EquivalenceCheckingManager::setGateCostProfile, "profile"_a = "", + R"pb(Set the :attr:`profile <.Configuration.Application.profile>` used in the :attr:`Gate Cost <.ApplicationScheme.gate_cost>` application scheme for all checkers (based on decision diagrams). + +Args: + profile: The path to the profile file.)pb") + + .def("__repr__", [](const EquivalenceCheckingManager& manager) { + return ""; + }); + + // EquivalenceCheckingManager::Results bindings + results + .def(nb::init<>(), "Initializes the results.") + + .def_rw("preprocessing_time", + &EquivalenceCheckingManager::Results::preprocessingTime, + R"pb(Time spent during preprocessing (in seconds).)pb") + + .def_rw("check_time", &EquivalenceCheckingManager::Results::checkTime, + R"pb(Time spent during equivalence check (in seconds).)pb") + + .def_rw("equivalence", &EquivalenceCheckingManager::Results::equivalence, + R"pb(Final result of the equivalence check.)pb") + + .def_rw("started_simulations", + &EquivalenceCheckingManager::Results::startedSimulations, + R"pb(Number of simulations that have been started.)pb") + + .def_rw("performed_simulations", + &EquivalenceCheckingManager::Results::performedSimulations, + R"pb(Number of simulations that have been finished.)pb") + + .def_rw( + "cex_input", &EquivalenceCheckingManager::Results::cexInput, + R"pb(DD representation of the initial state that produced a counterexample.)pb") + + .def_rw( + "cex_output1", &EquivalenceCheckingManager::Results::cexOutput1, + R"pb(DD representation of the first circuit's counterexample output state.)pb") + + .def_rw( + "cex_output2", &EquivalenceCheckingManager::Results::cexOutput2, + R"pb(DD representation of the second circuit's counterexample output state.)pb") + + .def_rw( + "performed_instantiations", + &EquivalenceCheckingManager::Results::performedInstantiations, + R"pb(Number of circuit instantiations performed during equivalence checking of parameterized quantum circuits.)pb") + + .def_prop_rw( + "checker_results", + [](const EquivalenceCheckingManager::Results& results) { + const auto json = nb::module_::import_("json"); + const auto loads = json.attr("loads"); + const auto dict = loads(results.checkerResults.dump()); + return nb::cast>(dict); + }, + [](EquivalenceCheckingManager::Results& results, + const nb::dict& value) { + const auto json = nb::module_::import_("json"); + const auto dumps = json.attr("dumps"); + const auto jsonString = nb::cast(dumps(value)); + results.checkerResults = nlohmann::json::parse(jsonString); + }, + R"pb(Dictionary of the results of the individual checkers.)pb") + + .def( + "considered_equivalent", + &EquivalenceCheckingManager::Results::consideredEquivalent, + R"pb(Convenience function to check whether the result is considered equivalent.)pb") + + .def( + "json", + [](const EquivalenceCheckingManager::Results& results) { + const auto json = nb::module_::import_("json"); + const auto loads = json.attr("loads"); + const auto dict = loads(results.json().dump()); + return nb::cast>(dict); + }, + R"pb(Returns a JSON-style dictionary of the results.)pb") + + .def("__str__", &EquivalenceCheckingManager::Results::toString) + .def("__repr__", [](const EquivalenceCheckingManager::Results& res) { + return ""; + }); +} + +} // namespace ec diff --git a/bindings/register_equivalence_criterion.cpp b/bindings/register_equivalence_criterion.cpp new file mode 100644 index 00000000..b556afbd --- /dev/null +++ b/bindings/register_equivalence_criterion.cpp @@ -0,0 +1,58 @@ +/* + * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM + * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH + * All rights reserved. + * + * SPDX-License-Identifier: MIT + * + * Licensed under the MIT License + */ + +#include "EquivalenceCriterion.hpp" + +#include + +namespace ec { + +namespace nb = nanobind; +using namespace nb::literals; + +// NOLINTNEXTLINE(misc-use-internal-linkage) +void registerEquivalenceCriterion(const nb::module_& m) { + nb::enum_( + m, "EquivalenceCriterion", nb::is_arithmetic(), + R"pb(Captures all the different notions of equivalence that can be the result of a :meth:`~.EquivalenceCheckingManager.run`.)pb") + + .value("no_information", EquivalenceCriterion::NoInformation, + R"pb(No information on the equivalence is available. + +This can be because the check has not been run or that a timeout happened.)pb") + + .value("not_equivalent", EquivalenceCriterion::NotEquivalent, + R"pb(Circuits are shown to be non-equivalent.)pb") + + .value("equivalent", EquivalenceCriterion::Equivalent, + R"pb(Circuits are shown to be equivalent.)pb") + + .value("equivalent_up_to_phase", + EquivalenceCriterion::EquivalentUpToPhase, + R"pb(Circuits are equivalent up to a global phase factor.)pb") + + .value( + "equivalent_up_to_global_phase", + EquivalenceCriterion::EquivalentUpToGlobalPhase, + R"pb(Circuits are equivalent up to a certain (global or relative) phase.)pb") + + .value("probably_equivalent", EquivalenceCriterion::ProbablyEquivalent, + R"pb(Circuits are probably equivalent. + +A result obtained whenever a couple of simulations did not show the non-equivalence in the simulation checker.)pb") + + .value("probably_not_equivalent", + EquivalenceCriterion::ProbablyNotEquivalent, + R"pb(Circuits are probably not equivalent. + +A result obtained whenever the ZX-calculus checker could not reduce the combined circuit to the identity.)pb"); +} + +} // namespace ec diff --git a/bindings/register_state_type.cpp b/bindings/register_state_type.cpp new file mode 100644 index 00000000..191b88b7 --- /dev/null +++ b/bindings/register_state_type.cpp @@ -0,0 +1,54 @@ +/* + * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM + * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH + * All rights reserved. + * + * SPDX-License-Identifier: MIT + * + * Licensed under the MIT License + */ + +#include "checker/dd/simulation/StateType.hpp" + +#include + +namespace ec { + +namespace nb = nanobind; +using namespace nb::literals; + +// NOLINTNEXTLINE(misc-use-internal-linkage) +void registerStateType(const nb::module_& m) { + nb::enum_( + m, "StateType", nb::is_arithmetic(), + R"pb(The type of states used in the simulation checker allows trading off efficiency versus performance. + +- Classical stimuli (i.e., random *computational basis states*) already offer extremely high error detection rates in general and are comparatively fast to simulate, which makes them the default. +- Local quantum stimuli (i.e., random *single-qubit basis states*) are a little bit more computationally intensive, but provide even better error detection rates. +- Global quantum stimuli (i.e., random *stabilizer states*) offer the highest available error detection rate, while at the same time incurring the highest computational effort. + +For details, see :cite:p:`burgholzer2021randomStimuliGenerationQuantum`.)pb") + + .value( + "computational_basis", StateType::ComputationalBasis, + R"pb(Randomly choose computational basis states. Also referred to as "*classical*".)pb") + + .value("classical", StateType::ComputationalBasis, + R"pb(Alias for :attr:`~StateType.computational_basis`.)pb") + + .value( + "random_1q_basis", StateType::Random1QBasis, + R"pb(Randomly choose a single-qubit basis state for each qubit from the six-tuple *(|0>, |1>, |+>, |->, |L>, |R>)*. Also referred to as *"local_random"*.)pb") + + .value("local_quantum", StateType::Random1QBasis, + R"pb(Alias for :attr:`~StateType.random_1q_basis`.)pb") + + .value( + "stabilizer", StateType::Stabilizer, + R"pb(Randomly choose a stabilizer state by creating a random Clifford circuit. Also referred to as *"global_random"*.)pb") + + .value("global_quantum", StateType::Stabilizer, + R"pb(Alias for :attr:`~StateType.stabilizer`.)pb"); +} + +} // namespace ec diff --git a/bindings/state_type.cpp b/bindings/state_type.cpp deleted file mode 100644 index d097d709..00000000 --- a/bindings/state_type.cpp +++ /dev/null @@ -1,31 +0,0 @@ -/* - * Copyright (c) 2023 - 2026 Chair for Design Automation, TUM - * Copyright (c) 2025 - 2026 Munich Quantum Software Company GmbH - * All rights reserved. - * - * SPDX-License-Identifier: MIT - * - * Licensed under the MIT License - */ - -#include "checker/dd/simulation/StateType.hpp" - -#include - -namespace ec { - -namespace nb = nanobind; -using namespace nb::literals; - -// NOLINTNEXTLINE(misc-use-internal-linkage) -void registerStateType(const nb::module_& m) { - nb::enum_(m, "StateType", nb::is_arithmetic()) - .value("computational_basis", StateType::ComputationalBasis) - .value("classical", StateType::ComputationalBasis) - .value("random_1Q_basis", StateType::Random1QBasis) - .value("local_quantum", StateType::Random1QBasis) - .value("stabilizer", StateType::Stabilizer) - .value("global_quantum", StateType::Stabilizer); -} - -} // namespace ec diff --git a/noxfile.py b/noxfile.py index 914dc0f7..3e3e81d5 100755 --- a/noxfile.py +++ b/noxfile.py @@ -21,6 +21,7 @@ import shutil import sys import tempfile +from pathlib import Path from typing import TYPE_CHECKING import nox @@ -187,5 +188,54 @@ def docs(session: nox.Session) -> None: ) +@nox.session(reuse_venv=True, venv_backend="uv") +def stubs(session: nox.Session) -> None: + """Generate type stubs for Python bindings using nanobind.""" + env = {"UV_PROJECT_ENVIRONMENT": session.virtualenv.location} + session.run( + "uv", + "sync", + "--no-dev", + "--group", + "build", + env=env, + ) + + package_root = Path(__file__).parent / "python" / "mqt" / "qcec" + pattern_file = Path(__file__).parent / "bindings" / "qcec_patterns.txt" + + session.run( + "python", + "-m", + "nanobind.stubgen", + "--recursive", + "--include-private", + "--output-dir", + package_root, + "--pattern-file", + pattern_file, + "--module", + "mqt.qcec.pyqcec", + ) + + pyi_files = list(package_root.glob("**/*.pyi")) + + if not pyi_files: + session.warn("No .pyi files found") + return + + if shutil.which("prek") is None: + session.install("prek") + + # Allow both 0 (no issues) and 1 as success codes for fixing up stubs + success_codes = [0, 1] + session.run("prek", "run", "license-tools", "--files", *pyi_files, external=True, success_codes=success_codes) + session.run("prek", "run", "ruff-check", "--files", *pyi_files, external=True, success_codes=success_codes) + session.run("prek", "run", "ruff-format", "--files", *pyi_files, external=True, success_codes=success_codes) + + # Run ruff-check again to ensure everything is clean + session.run("prek", "run", "ruff-check", "--files", *pyi_files, external=True) + + if __name__ == "__main__": nox.main() diff --git a/pyproject.toml b/pyproject.toml index 6d4c82c4..818c2b85 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -264,7 +264,7 @@ known-first-party = ["mqt.qcec"] "docs/**" = ["T20"] "noxfile.py" = ["T20", "TID251"] "python/mqt/qcec/_compat/**.py" = ["TID251"] -"*.pyi" = ["D418", "DOC202", "PYI011", "PYI021"] +"*.pyi" = ["D418", "E501", "PYI021"] "*.ipynb" = [ "D", # pydocstyle "E402", # Allow imports to appear anywhere in Jupyter notebooks diff --git a/python/mqt/qcec/pyqcec.pyi b/python/mqt/qcec/pyqcec.pyi index 6d095bd9..192a13c6 100644 --- a/python/mqt/qcec/pyqcec.pyi +++ b/python/mqt/qcec/pyqcec.pyi @@ -6,15 +6,13 @@ # # Licensed under the MIT License -"""Python bindings module for QCEC.""" - -from enum import Enum +import enum from typing import Any -from mqt.core.dd import VectorDD -from mqt.core.ir import QuantumComputation +import mqt.core.dd +import mqt.core.ir -class ApplicationScheme(Enum): +class ApplicationScheme(enum.IntEnum): """Describes the order in which the individual operations of both circuits are applied during the equivalence check. In case of the alternating equivalence checker, this is the key component to allow the intermediate decision diagrams to remain close to the identity (as proposed in :cite:p:`burgholzer2021advanced`). @@ -23,31 +21,34 @@ class ApplicationScheme(Enum): In case of the other checkers, which consider both circuits individually, using a non-sequential application scheme can significantly boost the operation caching performance in the underlying decision diagram package. """ - sequential = ... - """Applies all gates from the first circuit, before proceeding with the second circuit. + sequential = 0 + """ + Applies all gates from the first circuit, before proceeding with the second circuit. Referred to as *"reference"* in :cite:p:`burgholzer2021advanced`. """ - reference = ... + reference = 0 """Alias for :attr:`~ApplicationScheme.sequential`.""" - one_to_one = ... - """Alternates between applications from the first and the second circuit. + one_to_one = 1 + """ + Alternates between applications from the first and the second circuit. Referred to as *"naive"* in :cite:p:`burgholzer2021advanced`. """ - naive = ... + naive = 1 """Alias for :attr:`~ApplicationScheme.one_to_one`.""" - lookahead = ... - """Looks whether an application from the first circuit or the second circuit yields the smaller decision diagram. + lookahead = 2 + """ + Looks whether an application from the first circuit or the second circuit yields the smaller decision diagram. Only works for the alternating equivalence checker. """ - gate_cost = ... + gate_cost = 3 """ Each gate of the first circuit is associated with a corresponding cost according to some cost function *f(...)*. Whenever a gate *g* from the first circuit is applied *f(g)* gates are applied from the second circuit. @@ -55,11 +56,13 @@ class ApplicationScheme(Enum): Referred to as *"compilation_flow"* in :cite:p:`burgholzer2020verifyingResultsIBM`. """ - compilation_flow = ... + compilation_flow = 3 """Alias for :attr:`~ApplicationScheme.gate_cost`.""" - proportional = ... - """Alternates between applications from the first and the second circuit, but applies the gates in proportion to the number of gates in each circuit.""" + proportional = 4 + """ + Alternates between applications from the first and the second circuit, but applies the gates in proportion to the number of gates in each circuit. + """ class Configuration: """Provides all the means to configure QCEC. @@ -77,237 +80,340 @@ class Configuration: There, they are incorporated into the :class:`.Configuration` using the :func:`~.configuration.augment_config_from_kwargs` function. """ + def __init__(self) -> None: + """Initializes the configuration.""" + class Execution: """Options that orchestrate the :meth:`~.EquivalenceCheckingManager.run` method.""" - parallel: bool = True - """Set whether execution should happen in parallel. Defaults to :code:`True`.""" - - nthreads: int - """Set the maximum number of threads to use. Defaults to the maximum number of available threads reported by the OS.""" - - timeout: float = 0.0 - """Set a timeout for :meth:`~.EquivalenceCheckingManager.run` (in seconds). - - Defaults to :code:`0.`, which means no timeout. - - .. note:: - - Timeouts in QCEC work by checking an atomic flag in between the application of gates (for DD-based checkers) or rewrite rules (for the ZX-based checkers). - Unfortunately, this means that an operation needs to be fully applied before a timeout can set in. - If a certain operation during the equivalence check takes a very long time (e.g., because the DD is becoming very large), the timeout will not be triggered until that operation is finished. - Thus, it is possible that the timeout is not triggered at the expected time, and it might seem like the timeout is being ignored. - - Unfortunately, there is no clean way to kill a thread without letting it finish its computation. - That's something that could be made possible by switching from multi-threading to multi-processing, but the overhead of processes versus threads is huge on certain platforms and that would not be a good trade-off. - In addition, more fine-grained abortion checks would significantly decrease the overall performance due to all the branching that would be necessary. - - Consequently, timeouts in QCEC are a best-effort feature, and they should not be relied upon to always work as expected. - From experience, they tend to work reliably well for the ZX-based checkers, but they are less reliable for the DD-based checkers. - """ - - run_construction_checker: bool = False - """Set whether the construction checker should be executed. - - Defaults to :code:`False` since the alternating checker is to be preferred in most cases. - """ - - run_simulation_checker: bool = True - """Set whether the simulation checker should be executed. - - Defaults to :code:`True` since simulations can quickly show the non-equivalence of circuits in many cases. - """ - - run_alternating_checker: bool = True - """ - Set whether the alternating checker should be executed. - - Defaults to :code:`True` since staying close to the identity can quickly show the equivalence of circuits in many cases. - """ - - run_zx_checker: bool = True - """Set whether the ZX-calculus checker should be executed. - - Defaults to :code:`True` but arbitrary multi-controlled operations are only partially supported. - """ - - numerical_tolerance: float = 2e-13 - """ - Set the numerical tolerance of the underlying decision diagram package. - - Defaults to :code:`2e-13` and should only be changed by users who know what they are doing. - """ - - set_all_ancillae_garbage: bool = False - """ - Set whether all ancillae should be treated as garbage qubits. - - Defaults to :code:`False` but the ZX-calculus checker will not be able to handle circuits with non-garbage ancillae. - """ - def __init__(self) -> None: ... + @property + def parallel(self) -> bool: + """Set whether execution should happen in parallel. Defaults to :code:`True`.""" + + @parallel.setter + def parallel(self, arg: bool, /) -> None: ... + @property + def nthreads(self) -> int: + """Set the maximum number of threads to use. Defaults to the maximum number of available threads reported by the OS.""" + + @nthreads.setter + def nthreads(self, arg: int, /) -> None: ... + @property + def timeout(self) -> float: + """Set a timeout for :meth:`~.EquivalenceCheckingManager.run` (in seconds). + + Defaults to :code:`0.`, which means no timeout. + + .. note:: + + Timeouts in QCEC work by checking an atomic flag in between the application of gates (for DD-based checkers) or rewrite rules (for the ZX-based checkers). + Unfortunately, this means that an operation needs to be fully applied before a timeout can set in. + If a certain operation during the equivalence check takes a very long time (e.g., because the DD is becoming very large), the timeout will not be triggered until that operation is finished. + Thus, it is possible that the timeout is not triggered at the expected time, and it might seem like the timeout is being ignored. + + Unfortunately, there is no clean way to kill a thread without letting it finish its computation. + That's something that could be made possible by switching from multi-threading to multi-processing, but the overhead of processes versus threads is huge on certain platforms and that would not be a good trade-off. + In addition, more fine-grained abortion checks would significantly decrease the overall performance due to all the branching that would be necessary. + + Consequently, timeouts in QCEC are a best-effort feature, and they should not be relied upon to always work as expected. + From experience, they tend to work reliably well for the ZX-based checkers, but they are less reliable for the DD-based checkers. + """ + + @timeout.setter + def timeout(self, arg: float, /) -> None: ... + @property + def run_construction_checker(self) -> bool: + """Set whether the construction checker should be executed. + + Defaults to :code:`False` since the alternating checker is to be preferred in most cases. + """ + + @run_construction_checker.setter + def run_construction_checker(self, arg: bool, /) -> None: ... + @property + def run_simulation_checker(self) -> bool: + """Set whether the simulation checker should be executed. + + Defaults to :code:`True` since simulations can quickly show the non-equivalence of circuits in many cases. + """ + + @run_simulation_checker.setter + def run_simulation_checker(self, arg: bool, /) -> None: ... + @property + def run_alternating_checker(self) -> bool: + """Set whether the alternating checker should be executed. + + Defaults to :code:`True` since staying close to the identity can quickly show the equivalence of circuits in many cases. + """ + + @run_alternating_checker.setter + def run_alternating_checker(self, arg: bool, /) -> None: ... + @property + def run_zx_checker(self) -> bool: + """Set whether the ZX-calculus checker should be executed. + + Defaults to :code:`True` but arbitrary multi-controlled operations are only partially supported. + """ + + @run_zx_checker.setter + def run_zx_checker(self, arg: bool, /) -> None: ... + @property + def numerical_tolerance(self) -> float: + """Set the numerical tolerance of the underlying decision diagram package. + + Defaults to :code:`2e-13` and should only be changed by users who know what they are doing. + """ + + @numerical_tolerance.setter + def numerical_tolerance(self, arg: float, /) -> None: ... + @property + def set_all_ancillae_garbage(self) -> bool: + """Set whether all ancillae should be treated as garbage qubits. + + Defaults to :code:`False` but the ZX-calculus checker will not be able to handle circuits with non-garbage ancillae. + """ + + @set_all_ancillae_garbage.setter + def set_all_ancillae_garbage(self, arg: bool, /) -> None: ... class Optimizations: """Options that influence which circuit optimizations are applied during pre-processing.""" - fuse_single_qubit_gates: bool = True - """Fuse consecutive single-qubit gates by grouping them together. + def __init__(self) -> None: ... + @property + def fuse_single_qubit_gates(self) -> bool: + """Fuse consecutive single-qubit gates by grouping them together. - Defaults to :code:`True` as this typically increases the performance of the subsequent equivalence check. - """ + Defaults to :code:`True` as this typically increases the performance of the subsequent equivalence check. + """ - reconstruct_swaps: bool = True - """Try to reconstruct SWAP gates that have been decomposed (into a sequence of 3 CNOT gates) or optimized away (as a consequence of a SWAP preceded or followed by a CNOT on the same qubits). + @fuse_single_qubit_gates.setter + def fuse_single_qubit_gates(self, arg: bool, /) -> None: ... + @property + def reconstruct_swaps(self) -> bool: + """Try to reconstruct SWAP gates that have been decomposed (into a sequence of 3 CNOT gates) or optimized away (as a consequence of a SWAP preceded or followed by a CNOT on the same qubits). - Defaults to :code:`True` since this reconstruction enables the efficient tracking of logical to physical qubit permutations throughout circuits that have been mapped to a target architecture. - """ + Defaults to :code:`True` since this reconstruction enables the efficient tracking of logical to physical qubit permutations throughout circuits that have been mapped to a target architecture. + """ - remove_diagonal_gates_before_measure: bool = False - """Remove any diagonal gates at the end of the circuit. + @reconstruct_swaps.setter + def reconstruct_swaps(self, arg: bool, /) -> None: ... + @property + def remove_diagonal_gates_before_measure(self) -> bool: + """Remove any diagonal gates at the end of the circuit. - This might be desirable since any diagonal gate in front of a measurement does not influence the probabilities of the respective states. + This might be desirable since any diagonal gate in front of a measurement does not influence the probabilities of the respective states. - Defaults to :code:`False` since, in general, circuits differing by diagonal gates at the end should still be considered non-equivalent. - """ + Defaults to :code:`False` since, in general, circuits differing by diagonal gates at the end should still be considered non-equivalent. + """ - transform_dynamic_circuit: bool = False - """Circuits containing dynamic circuit primitives such as mid-circuit measurements, resets, or classically-controlled operations cannot be verified in a straight-forward fashion due to the non-unitary nature of these primitives, which is why this setting defaults to :code:`False`. + @remove_diagonal_gates_before_measure.setter + def remove_diagonal_gates_before_measure(self, arg: bool, /) -> None: ... + @property + def transform_dynamic_circuit(self) -> bool: + """Circuits containing dynamic circuit primitives such as mid-circuit measurements, resets, or classically-controlled operations cannot be verified in a straight-forward fashion due to the non-unitary nature of these primitives, which is why this setting defaults to :code:`False`. - By enabling this optimization, any dynamic circuit is first transformed to a circuit without non-unitary primitives by, first, substituting qubit resets with new qubits and, then, applying the deferred measurement principle to defer measurements to the end. - """ + By enabling this optimization, any dynamic circuit is first transformed to a circuit without non-unitary primitives by, first, substituting qubit resets with new qubits and, then, applying the deferred measurement principle to defer measurements to the end. + """ - reorder_operations: bool = True - """The operations of a circuit are stored in a sequential container. - This introduces some dependencies in the order of operations that are not naturally present in the quantum circuit. - As a consequence, two quantum circuits that contain exactly the same operations, list their operations in different ways, also apply there operations in a different order. - This optimization pass established a canonical ordering of operations by, first, constructing a directed, acyclic graph for the operations and, then, traversing it in a breadth-first fashion. + @transform_dynamic_circuit.setter + def transform_dynamic_circuit(self, arg: bool, /) -> None: ... + @property + def reorder_operations(self) -> bool: + """The operations of a circuit are stored in a sequential container. - Defaults to :code:`True`. - """ + This introduces some dependencies in the order of operations that are not naturally present in the quantum circuit. + As a consequence, two quantum circuits that contain exactly the same operations, list their operations in different ways, also apply there operations in a different order. + This optimization pass established a canonical ordering of operations by, first, constructing a directed, acyclic graph for the operations and, then, traversing it in a breadth-first fashion. - backpropagate_output_permutation: bool = False - """Backpropagate the output permutation to the input permutation. + Defaults to :code:`True`. + """ - Defaults to :code:`False` since this might mess up the initially given input permutation. - Can be helpful for dynamic quantum circuits that have been transformed to a static circuit by enabling the :attr:`~.Configuration.Optimizations.transform_dynamic_circuit` optimization. - """ + @reorder_operations.setter + def reorder_operations(self, arg: bool, /) -> None: ... + @property + def backpropagate_output_permutation(self) -> bool: + """Backpropagate the output permutation to the input permutation. - elide_permutations: bool = True - """Elide permutations from the circuit by permuting the qubits in the circuit and eliminating SWAP gates from the circuits. + Defaults to :code:`False` since this might mess up the initially given input permutation. + Can be helpful for dynamic quantum circuits that have been transformed to a static circuit by enabling the :attr:`~.Configuration.Optimizations.transform_dynamic_circuit` optimization. + """ - Defaults to :code:`True` as this typically boosts performance. - """ + @backpropagate_output_permutation.setter + def backpropagate_output_permutation(self, arg: bool, /) -> None: ... + @property + def elide_permutations(self) -> bool: + """Elide permutations from the circuit by permuting the qubits in the circuit and eliminating SWAP gates from the circuits. - def __init__(self) -> None: ... + Defaults to :code:`True` as this typically boosts performance. + """ + + @elide_permutations.setter + def elide_permutations(self, arg: bool, /) -> None: ... class Application: """Options describing the :class:`.ApplicationScheme` used for the individual equivalence checkers.""" - construction_scheme: ApplicationScheme - """The :class:`.ApplicationScheme` used for the construction checker.""" - - simulation_scheme: ApplicationScheme - """The :class:`.ApplicationScheme` used for the simulation checker.""" - - alternating_scheme: ApplicationScheme - """The :class:`.ApplicationScheme` used for the alternating checker.""" - - profile: str - """The :attr:`Gate Cost <.ApplicationScheme.gate_cost>` application scheme can be configured with a profile that specifies the cost of gates. - This profile can be set via a file constructed like a lookup table. - Every line :code:` ` specifies the cost for a given gate type and with a certain number of controls, e.g., :code:`X 0 1` denotes that a single-qubit X gate has a cost of :code:`1`, while :code:`X 2 15` denotes that a Toffoli gate has a cost of :code:`15`. - """ - def __init__(self) -> None: ... + @property + def construction_scheme(self) -> ApplicationScheme: + """The :class:`.ApplicationScheme` used for the construction checker.""" + + @construction_scheme.setter + def construction_scheme(self, arg: ApplicationScheme, /) -> None: ... + @property + def simulation_scheme(self) -> ApplicationScheme: + """The :class:`.ApplicationScheme` used for the simulation checker.""" + + @simulation_scheme.setter + def simulation_scheme(self, arg: ApplicationScheme, /) -> None: ... + @property + def alternating_scheme(self) -> ApplicationScheme: + """The :class:`.ApplicationScheme` used for the alternating checker.""" + + @alternating_scheme.setter + def alternating_scheme(self, arg: ApplicationScheme, /) -> None: ... + @property + def profile(self) -> str: + """The :attr:`Gate Cost <.ApplicationScheme.gate_cost>` application scheme can be configured with a profile that specifies the cost of gates. + + This profile can be set via a file constructed like a lookup table. + Every line :code:` ` specifies the cost for a given gate type and with a certain number of controls, e.g., :code:`X 0 1` denotes that a single-qubit X gate has a cost of :code:`1`, while :code:`X 2 15` denotes that a Toffoli gate has a cost of :code:`15`. + """ + + @profile.setter + def profile(self, arg: str, /) -> None: ... class Functionality: """Options for all checkers that consider the whole functionality of a circuit.""" - trace_threshold: float = 1e-8 - """While decision diagrams are canonical in theory, i.e., equivalent circuits produce equivalent decision diagrams, numerical inaccuracies and approximations can harm this property. + def __init__(self) -> None: ... + @property + def trace_threshold(self) -> float: + r"""While decision diagrams are canonical in theory, i.e., equivalent circuits produce equivalent decision diagrams, numerical inaccuracies and approximations can harm this property. - This can result in a scenario where two decision diagrams are really close to one another, but cannot be identified as such by standard methods (i.e., comparing their root pointers). - Instead, for two decision diagrams :code:`U` and :code:`U'` representing the functionalities of two circuits :code:`G` and :code:`G'`, the trace of the product of one decision diagram with the inverse of the other can be computed and compared to the trace of the identity. + This can result in a scenario where two decision diagrams are really close to one another, but cannot be identified as such by standard methods (i.e., comparing their root pointers). + Instead, for two decision diagrams :code:`U` and :code:`U'` representing the functionalities of two circuits :code:`G` and :code:`G'`, the trace of the product of one decision diagram with the inverse of the other can be computed and compared to the trace of the identity. - Alternatively, it can be checked, whether :code:`U*U`^-1` is \"close enough\" to the identity by recursively checking that each decision diagram node is close enough to the identity structure (i.e., the first and last successor have weights close to one, while the second and third successor have weights close to zero). - Whenever any decision diagram node differs from this structure by more than the configured threshold, the circuits are concluded to be non-equivalent. + Alternatively, it can be checked, whether :code:`U*U`^-1` is \"close enough\" to the identity by recursively checking that each decision diagram node is close enough to the identity structure (i.e., the first and last successor have weights close to one, while the second and third successor have weights close to zero). + Whenever any decision diagram node differs from this structure by more than the configured threshold, the circuits are concluded to be non-equivalent. - Defaults to :code:`1e-8`. - """ + Defaults to :code:`1e-8`. + """ - check_partial_equivalence: bool = False - """Two circuits are partially equivalent if, for each possible initial input state, they have the same probability for each measurement outcome. - If set to :code:`True`, a check for partial equivalence will be performed and the contributions of garbage qubits to the circuit are ignored. - If set to :code:`False`, the checker will output 'not equivalent' for circuits that are partially equivalent but not totally equivalent. - In particular, garbage qubits will be treated as if they were measured qubits. + @trace_threshold.setter + def trace_threshold(self, arg: float, /) -> None: ... + @property + def check_partial_equivalence(self) -> bool: + """Two circuits are partially equivalent if, for each possible initial input state, they have the same probability for each measurement outcome. - Defaults to :code:`False`. - """ + If set to :code:`True`, a check for partial equivalence will be performed and the contributions of garbage qubits to the circuit are ignored. + If set to :code:`False`, the checker will output 'not equivalent' for circuits that are partially equivalent but not totally equivalent. + In particular, garbage qubits will be treated as if they were measured qubits. - def __init__(self) -> None: ... + Defaults to :code:`False`. + """ + + @check_partial_equivalence.setter + def check_partial_equivalence(self, arg: bool, /) -> None: ... class Simulation: """Options that influence the simulation checker.""" - fidelity_threshold: float - """Similar to :attr:`~.Configuration.Functionality.trace_threshold`, this setting is here to tackle numerical inaccuracies in the simulation checker. - Instead of computing a trace, the fidelity between the states resulting from the simulation is computed. - Whenever the fidelity differs from :code:`1.` by more than the configured threshold, the circuits are concluded to be non-equivalent. + def __init__(self) -> None: ... + @property + def fidelity_threshold(self) -> float: + """Similar to :attr:`~.Configuration.Functionality.trace_threshold`, this setting is here to tackle numerical inaccuracies in the simulation checker. - Defaults to :code:`1e-8`. - """ + Instead of computing a trace, the fidelity between the states resulting from the simulation is computed. + Whenever the fidelity differs from :code:`1.` by more than the configured threshold, the circuits are concluded to be non-equivalent. - max_sims: int - """The maximum number of simulations to be started for the simulation checker. + Defaults to :code:`1e-8`. + """ - In practice, just a couple of simulations suffice in most cases to detect a potential non-equivalence. - Either defaults to :code:`16` or the maximum number of available threads minus 2, whichever is more. - """ + @fidelity_threshold.setter + def fidelity_threshold(self, arg: float, /) -> None: ... + @property + def max_sims(self) -> int: + """The maximum number of simulations to be started for the simulation checker. - state_type: StateType = ... - """The :class:`type of states <.StateType>` used for the simulations in the simulation checker. + In practice, just a couple of simulations suffice in most cases to detect a potential non-equivalence. + Either defaults to :code:`16` or the maximum number of available threads minus 2, whichever is more. + """ - Defaults to :attr:`.StateType.computational_basis`. - """ + @max_sims.setter + def max_sims(self, arg: int, /) -> None: ... + @property + def state_type(self) -> StateType: + """The :class:`type of states <.StateType>` used for the simulations in the simulation checker. - seed: int = 0 - """The seed used in the quantum state generator. + Defaults to :attr:`.StateType.computational_basis`. + """ - Defaults to :code:`0`, which means that the seed is chosen non-deterministically for each program run. - """ + @state_type.setter + def state_type(self, arg: StateType, /) -> None: ... + @property + def seed(self) -> int: + """The seed used in the quantum state generator. - def __init__(self) -> None: ... + Defaults to :code:`0`, which means that the seed is chosen non-deterministically for each program run. + """ + + @seed.setter + def seed(self, arg: int, /) -> None: ... class Parameterized: """Options that influence the equivalence checking scheme for parameterized circuits.""" - parameterized_tolerance: float = 1e-12 - """Set threshold below which instantiated parameters shall be considered zero. + def __init__(self) -> None: ... + @property + def parameterized_tolerance(self) -> float: + """Set threshold below which instantiated parameters shall be considered zero. - Defaults to :code:`1e-12`. - """ + Defaults to :code:`1e-12`. + """ - additional_instantiations: int = 0 - """Number of instantiations shall be performed in addition to the default ones. + @parameterized_tolerance.setter + def parameterized_tolerance(self, arg: float, /) -> None: ... + @property + def additional_instantiations(self) -> int: + """Number of instantiations shall be performed in addition to the default ones. - For parameterized circuits that cannot be shown to be equivalent by the ZX checker the circuits are instantiated with concrete values for parameters and subsequently checked with QCEC's default schemes. - The first instantiation tries to set as many gate parameters to 0. - The last instantiations initializes the parameters with random values to guarantee completeness of the equivalence check. - Because random instantiation is costly, additional instantiations can be performed that lead to simpler equivalence checking instances as the random instantiation. - This option changes how many of those additional checks are performed. - """ + For parameterized circuits that cannot be shown to be equivalent by the ZX checker the circuits are instantiated with concrete values for parameters and subsequently checked with QCEC's default schemes. + The first instantiation tries to set as many gate parameters to 0. + The last instantiations initializes the parameters with random values to guarantee completeness of the equivalence check. + Because random instantiation is costly, additional instantiations can be performed that lead to simpler equivalence checking instances as the random instantiation. + This option changes how many of those additional checks are performed. + """ - def __init__(self) -> None: ... - - application: Configuration.Application - execution: Configuration.Execution - functionality: Configuration.Functionality - optimizations: Configuration.Optimizations - parameterized: Configuration.Parameterized - simulation: Configuration.Simulation - def __init__(self) -> None: - """Initializes the configuration.""" + @additional_instantiations.setter + def additional_instantiations(self, arg: int, /) -> None: ... + @property + def execution(self) -> Configuration.Execution: ... + @execution.setter + def execution(self, arg: Configuration.Execution, /) -> None: ... + @property + def optimizations(self) -> Configuration.Optimizations: ... + @optimizations.setter + def optimizations(self, arg: Configuration.Optimizations, /) -> None: ... + @property + def application(self) -> Configuration.Application: ... + @application.setter + def application(self, arg: Configuration.Application, /) -> None: ... + @property + def functionality(self) -> Configuration.Functionality: ... + @functionality.setter + def functionality(self, arg: Configuration.Functionality, /) -> None: ... + @property + def simulation(self) -> Configuration.Simulation: ... + @simulation.setter + def simulation(self, arg: Configuration.Simulation, /) -> None: ... + @property + def parameterized(self) -> Configuration.Parameterized: ... + @parameterized.setter + def parameterized(self, arg: Configuration.Parameterized, /) -> None: ... def json(self) -> dict[str, Any]: """Returns a JSON-style dictionary of the configuration.""" @@ -317,28 +423,103 @@ class EquivalenceCheckingManager: Allows checking the equivalence of quantum circuits based on the methods proposed in :cite:p:`burgholzer2021advanced`. It features many configuration options that orchestrate the procedure. """ - def __init__(self, circ1: QuantumComputation, circ2: QuantumComputation, config: Configuration = ...) -> None: + + def __init__( + self, circ1: mqt.core.ir.QuantumComputation, circ2: mqt.core.ir.QuantumComputation, config: Configuration = ... + ) -> None: """Create an equivalence checking manager for two circuits and configure it with a :class:`.Configuration` object.""" + class Results: + """Captures the main results and statistics from :meth:`~.EquivalenceCheckingManager.run`.""" + + def __init__(self) -> None: + """Initializes the results.""" + + @property + def preprocessing_time(self) -> float: + """Time spent during preprocessing (in seconds).""" + + @preprocessing_time.setter + def preprocessing_time(self, arg: float, /) -> None: ... + @property + def check_time(self) -> float: + """Time spent during equivalence check (in seconds).""" + + @check_time.setter + def check_time(self, arg: float, /) -> None: ... + @property + def equivalence(self) -> EquivalenceCriterion: + """Final result of the equivalence check.""" + + @equivalence.setter + def equivalence(self, arg: EquivalenceCriterion, /) -> None: ... + @property + def started_simulations(self) -> int: + """Number of simulations that have been started.""" + + @started_simulations.setter + def started_simulations(self, arg: int, /) -> None: ... + @property + def performed_simulations(self) -> int: + """Number of simulations that have been finished.""" + + @performed_simulations.setter + def performed_simulations(self, arg: int, /) -> None: ... + @property + def cex_input(self) -> mqt.core.dd.VectorDD: + """DD representation of the initial state that produced a counterexample.""" + + @cex_input.setter + def cex_input(self, arg: mqt.core.dd.VectorDD, /) -> None: ... + @property + def cex_output1(self) -> mqt.core.dd.VectorDD: + """DD representation of the first circuit's counterexample output state.""" + + @cex_output1.setter + def cex_output1(self, arg: mqt.core.dd.VectorDD, /) -> None: ... + @property + def cex_output2(self) -> mqt.core.dd.VectorDD: + """DD representation of the second circuit's counterexample output state.""" + + @cex_output2.setter + def cex_output2(self, arg: mqt.core.dd.VectorDD, /) -> None: ... + @property + def performed_instantiations(self) -> int: + """Number of circuit instantiations performed during equivalence checking of parameterized quantum circuits.""" + + @performed_instantiations.setter + def performed_instantiations(self, arg: int, /) -> None: ... + @property + def checker_results(self) -> dict[str, Any]: + """Dictionary of the results of the individual checkers.""" + + @checker_results.setter + def checker_results(self, arg: dict, /) -> None: ... + def considered_equivalent(self) -> bool: + """Convenience function to check whether the result is considered equivalent.""" + + def json(self) -> dict[str, Any]: + """Returns a JSON-style dictionary of the results.""" + @property - def qc1(self) -> QuantumComputation: + def qc1(self) -> mqt.core.ir.QuantumComputation: """The first circuit to be checked.""" @property - def qc2(self) -> QuantumComputation: + def qc2(self) -> mqt.core.ir.QuantumComputation: """The second circuit to be checked.""" @property - def configuration(self) -> Configuration: ... - @configuration.setter - def configuration(self, config: Configuration) -> None: + def configuration(self) -> Configuration: """The configuration of the equivalence checking manager.""" + @configuration.setter + def configuration(self, arg: Configuration, /) -> None: ... def run(self) -> None: """Execute the equivalence check as configured.""" @property - def results(self) -> Results: + def results(self) -> EquivalenceCheckingManager.Results: """The results of the equivalence check.""" @property @@ -351,112 +532,83 @@ class EquivalenceCheckingManager: def set_application_scheme(self, scheme: ApplicationScheme = ...) -> None: """Set the :class:`.ApplicationScheme` used for all checkers (based on decision diagrams). - Arguments: + Args: scheme: The application scheme. Defaults to :attr:`.ApplicationScheme.proportional`. """ def set_gate_cost_profile(self, profile: str = "") -> None: """Set the :attr:`profile <.Configuration.Application.profile>` used in the :attr:`Gate Cost <.ApplicationScheme.gate_cost>` application scheme for all checkers (based on decision diagrams). - Arguments: + Args: profile: The path to the profile file. """ - class Results: - """Captures the main results and statistics from :meth:`~.EquivalenceCheckingManager.run`.""" - - preprocessing_time: float - """Time spent during preprocessing (in seconds).""" - - check_time: float - """Time spent during equivalence check (in seconds).""" - - equivalence: EquivalenceCriterion - """Final result of the equivalence check.""" - - started_simulations: int - """Number of simulations that have been started.""" - - performed_simulations: int - """Number of simulations that have been finished.""" - - cex_input: VectorDD - """DD representation of the initial state that produced a counterexample.""" - - cex_output1: VectorDD - """DD representation of the first circuit's counterexample output state.""" - - cex_output2: VectorDD - """DD representation of the second circuit's counterexample output state.""" - - performed_instantiations: int - """Number of circuit instantiations performed during equivalence checking of parameterized quantum circuits.""" - - checker_results: dict[str, Any] - """Dictionary of the results of the individual checkers.""" - - def __init__(self) -> None: - """Initializes the results.""" - - def considered_equivalent(self) -> bool: - """Convenience function to check whether the result is considered equivalent.""" - - def json(self) -> dict[str, Any]: - """Returns a JSON-style dictionary of the results.""" - -class EquivalenceCriterion(Enum): +class EquivalenceCriterion(enum.IntEnum): """Captures all the different notions of equivalence that can be the result of a :meth:`~.EquivalenceCheckingManager.run`.""" - no_information = ... - """No information on the equivalence is available. - This can be because the check has not been run or that a timeout happened.""" + no_information = 2 + """ + No information on the equivalence is available. + + This can be because the check has not been run or that a timeout happened. + """ - not_equivalent = ... + not_equivalent = 0 """Circuits are shown to be non-equivalent.""" - equivalent = ... + equivalent = 1 """Circuits are shown to be equivalent.""" - equivalent_up_to_global_phase = ... + equivalent_up_to_phase = 5 """Circuits are equivalent up to a global phase factor.""" - equivalent_up_to_phase = ... + equivalent_up_to_global_phase = 4 """Circuits are equivalent up to a certain (global or relative) phase.""" - probably_equivalent = ... - """Circuits are probably equivalent. - A result obtained whenever a couple of simulations did not show the non-equivalence in the simulation checker.""" + probably_equivalent = 3 + """ + Circuits are probably equivalent. - probably_not_equivalent = ... - """Circuits are probably not equivalent. - A result obtained whenever the ZX-calculus checker could not reduce the combined circuit to the identity.""" + A result obtained whenever a couple of simulations did not show the non-equivalence in the simulation checker. + """ -class StateType(Enum): - """The type of states used in the simulation checker allows trading off efficiency versus performance. + probably_not_equivalent = 6 + """ + Circuits are probably not equivalent. - * Classical stimuli (i.e., random *computational basis states*) already offer extremely high error detection rates in general and are comparatively fast to simulate, which makes them the default. + A result obtained whenever the ZX-calculus checker could not reduce the combined circuit to the identity. + """ - * Local quantum stimuli (i.e., random *single-qubit basis states*) are a little bit more computationally intensive, but provide even better error detection rates. +class StateType(enum.IntEnum): + """The type of states used in the simulation checker allows trading off efficiency versus performance. - * Global quantum stimuli (i.e., random *stabilizer states*) offer the highest available error detection rate, while at the same time incurring the highest computational effort. + - Classical stimuli (i.e., random *computational basis states*) already offer extremely high error detection rates in general and are comparatively fast to simulate, which makes them the default. + - Local quantum stimuli (i.e., random *single-qubit basis states*) are a little bit more computationally intensive, but provide even better error detection rates. + - Global quantum stimuli (i.e., random *stabilizer states*) offer the highest available error detection rate, while at the same time incurring the highest computational effort. For details, see :cite:p:`burgholzer2021randomStimuliGenerationQuantum`. """ - computational_basis = ... - """Randomly choose computational basis states. Also referred to as "*classical*".""" + computational_basis = 0 + """ + Randomly choose computational basis states. Also referred to as "*classical*". + """ - classical = ... + classical = 0 """Alias for :attr:`~StateType.computational_basis`.""" - random_1Q_basis = ... # noqa: N815 - """Randomly choose a single-qubit basis state for each qubit from the six-tuple *(|0>, |1>, |+>, |->, |L>, |R>)*. Also referred to as *"local_random"*.""" + random_1q_basis = 1 + """ + Randomly choose a single-qubit basis state for each qubit from the six-tuple *(|0>, |1>, |+>, |->, |L>, |R>)*. Also referred to as *"local_random"*. + """ - local_quantum = ... - """Alias for :attr:`~StateType.random_1Q_basis`.""" + local_quantum = 1 + """Alias for :attr:`~StateType.random_1q_basis`.""" - stabilizer = ... - """Randomly choose a stabilizer state by creating a random Clifford circuit. Also referred to as *"global_random"*.""" + stabilizer = 2 + """ + Randomly choose a stabilizer state by creating a random Clifford circuit. Also referred to as *"global_random"*. + """ - global_quantum = ... + global_quantum = 2 """Alias for :attr:`~StateType.stabilizer`.""" diff --git a/test/python/test_configuration.py b/test/python/test_configuration.py index 7774e50f..547e13aa 100644 --- a/test/python/test_configuration.py +++ b/test/python/test_configuration.py @@ -51,8 +51,8 @@ def test_timeout() -> None: [ ("computational_basis", StateType.computational_basis), ("classical", StateType.computational_basis), - ("random_1Q_basis", StateType.random_1Q_basis), - ("local_quantum", StateType.random_1Q_basis), + ("random_1q_basis", StateType.random_1q_basis), + ("local_quantum", StateType.random_1q_basis), ("stabilizer", StateType.stabilizer), ("global_quantum", StateType.stabilizer), ],