[verifier] Remove unused qubits when verifying transformation steps (#207)

* [verifier] Remove unused qubits when verifying transformation steps

* more output when verbose

Author: xumingkuan

src/quartz/circuitseq/circuitseq.cpp

@@ -1271,14 +1271,16 @@ bool CircuitSeq::to_canonical_representation(const Context *ctx) {
 std::unique_ptr<CircuitSeq>
 CircuitSeq::get_permuted_seq(const std::vector<int> &qubit_permutation,
                              const std::vector<int> &input_param_permutation,
-                             Context *ctx) const {
+                             Context *ctx, int result_num_qubits) const {
   auto result = std::make_unique<CircuitSeq>(0);
   if (input_param_permutation.empty()) {
-    result->clone_from(*this, qubit_permutation, input_param_permutation, ctx);
+    result->clone_from(*this, qubit_permutation, input_param_permutation, ctx,
+                       result_num_qubits);
   } else {
     auto all_param_permutation =
         ctx->get_param_permutation(input_param_permutation);
-    result->clone_from(*this, qubit_permutation, all_param_permutation, ctx);
+    result->clone_from(*this, qubit_permutation, all_param_permutation, ctx,
+                       result_num_qubits);
   }
   return result;
 }
@@ -1311,8 +1313,9 @@ CircuitSeq::get_suffix_seq(const std::unordered_set<CircuitGate *> &start_gates,
 void CircuitSeq::clone_from(const CircuitSeq &other,
                             const std::vector<int> &qubit_permutation,
                             const std::vector<int> &param_permutation,
-                            const Context *ctx) {
-  num_qubits = other.num_qubits;
+                            const Context *ctx, int result_num_qubits) {
+  num_qubits = (result_num_qubits == -1 ? other.num_qubits : result_num_qubits);
+  int num_qubits_difference = other.num_qubits - num_qubits;
   original_fingerprint_ = other.original_fingerprint_;
   std::unordered_map<CircuitWire *, CircuitWire *> wires_mapping;
   std::unordered_map<CircuitGate *, CircuitGate *> gates_mapping;
@@ -1337,28 +1340,39 @@ void CircuitSeq::clone_from(const CircuitSeq &other,
     hash_value_valid_ = false;
   }
   if (qubit_permutation.empty()) {
+    assert(result_num_qubits == -1);
     for (int i = 0; i < (int)other.wires.size(); i++) {
       wires.emplace_back(std::make_unique<CircuitWire>(*(other.wires[i])));
       assert(wires[i].get() !=
              other.wires[i].get());  // make sure we make a copy
       wires_mapping[other.wires[i].get()] = wires[i].get();
     }
   } else {
-    assert(qubit_permutation.size() == num_qubits);
-    wires.resize(other.wires.size());
-    for (int i = 0; i < num_qubits; i++) {
-      assert(qubit_permutation[i] >= 0 && qubit_permutation[i] < num_qubits);
+    assert(qubit_permutation.size() == other.num_qubits);
+    wires.resize(other.wires.size() - num_qubits_difference);
+    for (int i = 0; i < other.num_qubits; i++) {
+      if (result_num_qubits == -1) {
+        assert(qubit_permutation[i] >= 0 && qubit_permutation[i] < num_qubits);
+      } else {
+        if (qubit_permutation[i] < 0 || qubit_permutation[i] >= num_qubits) {
+          continue;
+        }
+      }
       wires[qubit_permutation[i]] =
           std::make_unique<CircuitWire>(*(other.wires[i]));
       wires[qubit_permutation[i]]->index =
           qubit_permutation[i];  // update index
       assert(wires[qubit_permutation[i]].get() != other.wires[i].get());
       wires_mapping[other.wires[i].get()] = wires[qubit_permutation[i]].get();
     }
-    for (int i = num_qubits; i < (int)other.wires.size(); i++) {
-      wires[i] = std::make_unique<CircuitWire>(*(other.wires[i]));
-      wires[i]->index = qubit_permutation[wires[i]->index];  // update index
-      wires_mapping[other.wires[i].get()] = wires[i].get();
+    for (int i = other.num_qubits; i < (int)other.wires.size(); i++) {
+      wires[i - num_qubits_difference] =
+          std::make_unique<CircuitWire>(*(other.wires[i]));
+      // update index
+      wires[i - num_qubits_difference]->index =
+          qubit_permutation[wires[i - num_qubits_difference]->index];
+      wires_mapping[other.wires[i].get()] =
+          wires[i - num_qubits_difference].get();
     }
   }
   if (!param_permutation.empty()) {
@@ -1392,8 +1406,19 @@ void CircuitSeq::clone_from(const CircuitSeq &other,
       wire = wires_mapping[wire];
     }
   }
-  for (auto &wire : other.outputs) {
-    outputs.emplace_back(wires_mapping[wire]);
+  if (qubit_permutation.empty()) {
+    for (auto &wire : other.outputs) {
+      outputs.emplace_back(wires_mapping[wire]);
+    }
+  } else {
+    outputs.resize(num_qubits);
+    for (auto &wire : other.outputs) {
+      if (wires_mapping.count(wire) > 0) {
+        assert(qubit_permutation[wire->index] >= 0 &&
+               qubit_permutation[wire->index] < num_qubits);
+        outputs[qubit_permutation[wire->index]] = wires_mapping[wire];
+      }
+    }
   }
 }
 

src/quartz/circuitseq/circuitseq.h

@@ -272,19 +272,23 @@ class CircuitSeq {
   /**
    * Permute the qubits and input parameters.
    * @param qubit_permutation The qubit permutation. The size must be the
-   * same as the number of qubits.
+   * same as the number of qubits. When |result_num_qubits| is not -1,
+   * all qubits mapped to a number greater than or equal to |result_num_qubits|
+   * must be unused in any gates in this circuit.
    * @param input_param_permutation The input parameter permutation. If the size
    * is smaller than the total number of input parameters, this function only
    * permutes a prefix of input parameters corresponding to |param_permutation|.
    * @param ctx The context, only needed when |input_param_permutation| is not
    * empty. When |input_param_permutation| is empty, it is safe to pass in a
    * nullptr.
+   * @param result_num_qubits The number of qubits of the permuted circuit
+   * sequence. Default is -1, which means to copy from this circuit sequence.
    * @return The permuted circuit sequence.
    */
   [[nodiscard]] std::unique_ptr<CircuitSeq>
   get_permuted_seq(const std::vector<int> &qubit_permutation,
                    const std::vector<int> &input_param_permutation,
-                   Context *ctx) const;
+                   Context *ctx, int result_num_qubits = -1) const;
   /**
    * Get a circuit with |start_gates| and all gates topologically after them.
    * @param start_gates The first gates at each qubit to include in the
@@ -346,18 +350,25 @@ class CircuitSeq {
    * Clone the circuit from another circuit sequence.
    * @param other The source circuit sequence.
    * @param qubit_permutation The qubit permutation (optional).
-   * If not empty, the size must be the same as the number of qubits.
+   * If not empty, the size must be the same as the number of qubits of the
+   * other circuit sequence. When |result_num_qubits| is not -1, any unmapped
+   * qubits must be unused (i.e., there should be no gates on that qubit in
+   * the other circuit sequence). When |result_num_qubits| is -1, this parameter
+   * must be empty.
    * @param param_permutation The parameter permutation (optional).
    * If empty, |ctx| is not used and all parameters will be from the same
    * context as |other|.
    * @param ctx The context, only needed when |param_permutation| is not empty.
    * When |param_permutation| is empty, it is safe to pass in a nullptr.
+   * @param result_num_qubits The number of qubits of the permuted circuit
+   * sequence. Default is -1, which means to copy from the other (original)
+   * circuit sequence.
    * @return The permuted circuit sequence.
    */
   void clone_from(const CircuitSeq &other,
                   const std::vector<int> &qubit_permutation,
-                  const std::vector<int> &param_permutation,
-                  const Context *ctx);
+                  const std::vector<int> &param_permutation, const Context *ctx,
+                  int result_num_qubits = -1);
 
   /**
    * Remove a quantum gate from the graph, remove its output wires by default,
@@ -386,8 +397,10 @@ class CircuitSeq {
       std::vector<std::pair<CircuitSeqHashType, PhaseShiftIdType>> *other_hash);
 
  public:
+  // Invariant: wires[i] is the i-th qubit input
   std::vector<std::unique_ptr<CircuitWire>> wires;
   std::vector<std::unique_ptr<CircuitGate>> gates;
+  // Invariant: outputs[i] is the i-th qubit
   std::vector<CircuitWire *> outputs;
 
  private:

src/quartz/verifier/verifier.cpp

@@ -192,6 +192,26 @@ bool Verifier::equivalent(Context *ctx, const CircuitSeq *circuit1,
     }
   }
 
+  // Remove qubits with no gates to avoid creating 2^num_qubits variables in the
+  // verifier.
+  std::vector<int> qubit_permutation(num_qubits, -1);
+  int remaining_qubits = 0;
+  for (int i = 0; i < num_qubits; i++) {
+    if (c1->outputs[i] != c1->wires[i].get() ||
+        c2->outputs[i] != c2->wires[i].get()) {
+      // qubit used in at least one of the two circuits
+      qubit_permutation[i] = remaining_qubits++;
+    }
+  }
+  if (remaining_qubits < num_qubits) {
+    if (verbose) {
+      std::cout << "Reducing the number of qubits from " << num_qubits << " to "
+                << remaining_qubits << std::endl;
+    }
+    c1 = c1->get_permuted_seq(qubit_permutation, {}, ctx, remaining_qubits);
+    c2 = c2->get_permuted_seq(qubit_permutation, {}, ctx, remaining_qubits);
+  }
+
   if (verbose) {
     std::cout << "Checking Verifier::equivalent() on:" << std::endl;
     std::cout << c1->to_string(/*line_number=*/true) << std::endl;
@@ -216,7 +236,8 @@ bool Verifier::equivalent(Context *ctx, const CircuitSeq *circuit1,
       std::string("python ") + kQuartzRootPath.string() +
       "/src/python/verifier/verify_equivalences.py " +
       kQuartzRootPath.string() + "/tmp_before_verify.json " +
-      kQuartzRootPath.string() + "/tmp_after_verify.json";
+      kQuartzRootPath.string() + "/tmp_after_verify.json" +
+      (verbose ? " True True" : "");
   system(command_string.c_str());
   EquivalenceSet equiv_set;
   ret = equiv_set.load_json(ctx,