While experimenting on some benchmarks, it turned out that, sometimes, the ZX checker would just stop simplification even though further simplifications were possible.
This PR adresses the underlying bug by revamping and simplifying the handling of the stopping criterion during ZX simplification.
A (not necessarily minimal) reproducer for the bug is:
from mqt.bench import CompilerSettings, QiskitSettings, get_benchmark
from mqt.qcec import verify_compilation
alg = "ae"
num_qubits = 7
# construct the first circuit
qc1 = get_benchmark(alg, circuit_size=num_qubits, level="alg")
# construct the second circuit
optimization_level = 2
settings = CompilerSettings(qiskit=QiskitSettings(optimization_level=2))
qc2 = get_benchmark(alg, circuit_size=num_qubits, level="nativegates", compiler_settings=settings)
# verify the compilation only using the ZX checker
result2 = verify_compilation(
qc1,
qc2,
optimization_level=optimization_level,
run_alternating_checker=False,
run_zx_checker=True,
run_simulation_checker=False,
)
print(f"ZX-Checker \t|\t {result2.considered_equivalent()} \t|\t {result2.check_time}")
Checklist:
[x] The pull request only contains commits that are related to it.
[x] I have added appropriate tests and documentation.
[x] I have made sure that all CI jobs on GitHub pass.
[x] The pull request introduces no new warnings and follows the project's style guidelines.
Description
While experimenting on some benchmarks, it turned out that, sometimes, the ZX checker would just stop simplification even though further simplifications were possible. This PR adresses the underlying bug by revamping and simplifying the handling of the stopping criterion during ZX simplification.
A (not necessarily minimal) reproducer for the bug is:
Checklist: