✨ Add Assertion Refinement tools to MQT Debugger (#35)

* feat: ✨ Define basic commutation rules for general assertions

* feat: ✨ Add some more commutation rule

* feat: ✨ Add assertion movement functionality to Diagnostics

* test: ✅ Refactor test structure and add new tests for assertion movement

* refactor(assertion-tools): ♻️ Change passing mode to reference for testing assertion movements

* ci(assertion-tools): 👷 Add assertion-tools branch to ci

* test(assertion-tools): ✅ Add new assertion movement tests

* feat(assertion-tools): ✨ Add entanglement-assertion creation tools and tests

* refactor(assertion-tools): ♻️ Fix some linting issues

* refactor(assertion-tools): ♻️ Update the commutativity rule logic

* refactor(assertion-tools): ♻️ Refactor commutativity rule logic

* test(assertion-tools): ✅ Add new tests and fix some minor issues

* feat(assertion-tools): ✨ Add assertion suggestion to CLI Frontend

* test(assertion-tools): 🧪 Add tests for new equality assertion splitting method

* style(assertion-tools): ♻️ Fix pre-commit issues

* refactor(assertion-tools): ♻️ Refactor maths methods from DDSimDebug into a common maths file

* feat(assertion-tools): :feat: Add equality assertion splitting method

* build(assertion-tools): ⬆️ Change python version for bindings to 3.9

* fix: 🐛 Fix parsing of negative complex numbers

* feat(assertion-tools): :feat: Allow moving assertions over other assertions

This has to be allowed, otherwise one stuck assertion would block all others. Later on, some changes should be made to ensure the sorting remains stable

* feat(assertion-tools): ✨ Calling the assertion-tool methods with count 0 now returns the maximum size

* feat(assertion-tools): ✨ Implement get quantum variable name method

* refactor(assertion-tools): ♻️ Increase epsilon when computing entanglement (it's better to be more lenient)

* build(assertion-tools): 🏗️ Update python bindings

* test(assertion-tools): ✅ Add test for assertion creation of eq assertions

* feat(assertion-tools): :feat: Stop ent-assertion generation when connection is not unique

* feat(assertion-tools): :feat: Ent-Assertion creation now builds 1:1 along the path instead of 1:n from the base

* test(assertion-tools): 🧪 Remove assertion movement test that requires stable sorting

* refactor(assertion-tools): ♻️ Rename "commutativity" to "commutation"

* feat(assertion-tools): 🏷️ Add new assertion refinement methods to `.pyi` file

* refactor(assertion-tools): 📝 Add docstrings to all new non-test functions

* refactor(assertion-tools): 📝 Add docstrings to new assertion refinement tests

* refactor(assertion-tools): ♻️ Resolve linting issues

* refactor(assertion-tools): ♻️ Resolve linting issues

* refactor(assertion-tools): ♻️ Remove unnecessary string import

.github/workflows/ci.yml

@@ -3,6 +3,7 @@ on:
   push:
     branches:
       - main
+      - assertion-tools
   pull_request:
   merge_group:
   workflow_dispatch:

.gitignore

@@ -180,3 +180,5 @@ wheelhouse/
 
 # test code for the CLIFrontEnd
 app/code/*.qasm
+
+.python-version

CMakeLists.txt

@@ -31,7 +31,7 @@ if(BUILD_MQT_DEBUGGER_BINDINGS)
 
   # top-level call to find Python
   find_package(
-    Python 3.8 REQUIRED
+    Python 3.9 REQUIRED
     COMPONENTS Interpreter Development.Module
     OPTIONAL_COMPONENTS Development.SABIModule)
 endif()

include/backend/dd/DDSimDebug.hpp

@@ -490,6 +490,20 @@ size_t ddsimGetNumClassicalVariables(SimulationState* self);
 Result ddsimGetClassicalVariableName(SimulationState* self,
                                      size_t variableIndex, char* output);
 
+/**
+ * @brief Gets the name of a quantum variable by its index.
+ *
+ * For registers, each index is counted as a separate variable and can be
+ * accessed separately. This method will return the name of the specific
+ * index of the register.
+ * @param self The instance to query.
+ * @param variableIndex The index of the variable.
+ * @param output A buffer to store the name of the variable.
+ * @return The result of the operation.
+ */
+Result ddsimGetQuantumVariableName(SimulationState* self, size_t variableIndex,
+                                   char* output);
+
 /**
  * @brief Gets the full state vector of the simulation at the current time.
  *
@@ -619,6 +633,14 @@ bool checkAssertion(DDSimulationState* ddsim,
  */
 std::string getClassicalBitName(DDSimulationState* ddsim, size_t index);
 
+/**
+ * @brief Gets the name of a qubit variable by its index.
+ * @param ddsim The simulation state to query.
+ * @param index The index of the qubit variable.
+ * @return The name of the qubit variable.
+ */
+std::string getQuantumBitName(DDSimulationState* ddsim, size_t index);
+
 /**
  * @brief Gets the qubit index from a variable name.
  *
@@ -659,17 +681,6 @@ std::pair<size_t, size_t> variableToQubitAt(DDSimulationState* ddsim,
 bool isSubStateVectorLegal(const Statevector& full,
                            std::vector<size_t>& targetQubits);
 
-/**
- * @brief Gets the partial state vector by tracing out individual qubits from
- * the full state vector.
- * @param sv The full state vector.
- * @param traceOut The indices of the qubits to trace out.
- * @return The partial state vector.
- */
-std::vector<std::vector<Complex>>
-getPartialTraceFromStateVector(const Statevector& sv,
-                               const std::vector<size_t>& traceOut);
-
 /**
  * @brief Gets the target variables of an instruction.
  *

include/backend/dd/DDSimDiagnostics.hpp

@@ -8,13 +8,73 @@
 #include "backend/diagnostics.h"
 #include "common.h"
 #include "common/parsing/AssertionParsing.hpp"
+#include "common/parsing/CodePreprocessing.hpp"
 
 #include <cstddef>
 #include <map>
 #include <memory>
 #include <set>
+#include <string>
+#include <utility>
 #include <vector>
 
+/**
+ * @brief Represents an equality assertion that should be inserted into the
+ * program.
+ */
+struct InsertEqualityAssertion {
+
+  /**
+   * @brief The index of the instruction where the assertion should be inserted.
+   */
+  size_t instructionIndex;
+
+  /**
+   * @brief The amplitudes that the assertion should check for equality.
+   */
+  std::vector<Complex> amplitudes;
+
+  /**
+   * @brief The similarity threshold for the assertion.
+   */
+  double similarity;
+
+  /**
+   * @brief The target qubits of the assertion.
+   */
+  std::vector<std::string> targets;
+
+  /**
+   * @brief Check whether two InsertEqualityAssertion instances are equal.
+   * @param other The other InsertEqualityAssertion instance to compare with.
+   * @return True if the instances are equal, false otherwise.
+   */
+  bool operator==(const InsertEqualityAssertion& other) const {
+    if (instructionIndex != other.instructionIndex ||
+        targets != other.targets) {
+      return false;
+    }
+
+    if ((similarity - other.similarity) < -1e-10 ||
+        (similarity - other.similarity) > 1e-10) {
+      return false;
+    }
+
+    for (size_t i = 0; i < amplitudes.size(); i++) {
+      if ((amplitudes[i].real - other.amplitudes[i].real) < -1e-10 ||
+          (amplitudes[i].real - other.amplitudes[i].real) > 1e-10) {
+        return false;
+      }
+      if ((amplitudes[i].imaginary - other.amplitudes[i].imaginary) < -1e-10 ||
+          (amplitudes[i].imaginary - other.amplitudes[i].imaginary) > 1e-10) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+};
+
 struct DDSimulationState;
 
 /**
@@ -43,6 +103,24 @@ struct DDDiagnostics {
    * @brief The actual qubits that each instruction has targeted.
    */
   std::map<size_t, std::set<std::vector<size_t>>> actualQubits;
+
+  /**
+   * @brief Assertions that have been identified to be moved in the program.
+   */
+  std::vector<std::pair<size_t, size_t>> assertionsToMove;
+
+  /**
+   * @brief The entanglement assertions that have been identified to be added to
+   * the program.
+   */
+  std::map<size_t, std::set<std::pair<std::set<std::string>, size_t>>>
+      assertionsEntToInsert;
+
+  /**
+   * @brief The equality assertions that have been identified to be added to the
+   * program.
+   */
+  std::map<size_t, std::vector<InsertEqualityAssertion>> assertionsEqToInsert;
 };
 
 /**
@@ -161,6 +239,40 @@ Result dddiagnosticsGetZeroControlInstructions(Diagnostics* self,
 size_t dddiagnosticsPotentialErrorCauses(Diagnostics* self, ErrorCause* output,
                                          size_t count);
 
+/**
+ * @brief Suggest movements of assertions to better positions.
+ * @param self The diagnostics instance to query.
+ * @param originalPositions An array of assertion positions to be filled.
+ * Contains the original positions of the assertions that should be moved.
+ * @param suggestedPositions An array of assertion positions to be filled.
+ * Contains the suggested positions of the assertions that should be moved.
+ * @param count The maximum number of assertions to suggest movements for.
+ * @return The number of suggested movements.
+ */
+size_t dddiagnosticsSuggestAssertionMovements(Diagnostics* self,
+                                              size_t* originalPositions,
+                                              size_t* suggestedPositions,
+                                              size_t count);
+
+/**
+ * @brief Suggest new assertions to be added to the code.
+ *
+ * These assertions are added by first observing assertions that failed during
+ * previous iterations. Therefore, the simulation must be run at least once
+ * before calling this function.
+ *
+ * @param self The diagnostics instance to query.
+ * @param suggestedPositions An array of assertion positions to be filled.
+ * @param suggestedAssertions An array of assertion instruction strings to be
+ * filled. Each string expects a size of up to 256 characters.
+ * @param count The maximum number of assertions to suggest.
+ * @return The number of suggested assertions.
+ */
+size_t dddiagnosticsSuggestNewAssertions(Diagnostics* self,
+                                         size_t* suggestedPositions,
+                                         char** suggestedAssertions,
+                                         size_t count);
+
 /**
  * @brief Creates a new `DDDiagnostics` instance.
  *
@@ -186,6 +298,22 @@ Result destroyDDDiagnostics([[maybe_unused]] DDDiagnostics* self);
  */
 void dddiagnosticsOnStepForward(DDDiagnostics* diagnostics, size_t instruction);
 
+/**
+ * @brief Called during code preprocessing after parsing all instructions.
+ * @param diagnostics The diagnostics instance to update.
+ * @param instructions The parsed instructions.
+ */
+void dddiagnosticsOnCodePreprocessing(
+    DDDiagnostics* diagnostics, const std::vector<Instruction>& instructions);
+
+/**
+ * @brief Called, whenever an assertion fails to update the diagnostics.
+ * @param diagnostics The diagnostics instance to update.
+ * @param instruction The instruction that was executed.
+ */
+void dddiagnosticsOnFailedAssertion(DDDiagnostics* diagnostics,
+                                    size_t instruction);
+
 /**
  * @brief Tries to find potential errors caused by missing interactions at
  * runtime.

include/backend/debug.h

@@ -291,6 +291,20 @@ struct SimulationStateStruct {
   Result (*getClassicalVariableName)(SimulationState* self,
                                      size_t variableIndex, char* output);
 
+  /**
+   * @brief Gets the name of a quantum variable by its index.
+   *
+   * For registers, each index is counted as a separate variable and can be
+   * accessed separately. This method will return the name of the specific
+   * index of the register.
+   * @param self The instance to query.
+   * @param variableIndex The index of the variable.
+   * @param output A buffer to store the name of the variable.
+   * @return The result of the operation.
+   */
+  Result (*getQuantumVariableName)(SimulationState* self, size_t variableIndex,
+                                   char* output);
+
   /**
    * @brief Gets the full state vector of the simulation at the current time.
    *

include/backend/diagnostics.h

@@ -174,6 +174,44 @@ struct DiagnosticsStruct {
    */
   size_t (*potentialErrorCauses)(Diagnostics* self, ErrorCause* output,
                                  size_t count);
+
+  /**
+   * @brief Suggest movements of assertions to better positions.\n\n
+   *
+   * Calling this function with a `count` of 0 will return the number of
+   * assertions that can be suggested.
+   *
+   * @param self The diagnostics instance to query.
+   * @param originalPositions An array of assertion positions to be filled.
+   * Contains the original positions of the assertions that should be moved.
+   * @param suggestedPositions An array of assertion positions to be filled.
+   * Contains the suggested positions of the assertions that should be moved.
+   * @param count The maximum number of assertions to suggest movements for.
+   * @return The number of suggested movements.
+   */
+  size_t (*suggestAssertionMovements)(Diagnostics* self,
+                                      size_t* originalPositions,
+                                      size_t* suggestedPositions, size_t count);
+
+  /**
+   * @brief Suggest new assertions to be added to the code.
+   *
+   * These assertions are added by first observing assertions that failed during
+   * previous iterations. Therefore, the simulation must be run at least once
+   * before calling this function.\n\n
+   *
+   * Calling this function with a `count` of 0 will return the number of
+   * assertions that can be suggested.
+   *
+   * @param self The diagnostics instance to query.
+   * @param suggestedPositions An array of assertion positions to be filled.
+   * @param suggestedAssertions An array of assertion instruction strings to be
+   * filled. Each string expects a size of up to 256 characters.
+   * @param count The maximum number of assertions to suggest.
+   * @return The number of suggested assertions.
+   */
+  size_t (*suggestNewAssertions)(Diagnostics* self, size_t* suggestedPositions,
+                                 char** suggestedAssertions, size_t count);
 };
 
 #ifdef __cplusplus