🎨 pre-commit fixes

include/cliffordsynthesis/Utils.hpp

@@ -10,14 +10,17 @@
 
 namespace cs {
 
-  const GateSet PAULIS {
-  qc::OpType::None, qc::OpType::X, qc::OpType::Y, qc::OpType::Z,
-  };
-
-    inline bool isPauli(const qc::OpType& gate) {
-    return PAULIS.containsGate(gate);
-  }
+const GateSet PAULIS{
+    qc::OpType::None,
+    qc::OpType::X,
+    qc::OpType::Y,
+    qc::OpType::Z,
+};
 
-  qc::OpType multiplyPaulis(const GateSet& paulis);
+inline bool isPauli(const qc::OpType& gate) {
+  return PAULIS.containsGate(gate);
+}
 
-} // namespace cs;
+qc::OpType multiplyPaulis(const GateSet& paulis);
+
+} // namespace cs

include/cliffordsynthesis/encoding/GateEncoder.hpp

@@ -27,10 +27,10 @@ class GateEncoder {
               const std::size_t                      timestepLimit,
               TableauEncoder::Variables*             tableauVars,
               std::shared_ptr<logicbase::LogicBlock> logicBlock,
-              GateSet                                singleQGates,
-              bool                                  ignorePhase = false)
+              GateSet singleQGates, bool ignorePhase = false)
       : N(nQubits), S(tableauSize), T(timestepLimit), tvars(tableauVars),
