Add Z3-based exact synthesis engine for Clifford encoding isometries (#740)

## Description

This PR expands the exact synthesis of encoding circuits. 

It provides `synthesize_isometry_exact` for provably **gate-optimal**
and **depth-optimal** encoding
circuits for both **CSS and non-CSS** stabilizer codes, with symmetry
breaking,
two-qubit-gate bounding, timeouts, and result verification.

Previously, there was the functionality for depth-optimal synthesis of
CSS and non-CSS encoders and gate-optimal synthesis of CSS encoders.
This PR unifies the synthesis so that both objectives are available for
both cases.

> [!NOTE]
> This PR was prepared with AI assistance (Claude Opus 4.8 via Claude
Code); see
> the `Assisted-by:` commit footer. All changes were reviewed by the
author.

## Checklist

- [x] The pull request only contains commits that are focused and
relevant to this change.
- [x] I have added appropriate tests that cover the new/changed
functionality.
- [x] I have updated the documentation to reflect these changes.
- [x] The changes follow the project's style guidelines and introduce no
new warnings.
- [x] The changes are fully tested and pass the CI checks.
- [x] I have reviewed my own code changes.

**If PR contains AI-assisted content:**

- [x] I have disclosed the use of AI tools in the PR description as per
our [AI Usage
Guidelines](https://github.com/munich-quantum-toolkit/qecc/blob/main/docs/ai_usage.md).
- [x] AI-assisted commits include an `Assisted-by: [Model Name] via
[Tool Name]` footer.
- [x] I confirm that I have personally reviewed and understood all
AI-generated content, and accept full responsibility for it.

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: pehamTom

docs/Encoders.md

@@ -47,6 +47,10 @@ There is not a unique encoding circuit but usually we would like to obtain an en
 
 Under the hood, this uses the SMT solver [z3](https://github.com/Z3Prover/z3). Of course this method scales only up to a few qubits. Synthesizing depth-optimal circuits is usually faster than synthesizing gate-optimal circuits.
 
+```{note}
+These optimal encoders are thin convenience wrappers around the general exact-synthesis engine. See {doc}`ExactSynthesis` for the full interface — non-CSS codes, gate-count vs. depth objectives, custom gate sets, and two-qubit-gate minimization.
+```
+
 ```{code-cell} ipython3
 depth_opt = depth_optimal_encoding_circuit(steane_code, max_timeout=2)
 q_enc = depth_opt.inputs()
@@ -241,18 +245,13 @@ For non-CSS codes, depth-optimal synthesis is also available:
 ```{code-cell} ipython3
 from mqt.qecc.circuit_synthesis import depth_optimal_encoding_circuit_non_css
 
-encoder = None
-for d in range(3, 9):
-    result = depth_optimal_encoding_circuit_non_css(five_qubit_code, max_depth=d, exact_two_qubit_count=True, max_two_qubit_gates=6)
-
-    if result == "UNSAT":
-        print(f"No solution for max_depth={d}")
-    else:
-        encoder = result
-        break
+# Search for a depth-optimal encoder with at most six two-qubit gates. `min_depth` skips the
+# (expensive) proofs that no shallower circuit exists.
+result = depth_optimal_encoding_circuit_non_css(five_qubit_code, min_depth=4, max_depth=8, max_two_qubit_gates=6)
 
-if encoder is None:
-    raise RuntimeError("No non-CSS encoder found in the tested depth range.")
+if isinstance(result, str):
+    raise RuntimeError(f"No non-CSS encoder found: {result}")
+encoder = result
 encoding_qubits = encoder.inputs()
 
 print(f"Encoding qubits (logical to physical mapping): {encoding_qubits}")