🐛 fix ZX-checker inadvertedly terminating early (#382)

## 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:
```python
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:

<!---
This checklist serves as a reminder of a couple of things that ensure
your pull request will be merged swiftly.
-->

- [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.

Signed-off-by: burgholzer <burgholzer@me.com>

include/checker/zx/ZXChecker.hpp

@@ -36,72 +36,72 @@ class ZXEquivalenceChecker : public EquivalenceChecker {
   // the following methods are adaptations of the core ZX simplification
   // routines that additionally check a criterion for early termination of the
   // simplification.
-  std::size_t fullReduceApproximate();
-  std::size_t fullReduce();
+  bool fullReduceApproximate();
+  bool fullReduce();
 
-  std::size_t gadgetSimp();
-  std::size_t interiorCliffordSimp();
-  std::size_t cliffordSimp();
+  bool gadgetSimp();
+  bool interiorCliffordSimp();
+  bool cliffordSimp();
 
-  std::size_t idSimp() {
-    return simplifyVertices(zx::checkIdSimp, zx::removeId);
-  }
+  bool idSimp() { return simplifyVertices(zx::checkIdSimp, zx::removeId); }
 
-  std::size_t spiderSimp() {
+  bool spiderSimp() {
     return simplifyEdges(zx::checkSpiderFusion, zx::fuseSpiders);
   }
 
-  std::size_t localCompSimp() {
+  bool localCompSimp() {
     return simplifyVertices(zx::checkLocalComp, zx::localComp);
   }
 
-  std::size_t pivotPauliSimp() {
+  bool pivotPauliSimp() {
     return simplifyEdges(zx::checkPivotPauli, zx::pivotPauli);
   }
 
-  std::size_t pivotSimp() { return simplifyEdges(zx::checkPivot, zx::pivot); }
+  bool pivotSimp() { return simplifyEdges(zx::checkPivot, zx::pivot); }
 
-  std::size_t pivotGadgetSimp() {
+  bool pivotGadgetSimp() {
     return simplifyEdges(zx::checkPivotGadget, zx::pivotGadget);
   }
 
   template <class CheckFun, class RuleFun>
-  std::size_t simplifyVertices(CheckFun check, RuleFun rule) {
-    std::size_t nSimplifications = 0U;
-    bool        newMatches       = true;
-
-    while (!isDone() && newMatches) {
-      newMatches = false;
+  bool simplifyVertices(CheckFun check, RuleFun rule) {
+    bool simplified = false;
+    while (!isDone()) {
+      auto moreSimplified = false;
       for (const auto& [v, _] : miter.getVertices()) {
         if (isDone() || !check(miter, v)) {
           continue;
         }
         rule(miter, v);
-        newMatches = true;
-        ++nSimplifications;
+        moreSimplified = true;
+      }
+      if (!moreSimplified) {
+        break;
       }
+      simplified |= true;
     }
-    return nSimplifications;
+    return simplified;
   }
 
   template <class CheckFun, class RuleFun>
-  std::size_t simplifyEdges(CheckFun check, RuleFun rule) {
-    std::size_t nSimplifications = 0U;
-    bool        newMatches       = true;
-
-    while (!isDone() && newMatches) {
-      newMatches = false;
+  bool simplifyEdges(CheckFun check, RuleFun rule) {
+    bool simplified = false;
+    while (!isDone()) {
+      auto moreSimplified = false;
       for (const auto& [v0, v1] : miter.getEdges()) {
         if (isDone() || miter.isDeleted(v0) || miter.isDeleted(v1) ||
             !check(miter, v0, v1)) {
           continue;
         }
         rule(miter, v0, v1);
-        newMatches = true;
-        ++nSimplifications;
+        moreSimplified = true;
+      }
+      if (!moreSimplified) {
+        break;
       }
+      simplified |= true;
     }
-    return nSimplifications;
+    return simplified;
   }
 };
 

src/checker/zx/ZXChecker.cpp

@@ -154,98 +154,85 @@ qc::Permutation invertPermutations(const qc::QuantumComputation& qc) {
                 complete(qc.initialLayout, qc.getNqubits()));
 }
 
-std::size_t ZXEquivalenceChecker::fullReduceApproximate() {
-  auto nSimplifications = fullReduce();
+bool ZXEquivalenceChecker::fullReduceApproximate() {
+  auto simplified = fullReduce();
   while (!isDone()) {
     miter.approximateCliffords(tolerance);
-    const auto newSimps = fullReduce();
-    if (newSimps == 0U) {
+    if (!fullReduce()) {
       break;
     }
-    nSimplifications += newSimps;
+    simplified = true;
   }
-  return nSimplifications;
+  return simplified;
 }
 
-std::size_t ZXEquivalenceChecker::fullReduce() {
+bool ZXEquivalenceChecker::fullReduce() {
   if (!isDone()) {
     miter.toGraphlike();
   }
-  interiorCliffordSimp();
-
-  bool        newMatches       = true;
-  std::size_t nSimplifications = 0U;
-  while (!isDone() && newMatches) {
-    newMatches = false;
-    cliffordSimp();
-    const auto nGadget = gadgetSimp();
-    interiorCliffordSimp();
-    const auto nPivot = pivotGadgetSimp();
-    if ((nGadget + nPivot) != 0U) {
-      newMatches = true;
-      ++nSimplifications;
+  auto simplified = interiorCliffordSimp();
+  while (!isDone()) {
+    auto moreSimplified = cliffordSimp();
+    moreSimplified |= gadgetSimp();
+    moreSimplified |= interiorCliffordSimp();
+    moreSimplified |= pivotGadgetSimp();
+    if (!moreSimplified) {
+      break;
     }
+    simplified = true;
   }
   if (!isDone()) {
     miter.removeDisconnectedSpiders();
   }
-
-  return nSimplifications;
+  return simplified;
 }
 
-std::size_t ZXEquivalenceChecker::gadgetSimp() {
-  std::size_t nSimplifications = 0U;
-  bool        newMatches       = true;
-
-  while (!isDone() && newMatches) {
-    newMatches = false;
+bool ZXEquivalenceChecker::gadgetSimp() {
+  auto simplified = false;
+  while (!isDone()) {
+    auto moreSimplified = false;
     for (const auto& [v, _] : miter.getVertices()) {
       if (miter.isDeleted(v)) {
         continue;
       }
-
-      if (!isDone() && checkAndFuseGadget(miter, v)) {
-        newMatches = true;
-        ++nSimplifications;
+      if (checkAndFuseGadget(miter, v)) {
+        moreSimplified = true;
       }
     }
+    if (!moreSimplified) {
+      break;
+    }
+    simplified = true;
   }
-  return nSimplifications;
+  return simplified;
 }
 
-std::size_t ZXEquivalenceChecker::interiorCliffordSimp() {
-  spiderSimp();
-
-  bool        newMatches       = true;
-  std::size_t nSimplifications = 0U;
-  while (!isDone() && newMatches) {
-    newMatches            = false;
-    const auto nId        = idSimp();
-    const auto nSpider    = spiderSimp();
-    const auto nPivot     = pivotPauliSimp();
-    const auto nLocalComp = localCompSimp();
-
-    if ((nId + nSpider + nPivot + nLocalComp) != 0U) {
-      newMatches = true;
-      ++nSimplifications;
+bool ZXEquivalenceChecker::interiorCliffordSimp() {
+  auto simplified = spiderSimp();
+  while (!isDone()) {
+    auto moreSimplified = idSimp();
+    moreSimplified |= spiderSimp();
+    moreSimplified |= pivotPauliSimp();
+    moreSimplified |= localCompSimp();
+    if (!moreSimplified) {
+      break;
     }
+    simplified = true;
   }
-  return nSimplifications;
+  return simplified;
 }
 
-std::size_t ZXEquivalenceChecker::cliffordSimp() {
-  bool        newMatches       = true;
-  std::size_t nSimplifications = 0U;
-  while (!isDone() && newMatches) {
-    newMatches           = false;
-    const auto nClifford = interiorCliffordSimp();
-    const auto nPivot    = pivotSimp();
-    if ((nClifford + nPivot) != 0U) {
-      newMatches = true;
-      ++nSimplifications;
+bool ZXEquivalenceChecker::cliffordSimp() {
+  auto simplified = false;
+  while (!isDone()) {
+    auto moreSimplified = interiorCliffordSimp();
+    moreSimplified |= pivotSimp();
+    if (!moreSimplified) {
+      break;
     }
+    simplified = true;
   }
-  return nSimplifications;
+  return simplified;
 }
 
 } // namespace ec