-        lb(std::move(logicBlock)), singleQubitGates(std::move(singleQGates)), ignoreRChanges(ignorePhase) {
+        lb(std::move(logicBlock)), singleQubitGates(std::move(singleQGates)),
+        ignoreRChanges(ignorePhase) {
     if (!singleQGates.isValidGateSet()) {
       throw qc::QFRException("Invalid gate set");
     }
@@ -68,7 +68,8 @@ class GateEncoder {
   virtual void encodeSymmetryBreakingConstraints();
 
   // extracting the circuit
-  qc::QuantumComputation extractCircuitFromModel(Results& res, logicbase::Model& model);
+  qc::QuantumComputation extractCircuitFromModel(Results&          res,
+                                                 logicbase::Model& model);
 
   [[nodiscard]] auto* getVariables() { return &vars; }
 

include/cliffordsynthesis/encoding/MultiGateEncoder.hpp

@@ -20,7 +20,7 @@ class MultiGateEncoder : public GateEncoder {
 protected:
   logicbase::LogicTerm   rChanges{};
   logicbase::LogicMatrix xorHelpers{};
-  
+
   void assertConsistency() const override;
   void assertGateConstraints() override;
   void assertRConstraints(std::size_t pos, std::size_t qubit) override;

include/cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp

@@ -5,56 +5,58 @@
 
 #pragma once
 
-#include <utility>
-
-#include "LogicTerm/Logic.hpp"
 #include "LogicBlock/LogicBlock.hpp"
+#include "LogicTerm/Logic.hpp"
 #include "LogicUtil/util_logicblock.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
 #include "operations/OpType.hpp"
+
 #include <memory>
+#include <utility>
 #include <vector>
 
 namespace cs::encoding {
-  using namespace logicbase;
-  class PhaseCorrectionEncoder {
-  public:
-    PhaseCorrectionEncoder(const std::size_t nQubits, const std::size_t tableauSize,
-                           Tableau  uncorrectedTableau, Tableau targetTableau)
-      : N{nQubits}, S{tableauSize}, uncorrected(std::move(uncorrectedTableau)), target(std::move(targetTableau)), paulis{N} {
-      bool success = true;
-      lb = logicutil::getZ3LogicBlock(success, true);
-        if (!success) {
-          FATAL() << "Could not initialize solver engine.";
-  }
+using namespace logicbase;
+class PhaseCorrectionEncoder {
+public:
+  PhaseCorrectionEncoder(const std::size_t nQubits,
+                         const std::size_t tableauSize,
+                         Tableau uncorrectedTableau, Tableau targetTableau)
+      : N{nQubits}, S{tableauSize}, uncorrected(std::move(uncorrectedTableau)),
+        target(std::move(targetTableau)), paulis{N} {
+    bool success = true;
+    lb           = logicutil::getZ3LogicBlock(success, true);
+    if (!success) {
+      FATAL() << "Could not initialize solver engine.";
     }
+  }
+
+  std::vector<qc::OpType> phaseCorrection();
 
-    std::vector<qc::OpType> phaseCorrection();
+protected:
+  // number of qubits N
+  std::size_t N{}; // NOLINT (readability-identifier-naming)
+  // number of rows in the tableau S
+  std::size_t S{}; // NOLINT (readability-identifier-naming)
+  // the logic block to use
+  std::shared_ptr<LogicBlock> lb{};
+  Tableau                     uncorrected{};
+  Tableau                     target{};
 
-  protected:
-        // number of qubits N
-    std::size_t N{}; // NOLINT (readability-identifier-naming)
-    // number of rows in the tableau S
-    std::size_t S{}; // NOLINT (readability-identifier-naming)
-    // the logic block to use
-    std::shared_ptr<LogicBlock> lb{}; 
-    Tableau uncorrected{};
-    Tableau target{};
-
-    logicbase::LogicMatrix paulis{}; //order: I, X, Y, Z
-    LogicVector        initialPhase{};
-    LogicVector         targetPhase{};
+  logicbase::LogicMatrix paulis{}; // order: I, X, Y, Z
+  LogicVector            initialPhase{};
+  LogicVector            targetPhase{};
 
-    LogicMatrix xorHelpers{};
+  LogicMatrix xorHelpers{};
 
-    void splitXorR(const LogicVector& changes);
+  void splitXorR(const LogicVector& changes);
 
-    [[nodiscard]] LogicVector vectorFromBitset(const std::bitset<64>& bs) const;
+  [[nodiscard]] LogicVector vectorFromBitset(const std::bitset<64>& bs) const;
 
-    void encodePauliConstraints();
+  void encodePauliConstraints();
 
-    void createVariables();
+  void createVariables();
 
-    std::vector<qc::OpType> extractResult();
-  }; 
-} // namespace cs;
+  std::vector<qc::OpType> extractResult();
+};
+} // namespace cs::encoding

include/cliffordsynthesis/encoding/SATEncoder.hpp

@@ -77,7 +77,7 @@ class SATEncoder {
   [[nodiscard]] logicbase::Result solve() const;
   void                            extractResultsFromModel(Results& res) const;
   void                            cleanup() const;
-  
+
   std::shared_ptr<logicbase::LogicBlock> lb;
   std::shared_ptr<TableauEncoder>        tableauEncoder;
   std::shared_ptr<GateEncoder>           gateEncoder;
@@ -90,8 +90,8 @@ class SATEncoder {
   std::size_t N{}; // NOLINT (readability-identifier-naming)
   // timestep limit T
   std::size_t T{}; // NOLINT (readability-identifier-naming)
-    // number of rows in the tableau S
-    std::size_t S{}; // NOLINT (readability-identifier-naming)
+  // number of rows in the tableau S
+  std::size_t S{}; // NOLINT (readability-identifier-naming)
 };
 
 } // namespace cs::encoding

include/cliffordsynthesis/encoding/TableauEncoder.hpp

@@ -20,9 +20,9 @@ class TableauEncoder {
   TableauEncoder(const std::size_t nQubits, const std::size_t tableauSize,
                  const std::size_t                      timestepLimit,
                  std::shared_ptr<logicbase::LogicBlock> logicBlock,
-                 bool ignorePhase=false)
-      : N(nQubits), S(tableauSize), T(timestepLimit),
-        lb(std::move(logicBlock)), ignoreR(ignorePhase) {}
+                 bool                                   ignorePhase = false)
+      : N(nQubits), S(tableauSize), T(timestepLimit), lb(std::move(logicBlock)),
+        ignoreR(ignorePhase) {}
 
   struct Variables {
     // variables for the X parts of the tableaus
@@ -59,8 +59,8 @@ class TableauEncoder {
   void assertTableau(const Tableau& tableau, std::size_t t);
 
   // extracting the tableau
-Tableau extractTableauFromModel(Results& results, std::size_t t,
-                               logicbase::Model& model) const;
+  Tableau extractTableauFromModel(Results& results, std::size_t t,
+                                  logicbase::Model& model) const;
 
   [[nodiscard]] auto* getVariables() { return &vars; }
 

src/cliffordsynthesis/CliffordSynthesizer.cpp

@@ -44,7 +44,7 @@ void CliffordSynthesizer::synthesize(const Configuration& config) {
   encoderConfig.solverParameters    = configuration.solverParameters;
   encoderConfig.useMultiGateEncoding =
       requiresMultiGateEncoding(encoderConfig.targetMetric);
-  encoderConfig.gateSet = configuration.gateSet;
+  encoderConfig.gateSet        = configuration.gateSet;
   encoderConfig.ignoreRChanges = config.delayPaulis;
 
   if (configuration.heuristic) {

src/cliffordsynthesis/encoding/SATEncoder.cpp

@@ -8,10 +8,10 @@
 #include "LogicUtil/util_logicblock.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
 #include "cliffordsynthesis/encoding/MultiGateEncoder.hpp"
+#include "cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp"
 #include "cliffordsynthesis/encoding/SingleGateEncoder.hpp"
 #include "operations/OpType.hpp"
 #include "utils/logging.hpp"
-#include "cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp"
 
 #include <chrono>
 #include <cstddef>
@@ -56,21 +56,24 @@ void SATEncoder::createFormulation() {
   initializeSolver();
 
   S = config.targetTableau->hasDestabilizers() &&
-                                config.initialTableau->hasDestabilizers()
-                            ? 2U * N
-                            : N;
+              config.initialTableau->hasDestabilizers()
+          ? 2U * N
+          : N;
 
-  tableauEncoder = std::make_shared<TableauEncoder>(N, S, T, lb, config.ignoreRChanges);
+  tableauEncoder =
+      std::make_shared<TableauEncoder>(N, S, T, lb, config.ignoreRChanges);
   tableauEncoder->createTableauVariables();
   tableauEncoder->assertTableau(*config.initialTableau, 0U);
   tableauEncoder->assertTableau(*config.targetTableau, T);
 
   if (config.useMultiGateEncoding) {
     gateEncoder = std::make_shared<MultiGateEncoder>(
-                                                     N, S, T, tableauEncoder->getVariables(), lb, config.gateSet, config.ignoreRChanges);
+        N, S, T, tableauEncoder->getVariables(), lb, config.gateSet,
+        config.ignoreRChanges);
   } else {
     gateEncoder = std::make_shared<SingleGateEncoder>(
-                                                      N, S, T, tableauEncoder->getVariables(), lb, config.gateSet, config.ignoreRChanges);
+        N, S, T, tableauEncoder->getVariables(), lb, config.gateSet,
+        config.ignoreRChanges);
   }
   gateEncoder->createSingleQubitGateVariables();
   gateEncoder->createTwoQubitGateVariables();
@@ -81,7 +84,7 @@ void SATEncoder::createFormulation() {
   }
 
   objectiveEncoder = std::make_shared<ObjectiveEncoder>(
-                                                        N, T, gateEncoder->getVariables(), lb, config.gateSet);
+      N, T, gateEncoder->getVariables(), lb, config.gateSet);
 
   if (config.gateLimit.has_value()) {
     objectiveEncoder->limitGateCount(*config.gateLimit, std::less_equal{});
@@ -121,31 +124,32 @@ void SATEncoder::extractResultsFromModel(Results& res) const {
   tableauEncoder->extractTableauFromModel(res, T, *model);
   auto qc = gateEncoder->extractCircuitFromModel(res, *model);
   if (config.ignoreRChanges) {
-      const auto start  = std::chrono::high_resolution_clock::now();
-      auto tab = *config.targetTableau;
-      auto qcTab = Tableau(qc, 0, std::numeric_limits<std::size_t>::max(), config.targetTableau->hasDestabilizers());
-      for(std::size_t row = 0U; row < S; ++row) {
-        DEBUG() << "Row " << std::to_string(row);
-        tab[row][2*N] = qcTab.at(row)[2*N];
-      }
+    const auto start = std::chrono::high_resolution_clock::now();
+    auto       tab   = *config.targetTableau;
+    auto       qcTab = Tableau(qc, 0, std::numeric_limits<std::size_t>::max(),
+                               config.targetTableau->hasDestabilizers());
+    for (std::size_t row = 0U; row < S; ++row) {
+      DEBUG() << "Row " << std::to_string(row);
+      tab[row][2 * N] = qcTab.at(row)[2 * N];
+    }
     PhaseCorrectionEncoder phaseCorrectionEncoder(N, S, tab,
                                                   *config.targetTableau);
-    auto paulis = phaseCorrectionEncoder.phaseCorrection();
-    
-    for(std::size_t row = 0U; row < S; ++row) {
-      tab[row][2*N] = config.targetTableau->at(row)[2*N];
+    auto                   paulis = phaseCorrectionEncoder.phaseCorrection();
+
+    for (std::size_t row = 0U; row < S; ++row) {
+      tab[row][2 * N] = config.targetTableau->at(row)[2 * N];
     }
-    
+
     for (std::size_t q = 0U; q < N; ++q) {
       if (paulis[q] != qc::OpType::None) {
         DEBUG() << "Phase correction for qubit " << q << ": "
                 << qc::toString(paulis[q]);
-      qc.emplace_back<qc::StandardOperation>(N, q, paulis[q]);
-      } 
+        qc.emplace_back<qc::StandardOperation>(N, q, paulis[q]);
+      }
     }
-      const auto end    = std::chrono::high_resolution_clock::now();
-      const auto runtime = std::chrono::duration<double>(end - start);
-      res.setRuntime(res.getRuntime() + runtime.count());
+    const auto end     = std::chrono::high_resolution_clock::now();
+    const auto runtime = std::chrono::duration<double>(end - start);
+    res.setRuntime(res.getRuntime() + runtime.count());
     res.setResultCircuit(qc);
     res.setResultTableau(tab);
     res.setDepth(qc.getDepth());

src/cliffordsynthesis/encoding/TableauEncoder.cpp

@@ -18,7 +18,7 @@ void TableauEncoder::createTableauVariables() {
   DEBUG() << "Creating tableau variables.";
   vars.x.reserve(T);
   vars.z.reserve(T);
-  if(!ignoreR){
+  if (!ignoreR) {
     vars.r.reserve(T);
   }
   for (std::size_t t = 0U; t <= T; ++t) {
@@ -36,7 +36,7 @@ void TableauEncoder::createTableauVariables() {
       TRACE() << "Creating variable " << zName;
       z.emplace_back(lb->makeVariable(zName, CType::BITVECTOR, n));
     }
-    if(!ignoreR){
+    if (!ignoreR) {
       const std::string rName = "r_" + std::to_string(t);
       TRACE() << "Creating variable " << rName;
       vars.r.emplace_back(lb->makeVariable(rName, CType::BITVECTOR, n));
@@ -58,26 +58,26 @@ void TableauEncoder::assertTableau(const Tableau&    tableau,
     lb->assertFormula(vars.z[t][a] == LogicTerm(targetZ, n));
   }
 
-  if(!ignoreR){
+  if (!ignoreR) {
     const auto targetR = tableau.getBVFrom(2U * N);
-    lb->assertFormula(vars.r[t] == LogicTerm(targetR, n));   
+    lb->assertFormula(vars.r[t] == LogicTerm(targetR, n));
   }
 }
 
 Tableau TableauEncoder::extractTableauFromModel(Results&          results,
-                                             const std::size_t t,
-                                             Model&            model) const {
+                                                const std::size_t t,
+                                                Model&            model) const {
   Tableau tableau(N, S > N);
   for (std::size_t i = 0; i < N; ++i) {
     const auto bvx = model.getBitvectorValue(vars.x[t][i], lb.get());
     tableau.populateTableauFrom(bvx, S, i);
     const auto bvz = model.getBitvectorValue(vars.z[t][i], lb.get());
     tableau.populateTableauFrom(bvz, S, i + N);
   }
-  if(!ignoreR){
+  if (!ignoreR) {
     const auto bvr = model.getBitvectorValue(vars.r[t], lb.get());
     tableau.populateTableauFrom(bvr, S, 2 * N);
-  } 
+  }
   results.setResultTableau(tableau);
   return tableau;
 }

src/python/bindings.cpp

@@ -527,8 +527,8 @@ PYBIND11_MODULE(pyqmap, m) {
                      "Gate Set to be used for the Synthesis. "
                      "Defaults to {H, S, Sdg, X, Y, Z, CX}.")
       .def_readwrite("delay_paulis", &cs::Configuration::delayPaulis,
-                      "Delay Pauli gates to the end of the circuit. "
-                      "Defaults to `false`.")
+                     "Delay Pauli gates to the end of the circuit. "
+                     "Defaults to `false`.")
       .def("json", &cs::Configuration::json,
            "Returns a JSON-style dictionary of all the information present in "
            "the :class:`.Configuration`")

test/cliffordsynthesis/test_synthesis.cpp

@@ -354,14 +354,14 @@ TEST_P(SynthesisTest, TestDestabilizerTwoQubitGates) {
 }
 
 TEST_P(SynthesisTest, DepthDelayedPhase) {
-  config.target    = TargetMetric::Depth;
+  config.target       = TargetMetric::Depth;
   config.linearSearch = true;
-  config.delayPaulis = true;
+  config.delayPaulis  = true;
   synthesizer.synthesize(config);
-  
+
   results = synthesizer.getResults();
 
-  EXPECT_LE(results.getDepth(), test.expectedMinimalDepth+1);
+  EXPECT_LE(results.getDepth(), test.expectedMinimalDepth + 1);
 }
 
 TEST(HeuristicTest, basic) {