From fcdb36ed66d84b38d42b9f72a95513696980dbab Mon Sep 17 00:00:00 2001 From: Jakob Date: Fri, 9 Aug 2024 18:45:49 +0200 Subject: [PATCH 01/36] add coupling maps for clifford synthesis --- .../cliffordsynthesis/CliffordSynthesizer.hpp | 36 ++++-- include/cliffordsynthesis/Results.hpp | 29 +++++ include/cliffordsynthesis/Tableau.hpp | 4 + .../encoding/GateEncoder.hpp | 15 ++- .../cliffordsynthesis/encoding/SATEncoder.hpp | 4 + .../encoding/TableauEncoder.hpp | 8 ++ src/cliffordsynthesis/CliffordSynthesizer.cpp | 1 + src/cliffordsynthesis/Tableau.cpp | 115 ++++++++++++++++++ .../encoding/GateEncoder.cpp | 23 ++-- .../encoding/MultiGateEncoder.cpp | 32 +++-- src/cliffordsynthesis/encoding/SATEncoder.cpp | 16 ++- .../encoding/SingleGateEncoder.cpp | 27 ++-- .../encoding/TableauEncoder.cpp | 62 ++++++++++ test/cliffordsynthesis/circuits.json | 100 +++++++++++++++ test/cliffordsynthesis/test_synthesis.cpp | 74 ++++++++++- 15 files changed, 489 insertions(+), 57 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 8f1d8d4b9..2cf55ff80 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -26,23 +26,44 @@ class CliffordSynthesizer { public: CliffordSynthesizer() = default; CliffordSynthesizer(Tableau initial, Tableau target) - : initialTableau(std::move(initial)), targetTableau(std::move(target)) {} + : initialTableau(std::move(initial)), targetTableau(std::move(target)), couplingMap(getFullyConnectedMap(target.getQubitCount())) {} + CliffordSynthesizer(Tableau initial, Tableau target, CouplingMap qm) + : initialTableau(std::move(initial)), targetTableau(std::move(target)), couplingMap(std::move(qm)) {} explicit CliffordSynthesizer(Tableau target) : initialTableau(target.getQubitCount(), target.hasDestabilizers()), - targetTableau(std::move(target)) {} + targetTableau(std::move(target)), + couplingMap(getFullyConnectedMap(target.getQubitCount())) {} CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc) : initialTableau(std::move(initial)), targetTableau(qc, 0, std::numeric_limits::max(), initialTableau.hasDestabilizers()), - initialCircuit(std::make_shared(qc)), - results(qc, targetTableau) {} + couplingMap(getFullyConnectedMap(initial.getQubitCount())), + initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(qc::QuantumComputation& qc, - const bool useDestabilizers = false) + const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), - initialCircuit(std::make_shared(qc)), - results(qc, targetTableau) {} + couplingMap(getFullyConnectedMap(qc.getNqubits())), + initialCircuit(std::make_shared(qc)) {} + explicit CliffordSynthesizer(Tableau target, CouplingMap qm) + : initialTableau(target.getQubitCount(), target.hasDestabilizers()), + targetTableau(std::move(target)), + couplingMap(std::move(qm)) {} + CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc, CouplingMap qm) + : initialTableau(std::move(initial)), + targetTableau(qc, 0, std::numeric_limits::max(), + initialTableau.hasDestabilizers()), + couplingMap(std::move(qm)), + initialCircuit(std::make_shared(qc)){} + explicit CliffordSynthesizer(qc::QuantumComputation& qc, + CouplingMap qm, + const bool useDestabilizers = false) + : initialTableau(qc.getNqubits(), useDestabilizers), + targetTableau(qc, 0, std::numeric_limits::max(), + useDestabilizers), + couplingMap(std::move(qm)), + initialCircuit(std::make_shared(qc)){} virtual ~CliffordSynthesizer() = default; @@ -71,6 +92,7 @@ class CliffordSynthesizer { protected: Tableau initialTableau{}; Tableau targetTableau{}; + CouplingMap couplingMap{}; std::shared_ptr initialCircuit{}; Configuration configuration{}; diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index 0f06cb3a7..d7d5977d0 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -12,6 +12,8 @@ #include #include #include +#include +#include namespace cs { class Results { @@ -49,6 +51,20 @@ class Results { [[nodiscard]] std::string getResultCircuit() const { return resultCircuit; } [[nodiscard]] std::string getResultTableau() const { return resultTableau; } + [[nodiscard]]std::string getMapping() const { + std::ostringstream oss; + for (const auto& row : pvector) { + for (bool val : row) { + oss << (val ? '1' : '0'); + } + oss << '\n'; + } + return oss.str(); + } + [[nodiscard]] std::vector> getMappingVector() const { + return pvector; + } + void setSingleQubitGates(const std::size_t g) { singleQubitGates = g; } void setTwoQubitGates(const std::size_t g) { twoQubitGates = g; } void setDepth(const std::size_t d) { depth = d; } @@ -66,6 +82,17 @@ class Results { ss << tableau; resultTableau = ss.str(); } + void setMapping(std::vector> p) { + std::ostringstream oss; + for (const auto& row : pvector) { + for (bool val : row) { + oss << (val ? '1' : '0'); + } + oss << '\n'; + } + pvals = oss.str(); + pvector = std::move(p); + } [[nodiscard]] bool sat() const { return getSolverResult() == logicbase::Result::SAT; @@ -99,6 +126,8 @@ class Results { double runtime = 0.0; std::size_t solverCalls = 0U; + std::string pvals{}; + std::vector> pvector{}; std::string resultTableau{}; std::string resultCircuit{}; }; diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index 9273920a7..ca82b23cc 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -158,5 +158,9 @@ class Tableau { [[nodiscard]] std::uint64_t getBVFrom(const std::size_t column) const { return getBVFrom<64>(column).to_ullong(); } + Tableau applyMapping(const std::vector> p); + Tableau reverseMapping(const std::vector> p); + Tableau reverseMappingOnRows(const std::vector> p, size_t nq); + void gaussianEliminationGF2(); }; } // namespace cs diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp index 2f1d6a6c3..63251f8cb 100644 --- a/include/cliffordsynthesis/encoding/GateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp @@ -9,6 +9,7 @@ #include "cliffordsynthesis/encoding/TableauEncoder.hpp" #include "logicblocks/LogicBlock.hpp" #include "operations/OpType.hpp" +#include "utils.hpp" #include #include @@ -20,8 +21,9 @@ class GateEncoder { GateEncoder(const std::size_t nQubits, const std::size_t tableauSize, const std::size_t timestepLimit, TableauEncoder::Variables* tableauVars, - std::shared_ptr logicBlock) - : N(nQubits), S(tableauSize), T(timestepLimit), tvars(tableauVars), + std::shared_ptr logicBlock, + CouplingMap cm) + : N(nQubits), S(tableauSize), T(timestepLimit), couplingMap(std::move(cm)), tvars(tableauVars), lb(std::move(logicBlock)) {} virtual ~GateEncoder() = default; @@ -36,7 +38,7 @@ class GateEncoder { logicbase::LogicVector& variables) const; void collectTwoQubitGateVariables(std::size_t pos, std::size_t qubit, bool target, - logicbase::LogicVector& variables) const; + logicbase::LogicVector& variables, CouplingMap cm) const; }; // variable creation @@ -49,7 +51,7 @@ class GateEncoder { assertGateConstraints(); } - virtual void encodeSymmetryBreakingConstraints(); + virtual void encodeSymmetryBreakingConstraints(CouplingMap couplingMap); // extracting the circuit void extractCircuitFromModel(Results& res, logicbase::Model& model); @@ -108,6 +110,9 @@ class GateEncoder { // timestep limit T std::size_t T{}; // NOLINT (readability-identifier-naming) + // coupling Map + CouplingMap couplingMap; + // the gate variables Variables vars{}; @@ -152,7 +157,7 @@ class GateEncoder { virtual void assertSingleQubitGateSymmetryBreakingConstraints(std::size_t pos); - virtual void assertTwoQubitGateSymmetryBreakingConstraints(std::size_t pos); + virtual void assertTwoQubitGateSymmetryBreakingConstraints(std::size_t pos, CouplingMap cm); virtual void assertSingleQubitGateOrderConstraints(std::size_t pos, std::size_t qubit) = 0; diff --git a/include/cliffordsynthesis/encoding/SATEncoder.hpp b/include/cliffordsynthesis/encoding/SATEncoder.hpp index 6997cce02..2faf59623 100644 --- a/include/cliffordsynthesis/encoding/SATEncoder.hpp +++ b/include/cliffordsynthesis/encoding/SATEncoder.hpp @@ -13,6 +13,7 @@ #include "cliffordsynthesis/encoding/TableauEncoder.hpp" #include "logicblocks/LogicBlock.hpp" #include "operations/OpType.hpp" +#include "utils.hpp" #include #include @@ -32,6 +33,9 @@ class SATEncoder { // the number of qubits to encode std::size_t nQubits{}; + // coupling Map of Qubits + CouplingMap couplingMap{}; + // the number of timesteps to encode std::size_t timestepLimit{}; diff --git a/include/cliffordsynthesis/encoding/TableauEncoder.hpp b/include/cliffordsynthesis/encoding/TableauEncoder.hpp index 58d9251bc..8ebbf379b 100644 --- a/include/cliffordsynthesis/encoding/TableauEncoder.hpp +++ b/include/cliffordsynthesis/encoding/TableauEncoder.hpp @@ -30,6 +30,8 @@ class TableauEncoder { logicbase::LogicMatrix z{}; // variables for the phase parts of the tableaus logicbase::LogicVector r{}; + // variables for mapping of qubits + logicbase::LogicMatrix p{}; // update rules for single-qubit gates [[nodiscard]] logicbase::LogicTerm @@ -63,6 +65,12 @@ class TableauEncoder { [[nodiscard]] auto* getVariables() { return &vars; } + // get mapping variables and store them in results + void extractMappingFromModel(Results& results, logicbase::Model& model) const; + + // assert constraints for mapping variables + void assertMappingConstraints(); + protected: // number of qubits N std::size_t N{}; // NOLINT (readability-identifier-naming) diff --git a/src/cliffordsynthesis/CliffordSynthesizer.cpp b/src/cliffordsynthesis/CliffordSynthesizer.cpp index ed83496da..4805a8657 100644 --- a/src/cliffordsynthesis/CliffordSynthesizer.cpp +++ b/src/cliffordsynthesis/CliffordSynthesizer.cpp @@ -39,6 +39,7 @@ void CliffordSynthesizer::synthesize(const Configuration& config) { encoderConfig.initialTableau = &initialTableau; encoderConfig.targetTableau = &targetTableau; encoderConfig.nQubits = initialTableau.getQubitCount(); + encoderConfig.couplingMap = couplingMap; encoderConfig.timestepLimit = configuration.initialTimestepLimit; encoderConfig.targetMetric = configuration.target; encoderConfig.useMaxSAT = configuration.useMaxSAT; diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 5cd95cdf5..231b297b5 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -484,4 +484,119 @@ bool Tableau::isIdentityTableau() const { } return true; } + +Tableau Tableau::applyMapping( const std::vector> p){ + Tableau mapped_tableau = Tableau(nQubits,hasDestabilizers()); + for(size_t i = 0; i < mapped_tableau.getTableauSize(); i++){ + for(size_t j = 0; j < mapped_tableau.tableau[i].size(); j++){ + mapped_tableau.tableau[i][j] = 0; + } + } + for (size_t i = 0; i < p.size(); i++) { + for (size_t j = 0; j < p[i].size(); j++) { + //apply mapping from column i to j if p is set + if(p[i][j]){ + //in every row swap x entry and z entry + for(size_t n = 0; n < mapped_tableau.getTableauSize(); n++){ + mapped_tableau.tableau[n][j] = tableau[n][i]; + mapped_tableau.tableau[n][j+mapped_tableau.nQubits] = tableau[n][i+mapped_tableau.nQubits]; + } + } + } + } + // copy r column without changes + for (size_t i = 0; i < tableau.size(); i++) { + mapped_tableau.tableau[i][2*nQubits] = tableau[i][2*nQubits]; + } + return mapped_tableau; +} + +Tableau Tableau::reverseMapping(const std::vector> p){ + Tableau mapped_tableau = Tableau(nQubits,hasDestabilizers()); + for(size_t i = 0; i < mapped_tableau.getTableauSize(); i++){ + for(size_t j = 0; j < mapped_tableau.tableau[i].size(); j++){ + mapped_tableau.tableau[i][j] = 0; + } + } + for (size_t i = 0; i < p.size(); i++) { + for (size_t j = 0; j < p[i].size(); j++) { + //apply mapping from column i to j if p is set + if(p[i][j]){ + //in every row swap x entry and z entry + for(size_t n = 0; n < mapped_tableau.getTableauSize(); n++){ + mapped_tableau.tableau[n][i] = tableau[n][j]; + mapped_tableau.tableau[n][i+mapped_tableau.nQubits] = tableau[n][j+mapped_tableau.nQubits]; + } + } + } + } + // copy r column without changes + for (size_t i = 0; i < tableau.size(); i++) { + mapped_tableau.tableau[i][2*nQubits] = tableau[i][2*nQubits]; + } + return mapped_tableau; +} + +// number of Qubits is passed because nQubits is not set in result Tableau of synthesis +Tableau Tableau::reverseMappingOnRows(const std::vector> p, size_t nq){ + Tableau mapped_tableau = Tableau(nq, true); + mapped_tableau.tableau = tableau; + for (size_t i = 0; i < p.size(); i++) { + for (size_t j = 0; j < p[i].size(); j++) { + //apply mapping from row i to j if p is set + if(p[i][j]){ + mapped_tableau.tableau[i] = tableau[j]; + mapped_tableau.tableau[i + nq] = tableau[j + nq]; + } + } + } + return mapped_tableau; +} + +// in place Gauss Elimination +void Tableau::gaussianEliminationGF2() { + size_t rows = tableau.size(); + size_t cols = tableau[0].size(); + if (rows == 1){ + return; + } + + size_t pivot = 0; + + for (size_t col = 0; col < cols; ++col) { + // find the pivot row for the current column + size_t maxRow = pivot; + if(maxRow >= rows){ + break; + } + for (size_t row = pivot; row < rows; ++row) { + if (tableau[row][col] == 1) { + maxRow = row; + break; + } + } + // if no pivot is found, continue to the next column + if (tableau[maxRow][col] == 0) { + continue; + } + // swap the pivot row with the current row + std::swap(tableau[pivot], tableau[maxRow]); + + // eliminate all other 1s in the current column + for (size_t row = 0; row < rows; ++row) { + if (row != pivot && tableau[row][col] == 1) { + for (size_t k = 0; k < cols; ++k) { + if(tableau[row][k] == tableau[pivot][k]){ + tableau[row][k] = 0; + } + else{ + tableau[row][k] = 1; + } + } + } + } + pivot++; + } + +} } // namespace cs diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp index 341ba209c..01ba80ea6 100644 --- a/src/cliffordsynthesis/encoding/GateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp @@ -4,6 +4,9 @@ // #include "cliffordsynthesis/encoding/GateEncoder.hpp" +#include "Logic.hpp" +#include "LogicTerm.hpp" +#include "utils.hpp" #include "Definitions.hpp" #include "logicblocks/Encodings.hpp" @@ -65,7 +68,7 @@ void GateEncoder::Variables::collectSingleQubitGateVariables( void GateEncoder::Variables::collectTwoQubitGateVariables( const std::size_t pos, const std::size_t qubit, const bool target, - LogicVector& variables) const { + LogicVector& variables, const CouplingMap cm) const { const auto& twoQubitGates = gC[pos]; const auto n = twoQubitGates.size(); for (std::size_t q = 0; q < n; ++q) { @@ -125,12 +128,12 @@ void GateEncoder::assertZConstraints(const std::size_t pos, const std::size_t qubit) { const auto& gatesToZTransformations = [this](const auto& p1, const auto& p2, const auto& p3) { - return tvars->singleQubitZChange(p1, p2, p3); + return tvars->singleQubitZChange(p1 + 1, p2, p3); }; auto gateTransformations = collectGateTransformations(pos, qubit, gatesToZTransformations); for (auto& [transformation, _] : gateTransformations) { - transformation = tvars->z[pos + 1][qubit] == transformation; + transformation = tvars->z[pos + 2][qubit] == transformation; } assertGatesImplyTransform(pos, qubit, gateTransformations); } @@ -139,12 +142,12 @@ void GateEncoder::assertXConstraints(const std::size_t pos, const std::size_t qubit) { const auto& gatesToXTransformations = [this](const auto& p1, const auto& p2, const auto& p3) { - return tvars->singleQubitXChange(p1, p2, p3); + return tvars->singleQubitXChange(p1 + 1, p2, p3); }; auto gateTransformations = collectGateTransformations(pos, qubit, gatesToXTransformations); for (auto& [transformation, _] : gateTransformations) { - transformation = tvars->x[pos + 1][qubit] == transformation; + transformation = tvars->x[pos + 2][qubit] == transformation; } assertGatesImplyTransform(pos, qubit, gateTransformations); } @@ -153,12 +156,12 @@ void GateEncoder::assertRConstraints(const std::size_t pos, const std::size_t qubit) { const auto& gatesToRTransformations = [this](const auto& p1, const auto& p2, const auto& p3) { - return tvars->singleQubitRChange(p1, p2, p3); + return tvars->singleQubitRChange(p1 + 1, p2, p3); }; auto gateTransformations = collectGateTransformations(pos, qubit, gatesToRTransformations); for (auto& [transformation, _] : gateTransformations) { - transformation = tvars->r[pos + 1] == (tvars->r[pos] ^ transformation); + transformation = tvars->r[pos + 2] == (tvars->r[pos + 1] ^ transformation); } assertGatesImplyTransform(pos, qubit, gateTransformations); } @@ -219,11 +222,11 @@ void GateEncoder::extractTwoQubitGatesFromModel(const std::size_t pos, } } -void GateEncoder::encodeSymmetryBreakingConstraints() { +void GateEncoder::encodeSymmetryBreakingConstraints(const CouplingMap couplingMap) { PLOG_DEBUG << "Encoding symmetry breaking constraints."; for (std::size_t t = 0U; t < T; ++t) { assertSingleQubitGateSymmetryBreakingConstraints(t); - assertTwoQubitGateSymmetryBreakingConstraints(t); + assertTwoQubitGateSymmetryBreakingConstraints(t, couplingMap); } } @@ -333,7 +336,7 @@ void GateEncoder::assertSingleQubitGateSymmetryBreakingConstraints( } void GateEncoder::assertTwoQubitGateSymmetryBreakingConstraints( - const std::size_t pos) { + const std::size_t pos, const CouplingMap cm) { for (std::size_t ctrl = 1U; ctrl < N; ++ctrl) { for (std::size_t trgt = 0U; trgt < ctrl; ++trgt) { assertTwoQubitGateOrderConstraints(pos, ctrl, trgt); diff --git a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp index 17316d2df..2d0d28c88 100644 --- a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp @@ -19,8 +19,8 @@ void encoding::MultiGateEncoder::assertConsistency() const { for (std::size_t q = 0U; q < N; ++q) { LogicVector gateVariables{}; vars.collectSingleQubitGateVariables(t, q, gateVariables); - vars.collectTwoQubitGateVariables(t, q, true, gateVariables); - vars.collectTwoQubitGateVariables(t, q, false, gateVariables); + vars.collectTwoQubitGateVariables(t, q, true, gateVariables, couplingMap); + vars.collectTwoQubitGateVariables(t, q, false, gateVariables, couplingMap); IF_PLOG(plog::verbose) { PLOG_VERBOSE << "Gate variables at time " << t << " and qubit " << q; @@ -39,12 +39,12 @@ void encoding::MultiGateEncoder::assertGateConstraints() { xorHelpers = logicbase::LogicMatrix{T}; for (std::size_t t = 0U; t < T; ++t) { PLOG_VERBOSE << "Asserting gate constraints at time " << t; - rChanges = tvars->r[t]; - splitXorR(tvars->r[t], t); + rChanges = tvars->r[t + 1]; + splitXorR(tvars->r[t + 1], t); assertSingleQubitGateConstraints(t); assertTwoQubitGateConstraints(t); PLOG_VERBOSE << "Asserting r changes at time " << t; - lb->assertFormula(tvars->r[t + 1] == xorHelpers[t].back()); + lb->assertFormula(tvars->r[t + 2] == xorHelpers[t].back()); } } @@ -62,7 +62,7 @@ void MultiGateEncoder::assertRConstraints(const std::size_t pos, for (const auto gate : SINGLE_QUBIT_GATES) { const auto& change = LogicTerm::ite(vars.gS[pos][gateToIndex(gate)][qubit], - tvars->singleQubitRChange(pos, qubit, gate), + tvars->singleQubitRChange(pos + 1, qubit, gate), LogicTerm(0, static_cast(S))); splitXorR(change, pos); } @@ -76,6 +76,12 @@ void encoding::MultiGateEncoder::assertTwoQubitGateConstraints( if (ctrl == trgt) { continue; } + // if no connection between ctrl and trgt then assert variable is false + if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { + PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt; + lb->assertFormula(LogicTerm(!twoQubitGates[ctrl][trgt])); + continue; + } const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt); lb->assertFormula(LogicTerm::implies(twoQubitGates[ctrl][trgt], changes)); @@ -87,16 +93,16 @@ void encoding::MultiGateEncoder::assertTwoQubitGateConstraints( LogicTerm encoding::MultiGateEncoder::createTwoQubitGateConstraint( std::size_t pos, std::size_t ctrl, std::size_t trgt) { auto changes = LogicTerm(true); - const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos, ctrl, trgt); - const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos, ctrl, trgt); + const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos + 1, ctrl, trgt); + const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos + 1, ctrl, trgt); - changes = changes && (tvars->x[pos + 1][ctrl] == xCtrl); - changes = changes && (tvars->x[pos + 1][trgt] == xTrgt); - changes = changes && (tvars->z[pos + 1][ctrl] == zCtrl); - changes = changes && (tvars->z[pos + 1][trgt] == zTrgt); + changes = changes && (tvars->x[pos + 2][ctrl] == xCtrl); + changes = changes && (tvars->x[pos + 2][trgt] == xTrgt); + changes = changes && (tvars->z[pos + 2][ctrl] == zCtrl); + changes = changes && (tvars->z[pos + 2][trgt] == zTrgt); const auto& newRChanges = LogicTerm::ite( - vars.gC[pos][ctrl][trgt], tvars->twoQubitRChange(pos, ctrl, trgt), + vars.gC[pos][ctrl][trgt], tvars->twoQubitRChange(pos + 1, ctrl, trgt), LogicTerm(0, static_cast(S))); splitXorR(newRChanges, pos); return changes; diff --git a/src/cliffordsynthesis/encoding/SATEncoder.cpp b/src/cliffordsynthesis/encoding/SATEncoder.cpp index a0700ebbd..467cc121e 100644 --- a/src/cliffordsynthesis/encoding/SATEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SATEncoder.cpp @@ -9,6 +9,7 @@ #include "cliffordsynthesis/encoding/SingleGateEncoder.hpp" #include "logicblocks/util_logicblock.hpp" #include "plog/Log.h" +#include "utils.hpp" #include #include @@ -62,24 +63,25 @@ void SATEncoder::createFormulation() { ? 2U * N : N; - tableauEncoder = std::make_shared(N, s, T, lb); + tableauEncoder = std::make_shared(N, s, T + 2, lb); tableauEncoder->createTableauVariables(); tableauEncoder->assertTableau(*config.initialTableau, 0U); - tableauEncoder->assertTableau(*config.targetTableau, T); + tableauEncoder->assertTableau(*config.targetTableau, T + 2); + tableauEncoder->assertMappingConstraints(); if (config.useMultiGateEncoding) { gateEncoder = std::make_shared( - N, s, T, tableauEncoder->getVariables(), lb); + N, s, T, tableauEncoder->getVariables(), lb, config.couplingMap); } else { gateEncoder = std::make_shared( - N, s, T, tableauEncoder->getVariables(), lb); + N, s, T, tableauEncoder->getVariables(), lb, config.couplingMap); } gateEncoder->createSingleQubitGateVariables(); gateEncoder->createTwoQubitGateVariables(); gateEncoder->encodeGates(); if (config.useSymmetryBreaking) { - gateEncoder->encodeSymmetryBreakingConstraints(); + gateEncoder->encodeSymmetryBreakingConstraints(config.couplingMap); } objectiveEncoder = @@ -120,7 +122,9 @@ Result SATEncoder::solve() const { void SATEncoder::extractResultsFromModel(Results& res) const { auto* const model = lb->getModel(); - tableauEncoder->extractTableauFromModel(res, T, *model); + // result is tableau with mapping applied + tableauEncoder->extractTableauFromModel(res, T + 1, *model); + tableauEncoder->extractMappingFromModel(res, *model); gateEncoder->extractCircuitFromModel(res, *model); } diff --git a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp index 04dc9a571..fe15f39e1 100644 --- a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp @@ -18,7 +18,7 @@ void SingleGateEncoder::assertConsistency() const { for (std::size_t t = 0U; t < T; ++t) { for (std::size_t q = 0U; q < N; ++q) { vars.collectSingleQubitGateVariables(t, q, gateVariables); - vars.collectTwoQubitGateVariables(t, q, true, gateVariables); + vars.collectTwoQubitGateVariables(t, q, true, gateVariables, couplingMap); } IF_PLOG(plog::verbose) { PLOG_VERBOSE << "Gate variables at time " << t; @@ -65,6 +65,11 @@ void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) { if (ctrl == trgt) { continue; } + if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { + PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt; + lb->assertFormula(LogicTerm(!twoQubitGates[ctrl][trgt])); + continue; + } const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt); PLOG_DEBUG << "Asserting CNOT on " << ctrl << " and " << trgt; @@ -77,16 +82,16 @@ void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) { LogicTerm SingleGateEncoder::createTwoQubitGateConstraint( const std::size_t pos, const std::size_t ctrl, const std::size_t trgt) { auto changes = LogicTerm(true); - const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos, ctrl, trgt); - const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos, ctrl, trgt); + const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos + 1, ctrl, trgt); + const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos + 1, ctrl, trgt); - changes = changes && (tvars->x[pos + 1][ctrl] == xCtrl); - changes = changes && (tvars->x[pos + 1][trgt] == xTrgt); - changes = changes && (tvars->z[pos + 1][ctrl] == zCtrl); - changes = changes && (tvars->z[pos + 1][trgt] == zTrgt); + changes = changes && (tvars->x[pos + 2][ctrl] == xCtrl); + changes = changes && (tvars->x[pos + 2][trgt] == xTrgt); + changes = changes && (tvars->z[pos + 2][ctrl] == zCtrl); + changes = changes && (tvars->z[pos + 2][trgt] == zTrgt); changes = - changes && (tvars->r[pos + 1] == - (tvars->r[pos] ^ tvars->twoQubitRChange(pos, ctrl, trgt))); + changes && (tvars->r[pos + 2] == + (tvars->r[pos + 1] ^ tvars->twoQubitRChange(pos + 1, ctrl, trgt))); return changes; } @@ -94,8 +99,8 @@ LogicTerm SingleGateEncoder::createTwoQubitGateConstraint( LogicTerm SingleGateEncoder::createNoChangeOnQubit(const std::size_t pos, const std::size_t q) { auto noChange = LogicTerm(true); - noChange = noChange && (tvars->x[pos + 1][q] == tvars->x[pos][q]); - noChange = noChange && (tvars->z[pos + 1][q] == tvars->z[pos][q]); + noChange = noChange && (tvars->x[pos + 2][q] == tvars->x[pos + 1][q]); + noChange = noChange && (tvars->z[pos + 2][q] == tvars->z[pos + 1][q]); return noChange; } diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 6767791f4..57b91300d 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -5,6 +5,7 @@ #include "cliffordsynthesis/encoding/TableauEncoder.hpp" +#include "LogicTerm.hpp" #include "logicblocks/Model.hpp" #include "plog/Log.h" @@ -38,6 +39,17 @@ void TableauEncoder::createTableauVariables() { PLOG_VERBOSE << "Creating variable " << rName; vars.r.emplace_back(lb->makeVariable(rName, CType::BITVECTOR, n)); } + PLOG_DEBUG << "Creating mapping variables."; + vars.p.reserve(N); + for (std::size_t i = 0U; i < N; ++i) { + auto& g = vars.p.emplace_back(); + g.reserve(N); + for (std::size_t j = 0U; j < N; ++j) { + const std::string pName = "p_" + std::to_string(i) + "_" + std::to_string(j); + PLOG_VERBOSE << "Creating variable " << pName; + g.emplace_back(lb->makeVariable(pName)); + } + } } void TableauEncoder::assertTableau(const Tableau& tableau, @@ -58,6 +70,45 @@ void TableauEncoder::assertTableau(const Tableau& tableau, lb->assertFormula(vars.r[t] == LogicTerm(targetR, n)); } +void TableauEncoder::assertMappingConstraints(){ + // if p_i_j is set column i is mapped to column j between 0 and 1 + for (std::size_t i = 0U; i < N; ++i) { + for (std::size_t j = 0U; j < N; ++j) { + lb->assertFormula(LogicTerm::implies(vars.p[i][j], vars.x[1][j] == vars.x[0][i])); + lb->assertFormula(LogicTerm::implies(vars.p[i][j], vars.z[1][j] == vars.z[0][i])); + } + } + // assert that r vals are unchanges between 0 and 1 + lb->assertFormula(LogicTerm::eq(vars.r[0],vars.r[1])); + // assert that for every i and j exactly one p variable is set + for (std::size_t i = 0U; i < N; ++i) { + int32_t vr = 0; + int32_t vr1 = 1; + LogicTerm sumRow = LogicTerm(vr); + for (std::size_t j = 0U; j < N; ++j) { + sumRow = sumRow + vars.p[i][j]; + } + lb->assertFormula(sumRow == LogicTerm(vr1)); + int32_t vc = 0; + int32_t vc1 = 1; + LogicTerm sumCol = LogicTerm(vc); + for (std::size_t j = 0U; j < N; ++j) { + sumCol = sumCol + vars.p[j][i]; + } + lb->assertFormula(sumCol == LogicTerm(vc1)); + } + // if p_i_j is set undo mapping between T-1 and T + for (std::size_t i = 0U; i < N; ++i) { + for (std::size_t j = 0U; j < N; ++j) { + lb->assertFormula(LogicTerm::implies(vars.p[i][j] , vars.x[T][i] == vars.x[T - 1][j])); + lb->assertFormula(LogicTerm::implies(vars.p[i][j] , vars.z[T][i] == vars.z[T - 1][j])); + + } + } + // assert that r vals are unchanges between T-1 and T + lb->assertFormula(LogicTerm::eq(vars.r[T - 1],vars.r[T])); +} + void TableauEncoder::extractTableauFromModel(Results& results, const std::size_t t, Model& model) const { @@ -74,6 +125,17 @@ void TableauEncoder::extractTableauFromModel(Results& results, results.setResultTableau(tableau); } +void TableauEncoder::extractMappingFromModel(Results& results, Model& model) const { + std::vector row(N,false); + std::vector> pvals(N,std::vector(N,false)); + for (std::size_t i = 0; i +#include using namespace qc::literals; @@ -17,6 +21,7 @@ struct TestConfiguration { std::string initialTableau; std::string targetTableau; std::string initialCircuit; + std::string couplingMap; // expected output std::size_t expectedMinimalGates{}; @@ -38,6 +43,9 @@ inline void from_json(const nlohmann::json& j, TestConfiguration& test) { if (j.contains("initial_circuit")) { test.initialCircuit = j.at("initial_circuit").get(); } + if (j.contains("couplingMap")) { + test.couplingMap = j.at("couplingMap").get(); + } test.expectedMinimalGates = j.at("expected_minimal_gates").get(); test.expectedMinimalDepth = j.at("expected_minimal_depth").get(); @@ -59,6 +67,30 @@ std::vector getTests(const std::string& path) { } } // namespace +CouplingMap parseEdges(const std::string &edgeString) { + CouplingMap edges; + std::stringstream ss(edgeString); + std::string item; + + while (getline(ss, item, ';')) { + item.erase(remove(item.begin(), item.end(), '{'), item.end()); + item.erase(remove(item.begin(), item.end(), '}'), item.end()); + size_t pos = item.find(','); + std::string first, second; + + first = item.substr(0, pos); + second = item.substr(pos+1); + + int u = stoi(first); + int v = stoi(second); + + // Insert the edge into the set + edges.insert(Edge{u, v}); + std::cout << "Edge " << u << "," << v << " inserted to cm\n"; + } + + return edges; +} class SynthesisTest : public ::testing::TestWithParam { protected: void SetUp() override { @@ -75,8 +107,13 @@ class SynthesisTest : public ::testing::TestWithParam { if (test.initialTableau.empty()) { initialTableau = Tableau(qc.getNqubits()); initialTableauWithDestabilizer = Tableau(qc.getNqubits(), true); - synthesizer = CliffordSynthesizer(qc); - synthesizerWithDestabilizer = CliffordSynthesizer(qc, true); + if(test.couplingMap.empty()){ + synthesizer = CliffordSynthesizer(qc); + synthesizerWithDestabilizer = CliffordSynthesizer(qc, true); + } else{ + synthesizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap)); + synthesizerWithDestabilizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap), true); + } } else { initialTableau = Tableau(test.initialTableau); std::cout << "Initial tableau:\n" << initialTableau; @@ -104,9 +141,31 @@ class SynthesisTest : public ::testing::TestWithParam { void TearDown() override { std::cout << "Results:\n" << results << "\n"; - resultTableau = synthesizer.getResultTableau(); - std::cout << "Resulting tableau:\n" << resultTableau; - EXPECT_EQ(resultTableau, targetTableau); + std::cout << "Mapping of Qubits:\n" << results.getMapping() << "\n"; + + resultTableau = Tableau(synthesizer.getResultTableau()); + + std::cout << "Result tableau:\n" << resultTableau; + + std::cout << "Target tableau:\n" << targetTableau; + + const std::vector> p = results.getMappingVector(); + Tableau targetPrime = targetTableau.applyMapping(p); + std::cout << "Target tableau with mapping:\n" << targetPrime; + if(!targetPrime.hasDestabilizers()){ + targetPrime.gaussianEliminationGF2(); + resultTableau.gaussianEliminationGF2(); + std::cout << "Target tableau with mapping and Gauss:\n" << targetPrime; + std::cout << "Result tableau with mapping and Gauss:\n" << resultTableau; + } else{ + targetPrime = targetPrime.reverseMappingOnRows(p, targetPrime.getQubitCount()); + resultTableau = resultTableau.reverseMappingOnRows(p, targetPrime.getQubitCount()); + std::cout << "Result tableau with destab mapping reversed:\n" << resultTableau; + std::cout << "Target tableau with destab mapping reversed:\n" << targetPrime; + + } + + EXPECT_EQ(resultTableau, targetPrime); const auto& resultCircuit = synthesizer.getResultCircuit(); std::cout << "Resulting Circuit:\n" << resultCircuit; @@ -118,6 +177,11 @@ class SynthesisTest : public ::testing::TestWithParam { for (const auto& gate : qc) { circuitTableau.applyGate(gate.get()); } + std::cout << "Circuit Tableau :\n" << circuitTableau; + if(!circuitTableau.hasDestabilizers()){ + circuitTableau.gaussianEliminationGF2(); + std::cout << "Circuit Tableau with Gauss" << circuitTableau; + } EXPECT_EQ(resultTableau, circuitTableau); } From 649c0b23fe988bf6933acc4329f7c5f8be852696 Mon Sep 17 00:00:00 2001 From: Jakob Date: Sat, 10 Aug 2024 00:29:54 +0200 Subject: [PATCH 02/36] fix unnecessary copies of coupling map --- include/cliffordsynthesis/CliffordSynthesizer.hpp | 9 +++++---- include/cliffordsynthesis/encoding/GateEncoder.hpp | 6 +++--- src/cliffordsynthesis/encoding/GateEncoder.cpp | 12 ++++++++---- src/cliffordsynthesis/encoding/MultiGateEncoder.cpp | 6 +++--- src/cliffordsynthesis/encoding/SATEncoder.cpp | 2 +- src/cliffordsynthesis/encoding/SingleGateEncoder.cpp | 4 ++-- 6 files changed, 22 insertions(+), 17 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 2cf55ff80..28dd8f281 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -12,6 +12,7 @@ #include "cliffordsynthesis/encoding/SATEncoder.hpp" #include "plog/Log.h" +#include #include #include #include @@ -26,25 +27,25 @@ class CliffordSynthesizer { public: CliffordSynthesizer() = default; CliffordSynthesizer(Tableau initial, Tableau target) - : initialTableau(std::move(initial)), targetTableau(std::move(target)), couplingMap(getFullyConnectedMap(target.getQubitCount())) {} + : initialTableau(std::move(initial)), targetTableau(std::move(target)), couplingMap(getFullyConnectedMap(static_cast(target.getQubitCount()))) {} CliffordSynthesizer(Tableau initial, Tableau target, CouplingMap qm) : initialTableau(std::move(initial)), targetTableau(std::move(target)), couplingMap(std::move(qm)) {} explicit CliffordSynthesizer(Tableau target) : initialTableau(target.getQubitCount(), target.hasDestabilizers()), targetTableau(std::move(target)), - couplingMap(getFullyConnectedMap(target.getQubitCount())) {} + couplingMap(getFullyConnectedMap(static_cast(target.getQubitCount()))) {} CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc) : initialTableau(std::move(initial)), targetTableau(qc, 0, std::numeric_limits::max(), initialTableau.hasDestabilizers()), - couplingMap(getFullyConnectedMap(initial.getQubitCount())), + couplingMap(getFullyConnectedMap(static_cast(initial.getQubitCount()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(qc::QuantumComputation& qc, const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), - couplingMap(getFullyConnectedMap(qc.getNqubits())), + couplingMap(getFullyConnectedMap(static_cast(qc.getNqubits()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(Tableau target, CouplingMap qm) : initialTableau(target.getQubitCount(), target.hasDestabilizers()), diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp index 63251f8cb..ba0b1348d 100644 --- a/include/cliffordsynthesis/encoding/GateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp @@ -38,7 +38,7 @@ class GateEncoder { logicbase::LogicVector& variables) const; void collectTwoQubitGateVariables(std::size_t pos, std::size_t qubit, bool target, - logicbase::LogicVector& variables, CouplingMap cm) const; + logicbase::LogicVector& variables) const; }; // variable creation @@ -51,7 +51,7 @@ class GateEncoder { assertGateConstraints(); } - virtual void encodeSymmetryBreakingConstraints(CouplingMap couplingMap); + virtual void encodeSymmetryBreakingConstraints(); // extracting the circuit void extractCircuitFromModel(Results& res, logicbase::Model& model); @@ -157,7 +157,7 @@ class GateEncoder { virtual void assertSingleQubitGateSymmetryBreakingConstraints(std::size_t pos); - virtual void assertTwoQubitGateSymmetryBreakingConstraints(std::size_t pos, CouplingMap cm); + virtual void assertTwoQubitGateSymmetryBreakingConstraints(std::size_t pos); virtual void assertSingleQubitGateOrderConstraints(std::size_t pos, std::size_t qubit) = 0; diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp index 01ba80ea6..db10b51e9 100644 --- a/src/cliffordsynthesis/encoding/GateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp @@ -68,7 +68,7 @@ void GateEncoder::Variables::collectSingleQubitGateVariables( void GateEncoder::Variables::collectTwoQubitGateVariables( const std::size_t pos, const std::size_t qubit, const bool target, - LogicVector& variables, const CouplingMap cm) const { + LogicVector& variables) const { const auto& twoQubitGates = gC[pos]; const auto n = twoQubitGates.size(); for (std::size_t q = 0; q < n; ++q) { @@ -222,11 +222,11 @@ void GateEncoder::extractTwoQubitGatesFromModel(const std::size_t pos, } } -void GateEncoder::encodeSymmetryBreakingConstraints(const CouplingMap couplingMap) { +void GateEncoder::encodeSymmetryBreakingConstraints() { PLOG_DEBUG << "Encoding symmetry breaking constraints."; for (std::size_t t = 0U; t < T; ++t) { assertSingleQubitGateSymmetryBreakingConstraints(t); - assertTwoQubitGateSymmetryBreakingConstraints(t, couplingMap); + assertTwoQubitGateSymmetryBreakingConstraints(t); } } @@ -336,9 +336,13 @@ void GateEncoder::assertSingleQubitGateSymmetryBreakingConstraints( } void GateEncoder::assertTwoQubitGateSymmetryBreakingConstraints( - const std::size_t pos, const CouplingMap cm) { + const std::size_t pos) { for (std::size_t ctrl = 1U; ctrl < N; ++ctrl) { for (std::size_t trgt = 0U; trgt < ctrl; ++trgt) { + // avoid unnecessary constraints if CNOT cannot be applied anyways + if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { + continue; + } assertTwoQubitGateOrderConstraints(pos, ctrl, trgt); } } diff --git a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp index 2d0d28c88..fff8c16da 100644 --- a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp @@ -19,8 +19,8 @@ void encoding::MultiGateEncoder::assertConsistency() const { for (std::size_t q = 0U; q < N; ++q) { LogicVector gateVariables{}; vars.collectSingleQubitGateVariables(t, q, gateVariables); - vars.collectTwoQubitGateVariables(t, q, true, gateVariables, couplingMap); - vars.collectTwoQubitGateVariables(t, q, false, gateVariables, couplingMap); + vars.collectTwoQubitGateVariables(t, q, true, gateVariables); + vars.collectTwoQubitGateVariables(t, q, false, gateVariables); IF_PLOG(plog::verbose) { PLOG_VERBOSE << "Gate variables at time " << t << " and qubit " << q; @@ -79,7 +79,7 @@ void encoding::MultiGateEncoder::assertTwoQubitGateConstraints( // if no connection between ctrl and trgt then assert variable is false if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt; - lb->assertFormula(LogicTerm(!twoQubitGates[ctrl][trgt])); + lb->assertFormula(!twoQubitGates[ctrl][trgt]); continue; } const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt); diff --git a/src/cliffordsynthesis/encoding/SATEncoder.cpp b/src/cliffordsynthesis/encoding/SATEncoder.cpp index 467cc121e..63f55942a 100644 --- a/src/cliffordsynthesis/encoding/SATEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SATEncoder.cpp @@ -81,7 +81,7 @@ void SATEncoder::createFormulation() { gateEncoder->encodeGates(); if (config.useSymmetryBreaking) { - gateEncoder->encodeSymmetryBreakingConstraints(config.couplingMap); + gateEncoder->encodeSymmetryBreakingConstraints(); } objectiveEncoder = diff --git a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp index fe15f39e1..a8a433f36 100644 --- a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp @@ -18,7 +18,7 @@ void SingleGateEncoder::assertConsistency() const { for (std::size_t t = 0U; t < T; ++t) { for (std::size_t q = 0U; q < N; ++q) { vars.collectSingleQubitGateVariables(t, q, gateVariables); - vars.collectTwoQubitGateVariables(t, q, true, gateVariables, couplingMap); + vars.collectTwoQubitGateVariables(t, q, true, gateVariables); } IF_PLOG(plog::verbose) { PLOG_VERBOSE << "Gate variables at time " << t; @@ -67,7 +67,7 @@ void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) { } if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt; - lb->assertFormula(LogicTerm(!twoQubitGates[ctrl][trgt])); + lb->assertFormula(!twoQubitGates[ctrl][trgt]); continue; } const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt); From cdaf138913d4d22210bd71974bc31c1063e052f5 Mon Sep 17 00:00:00 2001 From: Jakob Date: Sat, 10 Aug 2024 16:00:55 +0200 Subject: [PATCH 03/36] update codestyle for clifford synthesis with coupling map --- .../cliffordsynthesis/CliffordSynthesizer.hpp | 31 ++-- include/cliffordsynthesis/Results.hpp | 32 ++-- include/cliffordsynthesis/Tableau.hpp | 5 +- .../encoding/GateEncoder.hpp | 6 +- .../cliffordsynthesis/encoding/SATEncoder.hpp | 2 +- src/cliffordsynthesis/Tableau.cpp | 154 +++++++++--------- .../encoding/GateEncoder.cpp | 8 +- .../encoding/MultiGateEncoder.cpp | 2 +- .../encoding/SingleGateEncoder.cpp | 8 +- .../encoding/TableauEncoder.cpp | 55 ++++--- test/cliffordsynthesis/test_synthesis.cpp | 78 ++++----- 11 files changed, 199 insertions(+), 182 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 28dd8f281..dafa43a4d 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -27,44 +27,49 @@ class CliffordSynthesizer { public: CliffordSynthesizer() = default; CliffordSynthesizer(Tableau initial, Tableau target) - : initialTableau(std::move(initial)), targetTableau(std::move(target)), couplingMap(getFullyConnectedMap(static_cast(target.getQubitCount()))) {} + : initialTableau(std::move(initial)), targetTableau(std::move(target)), + couplingMap(getFullyConnectedMap( + static_cast(target.getQubitCount()))) {} CliffordSynthesizer(Tableau initial, Tableau target, CouplingMap qm) - : initialTableau(std::move(initial)), targetTableau(std::move(target)), couplingMap(std::move(qm)) {} + : initialTableau(std::move(initial)), targetTableau(std::move(target)), + couplingMap(std::move(qm)) {} explicit CliffordSynthesizer(Tableau target) : initialTableau(target.getQubitCount(), target.hasDestabilizers()), targetTableau(std::move(target)), - couplingMap(getFullyConnectedMap(static_cast(target.getQubitCount()))) {} + couplingMap(getFullyConnectedMap( + static_cast(target.getQubitCount()))) {} CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc) : initialTableau(std::move(initial)), targetTableau(qc, 0, std::numeric_limits::max(), initialTableau.hasDestabilizers()), - couplingMap(getFullyConnectedMap(static_cast(initial.getQubitCount()))), + couplingMap(getFullyConnectedMap( + static_cast(initial.getQubitCount()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(qc::QuantumComputation& qc, - const bool useDestabilizers = false) + const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), - couplingMap(getFullyConnectedMap(static_cast(qc.getNqubits()))), + couplingMap( + getFullyConnectedMap(static_cast(qc.getNqubits()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(Tableau target, CouplingMap qm) : initialTableau(target.getQubitCount(), target.hasDestabilizers()), - targetTableau(std::move(target)), - couplingMap(std::move(qm)) {} - CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc, CouplingMap qm) + targetTableau(std::move(target)), couplingMap(std::move(qm)) {} + CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc, + CouplingMap qm) : initialTableau(std::move(initial)), targetTableau(qc, 0, std::numeric_limits::max(), initialTableau.hasDestabilizers()), couplingMap(std::move(qm)), - initialCircuit(std::make_shared(qc)){} - explicit CliffordSynthesizer(qc::QuantumComputation& qc, - CouplingMap qm, + initialCircuit(std::make_shared(qc)) {} + explicit CliffordSynthesizer(qc::QuantumComputation& qc, CouplingMap qm, const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), couplingMap(std::move(qm)), - initialCircuit(std::make_shared(qc)){} + initialCircuit(std::make_shared(qc)) {} virtual ~CliffordSynthesizer() = default; diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index d7d5977d0..d45f77faf 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -51,19 +51,19 @@ class Results { [[nodiscard]] std::string getResultCircuit() const { return resultCircuit; } [[nodiscard]] std::string getResultTableau() const { return resultTableau; } - [[nodiscard]]std::string getMapping() const { + [[nodiscard]] std::string getMapping() const { std::ostringstream oss; for (const auto& row : pvector) { - for (bool val : row) { - oss << (val ? '1' : '0'); - } - oss << '\n'; + for (bool val : row) { + oss << (val ? '1' : '0'); + } + oss << '\n'; } - return oss.str(); + return oss.str(); } - [[nodiscard]] std::vector> getMappingVector() const { + [[nodiscard]] std::vector> getMappingVector() const { return pvector; - } + } void setSingleQubitGates(const std::size_t g) { singleQubitGates = g; } void setTwoQubitGates(const std::size_t g) { twoQubitGates = g; } @@ -85,12 +85,12 @@ class Results { void setMapping(std::vector> p) { std::ostringstream oss; for (const auto& row : pvector) { - for (bool val : row) { - oss << (val ? '1' : '0'); - } - oss << '\n'; + for (bool val : row) { + oss << (val ? '1' : '0'); + } + oss << '\n'; } - pvals = oss.str(); + pvals = oss.str(); pvector = std::move(p); } @@ -126,10 +126,10 @@ class Results { double runtime = 0.0; std::size_t solverCalls = 0U; - std::string pvals{}; + std::string pvals{}; std::vector> pvector{}; - std::string resultTableau{}; - std::string resultCircuit{}; + std::string resultTableau{}; + std::string resultCircuit{}; }; } // namespace cs diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index ca82b23cc..2531ff791 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -160,7 +160,8 @@ class Tableau { } Tableau applyMapping(const std::vector> p); Tableau reverseMapping(const std::vector> p); - Tableau reverseMappingOnRows(const std::vector> p, size_t nq); - void gaussianEliminationGF2(); + Tableau reverseMappingOnRows(const std::vector> p, + size_t nq); + void gaussianEliminationGF2(); }; } // namespace cs diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp index ba0b1348d..2ce308ae2 100644 --- a/include/cliffordsynthesis/encoding/GateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp @@ -21,9 +21,9 @@ class GateEncoder { GateEncoder(const std::size_t nQubits, const std::size_t tableauSize, const std::size_t timestepLimit, TableauEncoder::Variables* tableauVars, - std::shared_ptr logicBlock, - CouplingMap cm) - : N(nQubits), S(tableauSize), T(timestepLimit), couplingMap(std::move(cm)), tvars(tableauVars), + std::shared_ptr logicBlock, CouplingMap cm) + : N(nQubits), S(tableauSize), T(timestepLimit), + couplingMap(std::move(cm)), tvars(tableauVars), lb(std::move(logicBlock)) {} virtual ~GateEncoder() = default; diff --git a/include/cliffordsynthesis/encoding/SATEncoder.hpp b/include/cliffordsynthesis/encoding/SATEncoder.hpp index 2faf59623..1a6a51de8 100644 --- a/include/cliffordsynthesis/encoding/SATEncoder.hpp +++ b/include/cliffordsynthesis/encoding/SATEncoder.hpp @@ -35,7 +35,7 @@ class SATEncoder { // coupling Map of Qubits CouplingMap couplingMap{}; - + // the number of timesteps to encode std::size_t timestepLimit{}; diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 231b297b5..053e275f0 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -485,118 +485,120 @@ bool Tableau::isIdentityTableau() const { return true; } -Tableau Tableau::applyMapping( const std::vector> p){ - Tableau mapped_tableau = Tableau(nQubits,hasDestabilizers()); - for(size_t i = 0; i < mapped_tableau.getTableauSize(); i++){ - for(size_t j = 0; j < mapped_tableau.tableau[i].size(); j++){ - mapped_tableau.tableau[i][j] = 0; +Tableau Tableau::applyMapping(const std::vector> p) { + Tableau mapped_tableau = Tableau(nQubits, hasDestabilizers()); + for (size_t i = 0; i < mapped_tableau.getTableauSize(); i++) { + for (size_t j = 0; j < mapped_tableau.tableau[i].size(); j++) { + mapped_tableau.tableau[i][j] = 0; } } for (size_t i = 0; i < p.size(); i++) { for (size_t j = 0; j < p[i].size(); j++) { - //apply mapping from column i to j if p is set - if(p[i][j]){ - //in every row swap x entry and z entry - for(size_t n = 0; n < mapped_tableau.getTableauSize(); n++){ - mapped_tableau.tableau[n][j] = tableau[n][i]; - mapped_tableau.tableau[n][j+mapped_tableau.nQubits] = tableau[n][i+mapped_tableau.nQubits]; - } + // apply mapping from column i to j if p is set + if (p[i][j]) { + // in every row swap x entry and z entry + for (size_t n = 0; n < mapped_tableau.getTableauSize(); n++) { + mapped_tableau.tableau[n][j] = tableau[n][i]; + mapped_tableau.tableau[n][j + mapped_tableau.nQubits] = + tableau[n][i + mapped_tableau.nQubits]; + } } } } // copy r column without changes for (size_t i = 0; i < tableau.size(); i++) { - mapped_tableau.tableau[i][2*nQubits] = tableau[i][2*nQubits]; + mapped_tableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits]; } - return mapped_tableau; + return mapped_tableau; } -Tableau Tableau::reverseMapping(const std::vector> p){ - Tableau mapped_tableau = Tableau(nQubits,hasDestabilizers()); - for(size_t i = 0; i < mapped_tableau.getTableauSize(); i++){ - for(size_t j = 0; j < mapped_tableau.tableau[i].size(); j++){ - mapped_tableau.tableau[i][j] = 0; +Tableau Tableau::reverseMapping(const std::vector> p) { + Tableau mapped_tableau = Tableau(nQubits, hasDestabilizers()); + for (size_t i = 0; i < mapped_tableau.getTableauSize(); i++) { + for (size_t j = 0; j < mapped_tableau.tableau[i].size(); j++) { + mapped_tableau.tableau[i][j] = 0; } } for (size_t i = 0; i < p.size(); i++) { for (size_t j = 0; j < p[i].size(); j++) { - //apply mapping from column i to j if p is set - if(p[i][j]){ - //in every row swap x entry and z entry - for(size_t n = 0; n < mapped_tableau.getTableauSize(); n++){ - mapped_tableau.tableau[n][i] = tableau[n][j]; - mapped_tableau.tableau[n][i+mapped_tableau.nQubits] = tableau[n][j+mapped_tableau.nQubits]; - } + // apply mapping from column i to j if p is set + if (p[i][j]) { + // in every row swap x entry and z entry + for (size_t n = 0; n < mapped_tableau.getTableauSize(); n++) { + mapped_tableau.tableau[n][i] = tableau[n][j]; + mapped_tableau.tableau[n][i + mapped_tableau.nQubits] = + tableau[n][j + mapped_tableau.nQubits]; + } } } } // copy r column without changes for (size_t i = 0; i < tableau.size(); i++) { - mapped_tableau.tableau[i][2*nQubits] = tableau[i][2*nQubits]; + mapped_tableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits]; } - return mapped_tableau; + return mapped_tableau; } -// number of Qubits is passed because nQubits is not set in result Tableau of synthesis -Tableau Tableau::reverseMappingOnRows(const std::vector> p, size_t nq){ - Tableau mapped_tableau = Tableau(nq, true); +// number of Qubits is passed because nQubits is not set in result Tableau of +// synthesis +Tableau Tableau::reverseMappingOnRows(const std::vector> p, + size_t nq) { + Tableau mapped_tableau = Tableau(nq, true); mapped_tableau.tableau = tableau; for (size_t i = 0; i < p.size(); i++) { for (size_t j = 0; j < p[i].size(); j++) { - //apply mapping from row i to j if p is set - if(p[i][j]){ - mapped_tableau.tableau[i] = tableau[j]; - mapped_tableau.tableau[i + nq] = tableau[j + nq]; + // apply mapping from row i to j if p is set + if (p[i][j]) { + mapped_tableau.tableau[i] = tableau[j]; + mapped_tableau.tableau[i + nq] = tableau[j + nq]; } } } - return mapped_tableau; + return mapped_tableau; } // in place Gauss Elimination void Tableau::gaussianEliminationGF2() { - size_t rows = tableau.size(); - size_t cols = tableau[0].size(); - if (rows == 1){ - return; - } + size_t rows = tableau.size(); + size_t cols = tableau[0].size(); + if (rows == 1) { + return; + } - size_t pivot = 0; - - for (size_t col = 0; col < cols; ++col) { - // find the pivot row for the current column - size_t maxRow = pivot; - if(maxRow >= rows){ - break; - } - for (size_t row = pivot; row < rows; ++row) { - if (tableau[row][col] == 1) { - maxRow = row; - break; - } - } - // if no pivot is found, continue to the next column - if (tableau[maxRow][col] == 0) { - continue; - } - // swap the pivot row with the current row - std::swap(tableau[pivot], tableau[maxRow]); - - // eliminate all other 1s in the current column - for (size_t row = 0; row < rows; ++row) { - if (row != pivot && tableau[row][col] == 1) { - for (size_t k = 0; k < cols; ++k) { - if(tableau[row][k] == tableau[pivot][k]){ - tableau[row][k] = 0; - } - else{ - tableau[row][k] = 1; - } - } - } + size_t pivot = 0; + + for (size_t col = 0; col < cols; ++col) { + // find the pivot row for the current column + size_t maxRow = pivot; + if (maxRow >= rows) { + break; + } + for (size_t row = pivot; row < rows; ++row) { + if (tableau[row][col] == 1) { + maxRow = row; + break; + } + } + // if no pivot is found, continue to the next column + if (tableau[maxRow][col] == 0) { + continue; + } + // swap the pivot row with the current row + std::swap(tableau[pivot], tableau[maxRow]); + + // eliminate all other 1s in the current column + for (size_t row = 0; row < rows; ++row) { + if (row != pivot && tableau[row][col] == 1) { + for (size_t k = 0; k < cols; ++k) { + if (tableau[row][k] == tableau[pivot][k]) { + tableau[row][k] = 0; + } else { + tableau[row][k] = 1; + } } - pivot++; + } } - + pivot++; + } } } // namespace cs diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp index db10b51e9..de333613d 100644 --- a/src/cliffordsynthesis/encoding/GateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp @@ -4,15 +4,15 @@ // #include "cliffordsynthesis/encoding/GateEncoder.hpp" -#include "Logic.hpp" -#include "LogicTerm.hpp" -#include "utils.hpp" #include "Definitions.hpp" +#include "Logic.hpp" +#include "LogicTerm.hpp" #include "logicblocks/Encodings.hpp" #include "logicblocks/Model.hpp" #include "operations/StandardOperation.hpp" #include "plog/Log.h" +#include "utils.hpp" namespace cs::encoding { @@ -340,7 +340,7 @@ void GateEncoder::assertTwoQubitGateSymmetryBreakingConstraints( for (std::size_t ctrl = 1U; ctrl < N; ++ctrl) { for (std::size_t trgt = 0U; trgt < ctrl; ++trgt) { // avoid unnecessary constraints if CNOT cannot be applied anyways - if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { + if (couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { continue; } assertTwoQubitGateOrderConstraints(pos, ctrl, trgt); diff --git a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp index fff8c16da..f273ad9c2 100644 --- a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp @@ -77,7 +77,7 @@ void encoding::MultiGateEncoder::assertTwoQubitGateConstraints( continue; } // if no connection between ctrl and trgt then assert variable is false - if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { + if (couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt; lb->assertFormula(!twoQubitGates[ctrl][trgt]); continue; diff --git a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp index a8a433f36..bc5ba7a2e 100644 --- a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp @@ -65,7 +65,7 @@ void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) { if (ctrl == trgt) { continue; } - if(couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { + if (couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) { PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt; lb->assertFormula(!twoQubitGates[ctrl][trgt]); continue; @@ -89,9 +89,9 @@ LogicTerm SingleGateEncoder::createTwoQubitGateConstraint( changes = changes && (tvars->x[pos + 2][trgt] == xTrgt); changes = changes && (tvars->z[pos + 2][ctrl] == zCtrl); changes = changes && (tvars->z[pos + 2][trgt] == zTrgt); - changes = - changes && (tvars->r[pos + 2] == - (tvars->r[pos + 1] ^ tvars->twoQubitRChange(pos + 1, ctrl, trgt))); + changes = changes && + (tvars->r[pos + 2] == + (tvars->r[pos + 1] ^ tvars->twoQubitRChange(pos + 1, ctrl, trgt))); return changes; } diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 57b91300d..a2e966a9e 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -42,14 +42,15 @@ void TableauEncoder::createTableauVariables() { PLOG_DEBUG << "Creating mapping variables."; vars.p.reserve(N); for (std::size_t i = 0U; i < N; ++i) { - auto& g = vars.p.emplace_back(); - g.reserve(N); - for (std::size_t j = 0U; j < N; ++j) { - const std::string pName = "p_" + std::to_string(i) + "_" + std::to_string(j); - PLOG_VERBOSE << "Creating variable " << pName; - g.emplace_back(lb->makeVariable(pName)); - } + auto& g = vars.p.emplace_back(); + g.reserve(N); + for (std::size_t j = 0U; j < N; ++j) { + const std::string pName = + "p_" + std::to_string(i) + "_" + std::to_string(j); + PLOG_VERBOSE << "Creating variable " << pName; + g.emplace_back(lb->makeVariable(pName)); } + } } void TableauEncoder::assertTableau(const Tableau& tableau, @@ -70,27 +71,29 @@ void TableauEncoder::assertTableau(const Tableau& tableau, lb->assertFormula(vars.r[t] == LogicTerm(targetR, n)); } -void TableauEncoder::assertMappingConstraints(){ +void TableauEncoder::assertMappingConstraints() { // if p_i_j is set column i is mapped to column j between 0 and 1 for (std::size_t i = 0U; i < N; ++i) { for (std::size_t j = 0U; j < N; ++j) { - lb->assertFormula(LogicTerm::implies(vars.p[i][j], vars.x[1][j] == vars.x[0][i])); - lb->assertFormula(LogicTerm::implies(vars.p[i][j], vars.z[1][j] == vars.z[0][i])); + lb->assertFormula( + LogicTerm::implies(vars.p[i][j], vars.x[1][j] == vars.x[0][i])); + lb->assertFormula( + LogicTerm::implies(vars.p[i][j], vars.z[1][j] == vars.z[0][i])); } } // assert that r vals are unchanges between 0 and 1 - lb->assertFormula(LogicTerm::eq(vars.r[0],vars.r[1])); + lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); // assert that for every i and j exactly one p variable is set for (std::size_t i = 0U; i < N; ++i) { - int32_t vr = 0; - int32_t vr1 = 1; + int32_t vr = 0; + int32_t vr1 = 1; LogicTerm sumRow = LogicTerm(vr); for (std::size_t j = 0U; j < N; ++j) { sumRow = sumRow + vars.p[i][j]; } lb->assertFormula(sumRow == LogicTerm(vr1)); - int32_t vc = 0; - int32_t vc1 = 1; + int32_t vc = 0; + int32_t vc1 = 1; LogicTerm sumCol = LogicTerm(vc); for (std::size_t j = 0U; j < N; ++j) { sumCol = sumCol + vars.p[j][i]; @@ -100,13 +103,14 @@ void TableauEncoder::assertMappingConstraints(){ // if p_i_j is set undo mapping between T-1 and T for (std::size_t i = 0U; i < N; ++i) { for (std::size_t j = 0U; j < N; ++j) { - lb->assertFormula(LogicTerm::implies(vars.p[i][j] , vars.x[T][i] == vars.x[T - 1][j])); - lb->assertFormula(LogicTerm::implies(vars.p[i][j] , vars.z[T][i] == vars.z[T - 1][j])); - + lb->assertFormula( + LogicTerm::implies(vars.p[i][j], vars.x[T][i] == vars.x[T - 1][j])); + lb->assertFormula( + LogicTerm::implies(vars.p[i][j], vars.z[T][i] == vars.z[T - 1][j])); } } // assert that r vals are unchanges between T-1 and T - lb->assertFormula(LogicTerm::eq(vars.r[T - 1],vars.r[T])); + lb->assertFormula(LogicTerm::eq(vars.r[T - 1], vars.r[T])); } void TableauEncoder::extractTableauFromModel(Results& results, @@ -125,12 +129,13 @@ void TableauEncoder::extractTableauFromModel(Results& results, results.setResultTableau(tableau); } -void TableauEncoder::extractMappingFromModel(Results& results, Model& model) const { - std::vector row(N,false); - std::vector> pvals(N,std::vector(N,false)); - for (std::size_t i = 0; i row(N, false); + std::vector> pvals(N, std::vector(N, false)); + for (std::size_t i = 0; i < N; ++i) { + for (std::size_t j = 0; j < N; ++j) { + pvals[i][j] = model.getBoolValue(vars.p[i][j], lb.get()); } } results.setMapping(pvals); diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 75f36ab4a..9a5c1307b 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -67,29 +67,29 @@ std::vector getTests(const std::string& path) { } } // namespace -CouplingMap parseEdges(const std::string &edgeString) { - CouplingMap edges; - std::stringstream ss(edgeString); - std::string item; - - while (getline(ss, item, ';')) { - item.erase(remove(item.begin(), item.end(), '{'), item.end()); - item.erase(remove(item.begin(), item.end(), '}'), item.end()); - size_t pos = item.find(','); - std::string first, second; - - first = item.substr(0, pos); - second = item.substr(pos+1); - - int u = stoi(first); - int v = stoi(second); - - // Insert the edge into the set - edges.insert(Edge{u, v}); - std::cout << "Edge " << u << "," << v << " inserted to cm\n"; - } - - return edges; +CouplingMap parseEdges(const std::string& edgeString) { + CouplingMap edges; + std::stringstream ss(edgeString); + std::string item; + + while (getline(ss, item, ';')) { + item.erase(remove(item.begin(), item.end(), '{'), item.end()); + item.erase(remove(item.begin(), item.end(), '}'), item.end()); + size_t pos = item.find(','); + std::string first, second; + + first = item.substr(0, pos); + second = item.substr(pos + 1); + + int u = stoi(first); + int v = stoi(second); + + // Insert the edge into the set + edges.insert(Edge{u, v}); + std::cout << "Edge " << u << "," << v << " inserted to cm\n"; + } + + return edges; } class SynthesisTest : public ::testing::TestWithParam { protected: @@ -107,12 +107,13 @@ class SynthesisTest : public ::testing::TestWithParam { if (test.initialTableau.empty()) { initialTableau = Tableau(qc.getNqubits()); initialTableauWithDestabilizer = Tableau(qc.getNqubits(), true); - if(test.couplingMap.empty()){ - synthesizer = CliffordSynthesizer(qc); - synthesizerWithDestabilizer = CliffordSynthesizer(qc, true); - } else{ + if (test.couplingMap.empty()) { + synthesizer = CliffordSynthesizer(qc); + synthesizerWithDestabilizer = CliffordSynthesizer(qc, true); + } else { synthesizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap)); - synthesizerWithDestabilizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap), true); + synthesizerWithDestabilizer = + CliffordSynthesizer(qc, parseEdges(test.couplingMap), true); } } else { initialTableau = Tableau(test.initialTableau); @@ -150,19 +151,22 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Target tableau:\n" << targetTableau; const std::vector> p = results.getMappingVector(); - Tableau targetPrime = targetTableau.applyMapping(p); + Tableau targetPrime = targetTableau.applyMapping(p); std::cout << "Target tableau with mapping:\n" << targetPrime; - if(!targetPrime.hasDestabilizers()){ + if (!targetPrime.hasDestabilizers()) { targetPrime.gaussianEliminationGF2(); resultTableau.gaussianEliminationGF2(); std::cout << "Target tableau with mapping and Gauss:\n" << targetPrime; std::cout << "Result tableau with mapping and Gauss:\n" << resultTableau; - } else{ - targetPrime = targetPrime.reverseMappingOnRows(p, targetPrime.getQubitCount()); - resultTableau = resultTableau.reverseMappingOnRows(p, targetPrime.getQubitCount()); - std::cout << "Result tableau with destab mapping reversed:\n" << resultTableau; - std::cout << "Target tableau with destab mapping reversed:\n" << targetPrime; - + } else { + targetPrime = + targetPrime.reverseMappingOnRows(p, targetPrime.getQubitCount()); + resultTableau = + resultTableau.reverseMappingOnRows(p, targetPrime.getQubitCount()); + std::cout << "Result tableau with destab mapping reversed:\n" + << resultTableau; + std::cout << "Target tableau with destab mapping reversed:\n" + << targetPrime; } EXPECT_EQ(resultTableau, targetPrime); @@ -178,7 +182,7 @@ class SynthesisTest : public ::testing::TestWithParam { circuitTableau.applyGate(gate.get()); } std::cout << "Circuit Tableau :\n" << circuitTableau; - if(!circuitTableau.hasDestabilizers()){ + if (!circuitTableau.hasDestabilizers()) { circuitTableau.gaussianEliminationGF2(); std::cout << "Circuit Tableau with Gauss" << circuitTableau; } From ae41406b70e197e0709115d325f3833f5ffbcb13 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 10 Aug 2024 19:23:03 +0000 Subject: [PATCH 04/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../cliffordsynthesis/CliffordSynthesizer.hpp | 8 +++---- include/cliffordsynthesis/Results.hpp | 16 +++++++------- include/cliffordsynthesis/Tableau.hpp | 4 ++-- .../encoding/GateEncoder.hpp | 7 +++--- src/cliffordsynthesis/Tableau.cpp | 4 ++-- .../encoding/GateEncoder.cpp | 2 +- .../encoding/TableauEncoder.cpp | 22 +++++++++---------- test/cliffordsynthesis/test_synthesis.cpp | 17 +++++++------- 8 files changed, 40 insertions(+), 40 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 2e02ff0b8..974e57336 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -48,7 +48,7 @@ class CliffordSynthesizer { static_cast(initial.getQubitCount()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(qc::QuantumComputation& qc, - const bool useDestabilizers = false) + const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), @@ -98,9 +98,9 @@ class CliffordSynthesizer { } protected: - Tableau initialTableau{}; - Tableau targetTableau{}; - CouplingMap couplingMap{}; + Tableau initialTableau{}; + Tableau targetTableau{}; + CouplingMap couplingMap{}; std::shared_ptr initialCircuit{}; Configuration configuration{}; diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index 19945be16..074681491 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -94,7 +94,7 @@ class Results { } oss << '\n'; } - pvals = oss.str(); + pvals = oss.str(); pvector = std::move(p); } @@ -130,15 +130,15 @@ class Results { double runtime = 0.0; std::size_t solverCalls = 0U; - std::string pvals; + std::string pvals; std::vector> pvector; - std::string resultTableau; - std::string resultCircuit; + std::string resultTableau; + std::string resultCircuit; }; } // namespace cs - solverCalls = 0U; +solverCalls = 0U; - std::string pvals{}; - std::vector> pvector{}; - std::string resultTableau{}; +std::string pvals{}; +std::vector> pvector{}; +std::string resultTableau{}; diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index dd9f7474f..984374029 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -166,7 +166,7 @@ class Tableau { Tableau applyMapping(const std::vector> p); Tableau reverseMapping(const std::vector> p); Tableau reverseMappingOnRows(const std::vector> p, - size_t nq); - void gaussianEliminationGF2(); + size_t nq); + void gaussianEliminationGF2(); }; } // namespace cs diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp index a23f311c4..9e54ecbf1 100644 --- a/include/cliffordsynthesis/encoding/GateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp @@ -26,10 +26,9 @@ namespace cs::encoding { class GateEncoder { public: GateEncoder(const std::size_t nQubits, const std::size_t tableauSize, - const std::size_t timestepLimit, - TableauEncoder::Variables* tableauVars, - std::shared_ptr logicBlock, - CouplingMap cm) + const std::size_t timestepLimit, + TableauEncoder::Variables* tableauVars, + std::shared_ptr logicBlock, CouplingMap cm) : N(nQubits), S(tableauSize), T(timestepLimit), couplingMap(std::move(cm)), tvars(tableauVars), lb(std::move(logicBlock)) {} diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 363cfa1a3..f4df13f21 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -550,14 +550,14 @@ Tableau Tableau::reverseMapping(const std::vector> p) { // number of Qubits is passed because nQubits is not set in result Tableau of // synthesis Tableau Tableau::reverseMappingOnRows(const std::vector> p, - size_t nq) { + size_t nq) { Tableau mapped_tableau = Tableau(nq, true); mapped_tableau.tableau = tableau; for (size_t i = 0; i < p.size(); i++) { for (size_t j = 0; j < p[i].size(); j++) { // apply mapping from row i to j if p is set if (p[i][j]) { - mapped_tableau.tableau[i] = tableau[j]; + mapped_tableau.tableau[i] = tableau[j]; mapped_tableau.tableau[i + nq] = tableau[j + nq]; } } diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp index 10ba003a1..e47a44865 100644 --- a/src/cliffordsynthesis/encoding/GateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp @@ -14,13 +14,13 @@ #include "logicblocks/Model.hpp" #include "operations/OpType.hpp" #include "operations/StandardOperation.hpp" +#include "utils.hpp" #include #include #include #include #include -#include "utils.hpp" namespace cs::encoding { diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 06baf6e19..305267706 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -5,8 +5,8 @@ #include "cliffordsynthesis/encoding/TableauEncoder.hpp" -#include "LogicTerm.hpp" #include "Logic.hpp" +#include "LogicTerm.hpp" #include "cliffordsynthesis/Results.hpp" #include "cliffordsynthesis/Tableau.hpp" #include "logicblocks/Model.hpp" @@ -95,15 +95,15 @@ void TableauEncoder::assertMappingConstraints() { lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); // assert that for every i and j exactly one p variable is set for (std::size_t i = 0U; i < N; ++i) { - int32_t vr = 0; - int32_t vr1 = 1; + int32_t vr = 0; + int32_t vr1 = 1; LogicTerm sumRow = LogicTerm(vr); for (std::size_t j = 0U; j < N; ++j) { sumRow = sumRow + vars.p[i][j]; } lb->assertFormula(sumRow == LogicTerm(vr1)); - int32_t vc = 0; - int32_t vc1 = 1; + int32_t vc = 0; + int32_t vc1 = 1; LogicTerm sumCol = LogicTerm(vc); for (std::size_t j = 0U; j < N; ++j) { sumCol = sumCol + vars.p[j][i]; @@ -137,15 +137,15 @@ void TableauEncoder::assertMappingConstraints() { lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); // assert that for every i and j exactly one p variable is set for (std::size_t i = 0U; i < N; ++i) { - int32_t vr = 0; - int32_t vr1 = 1; + int32_t vr = 0; + int32_t vr1 = 1; LogicTerm sumRow = LogicTerm(vr); for (std::size_t j = 0U; j < N; ++j) { sumRow = sumRow + vars.p[i][j]; } lb->assertFormula(sumRow == LogicTerm(vr1)); - int32_t vc = 0; - int32_t vc1 = 1; + int32_t vc = 0; + int32_t vc1 = 1; LogicTerm sumCol = LogicTerm(vc); for (std::size_t j = 0U; j < N; ++j) { sumCol = sumCol + vars.p[j][i]; @@ -182,8 +182,8 @@ void TableauEncoder::extractTableauFromModel(Results& results, } void TableauEncoder::extractMappingFromModel(Results& results, - Model& model) const { - std::vector row(N, false); + Model& model) const { + std::vector row(N, false); std::vector> pvals(N, std::vector(N, false)); for (std::size_t i = 0; i < N; ++i) { for (std::size_t j = 0; j < N; ++j) { diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 03ee09b98..1e74df044 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -6,11 +6,11 @@ #include "Definitions.hpp" #include "QuantumComputation.hpp" #include "cliffordsynthesis/CliffordSynthesizer.hpp" -#include "cliffordsynthesis/Tableau.hpp" -#include "utils.hpp" #include "cliffordsynthesis/Results.hpp" +#include "cliffordsynthesis/Tableau.hpp" #include "cliffordsynthesis/TargetMetric.hpp" #include "operations/Control.hpp" +#include "utils.hpp" #include #include @@ -79,17 +79,17 @@ std::vector getTests(const std::string& path) { } // namespace CouplingMap parseEdges(const std::string& edgeString) { - CouplingMap edges; + CouplingMap edges; std::stringstream ss(edgeString); - std::string item; + std::string item; while (getline(ss, item, ';')) { item.erase(remove(item.begin(), item.end(), '{'), item.end()); item.erase(remove(item.begin(), item.end(), '}'), item.end()); - size_t pos = item.find(','); + size_t pos = item.find(','); std::string first, second; - first = item.substr(0, pos); + first = item.substr(0, pos); second = item.substr(pos + 1); int u = stoi(first); @@ -123,7 +123,8 @@ class SynthesisTest : public ::testing::TestWithParam { synthesizerWithDestabilizer = CliffordSynthesizer(qc, true); } else { synthesizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap)); - synthesizerWithDestabilizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap), true); + synthesizerWithDestabilizer = + CliffordSynthesizer(qc, parseEdges(test.couplingMap), true); } } else { initialTableau = Tableau(test.initialTableau); @@ -161,7 +162,7 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Target tableau:\n" << targetTableau; const std::vector> p = results.getMappingVector(); - Tableau targetPrime = targetTableau.applyMapping(p); + Tableau targetPrime = targetTableau.applyMapping(p); std::cout << "Target tableau with mapping:\n" << targetPrime; if (!targetPrime.hasDestabilizers()) { targetPrime.gaussianEliminationGF2(); From 3381e941af6d2390e58f079cf6ca3e523daac3e7 Mon Sep 17 00:00:00 2001 From: Jakob Date: Sat, 10 Aug 2024 21:25:51 +0200 Subject: [PATCH 05/36] code formatting --- .../cliffordsynthesis/CliffordSynthesizer.hpp | 8 +++---- include/cliffordsynthesis/Results.hpp | 16 +++++++------- include/cliffordsynthesis/Tableau.hpp | 4 ++-- .../encoding/GateEncoder.hpp | 7 +++--- src/cliffordsynthesis/Tableau.cpp | 4 ++-- .../encoding/GateEncoder.cpp | 2 +- .../encoding/TableauEncoder.cpp | 22 +++++++++---------- test/cliffordsynthesis/test_synthesis.cpp | 17 +++++++------- 8 files changed, 40 insertions(+), 40 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 2e02ff0b8..974e57336 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -48,7 +48,7 @@ class CliffordSynthesizer { static_cast(initial.getQubitCount()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(qc::QuantumComputation& qc, - const bool useDestabilizers = false) + const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), @@ -98,9 +98,9 @@ class CliffordSynthesizer { } protected: - Tableau initialTableau{}; - Tableau targetTableau{}; - CouplingMap couplingMap{}; + Tableau initialTableau{}; + Tableau targetTableau{}; + CouplingMap couplingMap{}; std::shared_ptr initialCircuit{}; Configuration configuration{}; diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index 19945be16..074681491 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -94,7 +94,7 @@ class Results { } oss << '\n'; } - pvals = oss.str(); + pvals = oss.str(); pvector = std::move(p); } @@ -130,15 +130,15 @@ class Results { double runtime = 0.0; std::size_t solverCalls = 0U; - std::string pvals; + std::string pvals; std::vector> pvector; - std::string resultTableau; - std::string resultCircuit; + std::string resultTableau; + std::string resultCircuit; }; } // namespace cs - solverCalls = 0U; +solverCalls = 0U; - std::string pvals{}; - std::vector> pvector{}; - std::string resultTableau{}; +std::string pvals{}; +std::vector> pvector{}; +std::string resultTableau{}; diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index dd9f7474f..984374029 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -166,7 +166,7 @@ class Tableau { Tableau applyMapping(const std::vector> p); Tableau reverseMapping(const std::vector> p); Tableau reverseMappingOnRows(const std::vector> p, - size_t nq); - void gaussianEliminationGF2(); + size_t nq); + void gaussianEliminationGF2(); }; } // namespace cs diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp index a23f311c4..9e54ecbf1 100644 --- a/include/cliffordsynthesis/encoding/GateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp @@ -26,10 +26,9 @@ namespace cs::encoding { class GateEncoder { public: GateEncoder(const std::size_t nQubits, const std::size_t tableauSize, - const std::size_t timestepLimit, - TableauEncoder::Variables* tableauVars, - std::shared_ptr logicBlock, - CouplingMap cm) + const std::size_t timestepLimit, + TableauEncoder::Variables* tableauVars, + std::shared_ptr logicBlock, CouplingMap cm) : N(nQubits), S(tableauSize), T(timestepLimit), couplingMap(std::move(cm)), tvars(tableauVars), lb(std::move(logicBlock)) {} diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 363cfa1a3..f4df13f21 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -550,14 +550,14 @@ Tableau Tableau::reverseMapping(const std::vector> p) { // number of Qubits is passed because nQubits is not set in result Tableau of // synthesis Tableau Tableau::reverseMappingOnRows(const std::vector> p, - size_t nq) { + size_t nq) { Tableau mapped_tableau = Tableau(nq, true); mapped_tableau.tableau = tableau; for (size_t i = 0; i < p.size(); i++) { for (size_t j = 0; j < p[i].size(); j++) { // apply mapping from row i to j if p is set if (p[i][j]) { - mapped_tableau.tableau[i] = tableau[j]; + mapped_tableau.tableau[i] = tableau[j]; mapped_tableau.tableau[i + nq] = tableau[j + nq]; } } diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp index 10ba003a1..e47a44865 100644 --- a/src/cliffordsynthesis/encoding/GateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp @@ -14,13 +14,13 @@ #include "logicblocks/Model.hpp" #include "operations/OpType.hpp" #include "operations/StandardOperation.hpp" +#include "utils.hpp" #include #include #include #include #include -#include "utils.hpp" namespace cs::encoding { diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 06baf6e19..305267706 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -5,8 +5,8 @@ #include "cliffordsynthesis/encoding/TableauEncoder.hpp" -#include "LogicTerm.hpp" #include "Logic.hpp" +#include "LogicTerm.hpp" #include "cliffordsynthesis/Results.hpp" #include "cliffordsynthesis/Tableau.hpp" #include "logicblocks/Model.hpp" @@ -95,15 +95,15 @@ void TableauEncoder::assertMappingConstraints() { lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); // assert that for every i and j exactly one p variable is set for (std::size_t i = 0U; i < N; ++i) { - int32_t vr = 0; - int32_t vr1 = 1; + int32_t vr = 0; + int32_t vr1 = 1; LogicTerm sumRow = LogicTerm(vr); for (std::size_t j = 0U; j < N; ++j) { sumRow = sumRow + vars.p[i][j]; } lb->assertFormula(sumRow == LogicTerm(vr1)); - int32_t vc = 0; - int32_t vc1 = 1; + int32_t vc = 0; + int32_t vc1 = 1; LogicTerm sumCol = LogicTerm(vc); for (std::size_t j = 0U; j < N; ++j) { sumCol = sumCol + vars.p[j][i]; @@ -137,15 +137,15 @@ void TableauEncoder::assertMappingConstraints() { lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); // assert that for every i and j exactly one p variable is set for (std::size_t i = 0U; i < N; ++i) { - int32_t vr = 0; - int32_t vr1 = 1; + int32_t vr = 0; + int32_t vr1 = 1; LogicTerm sumRow = LogicTerm(vr); for (std::size_t j = 0U; j < N; ++j) { sumRow = sumRow + vars.p[i][j]; } lb->assertFormula(sumRow == LogicTerm(vr1)); - int32_t vc = 0; - int32_t vc1 = 1; + int32_t vc = 0; + int32_t vc1 = 1; LogicTerm sumCol = LogicTerm(vc); for (std::size_t j = 0U; j < N; ++j) { sumCol = sumCol + vars.p[j][i]; @@ -182,8 +182,8 @@ void TableauEncoder::extractTableauFromModel(Results& results, } void TableauEncoder::extractMappingFromModel(Results& results, - Model& model) const { - std::vector row(N, false); + Model& model) const { + std::vector row(N, false); std::vector> pvals(N, std::vector(N, false)); for (std::size_t i = 0; i < N; ++i) { for (std::size_t j = 0; j < N; ++j) { diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 03ee09b98..1e74df044 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -6,11 +6,11 @@ #include "Definitions.hpp" #include "QuantumComputation.hpp" #include "cliffordsynthesis/CliffordSynthesizer.hpp" -#include "cliffordsynthesis/Tableau.hpp" -#include "utils.hpp" #include "cliffordsynthesis/Results.hpp" +#include "cliffordsynthesis/Tableau.hpp" #include "cliffordsynthesis/TargetMetric.hpp" #include "operations/Control.hpp" +#include "utils.hpp" #include #include @@ -79,17 +79,17 @@ std::vector getTests(const std::string& path) { } // namespace CouplingMap parseEdges(const std::string& edgeString) { - CouplingMap edges; + CouplingMap edges; std::stringstream ss(edgeString); - std::string item; + std::string item; while (getline(ss, item, ';')) { item.erase(remove(item.begin(), item.end(), '{'), item.end()); item.erase(remove(item.begin(), item.end(), '}'), item.end()); - size_t pos = item.find(','); + size_t pos = item.find(','); std::string first, second; - first = item.substr(0, pos); + first = item.substr(0, pos); second = item.substr(pos + 1); int u = stoi(first); @@ -123,7 +123,8 @@ class SynthesisTest : public ::testing::TestWithParam { synthesizerWithDestabilizer = CliffordSynthesizer(qc, true); } else { synthesizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap)); - synthesizerWithDestabilizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap), true); + synthesizerWithDestabilizer = + CliffordSynthesizer(qc, parseEdges(test.couplingMap), true); } } else { initialTableau = Tableau(test.initialTableau); @@ -161,7 +162,7 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Target tableau:\n" << targetTableau; const std::vector> p = results.getMappingVector(); - Tableau targetPrime = targetTableau.applyMapping(p); + Tableau targetPrime = targetTableau.applyMapping(p); std::cout << "Target tableau with mapping:\n" << targetPrime; if (!targetPrime.hasDestabilizers()) { targetPrime.gaussianEliminationGF2(); From 583b9c9556ffa6f1256e265af7ca26fd6cebeeb6 Mon Sep 17 00:00:00 2001 From: Jakob Date: Sat, 10 Aug 2024 21:42:36 +0200 Subject: [PATCH 06/36] fix merge of clifford and main --- include/cliffordsynthesis/Results.hpp | 5 --- .../encoding/TableauEncoder.cpp | 42 ------------------- 2 files changed, 47 deletions(-) diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index 074681491..aceb18952 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -137,8 +137,3 @@ class Results { }; } // namespace cs -solverCalls = 0U; - -std::string pvals{}; -std::vector> pvector{}; -std::string resultTableau{}; diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 305267706..0ebd3a2d7 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -123,48 +123,6 @@ void TableauEncoder::assertMappingConstraints() { lb->assertFormula(LogicTerm::eq(vars.r[T - 1], vars.r[T])); } -void TableauEncoder::assertMappingConstraints() { - // if p_i_j is set column i is mapped to column j between 0 and 1 - for (std::size_t i = 0U; i < N; ++i) { - for (std::size_t j = 0U; j < N; ++j) { - lb->assertFormula( - LogicTerm::implies(vars.p[i][j], vars.x[1][j] == vars.x[0][i])); - lb->assertFormula( - LogicTerm::implies(vars.p[i][j], vars.z[1][j] == vars.z[0][i])); - } - } - // assert that r vals are unchanges between 0 and 1 - lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); - // assert that for every i and j exactly one p variable is set - for (std::size_t i = 0U; i < N; ++i) { - int32_t vr = 0; - int32_t vr1 = 1; - LogicTerm sumRow = LogicTerm(vr); - for (std::size_t j = 0U; j < N; ++j) { - sumRow = sumRow + vars.p[i][j]; - } - lb->assertFormula(sumRow == LogicTerm(vr1)); - int32_t vc = 0; - int32_t vc1 = 1; - LogicTerm sumCol = LogicTerm(vc); - for (std::size_t j = 0U; j < N; ++j) { - sumCol = sumCol + vars.p[j][i]; - } - lb->assertFormula(sumCol == LogicTerm(vc1)); - } - // if p_i_j is set undo mapping between T-1 and T - for (std::size_t i = 0U; i < N; ++i) { - for (std::size_t j = 0U; j < N; ++j) { - lb->assertFormula( - LogicTerm::implies(vars.p[i][j], vars.x[T][i] == vars.x[T - 1][j])); - lb->assertFormula( - LogicTerm::implies(vars.p[i][j], vars.z[T][i] == vars.z[T - 1][j])); - } - } - // assert that r vals are unchanges between T-1 and T - lb->assertFormula(LogicTerm::eq(vars.r[T - 1], vars.r[T])); -} - void TableauEncoder::extractTableauFromModel(Results& results, const std::size_t t, Model& model) const { From 07b7b098d7fb4d4d4082fb36835ca3a50aa8258a Mon Sep 17 00:00:00 2001 From: Jakob Date: Sat, 10 Aug 2024 23:33:34 +0200 Subject: [PATCH 07/36] update codestyle --- .../cliffordsynthesis/CliffordSynthesizer.hpp | 9 +-- include/cliffordsynthesis/Tableau.hpp | 6 +- .../cliffordsynthesis/encoding/SATEncoder.hpp | 2 +- src/cliffordsynthesis/Tableau.cpp | 80 +++++++++---------- test/cliffordsynthesis/test_synthesis.cpp | 11 +-- 5 files changed, 54 insertions(+), 54 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 974e57336..d5b6fa14b 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -13,7 +13,6 @@ #include "cliffordsynthesis/TargetMetric.hpp" #include "cliffordsynthesis/encoding/SATEncoder.hpp" -#include #include #include #include @@ -98,10 +97,10 @@ class CliffordSynthesizer { } protected: - Tableau initialTableau{}; - Tableau targetTableau{}; - CouplingMap couplingMap{}; - std::shared_ptr initialCircuit{}; + Tableau initialTableau; + Tableau targetTableau; + CouplingMap couplingMap; + std::shared_ptr initialCircuit; Configuration configuration{}; diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index 984374029..f60e5af04 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -163,9 +163,9 @@ class Tableau { [[nodiscard]] std::uint64_t getBVFrom(const std::size_t column) const { return getBVFrom<64>(column).to_ullong(); } - Tableau applyMapping(const std::vector> p); - Tableau reverseMapping(const std::vector> p); - Tableau reverseMappingOnRows(const std::vector> p, + Tableau applyMapping(const std::vector>* p); + Tableau reverseMapping(const std::vector>* p); + Tableau reverseMappingOnRows(const std::vector>* p, size_t nq); void gaussianEliminationGF2(); }; diff --git a/include/cliffordsynthesis/encoding/SATEncoder.hpp b/include/cliffordsynthesis/encoding/SATEncoder.hpp index a2905919f..b5213baf3 100644 --- a/include/cliffordsynthesis/encoding/SATEncoder.hpp +++ b/include/cliffordsynthesis/encoding/SATEncoder.hpp @@ -35,7 +35,7 @@ class SATEncoder { std::size_t nQubits{}; // coupling Map of Qubits - CouplingMap couplingMap{}; + CouplingMap couplingMap; // the number of timesteps to encode std::size_t timestepLimit{}; diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index f4df13f21..839f2f280 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -493,82 +493,82 @@ bool Tableau::isIdentityTableau() const { return true; } -Tableau Tableau::applyMapping(const std::vector> p) { - Tableau mapped_tableau = Tableau(nQubits, hasDestabilizers()); - for (size_t i = 0; i < mapped_tableau.getTableauSize(); i++) { - for (size_t j = 0; j < mapped_tableau.tableau[i].size(); j++) { - mapped_tableau.tableau[i][j] = 0; +Tableau Tableau::applyMapping(const std::vector>* p) { + Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); + for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { + for (unsigned char & j : mappedTableau.tableau[i]) { + j = 0; } } - for (size_t i = 0; i < p.size(); i++) { - for (size_t j = 0; j < p[i].size(); j++) { + for (size_t i = 0; i < p->size(); i++) { + for (size_t j = 0; j < (*p)[i].size(); j++) { // apply mapping from column i to j if p is set - if (p[i][j]) { + if ((*p)[i][j]) { // in every row swap x entry and z entry - for (size_t n = 0; n < mapped_tableau.getTableauSize(); n++) { - mapped_tableau.tableau[n][j] = tableau[n][i]; - mapped_tableau.tableau[n][j + mapped_tableau.nQubits] = - tableau[n][i + mapped_tableau.nQubits]; + for (size_t n = 0; n < mappedTableau.getTableauSize(); n++) { + mappedTableau.tableau[n][j] = tableau[n][i]; + mappedTableau.tableau[n][j + mappedTableau.nQubits] = + tableau[n][i + mappedTableau.nQubits]; } } } } // copy r column without changes for (size_t i = 0; i < tableau.size(); i++) { - mapped_tableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits]; + mappedTableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits]; } - return mapped_tableau; + return mappedTableau; } -Tableau Tableau::reverseMapping(const std::vector> p) { - Tableau mapped_tableau = Tableau(nQubits, hasDestabilizers()); - for (size_t i = 0; i < mapped_tableau.getTableauSize(); i++) { - for (size_t j = 0; j < mapped_tableau.tableau[i].size(); j++) { - mapped_tableau.tableau[i][j] = 0; +Tableau Tableau::reverseMapping(const std::vector>* p) { + Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); + for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { + for (unsigned char & j : mappedTableau.tableau[i]) { + j = 0; } } - for (size_t i = 0; i < p.size(); i++) { - for (size_t j = 0; j < p[i].size(); j++) { + for (size_t i = 0; i < p->size(); i++) { + for (size_t j = 0; j < (*p)[i].size(); j++) { // apply mapping from column i to j if p is set - if (p[i][j]) { + if ((*p)[i][j]) { // in every row swap x entry and z entry - for (size_t n = 0; n < mapped_tableau.getTableauSize(); n++) { - mapped_tableau.tableau[n][i] = tableau[n][j]; - mapped_tableau.tableau[n][i + mapped_tableau.nQubits] = - tableau[n][j + mapped_tableau.nQubits]; + for (size_t n = 0; n < mappedTableau.getTableauSize(); n++) { + mappedTableau.tableau[n][i] = tableau[n][j]; + mappedTableau.tableau[n][i + mappedTableau.nQubits] = + tableau[n][j + mappedTableau.nQubits]; } } } } // copy r column without changes for (size_t i = 0; i < tableau.size(); i++) { - mapped_tableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits]; + mappedTableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits]; } - return mapped_tableau; + return mappedTableau; } // number of Qubits is passed because nQubits is not set in result Tableau of // synthesis -Tableau Tableau::reverseMappingOnRows(const std::vector> p, - size_t nq) { - Tableau mapped_tableau = Tableau(nq, true); - mapped_tableau.tableau = tableau; - for (size_t i = 0; i < p.size(); i++) { - for (size_t j = 0; j < p[i].size(); j++) { +Tableau Tableau::reverseMappingOnRows(const std::vector>* p, + const size_t nq) { + auto mappedTableau = Tableau(nq, true); + mappedTableau.tableau = tableau; + for (size_t i = 0; i < p->size(); i++) { + for (size_t j = 0; j < (*p)[i].size(); j++) { // apply mapping from row i to j if p is set - if (p[i][j]) { - mapped_tableau.tableau[i] = tableau[j]; - mapped_tableau.tableau[i + nq] = tableau[j + nq]; + if ((*p)[i][j]) { + mappedTableau.tableau[i] = tableau[j]; + mappedTableau.tableau[i + nq] = tableau[j + nq]; } } } - return mapped_tableau; + return mappedTableau; } // in place Gauss Elimination void Tableau::gaussianEliminationGF2() { - size_t rows = tableau.size(); - size_t cols = tableau[0].size(); + const size_t rows = tableau.size(); + const size_t cols = tableau[0].size(); if (rows == 1) { return; } diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 1e74df044..b5ef73941 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -86,8 +86,9 @@ CouplingMap parseEdges(const std::string& edgeString) { while (getline(ss, item, ';')) { item.erase(remove(item.begin(), item.end(), '{'), item.end()); item.erase(remove(item.begin(), item.end(), '}'), item.end()); - size_t pos = item.find(','); - std::string first, second; + const size_t pos = item.find(','); + std::string first; + std::string second; first = item.substr(0, pos); second = item.substr(pos + 1); @@ -162,7 +163,7 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Target tableau:\n" << targetTableau; const std::vector> p = results.getMappingVector(); - Tableau targetPrime = targetTableau.applyMapping(p); + Tableau targetPrime = targetTableau.applyMapping(&p); std::cout << "Target tableau with mapping:\n" << targetPrime; if (!targetPrime.hasDestabilizers()) { targetPrime.gaussianEliminationGF2(); @@ -171,9 +172,9 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Result tableau with mapping and Gauss:\n" << resultTableau; } else { targetPrime = - targetPrime.reverseMappingOnRows(p, targetPrime.getQubitCount()); + targetPrime.reverseMappingOnRows(&p, targetPrime.getQubitCount()); resultTableau = - resultTableau.reverseMappingOnRows(p, targetPrime.getQubitCount()); + resultTableau.reverseMappingOnRows(&p, targetPrime.getQubitCount()); std::cout << "Result tableau with destab mapping reversed:\n" << resultTableau; std::cout << "Target tableau with destab mapping reversed:\n" From 9cd3f721af796ab262873856019b7d6635eb57d9 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 10 Aug 2024 21:34:16 +0000 Subject: [PATCH 08/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/cliffordsynthesis/Tableau.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 839f2f280..f73e2627e 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -496,7 +496,7 @@ bool Tableau::isIdentityTableau() const { Tableau Tableau::applyMapping(const std::vector>* p) { Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { - for (unsigned char & j : mappedTableau.tableau[i]) { + for (unsigned char& j : mappedTableau.tableau[i]) { j = 0; } } @@ -523,7 +523,7 @@ Tableau Tableau::applyMapping(const std::vector>* p) { Tableau Tableau::reverseMapping(const std::vector>* p) { Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { - for (unsigned char & j : mappedTableau.tableau[i]) { + for (unsigned char& j : mappedTableau.tableau[i]) { j = 0; } } From 3c0773ffe4243485a634cf4384bae89c096c2739 Mon Sep 17 00:00:00 2001 From: Jakob Date: Sun, 11 Aug 2024 00:51:29 +0200 Subject: [PATCH 09/36] update clang-tidy --- .../cliffordsynthesis/CliffordSynthesizer.hpp | 32 ++++++++++--------- include/cliffordsynthesis/Results.hpp | 4 +-- .../encoding/TableauEncoder.hpp | 4 +-- src/cliffordsynthesis/CliffordSynthesizer.cpp | 1 + src/cliffordsynthesis/Tableau.cpp | 4 +-- .../encoding/MultiGateEncoder.cpp | 1 + src/cliffordsynthesis/encoding/SATEncoder.cpp | 1 - .../encoding/SingleGateEncoder.cpp | 1 + .../encoding/TableauEncoder.cpp | 15 +++++---- test/cliffordsynthesis/test_synthesis.cpp | 5 +-- 10 files changed, 37 insertions(+), 31 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index d5b6fa14b..8817329a0 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -12,8 +12,10 @@ #include "cliffordsynthesis/Tableau.hpp" #include "cliffordsynthesis/TargetMetric.hpp" #include "cliffordsynthesis/encoding/SATEncoder.hpp" +#include "utils.hpp" #include +#include #include #include #include @@ -28,48 +30,48 @@ class CliffordSynthesizer { public: CliffordSynthesizer() = default; CliffordSynthesizer(Tableau initial, Tableau target) - : initialTableau(std::move(initial)), targetTableau(std::move(target)), + : initialTableau(std::move(initial)), couplingMap(getFullyConnectedMap( - static_cast(target.getQubitCount()))) {} + static_cast(target.getQubitCount()))), + targetTableau(std::move(target)) {} CliffordSynthesizer(Tableau initial, Tableau target, CouplingMap qm) - : initialTableau(std::move(initial)), targetTableau(std::move(target)), - couplingMap(std::move(qm)) {} + : initialTableau(std::move(initial)), couplingMap(std::move(qm)), + targetTableau(std::move(target)) {} explicit CliffordSynthesizer(Tableau target) : initialTableau(target.getQubitCount(), target.hasDestabilizers()), - targetTableau(std::move(target)), couplingMap(getFullyConnectedMap( - static_cast(target.getQubitCount()))) {} + static_cast(target.getQubitCount()))), + targetTableau(std::move(target)) {} CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc) : initialTableau(std::move(initial)), + couplingMap( + getFullyConnectedMap(static_cast(qc.getNqubits()))), targetTableau(qc, 0, std::numeric_limits::max(), initialTableau.hasDestabilizers()), - couplingMap(getFullyConnectedMap( - static_cast(initial.getQubitCount()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(qc::QuantumComputation& qc, const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), + couplingMap( + getFullyConnectedMap(static_cast(qc.getNqubits()))), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), - couplingMap( - getFullyConnectedMap(static_cast(qc.getNqubits()))), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(Tableau target, CouplingMap qm) : initialTableau(target.getQubitCount(), target.hasDestabilizers()), - targetTableau(std::move(target)), couplingMap(std::move(qm)) {} + couplingMap(std::move(qm)), targetTableau(std::move(target)) {} CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc, CouplingMap qm) - : initialTableau(std::move(initial)), + : initialTableau(std::move(initial)), couplingMap(std::move(qm)), targetTableau(qc, 0, std::numeric_limits::max(), initialTableau.hasDestabilizers()), - couplingMap(std::move(qm)), initialCircuit(std::make_shared(qc)) {} explicit CliffordSynthesizer(qc::QuantumComputation& qc, CouplingMap qm, const bool useDestabilizers = false) : initialTableau(qc.getNqubits(), useDestabilizers), + couplingMap(std::move(qm)), targetTableau(qc, 0, std::numeric_limits::max(), useDestabilizers), - couplingMap(std::move(qm)), initialCircuit(std::make_shared(qc)) {} virtual ~CliffordSynthesizer() = default; @@ -98,8 +100,8 @@ class CliffordSynthesizer { protected: Tableau initialTableau; - Tableau targetTableau; CouplingMap couplingMap; + Tableau targetTableau; std::shared_ptr initialCircuit; Configuration configuration{}; diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index aceb18952..9abcbc4c1 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -58,7 +58,7 @@ class Results { [[nodiscard]] std::string getMapping() const { std::ostringstream oss; for (const auto& row : pvector) { - for (bool val : row) { + for (const bool val : row) { oss << (val ? '1' : '0'); } oss << '\n'; @@ -89,7 +89,7 @@ class Results { void setMapping(std::vector> p) { std::ostringstream oss; for (const auto& row : pvector) { - for (bool val : row) { + for (const bool val : row) { oss << (val ? '1' : '0'); } oss << '\n'; diff --git a/include/cliffordsynthesis/encoding/TableauEncoder.hpp b/include/cliffordsynthesis/encoding/TableauEncoder.hpp index a5afa8d5e..6507bbf2b 100644 --- a/include/cliffordsynthesis/encoding/TableauEncoder.hpp +++ b/include/cliffordsynthesis/encoding/TableauEncoder.hpp @@ -60,7 +60,7 @@ class TableauEncoder { void createTableauVariables(); // fixing the tableau - void assertTableau(const Tableau& tableau, std::size_t t); + void assertTableau(const Tableau& tableau, std::size_t t) const; // extracting the tableau void extractTableauFromModel(Results& results, std::size_t t, @@ -72,7 +72,7 @@ class TableauEncoder { void extractMappingFromModel(Results& results, logicbase::Model& model) const; // assert constraints for mapping variables - void assertMappingConstraints(); + void assertMappingConstraints() const; protected: // number of qubits N diff --git a/src/cliffordsynthesis/CliffordSynthesizer.cpp b/src/cliffordsynthesis/CliffordSynthesizer.cpp index 1039d1ac6..0a7a0d438 100644 --- a/src/cliffordsynthesis/CliffordSynthesizer.cpp +++ b/src/cliffordsynthesis/CliffordSynthesizer.cpp @@ -7,6 +7,7 @@ #include "QuantumComputation.hpp" #include "cliffordsynthesis/Configuration.hpp" +#include "cliffordsynthesis/Results.hpp" #include "cliffordsynthesis/Tableau.hpp" #include "cliffordsynthesis/TargetMetric.hpp" #include "cliffordsynthesis/encoding/SATEncoder.hpp" diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 839f2f280..f73e2627e 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -496,7 +496,7 @@ bool Tableau::isIdentityTableau() const { Tableau Tableau::applyMapping(const std::vector>* p) { Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { - for (unsigned char & j : mappedTableau.tableau[i]) { + for (unsigned char& j : mappedTableau.tableau[i]) { j = 0; } } @@ -523,7 +523,7 @@ Tableau Tableau::applyMapping(const std::vector>* p) { Tableau Tableau::reverseMapping(const std::vector>* p) { Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { - for (unsigned char & j : mappedTableau.tableau[i]) { + for (unsigned char& j : mappedTableau.tableau[i]) { j = 0; } } diff --git a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp index e5bf60893..dd6060ece 100644 --- a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp @@ -8,6 +8,7 @@ #include "Logic.hpp" #include "logicblocks/LogicTerm.hpp" #include "operations/OpType.hpp" +#include "utils.hpp" #include #include diff --git a/src/cliffordsynthesis/encoding/SATEncoder.cpp b/src/cliffordsynthesis/encoding/SATEncoder.cpp index 9e626aea3..6e2249fd5 100644 --- a/src/cliffordsynthesis/encoding/SATEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SATEncoder.cpp @@ -12,7 +12,6 @@ #include "cliffordsynthesis/encoding/SingleGateEncoder.hpp" #include "cliffordsynthesis/encoding/TableauEncoder.hpp" #include "logicblocks/util_logicblock.hpp" -#include "utils.hpp" #include #include diff --git a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp index b6b5bfe79..1a647cadc 100644 --- a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp @@ -7,6 +7,7 @@ #include "Logic.hpp" #include "operations/OpType.hpp" +#include "utils.hpp" #include #include diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 0ebd3a2d7..ab10fe950 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -18,6 +18,7 @@ #include #include #include +#include namespace cs::encoding { @@ -64,7 +65,7 @@ void TableauEncoder::createTableauVariables() { } void TableauEncoder::assertTableau(const Tableau& tableau, - const std::size_t t) { + const std::size_t t) const { const auto n = static_cast(S); PLOG_DEBUG << "Asserting tableau at time step " << t; @@ -81,7 +82,7 @@ void TableauEncoder::assertTableau(const Tableau& tableau, lb->assertFormula(vars.r[t] == LogicTerm(targetR, n)); } -void TableauEncoder::assertMappingConstraints() { +void TableauEncoder::assertMappingConstraints() const { // if p_i_j is set column i is mapped to column j between 0 and 1 for (std::size_t i = 0U; i < N; ++i) { for (std::size_t j = 0U; j < N; ++j) { @@ -95,15 +96,15 @@ void TableauEncoder::assertMappingConstraints() { lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); // assert that for every i and j exactly one p variable is set for (std::size_t i = 0U; i < N; ++i) { - int32_t vr = 0; - int32_t vr1 = 1; + const int32_t vr = 0; + const int32_t vr1 = 1; LogicTerm sumRow = LogicTerm(vr); for (std::size_t j = 0U; j < N; ++j) { sumRow = sumRow + vars.p[i][j]; } lb->assertFormula(sumRow == LogicTerm(vr1)); - int32_t vc = 0; - int32_t vc1 = 1; + const int32_t vc = 0; + const int32_t vc1 = 1; LogicTerm sumCol = LogicTerm(vc); for (std::size_t j = 0U; j < N; ++j) { sumCol = sumCol + vars.p[j][i]; @@ -141,7 +142,7 @@ void TableauEncoder::extractTableauFromModel(Results& results, void TableauEncoder::extractMappingFromModel(Results& results, Model& model) const { - std::vector row(N, false); + const std::vector row(N, false); std::vector> pvals(N, std::vector(N, false)); for (std::size_t i = 0; i < N; ++i) { for (std::size_t j = 0; j < N; ++j) { diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index b5ef73941..95952dae7 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -12,6 +12,7 @@ #include "operations/Control.hpp" #include "utils.hpp" +#include #include #include #include @@ -93,8 +94,8 @@ CouplingMap parseEdges(const std::string& edgeString) { first = item.substr(0, pos); second = item.substr(pos + 1); - int u = stoi(first); - int v = stoi(second); + const int u = stoi(first); + const int v = stoi(second); // Insert the edge into the set edges.insert(Edge{u, v}); From f811b22c05ef74a764e33b2b7faa75091255ee30 Mon Sep 17 00:00:00 2001 From: Jakob Date: Sun, 11 Aug 2024 15:57:44 +0200 Subject: [PATCH 10/36] implement python part of coupling maps for clifford synthesis --- src/mqt/qmap/clifford_synthesis.py | 27 ++++++++++++++++++++--- src/mqt/qmap/pyqmap.pyi | 12 ++++++++++ test/cliffordsynthesis/circuits.json | 20 ++++++++--------- test/cliffordsynthesis/test_synthesis.cpp | 4 ++-- test/python/test_cliffordsynthesis.py | 10 ++++++++- 5 files changed, 57 insertions(+), 16 deletions(-) diff --git a/src/mqt/qmap/clifford_synthesis.py b/src/mqt/qmap/clifford_synthesis.py index 444d32afb..82d732af7 100644 --- a/src/mqt/qmap/clifford_synthesis.py +++ b/src/mqt/qmap/clifford_synthesis.py @@ -2,7 +2,7 @@ from __future__ import annotations -from typing import Any +from typing import TYPE_CHECKING, Any from qiskit import QuantumCircuit, qasm3 from qiskit.quantum_info import Clifford, PauliList @@ -17,6 +17,9 @@ Tableau, ) +if TYPE_CHECKING: + from collections.abc import Iterable + def _import_circuit(circuit: str | QuantumCircuit | QuantumComputation) -> QuantumComputation: """Import a circuit from a string, a QuantumCircuit, or a QuantumComputation.""" @@ -96,6 +99,7 @@ def synthesize_clifford( target_tableau: str | Clifford | PauliList | Tableau, initial_tableau: str | Clifford | PauliList | Tableau | None = None, include_destabilizers: bool = False, + coupling_map: Iterable[tuple[int, int]] | None = None, **kwargs: Any, # noqa: ANN401 ) -> tuple[QuantumCircuit, SynthesisResults]: """Synthesize a Clifford circuit from a given tableau starting from an (optional) initial tableau. @@ -114,6 +118,8 @@ def synthesize_clifford( If no initial tableau is given, the synthesis starts from the identity tableau. include_destabilizers: Flag to set whether destabilizers should be considered in the synthesis + coupling_map: + Iterable of tuples of connected qubits of the architecture to synthesize for. **kwargs: Additional keyword arguments to configure the synthesis. See :class:`SynthesisConfiguration` for a list of available options. @@ -125,7 +131,12 @@ def synthesize_clifford( tableau = _import_tableau(target_tableau, include_destabilizers) if initial_tableau is not None: - synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), tableau) + if coupling_map is not None: + synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), tableau, set(coupling_map)) + else: + synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), tableau) + elif coupling_map is not None: + synthesizer = CliffordSynthesizer(tableau, set(coupling_map)) else: synthesizer = CliffordSynthesizer(tableau) @@ -141,6 +152,7 @@ def optimize_clifford( circuit: str | QuantumCircuit | QuantumComputation, initial_tableau: str | Clifford | PauliList | Tableau | None = None, include_destabilizers: bool = False, + coupling_map: Iterable[tuple[int, int]] | None = None, **kwargs: Any, # noqa: ANN401 ) -> tuple[QuantumCircuit, SynthesisResults]: """Optimize a Clifford circuit starting from an (optional) initial tableau. @@ -159,6 +171,8 @@ def optimize_clifford( If no initial tableau is given, the synthesis starts from the identity tableau. include_destabilizers: Flag to set whether destabilizers should be considered in the synthesis + coupling_map: + Iterable of tuples of connected qubits of the architecture to synthesize for. **kwargs: Additional keyword arguments to configure the synthesis. See :class:`SynthesisConfiguration` for a list of available options. @@ -170,7 +184,14 @@ def optimize_clifford( qc = _import_circuit(circuit) if initial_tableau is not None: - synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau, include_destabilizers), qc) + if coupling_map is not None: + synthesizer = CliffordSynthesizer( + _import_tableau(initial_tableau, include_destabilizers), qc, set(coupling_map) + ) + else: + synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau, include_destabilizers), qc) + elif coupling_map is not None: + synthesizer = CliffordSynthesizer(qc, include_destabilizers, set(coupling_map)) else: synthesizer = CliffordSynthesizer(qc, include_destabilizers) diff --git a/src/mqt/qmap/pyqmap.pyi b/src/mqt/qmap/pyqmap.pyi index 34efe68bb..6c89807fb 100644 --- a/src/mqt/qmap/pyqmap.pyi +++ b/src/mqt/qmap/pyqmap.pyi @@ -514,6 +514,18 @@ class CliffordSynthesizer: def __init__(self, qc: QuantumComputation, use_destabilizers: bool) -> None: ... @overload def __init__(self, initial_tableau: Tableau, qc: QuantumComputation) -> None: ... + @overload + def __init__( + self, initial_tableau: Tableau, target_tableau: Tableau, coupling_map: set[tuple[int, int]] + ) -> None: ... + @overload + def __init__(self, target_tableau: Tableau, coupling_map: set[tuple[int, int]]) -> None: ... + @overload + def __init__(self, qc: QuantumComputation, use_destabilizers: bool, coupling_map: set[tuple[int, int]]) -> None: ... + @overload + def __init__( + self, initial_tableau: Tableau, qc: QuantumComputation, coupling_map: set[tuple[int, int]] + ) -> None: ... def synthesize(self, config: SynthesisConfiguration = ...) -> None: ... @property def results(self) -> SynthesisResults: ... diff --git a/test/cliffordsynthesis/circuits.json b/test/cliffordsynthesis/circuits.json index af5972ae3..2d73fa8ab 100644 --- a/test/cliffordsynthesis/circuits.json +++ b/test/cliffordsynthesis/circuits.json @@ -52,7 +52,7 @@ "expected_minimal_gates_at_minimal_depth": 2, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 2, - "couplingMap": "{0,1};{1,0}" + "coupling_map": "{0,1};{1,0}" }, { "description": "cx_coupling_test", @@ -62,7 +62,7 @@ "expected_minimal_gates_at_minimal_depth": 3, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 3, - "couplingMap": "{0,1};{1,0};{1,2};{2,1}" + "coupling_map": "{0,1};{1,0};{1,2};{2,1}" }, { "description": "cx_coupling_test_init_1_final_2", @@ -72,7 +72,7 @@ "expected_minimal_gates_at_minimal_depth": 3, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 3, - "couplingMap": "{0,2};{2,0};{1,2};{2,1}" + "coupling_map": "{0,2};{2,0};{1,2};{2,1}" }, { "description": "cx_coupling_test_init_1_final_0", @@ -82,7 +82,7 @@ "expected_minimal_gates_at_minimal_depth": 3, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 3, - "couplingMap": "{0,2};{2,0};{1,0};{0,1}" + "coupling_map": "{0,2};{2,0};{1,0};{0,1}" }, { "description": "cx_coupling_test_init_2_final_0", @@ -92,7 +92,7 @@ "expected_minimal_gates_at_minimal_depth": 3, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 3, - "couplingMap": "{0,2};{2,0};{1,0};{0,1}" + "coupling_map": "{0,2};{2,0};{1,0};{0,1}" }, { "description": "coupling_test_3qubit_cnots_at_0", @@ -102,7 +102,7 @@ "expected_minimal_gates_at_minimal_depth": 5, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 5, - "couplingMap": "{0,2};{2,0};{1,0};{0,1}" + "coupling_map": "{0,2};{2,0};{1,0};{0,1}" }, { "description": "coupling_test_3qubit_cnots_at_1", @@ -112,7 +112,7 @@ "expected_minimal_gates_at_minimal_depth": 5, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 5, - "couplingMap": "{1,2};{2,1};{1,0};{0,1}" + "coupling_map": "{1,2};{2,1};{1,0};{0,1}" }, { "description": "coupling_test_irred_3qubit_cnots_at_1", @@ -122,7 +122,7 @@ "expected_minimal_gates_at_minimal_depth": 9, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 8, - "couplingMap": "{1,2};{2,1};{1,0};{0,1}" + "coupling_map": "{1,2};{2,1};{1,0};{0,1}" }, { "description": "coupling_test_irred_3qubit_cnots_at_2", @@ -132,7 +132,7 @@ "expected_minimal_gates_at_minimal_depth": 9, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 8, - "couplingMap": "{0,2};{2,0};{2,1};{1,2}" + "coupling_map": "{0,2};{2,0};{2,1};{1,2}" }, { "description": "coupling_test_irred_3qubit_cnots_at_0", @@ -142,6 +142,6 @@ "expected_minimal_gates_at_minimal_depth": 9, "expected_minimal_two_qubit_gates": 2, "expected_minimal_gates_at_minimal_two_qubit_gates": 8, - "couplingMap": "{0,2};{2,0};{0,1};{1,0}" + "coupling_map": "{0,2};{2,0};{0,1};{1,0}" } ] diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 95952dae7..cd87f68ad 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -55,8 +55,8 @@ inline void from_json(const nlohmann::json& j, TestConfiguration& test) { if (j.contains("initial_circuit")) { test.initialCircuit = j.at("initial_circuit").get(); } - if (j.contains("couplingMap")) { - test.couplingMap = j.at("couplingMap").get(); + if (j.contains("coupling_map")) { + test.couplingMap = j.at("coupling_map").get(); } test.expectedMinimalGates = j.at("expected_minimal_gates").get(); diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index 7480ee3b0..b464cbc38 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -27,6 +27,7 @@ class Configuration: initial_tableau: str | None = None target_tableau: str | None = None initial_circuit: str | None = None + coupling_map: str | None = None def create_circuit_tests() -> list[Configuration]: @@ -49,8 +50,15 @@ def create_tableau_tests() -> list[Configuration]: @pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"]) def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) -> None: """Test gate-optimal Clifford synthesis.""" + cm = None + if test_config.coupling_map is not None: + pairs = test_config.coupling_map.split(";") + cm = [(int(pair.strip("{}").split(",")[0]), int(pair.strip("{}").split(",")[1])) for pair in pairs] circ, results = qmap.optimize_clifford( - circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="gates" + circuit=test_config.initial_circuit, + use_maxsat=use_maxsat, + target_metric="gates", + coupling_map=cm, ) assert results.gates == test_config.expected_minimal_gates From 320114643c07328bfc33a6a171cbf3fe3facda61 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 11:48:51 +0200 Subject: [PATCH 11/36] update bindings for synthesis with coupling map --- include/cliffordsynthesis/Tableau.hpp | 1 + src/cliffordsynthesis/Tableau.cpp | 13 +++++++++++++ src/mqt/qmap/clifford_synthesis.py | 2 +- src/mqt/qmap/pyqmap.pyi | 2 +- src/python/bindings.cpp | 22 ++++++++++++++++++++++ 5 files changed, 38 insertions(+), 2 deletions(-) diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index f60e5af04..f27c5793a 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -168,5 +168,6 @@ class Tableau { Tableau reverseMappingOnRows(const std::vector>* p, size_t nq); void gaussianEliminationGF2(); + bool equivalentUpToStabilizer(const Tableau* t) const; }; } // namespace cs diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index f73e2627e..3ae46cd67 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -609,4 +609,17 @@ void Tableau::gaussianEliminationGF2() { pivot++; } } +// equivalence check for two Tableaus without destablilizers +bool Tableau::equivalentUpToStabilizer(const Tableau* t) const { + assert(getTableauSize() == t->getTableauSize()); + + Tableau tEliminated = Tableau(nQubits, hasDestabilizers()); + tEliminated.tableau = tableau; + tEliminated.gaussianEliminationGF2(); + + Tableau t2Eliminated = Tableau(nQubits, hasDestabilizers()); + t2Eliminated.tableau = t->getTableau(); + t2Eliminated.gaussianEliminationGF2(); + return tEliminated == t2Eliminated; +} } // namespace cs diff --git a/src/mqt/qmap/clifford_synthesis.py b/src/mqt/qmap/clifford_synthesis.py index 82d732af7..67b95bf31 100644 --- a/src/mqt/qmap/clifford_synthesis.py +++ b/src/mqt/qmap/clifford_synthesis.py @@ -191,7 +191,7 @@ def optimize_clifford( else: synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau, include_destabilizers), qc) elif coupling_map is not None: - synthesizer = CliffordSynthesizer(qc, include_destabilizers, set(coupling_map)) + synthesizer = CliffordSynthesizer(qc, set(coupling_map), include_destabilizers) else: synthesizer = CliffordSynthesizer(qc, include_destabilizers) diff --git a/src/mqt/qmap/pyqmap.pyi b/src/mqt/qmap/pyqmap.pyi index 6c89807fb..14ffd495d 100644 --- a/src/mqt/qmap/pyqmap.pyi +++ b/src/mqt/qmap/pyqmap.pyi @@ -521,7 +521,7 @@ class CliffordSynthesizer: @overload def __init__(self, target_tableau: Tableau, coupling_map: set[tuple[int, int]]) -> None: ... @overload - def __init__(self, qc: QuantumComputation, use_destabilizers: bool, coupling_map: set[tuple[int, int]]) -> None: ... + def __init__(self, qc: QuantumComputation, coupling_map: set[tuple[int, int]], use_destabilizers: bool) -> None: ... @overload def __init__( self, initial_tableau: Tableau, qc: QuantumComputation, coupling_map: set[tuple[int, int]] diff --git a/src/python/bindings.cpp b/src/python/bindings.cpp index 7b12a6ca1..4634df9c8 100644 --- a/src/python/bindings.cpp +++ b/src/python/bindings.cpp @@ -707,6 +707,28 @@ PYBIND11_MODULE(pyqmap, m, py::mod_gil_not_used()) { "qc"_a, "Constructs a synthesizer for a quantum computation representing the " "target state that starts in an initial state represented by a tableau."); + synthesizer.def(py::init(), + "initial_tableau"_a, "target_tableau"_a, "coupling_map"_a, + "Constructs a synthesizer for two tableaus representing the " + "initial and target state with a coupling map."); + + synthesizer.def(py::init(), "target_tableau"_a, + "coupling_map"_a, + "Constructs a synthesizer for a tableau representing the " + "target state with a coupling map."); + + synthesizer.def(py::init(), + "qc"_a, "coupling_map"_a, + "use_destabilizers"_a + "Constructs a synthesizer for a quantum computation " + "representing the target state with a coupling map."); + + synthesizer.def( + py::init(), + "initial_tableau"_a, "qc"_a, "coupling_map"_a, + "Constructs a synthesizer for a quantum computation representing the " + "target state that starts in an initial state represented by a tableau " + "with a coupling map."); synthesizer.def("synthesize", &cs::CliffordSynthesizer::synthesize, "config"_a = cs::Configuration(), "Runs the synthesis with the given configuration."); From d905ca7ad915b17c887f8092f26d2fa5a627fdc8 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 16:06:59 +0200 Subject: [PATCH 12/36] add bindings for mapping --- src/mqt/qmap/pyqmap.pyi | 4 + src/python/bindings.cpp | 4 + test/python/test_cliffordsynthesis.py | 117 ++++++++++++++++++++++---- 3 files changed, 108 insertions(+), 17 deletions(-) diff --git a/src/mqt/qmap/pyqmap.pyi b/src/mqt/qmap/pyqmap.pyi index 14ffd495d..e9b2d046e 100644 --- a/src/mqt/qmap/pyqmap.pyi +++ b/src/mqt/qmap/pyqmap.pyi @@ -487,6 +487,10 @@ class SynthesisResults: def tableau(self) -> str: ... @property def two_qubit_gates(self) -> int: ... + @property + def mapping(self) -> list[list[bool]]: ... + @property + def mapping_string(self) -> str: ... class QuantumComputation: def __init__(self) -> None: ... diff --git a/src/python/bindings.cpp b/src/python/bindings.cpp index 4634df9c8..fd6b4ac50 100644 --- a/src/python/bindings.cpp +++ b/src/python/bindings.cpp @@ -639,6 +639,10 @@ PYBIND11_MODULE(pyqmap, m, py::mod_gil_not_used()) { .def_property_readonly("tableau", &cs::Results::getResultTableau, "Returns a string representation of the " "synthesized circuit's tableau.") + .def_property_readonly("mapping", &cs::Results::getMappingVector, + "Returns a vector of vectors representing the mapping.") + .def_property_readonly("mapping_string", &cs::Results::getMapping, + "Returns a string representation of the mapping.") .def("sat", &cs::Results::sat, "Returns `true` if the synthesis was successful.") .def("unsat", &cs::Results::unsat, diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index b464cbc38..4b969e511 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -5,6 +5,7 @@ import json from dataclasses import dataclass from pathlib import Path +import itertools import pytest from qiskit import QuantumCircuit, qasm2 @@ -29,6 +30,16 @@ class Configuration: initial_circuit: str | None = None coupling_map: str | None = None +def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int]) -> QuantumCircuit: + """Return a new circuit with qubits permuted according to the given permutation.""" + permuted_circ = QuantumCircuit(circuit.num_qubits) + qubit_map = {qubit: i for i, qubit in enumerate(circuit.qubits)} + + for gate, qubits, clbits in circuit.data: + new_qubits = [circuit.qubits[permutation[qubit_map[q]]] for q in qubits] + permuted_circ.append(gate, new_qubits, clbits) + + return permuted_circ def create_circuit_tests() -> list[Configuration]: """Create test cases for Clifford synthesis.""" @@ -46,19 +57,22 @@ def create_tableau_tests() -> list[Configuration]: return [Configuration(**t) for t in tableaus] +def convert_coupling_map(cm): + if cm is not None: + pairs = cm.split(";") + cm = [(int(pair.strip("{}").split(",")[0]), int(pair.strip("{}").split(",")[1])) for pair in pairs] + return cm + + @pytest.mark.parametrize("test_config", create_circuit_tests()) @pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"]) def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) -> None: """Test gate-optimal Clifford synthesis.""" - cm = None - if test_config.coupling_map is not None: - pairs = test_config.coupling_map.split(";") - cm = [(int(pair.strip("{}").split(",")[0]), int(pair.strip("{}").split(",")[1])) for pair in pairs] circ, results = qmap.optimize_clifford( circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="gates", - coupling_map=cm, + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.gates == test_config.expected_minimal_gates @@ -70,7 +84,7 @@ def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) - def test_optimize_clifford_depth(test_config: Configuration, use_maxsat: bool) -> None: """Test depth-optimal Clifford synthesis.""" circ, results = qmap.optimize_clifford( - circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="depth" + circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="depth", coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.depth == test_config.expected_minimal_depth @@ -86,8 +100,8 @@ def test_optimize_clifford_gates_at_minimal_depth(test_config: Configuration, us use_maxsat=use_maxsat, target_metric="depth", minimize_gates_after_depth_optimization=True, + coupling_map=convert_coupling_map(test_config.coupling_map) ) - assert results.gates == test_config.expected_minimal_gates_at_minimal_depth print("\n", circ) @@ -101,6 +115,7 @@ def test_optimize_clifford_two_qubit_gates(test_config: Configuration, use_maxsa use_maxsat=use_maxsat, target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, + coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates @@ -117,6 +132,7 @@ def test_optimize_clifford_gates_at_minimal_two_qubit_gates(test_config: Configu target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, minimize_gates_after_two_qubit_gate_optimization=True, + coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates @@ -137,7 +153,6 @@ def test_heuristic(test_config: Configuration) -> None: circ_opt, _ = qmap.optimize_clifford( circuit=test_config.initial_circuit, heuristic=False, target_metric="depth", include_destabilizers=True ) - assert circ.depth() >= circ_opt.depth() assert Clifford(circ) == Clifford(circ_opt) print("\n", circ) @@ -152,6 +167,7 @@ def test_synthesize_clifford_gates(test_config: Configuration, use_maxsat: bool) initial_tableau=test_config.initial_tableau, use_maxsat=use_maxsat, target_metric="gates", + coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.gates == test_config.expected_minimal_gates @@ -167,6 +183,7 @@ def test_synthesize_clifford_depth(test_config: Configuration, use_maxsat: bool) initial_tableau=test_config.initial_tableau, use_maxsat=use_maxsat, target_metric="depth", + coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.depth == test_config.expected_minimal_depth @@ -183,6 +200,7 @@ def test_synthesize_clifford_gates_at_minimal_depth(test_config: Configuration, use_maxsat=use_maxsat, target_metric="depth", minimize_gates_after_depth_optimization=True, + coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.gates == test_config.expected_minimal_gates_at_minimal_depth @@ -199,6 +217,7 @@ def test_synthesize_clifford_two_qubit_gates(test_config: Configuration, use_max use_maxsat=use_maxsat, target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, + coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates @@ -216,6 +235,7 @@ def test_synthesize_clifford_gates_at_minimal_two_qubit_gates(test_config: Confi target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, minimize_gates_after_two_qubit_gate_optimization=True, + coupling_map=convert_coupling_map(test_config.coupling_map) ) assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates @@ -239,54 +259,117 @@ def test_optimize_quantum_computation(bell_circuit: QuantumCircuit) -> None: """Test that we can optimize an MQT QuantumComputation.""" qc = qmap.QuantumComputation.from_qiskit(bell_circuit) circ, _ = qmap.optimize_clifford(circuit=qc) - assert qcec.verify(circ, bell_circuit).considered_equivalent() + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_optimize_from_qasm_file(bell_circuit: QuantumCircuit) -> None: """Test that we can optimize from a QASM file.""" qasm2.dump(bell_circuit, Path("bell.qasm")) circ, _ = qmap.optimize_clifford(circuit="bell.qasm") - assert qcec.verify(circ, bell_circuit).considered_equivalent() + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_optimize_qiskit_circuit(bell_circuit: QuantumCircuit) -> None: """Test that we can optimize a Qiskit QuantumCircuit.""" circ, _ = qmap.optimize_clifford(circuit=bell_circuit) - assert qcec.verify(circ, bell_circuit).considered_equivalent() + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_optimize_with_initial_tableau(bell_circuit: QuantumCircuit) -> None: """Test that we can optimize a circuit with an initial tableau.""" circ, _ = qmap.optimize_clifford(circuit=bell_circuit, initial_tableau=qmap.Tableau(bell_circuit.num_qubits)) - assert qcec.verify(circ, bell_circuit).considered_equivalent() - + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_synthesize_from_tableau(bell_circuit: QuantumCircuit) -> None: """Test that we can synthesize a circuit from an MQT Tableau.""" tableau = qmap.Tableau("['XX', 'ZZ']") circ, _ = qmap.synthesize_clifford(target_tableau=tableau) - assert qcec.verify(circ, bell_circuit).considered_equivalent() + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_synthesize_from_qiskit_clifford(bell_circuit: QuantumCircuit) -> None: """Test that we can synthesize a circuit from a Qiskit Clifford.""" cliff = Clifford(bell_circuit) circ, _ = qmap.synthesize_clifford(target_tableau=cliff) - assert qcec.verify(circ, bell_circuit).considered_equivalent() + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_synthesize_from_qiskit_pauli_list(bell_circuit: QuantumCircuit) -> None: """Test that we can synthesize a circuit from a Qiskit PauliList.""" pauli_list = PauliList(["XX", "ZZ"]) circ, _ = qmap.synthesize_clifford(target_tableau=pauli_list) - assert qcec.verify(circ, bell_circuit).considered_equivalent() + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_synthesize_from_string(bell_circuit: QuantumCircuit) -> None: """Test that we can synthesize a circuit from a String.""" pauli_str = "[XX,ZZ]" circ, _ = qmap.synthesize_clifford(target_tableau=pauli_str) - assert qcec.verify(circ, bell_circuit).considered_equivalent() + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent def test_invalid_kwarg_to_synthesis() -> None: From 1ec68f9e6e5726b503df01df93a24fec2266b8e3 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Tue, 13 Aug 2024 14:07:29 +0000 Subject: [PATCH 13/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/python/bindings.cpp | 5 +++-- test/python/test_cliffordsynthesis.py | 26 ++++++++++++++++---------- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/src/python/bindings.cpp b/src/python/bindings.cpp index fd6b4ac50..17bf79539 100644 --- a/src/python/bindings.cpp +++ b/src/python/bindings.cpp @@ -639,8 +639,9 @@ PYBIND11_MODULE(pyqmap, m, py::mod_gil_not_used()) { .def_property_readonly("tableau", &cs::Results::getResultTableau, "Returns a string representation of the " "synthesized circuit's tableau.") - .def_property_readonly("mapping", &cs::Results::getMappingVector, - "Returns a vector of vectors representing the mapping.") + .def_property_readonly( + "mapping", &cs::Results::getMappingVector, + "Returns a vector of vectors representing the mapping.") .def_property_readonly("mapping_string", &cs::Results::getMapping, "Returns a string representation of the mapping.") .def("sat", &cs::Results::sat, diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index 4b969e511..a5c92b469 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -2,10 +2,10 @@ from __future__ import annotations +import itertools import json from dataclasses import dataclass from pathlib import Path -import itertools import pytest from qiskit import QuantumCircuit, qasm2 @@ -30,6 +30,7 @@ class Configuration: initial_circuit: str | None = None coupling_map: str | None = None + def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int]) -> QuantumCircuit: """Return a new circuit with qubits permuted according to the given permutation.""" permuted_circ = QuantumCircuit(circuit.num_qubits) @@ -41,6 +42,7 @@ def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int]) -> QuantumC return permuted_circ + def create_circuit_tests() -> list[Configuration]: """Create test cases for Clifford synthesis.""" path = Path(__file__).resolve().parent.parent / "cliffordsynthesis" / "circuits.json" @@ -84,7 +86,10 @@ def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) - def test_optimize_clifford_depth(test_config: Configuration, use_maxsat: bool) -> None: """Test depth-optimal Clifford synthesis.""" circ, results = qmap.optimize_clifford( - circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="depth", coupling_map=convert_coupling_map(test_config.coupling_map) + circuit=test_config.initial_circuit, + use_maxsat=use_maxsat, + target_metric="depth", + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.depth == test_config.expected_minimal_depth @@ -100,7 +105,7 @@ def test_optimize_clifford_gates_at_minimal_depth(test_config: Configuration, us use_maxsat=use_maxsat, target_metric="depth", minimize_gates_after_depth_optimization=True, - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.gates == test_config.expected_minimal_gates_at_minimal_depth print("\n", circ) @@ -115,7 +120,7 @@ def test_optimize_clifford_two_qubit_gates(test_config: Configuration, use_maxsa use_maxsat=use_maxsat, target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates @@ -132,7 +137,7 @@ def test_optimize_clifford_gates_at_minimal_two_qubit_gates(test_config: Configu target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, minimize_gates_after_two_qubit_gate_optimization=True, - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates @@ -167,7 +172,7 @@ def test_synthesize_clifford_gates(test_config: Configuration, use_maxsat: bool) initial_tableau=test_config.initial_tableau, use_maxsat=use_maxsat, target_metric="gates", - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.gates == test_config.expected_minimal_gates @@ -183,7 +188,7 @@ def test_synthesize_clifford_depth(test_config: Configuration, use_maxsat: bool) initial_tableau=test_config.initial_tableau, use_maxsat=use_maxsat, target_metric="depth", - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.depth == test_config.expected_minimal_depth @@ -200,7 +205,7 @@ def test_synthesize_clifford_gates_at_minimal_depth(test_config: Configuration, use_maxsat=use_maxsat, target_metric="depth", minimize_gates_after_depth_optimization=True, - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.gates == test_config.expected_minimal_gates_at_minimal_depth @@ -217,7 +222,7 @@ def test_synthesize_clifford_two_qubit_gates(test_config: Configuration, use_max use_maxsat=use_maxsat, target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates @@ -235,7 +240,7 @@ def test_synthesize_clifford_gates_at_minimal_two_qubit_gates(test_config: Confi target_metric="two_qubit_gates", try_higher_gate_limit_for_two_qubit_gate_optimization=True, minimize_gates_after_two_qubit_gate_optimization=True, - coupling_map=convert_coupling_map(test_config.coupling_map) + coupling_map=convert_coupling_map(test_config.coupling_map), ) assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates @@ -312,6 +317,7 @@ def test_optimize_with_initial_tableau(bell_circuit: QuantumCircuit) -> None: break assert equivalent + def test_synthesize_from_tableau(bell_circuit: QuantumCircuit) -> None: """Test that we can synthesize a circuit from an MQT Tableau.""" tableau = qmap.Tableau("['XX', 'ZZ']") From 0754a683f79def54cd9cd4fa544b2cd3b31b9980 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 17:43:44 +0200 Subject: [PATCH 14/36] fix lint in clifford test functions --- test/python/test_cliffordsynthesis.py | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index a5c92b469..0b40e7a42 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -31,7 +31,7 @@ class Configuration: coupling_map: str | None = None -def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int]) -> QuantumCircuit: +def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int, ...]) -> QuantumCircuit: """Return a new circuit with qubits permuted according to the given permutation.""" permuted_circ = QuantumCircuit(circuit.num_qubits) qubit_map = {qubit: i for i, qubit in enumerate(circuit.qubits)} @@ -43,6 +43,15 @@ def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int]) -> QuantumC return permuted_circ +def convert_coupling_map(cm: str | None = None) -> list[tuple[int, int]] | None: + """Convert a coupling map passed as a string to a CouplingMap.""" + coupling_map = None + if cm is not None: + pairs = cm.split(";") + coupling_map = [(int(pair.strip("{}").split(",")[0]), int(pair.strip("{}").split(",")[1])) for pair in pairs] + return coupling_map + + def create_circuit_tests() -> list[Configuration]: """Create test cases for Clifford synthesis.""" path = Path(__file__).resolve().parent.parent / "cliffordsynthesis" / "circuits.json" @@ -59,13 +68,6 @@ def create_tableau_tests() -> list[Configuration]: return [Configuration(**t) for t in tableaus] -def convert_coupling_map(cm): - if cm is not None: - pairs = cm.split(";") - cm = [(int(pair.strip("{}").split(",")[0]), int(pair.strip("{}").split(",")[1])) for pair in pairs] - return cm - - @pytest.mark.parametrize("test_config", create_circuit_tests()) @pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"]) def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) -> None: From 93c0df83f86edb5c165d44dab665e898a1ff001a Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 19:22:34 +0200 Subject: [PATCH 15/36] specify result circuit on empty circuits for heuristic synthesis --- src/cliffordsynthesis/CliffordSynthesizer.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cliffordsynthesis/CliffordSynthesizer.cpp b/src/cliffordsynthesis/CliffordSynthesizer.cpp index 0a7a0d438..aa611bc91 100644 --- a/src/cliffordsynthesis/CliffordSynthesizer.cpp +++ b/src/cliffordsynthesis/CliffordSynthesizer.cpp @@ -493,6 +493,7 @@ std::vector getLayers(const qc::QuantumComputation& qc) { void CliffordSynthesizer::depthHeuristicSynthesis() { PLOG_INFO << "Optimizing Circuit with Heuristic"; if (initialCircuit->getDepth() == 0) { + results.setResultCircuit(*initialCircuit); return; } auto optimalConfig = configuration; From 6d227f0c25304bc7dc8b2cca14c2bed6de87e8f0 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 21:33:29 +0200 Subject: [PATCH 16/36] add equivalence check function in clifford tests --- src/cliffordsynthesis/Tableau.cpp | 27 ----------------------- test/cliffordsynthesis/test_synthesis.cpp | 2 +- 2 files changed, 1 insertion(+), 28 deletions(-) diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 3ae46cd67..c3e5d2977 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -520,33 +520,6 @@ Tableau Tableau::applyMapping(const std::vector>* p) { return mappedTableau; } -Tableau Tableau::reverseMapping(const std::vector>* p) { - Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); - for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { - for (unsigned char& j : mappedTableau.tableau[i]) { - j = 0; - } - } - for (size_t i = 0; i < p->size(); i++) { - for (size_t j = 0; j < (*p)[i].size(); j++) { - // apply mapping from column i to j if p is set - if ((*p)[i][j]) { - // in every row swap x entry and z entry - for (size_t n = 0; n < mappedTableau.getTableauSize(); n++) { - mappedTableau.tableau[n][i] = tableau[n][j]; - mappedTableau.tableau[n][i + mappedTableau.nQubits] = - tableau[n][j + mappedTableau.nQubits]; - } - } - } - } - // copy r column without changes - for (size_t i = 0; i < tableau.size(); i++) { - mappedTableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits]; - } - return mappedTableau; -} - // number of Qubits is passed because nQubits is not set in result Tableau of // synthesis Tableau Tableau::reverseMappingOnRows(const std::vector>* p, diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index cd87f68ad..36b54ce2d 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -169,6 +169,7 @@ class SynthesisTest : public ::testing::TestWithParam { if (!targetPrime.hasDestabilizers()) { targetPrime.gaussianEliminationGF2(); resultTableau.gaussianEliminationGF2(); + assert(targetPrime.equivalentUpToStabilizer(&resultTableau)); std::cout << "Target tableau with mapping and Gauss:\n" << targetPrime; std::cout << "Result tableau with mapping and Gauss:\n" << resultTableau; } else { @@ -181,7 +182,6 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Target tableau with destab mapping reversed:\n" << targetPrime; } - EXPECT_EQ(resultTableau, targetPrime); const auto& resultCircuit = synthesizer.getResultCircuit(); From 810121ccac9b36ad3457e021c0e7a172d4442d1f Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 21:46:41 +0200 Subject: [PATCH 17/36] add missing headers to test_synthesis.cpp --- test/cliffordsynthesis/test_synthesis.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 36b54ce2d..ae6fbe44d 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -22,6 +22,7 @@ #include #include #include +#include using namespace qc::literals; From be7f14f5d8a5b772f8be5cb01386b7218e204f24 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Tue, 13 Aug 2024 19:47:22 +0000 Subject: [PATCH 18/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- test/cliffordsynthesis/test_synthesis.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index ae6fbe44d..ea49e15a3 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -13,6 +13,7 @@ #include "utils.hpp" #include +#include #include #include #include @@ -22,7 +23,6 @@ #include #include #include -#include using namespace qc::literals; From 5ac7c6f40a642064068bcdad3617678087107da3 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 22:39:30 +0200 Subject: [PATCH 19/36] add more python tests for clifford coupling --- test/python/test_cliffordsynthesis.py | 33 +++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index 0b40e7a42..4ef7efbaf 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -380,6 +380,39 @@ def test_synthesize_from_string(bell_circuit: QuantumCircuit) -> None: assert equivalent +def test_synthesize_with_coupling_from_tableau(bell_circuit: QuantumCircuit) -> None: + """Test that we can synthesize a circuit from an MQT Tableau.""" + tableau = qmap.Tableau("['XX', 'ZZ']") + coupling_map = [(0, 1), (1, 0)] + circ, _ = qmap.synthesize_clifford(target_tableau=tableau, coupling_map=coupling_map) + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent + + +def test_synthesize_with_coupling_with_initial_tableau_from_tableau(bell_circuit: QuantumCircuit) -> None: + """Test that we can synthesize a circuit from an MQT Tableau.""" + tableau = qmap.Tableau("['XX', 'ZZ']") + init_tableau = qmap.Tableau("['ZI','IZ']") + coupling_map = [(0, 1), (1, 0)] + circ, _ = qmap.synthesize_clifford(target_tableau=tableau, initial_tableau=init_tableau, coupling_map=coupling_map) + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent + + def test_invalid_kwarg_to_synthesis() -> None: """Test that we raise an error if we pass an invalid kwarg to synthesis.""" with pytest.raises(ValueError, match="Invalid keyword argument"): From 1dedddcc4da383d7044eb30dc6c0ca00a8782694 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 13 Aug 2024 23:22:58 +0200 Subject: [PATCH 20/36] add tests to clifford synthesis --- test/python/test_cliffordsynthesis.py | 34 +++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index 4ef7efbaf..2930523d4 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -320,6 +320,23 @@ def test_optimize_with_initial_tableau(bell_circuit: QuantumCircuit) -> None: assert equivalent +def test_optimize_with_initial_tableau_with_mapping(bell_circuit: QuantumCircuit) -> None: + """Test that we can optimize a circuit with an initial tableau.""" + coupling_map = [(0, 1), (1, 0)] + circ, _ = qmap.optimize_clifford( + circuit=bell_circuit, initial_tableau=qmap.Tableau(bell_circuit.num_qubits), coupling_map=coupling_map + ) + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): + equivalent = True + break + assert equivalent + + def test_synthesize_from_tableau(bell_circuit: QuantumCircuit) -> None: """Test that we can synthesize a circuit from an MQT Tableau.""" tableau = qmap.Tableau("['XX', 'ZZ']") @@ -417,3 +434,20 @@ def test_invalid_kwarg_to_synthesis() -> None: """Test that we raise an error if we pass an invalid kwarg to synthesis.""" with pytest.raises(ValueError, match="Invalid keyword argument"): qmap.synthesize_clifford(target_tableau=qmap.Tableau("Z"), invalid_kwarg=True) + + +def test_import_tableau_exception(bell_circuit: QuantumCircuit) -> None: + """Test that we raise an error if we pass an invalid kwarg to synthesis.""" + cliff = Clifford(bell_circuit) + qc = qmap.QuantumComputation.from_qiskit(bell_circuit) + circ, _ = qmap.optimize_clifford(circuit=qc, include_destabilizers=True) + circ2, _ = qmap.synthesize_clifford(target_tableau=cliff, include_destabilizers=True) + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ, perm) + if qcec.verify(permuted_circ, circ2).considered_equivalent(): + equivalent = True + break + assert equivalent From 51f1872c04216b118b83415d1c4bf76436e15a13 Mon Sep 17 00:00:00 2001 From: Jakob Date: Wed, 14 Aug 2024 00:08:53 +0200 Subject: [PATCH 21/36] adapt test for codecov --- test/python/test_cliffordsynthesis.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index 2930523d4..b01f9e981 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -439,9 +439,10 @@ def test_invalid_kwarg_to_synthesis() -> None: def test_import_tableau_exception(bell_circuit: QuantumCircuit) -> None: """Test that we raise an error if we pass an invalid kwarg to synthesis.""" cliff = Clifford(bell_circuit) + init_tableau = qmap.Tableau("['ZI','IZ']") qc = qmap.QuantumComputation.from_qiskit(bell_circuit) - circ, _ = qmap.optimize_clifford(circuit=qc, include_destabilizers=True) - circ2, _ = qmap.synthesize_clifford(target_tableau=cliff, include_destabilizers=True) + circ, _ = qmap.optimize_clifford(circuit=qc, initial_tableau=init_tableau, include_destabilizers=True) + circ2, _ = qmap.synthesize_clifford(target_tableau=cliff, initial_tableau=init_tableau, include_destabilizers=True) num_qubits = circ.num_qubits qubit_permutations = list(itertools.permutations(range(num_qubits))) equivalent = False From 2e53dd9d97e16c0dc10a4c171b1e630a1bfefc03 Mon Sep 17 00:00:00 2001 From: Jakob Date: Wed, 14 Aug 2024 00:43:24 +0200 Subject: [PATCH 22/36] add clifford test for codecov --- test/python/test_cliffordsynthesis.py | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index b01f9e981..9ebe05f7c 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -430,25 +430,23 @@ def test_synthesize_with_coupling_with_initial_tableau_from_tableau(bell_circuit assert equivalent -def test_invalid_kwarg_to_synthesis() -> None: - """Test that we raise an error if we pass an invalid kwarg to synthesis.""" - with pytest.raises(ValueError, match="Invalid keyword argument"): - qmap.synthesize_clifford(target_tableau=qmap.Tableau("Z"), invalid_kwarg=True) - - -def test_import_tableau_exception(bell_circuit: QuantumCircuit) -> None: - """Test that we raise an error if we pass an invalid kwarg to synthesis.""" - cliff = Clifford(bell_circuit) +def test_synthesize_with_coupling_with_initial_tableau_from_qc(bell_circuit: QuantumCircuit) -> None: + """Test that we can synthesize a circuit from an MQT Tableau.""" init_tableau = qmap.Tableau("['ZI','IZ']") - qc = qmap.QuantumComputation.from_qiskit(bell_circuit) - circ, _ = qmap.optimize_clifford(circuit=qc, initial_tableau=init_tableau, include_destabilizers=True) - circ2, _ = qmap.synthesize_clifford(target_tableau=cliff, initial_tableau=init_tableau, include_destabilizers=True) + coupling_map = [(0, 1), (1, 0)] + circ, _ = qmap.optimize_clifford(circuit=bell_circuit, initial_tableau=init_tableau, coupling_map=coupling_map) num_qubits = circ.num_qubits qubit_permutations = list(itertools.permutations(range(num_qubits))) equivalent = False for perm in qubit_permutations: permuted_circ = permute_qubits(circ, perm) - if qcec.verify(permuted_circ, circ2).considered_equivalent(): + if qcec.verify(permuted_circ, bell_circuit).considered_equivalent(): equivalent = True break assert equivalent + + +def test_invalid_kwarg_to_synthesis() -> None: + """Test that we raise an error if we pass an invalid kwarg to synthesis.""" + with pytest.raises(ValueError, match="Invalid keyword argument"): + qmap.synthesize_clifford(target_tableau=qmap.Tableau("Z"), invalid_kwarg=True) From 5e17c6cc6b774101e2defba9a31ad10b57a884c1 Mon Sep 17 00:00:00 2001 From: Jakob Date: Wed, 14 Aug 2024 00:56:33 +0200 Subject: [PATCH 23/36] remove unreachable code, Clifford has no .stabilizer/destabilizer --- src/mqt/qmap/clifford_synthesis.py | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/mqt/qmap/clifford_synthesis.py b/src/mqt/qmap/clifford_synthesis.py index 67b95bf31..d942113ff 100644 --- a/src/mqt/qmap/clifford_synthesis.py +++ b/src/mqt/qmap/clifford_synthesis.py @@ -40,15 +40,7 @@ def _import_tableau(tableau: str | Clifford | PauliList | Tableau, include_desta """Import a tableau from a string, a Clifford, a PauliList, or a Tableau.""" if isinstance(tableau, Clifford): mode = "B" if include_destabilizers else "S" - try: - return Tableau(str(_reverse_paulis(tableau.to_labels(mode=mode)))) - except AttributeError: - if include_destabilizers: - return Tableau( - str(_reverse_paulis(tableau.stabilizer.to_labels())), - str(_reverse_paulis(tableau.destabilizer.to_labels())), - ) - return Tableau(str(_reverse_paulis(tableau.stabilizer.to_labels()))) + return Tableau(str(_reverse_paulis(tableau.to_labels(mode=mode)))) elif isinstance(tableau, PauliList): return Tableau(str(_reverse_paulis(tableau.to_labels()))) elif isinstance(tableau, str): From 59531335f11d0396714557e29f1d95abf4b03a88 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Tue, 13 Aug 2024 22:57:06 +0000 Subject: [PATCH 24/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/mqt/qmap/clifford_synthesis.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mqt/qmap/clifford_synthesis.py b/src/mqt/qmap/clifford_synthesis.py index d942113ff..935c0e67d 100644 --- a/src/mqt/qmap/clifford_synthesis.py +++ b/src/mqt/qmap/clifford_synthesis.py @@ -41,9 +41,9 @@ def _import_tableau(tableau: str | Clifford | PauliList | Tableau, include_desta if isinstance(tableau, Clifford): mode = "B" if include_destabilizers else "S" return Tableau(str(_reverse_paulis(tableau.to_labels(mode=mode)))) - elif isinstance(tableau, PauliList): + if isinstance(tableau, PauliList): return Tableau(str(_reverse_paulis(tableau.to_labels()))) - elif isinstance(tableau, str): + if isinstance(tableau, str): return Tableau(tableau) return tableau From bda704dbdca40dd632bc15317e8e1a756d7239f3 Mon Sep 17 00:00:00 2001 From: Jakob Date: Wed, 14 Aug 2024 10:05:49 +0200 Subject: [PATCH 25/36] remove unnecessary coupling map test --- test/cliffordsynthesis/circuits.json | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/test/cliffordsynthesis/circuits.json b/test/cliffordsynthesis/circuits.json index 2d73fa8ab..ff06a1b13 100644 --- a/test/cliffordsynthesis/circuits.json +++ b/test/cliffordsynthesis/circuits.json @@ -44,16 +44,6 @@ "expected_minimal_two_qubit_gates": 0, "expected_minimal_gates_at_minimal_two_qubit_gates": 2 }, - { - "description": "coupling_test_iswap", - "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[2];cx q[0], q[1]; cx q[1], q[0];\n", - "expected_minimal_gates": 2, - "expected_minimal_depth": 2, - "expected_minimal_gates_at_minimal_depth": 2, - "expected_minimal_two_qubit_gates": 2, - "expected_minimal_gates_at_minimal_two_qubit_gates": 2, - "coupling_map": "{0,1};{1,0}" - }, { "description": "cx_coupling_test", "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3];h q[1]; cx q[1], q[0]; cx q[1], q[2];\n", From 7d4c5f4f41b324e7837b7ef792a6466a636a4c76 Mon Sep 17 00:00:00 2001 From: Jakob Date: Sun, 25 Aug 2024 19:55:08 +0200 Subject: [PATCH 26/36] add clifford connectivity constraint doc + code cleanup --- docs/source/Synthesis.ipynb | 50 +++++++++++++++++++ include/cliffordsynthesis/Results.hpp | 14 +++--- include/cliffordsynthesis/Tableau.hpp | 5 +- src/cliffordsynthesis/Tableau.cpp | 25 ++++------ .../encoding/TableauEncoder.cpp | 28 ++++++----- test/cliffordsynthesis/test_synthesis.cpp | 6 +-- 6 files changed, 88 insertions(+), 40 deletions(-) diff --git a/docs/source/Synthesis.ipynb b/docs/source/Synthesis.ipynb index 1012b44af..2d93fb0df 100644 --- a/docs/source/Synthesis.ipynb +++ b/docs/source/Synthesis.ipynb @@ -286,6 +286,56 @@ "qc_synth.draw(output=\"mpl\")" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Connectivity Constraints on qubits" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "\n", + "Limited qubit connectivity is implemented to handle the physical constraints of quantum hardware, where certain qubits can only interact with specific other qubits.\n", + "For this a custom coupling map can be passed to the synthesizer, which ensures that the generated circuit from the synthesis respects these connectivity constraints.\n", + "The mapping used in the synthesis is also stored in the result returned by the synthesis\n", + "\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "from qiskit import QuantumCircuit\n", + "\n", + "from mqt import qmap\n", + "\n", + "circ = QuantumCircuit(3)\n", + "circ.h(1)\n", + "circ.h(0)\n", + "circ.cx(0, 1)\n", + "circ.cx(0, 2)\n", + "circ.draw(output=\"mpl\")\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + + "circ_opt, results = qmap.optimize_clifford(circ, coupling_map={(1, 0), (0, 1), (1, 2), (2, 1)})\n", + "\n", + "print(results.mapping)\n", + "print(results.mapping_string)\n", + "circ_opt.draw(output=\"mpl\")" + ] + }, { "cell_type": "markdown", "metadata": {}, diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index 4b1f8b2c3..4d96e38d6 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -57,7 +57,7 @@ class Results { [[nodiscard]] std::string getMapping() const { std::ostringstream oss; - for (const auto& row : pvector) { + for (const auto& row : permutationVector) { for (const bool val : row) { oss << (val ? '1' : '0'); } @@ -66,7 +66,7 @@ class Results { return oss.str(); } [[nodiscard]] std::vector> getMappingVector() const { - return pvector; + return permutationVector; } void setSingleQubitGates(const std::size_t g) { singleQubitGates = g; } @@ -88,14 +88,14 @@ class Results { } void setMapping(std::vector> p) { std::ostringstream oss; - for (const auto& row : pvector) { + for (const auto& row : permutationVector) { for (const bool val : row) { oss << (val ? '1' : '0'); } oss << '\n'; } - pvals = oss.str(); - pvector = std::move(p); + permutationString = oss.str(); + permutationVector = std::move(p); } [[nodiscard]] bool sat() const { @@ -130,8 +130,8 @@ class Results { double runtime = 0.0; std::size_t solverCalls = 0U; - std::string pvals; - std::vector> pvector; + std::string permutationString; + std::vector> permutationVector; std::string resultTableau; std::string resultCircuit; }; diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index 9ddaf337e..f2b3f77be 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -163,9 +163,8 @@ class Tableau { [[nodiscard]] std::uint64_t getBVFrom(const std::size_t column) const { return getBVFrom<64>(column).to_ullong(); } - Tableau applyMapping(const std::vector>* p); - Tableau reverseMapping(const std::vector>* p); - Tableau reverseMappingOnRows(const std::vector>* p, + Tableau applyMapping(const std::vector> p); + Tableau reverseMappingOnRows(const std::vector> p, size_t nq); void gaussianEliminationGF2(); bool equivalentUpToStabilizer(const Tableau* t) const; diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 47bec252c..e7c4cac9e 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -493,17 +493,12 @@ bool Tableau::isIdentityTableau() const { return true; } -Tableau Tableau::applyMapping(const std::vector>* p) { +Tableau Tableau::applyMapping(const std::vector> p) { Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); - for (size_t i = 0; i < mappedTableau.getTableauSize(); i++) { - for (unsigned char& j : mappedTableau.tableau[i]) { - j = 0; - } - } - for (size_t i = 0; i < p->size(); i++) { - for (size_t j = 0; j < (*p)[i].size(); j++) { + for (size_t i = 0; i < p.size(); i++) { + for (size_t j = 0; j < p[i].size(); j++) { // apply mapping from column i to j if p is set - if ((*p)[i][j]) { + if (p[i][j]) { // in every row swap x entry and z entry for (size_t n = 0; n < mappedTableau.getTableauSize(); n++) { mappedTableau.tableau[n][j] = tableau[n][i]; @@ -522,14 +517,14 @@ Tableau Tableau::applyMapping(const std::vector>* p) { // number of Qubits is passed because nQubits is not set in result Tableau of // synthesis -Tableau Tableau::reverseMappingOnRows(const std::vector>* p, +Tableau Tableau::reverseMappingOnRows(const std::vector> p, const size_t nq) { auto mappedTableau = Tableau(nq, true); mappedTableau.tableau = tableau; - for (size_t i = 0; i < p->size(); i++) { - for (size_t j = 0; j < (*p)[i].size(); j++) { + for (size_t i = 0; i < p.size(); i++) { + for (size_t j = 0; j < p[i].size(); j++) { // apply mapping from row i to j if p is set - if ((*p)[i][j]) { + if (p[i][j]) { mappedTableau.tableau[i] = tableau[j]; mappedTableau.tableau[i + nq] = tableau[j + nq]; } @@ -584,7 +579,9 @@ void Tableau::gaussianEliminationGF2() { } // equivalence check for two Tableaus without destablilizers bool Tableau::equivalentUpToStabilizer(const Tableau* t) const { - assert(getTableauSize() == t->getTableauSize()); + if (getTableauSize() != t->getTableauSize()) { + return false; + } Tableau tEliminated = Tableau(nQubits, hasDestabilizers()); tEliminated.tableau = tableau; diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 486e09028..864a136ee 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -10,6 +10,7 @@ #include "cliffordsynthesis/Results.hpp" #include "cliffordsynthesis/Tableau.hpp" #include "ir/operations/OpType.hpp" +#include "logicblocks/Encodings.hpp" #include "logicblocks/Model.hpp" #include @@ -94,22 +95,22 @@ void TableauEncoder::assertMappingConstraints() const { } // assert that r vals are unchanges between 0 and 1 lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1])); + // assert that for every i and j exactly one p variable is set for (std::size_t i = 0U; i < N; ++i) { - const int32_t vr = 0; - const int32_t vr1 = 1; - LogicTerm sumRow = LogicTerm(vr); + std::vector rowVars; for (std::size_t j = 0U; j < N; ++j) { - sumRow = sumRow + vars.p[i][j]; + rowVars.emplace_back(vars.p[i][j]); } - lb->assertFormula(sumRow == LogicTerm(vr1)); - const int32_t vc = 0; - const int32_t vc1 = 1; - LogicTerm sumCol = LogicTerm(vc); + lb->assertFormula( + encodings::exactlyOneCmdr(rowVars, LogicTerm::noneTerm(), lb.get())); + + std::vector colVars; for (std::size_t j = 0U; j < N; ++j) { - sumCol = sumCol + vars.p[j][i]; + colVars.emplace_back(vars.p[j][i]); } - lb->assertFormula(sumCol == LogicTerm(vc1)); + lb->assertFormula( + encodings::exactlyOneCmdr(colVars, LogicTerm::noneTerm(), lb.get())); } // if p_i_j is set undo mapping between T-1 and T for (std::size_t i = 0U; i < N; ++i) { @@ -143,13 +144,14 @@ void TableauEncoder::extractTableauFromModel(Results& results, void TableauEncoder::extractMappingFromModel(Results& results, Model& model) const { const std::vector row(N, false); - std::vector> pvals(N, std::vector(N, false)); + std::vector> permutationValues(N, + std::vector(N, false)); for (std::size_t i = 0; i < N; ++i) { for (std::size_t j = 0; j < N; ++j) { - pvals[i][j] = model.getBoolValue(vars.p[i][j], lb.get()); + permutationValues[i][j] = model.getBoolValue(vars.p[i][j], lb.get()); } } - results.setMapping(pvals); + results.setMapping(permutationValues); } LogicTerm diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 5db78bcf7..6010e832b 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -165,7 +165,7 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Target tableau:\n" << targetTableau; const std::vector> p = results.getMappingVector(); - Tableau targetPrime = targetTableau.applyMapping(&p); + Tableau targetPrime = targetTableau.applyMapping(p); std::cout << "Target tableau with mapping:\n" << targetPrime; if (!targetPrime.hasDestabilizers()) { targetPrime.gaussianEliminationGF2(); @@ -175,9 +175,9 @@ class SynthesisTest : public ::testing::TestWithParam { std::cout << "Result tableau with mapping and Gauss:\n" << resultTableau; } else { targetPrime = - targetPrime.reverseMappingOnRows(&p, targetPrime.getQubitCount()); + targetPrime.reverseMappingOnRows(p, targetPrime.getQubitCount()); resultTableau = - resultTableau.reverseMappingOnRows(&p, targetPrime.getQubitCount()); + resultTableau.reverseMappingOnRows(p, targetPrime.getQubitCount()); std::cout << "Result tableau with destab mapping reversed:\n" << resultTableau; std::cout << "Target tableau with destab mapping reversed:\n" From b7f67f18e1a99d9095969bfaede68c35dc933bdb Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sun, 25 Aug 2024 17:55:36 +0000 Subject: [PATCH 27/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/source/Synthesis.ipynb | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/source/Synthesis.ipynb b/docs/source/Synthesis.ipynb index 2d93fb0df..3f54c39ed 100644 --- a/docs/source/Synthesis.ipynb +++ b/docs/source/Synthesis.ipynb @@ -319,7 +319,7 @@ "circ.h(0)\n", "circ.cx(0, 1)\n", "circ.cx(0, 2)\n", - "circ.draw(output=\"mpl\")\n" + "circ.draw(output=\"mpl\")" ] }, { @@ -328,13 +328,12 @@ "metadata": {}, "outputs": [], "source": [ - "circ_opt, results = qmap.optimize_clifford(circ, coupling_map={(1, 0), (0, 1), (1, 2), (2, 1)})\n", "\n", "print(results.mapping)\n", - "print(results.mapping_string)\n", + "print(results.mapping_string)\n", "circ_opt.draw(output=\"mpl\")" - ] + ] }, { "cell_type": "markdown", From 120ac01cb84958cd91ff533c4afe91f63db42927 Mon Sep 17 00:00:00 2001 From: Jakob Date: Mon, 26 Aug 2024 11:20:30 +0200 Subject: [PATCH 28/36] adapt python heuristic test for connectivity constraints + cleanup --- include/cliffordsynthesis/Tableau.hpp | 4 ++-- src/cliffordsynthesis/Tableau.cpp | 4 ++-- test/python/test_cliffordsynthesis.py | 11 ++++++++++- 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index f2b3f77be..fcff1d96a 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -163,8 +163,8 @@ class Tableau { [[nodiscard]] std::uint64_t getBVFrom(const std::size_t column) const { return getBVFrom<64>(column).to_ullong(); } - Tableau applyMapping(const std::vector> p); - Tableau reverseMappingOnRows(const std::vector> p, + Tableau applyMapping(const std::vector>& p); + Tableau reverseMappingOnRows(const std::vector>& p, size_t nq); void gaussianEliminationGF2(); bool equivalentUpToStabilizer(const Tableau* t) const; diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index e7c4cac9e..b8c55bd1c 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -493,7 +493,7 @@ bool Tableau::isIdentityTableau() const { return true; } -Tableau Tableau::applyMapping(const std::vector> p) { +Tableau Tableau::applyMapping(const std::vector>& p) { Tableau mappedTableau = Tableau(nQubits, hasDestabilizers()); for (size_t i = 0; i < p.size(); i++) { for (size_t j = 0; j < p[i].size(); j++) { @@ -517,7 +517,7 @@ Tableau Tableau::applyMapping(const std::vector> p) { // number of Qubits is passed because nQubits is not set in result Tableau of // synthesis -Tableau Tableau::reverseMappingOnRows(const std::vector> p, +Tableau Tableau::reverseMappingOnRows(const std::vector>& p, const size_t nq) { auto mappedTableau = Tableau(nq, true); mappedTableau.tableau = tableau; diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index 9ebe05f7c..7ce2a9eea 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -161,7 +161,16 @@ def test_heuristic(test_config: Configuration) -> None: circuit=test_config.initial_circuit, heuristic=False, target_metric="depth", include_destabilizers=True ) assert circ.depth() >= circ_opt.depth() - assert Clifford(circ) == Clifford(circ_opt) + + num_qubits = circ.num_qubits + qubit_permutations = list(itertools.permutations(range(num_qubits))) + equivalent = False + for perm in qubit_permutations: + permuted_circ = permute_qubits(circ_opt, perm) + if Clifford(permuted_circ) == Clifford(circ): + equivalent = True + break + assert equivalent print("\n", circ) From 95e4e8dca070daa41fa51571ef395a3911166715 Mon Sep 17 00:00:00 2001 From: Jakob Date: Mon, 26 Aug 2024 11:26:55 +0200 Subject: [PATCH 29/36] rename gaussianEliminationGF2() to rref() --- include/cliffordsynthesis/Tableau.hpp | 2 +- src/cliffordsynthesis/Tableau.cpp | 6 +++--- test/cliffordsynthesis/test_synthesis.cpp | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index fcff1d96a..226d59e1d 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -166,7 +166,7 @@ class Tableau { Tableau applyMapping(const std::vector>& p); Tableau reverseMappingOnRows(const std::vector>& p, size_t nq); - void gaussianEliminationGF2(); + void rref(); bool equivalentUpToStabilizer(const Tableau* t) const; }; } // namespace cs diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index b8c55bd1c..886155bea 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -534,7 +534,7 @@ Tableau Tableau::reverseMappingOnRows(const std::vector>& p, } // in place Gauss Elimination -void Tableau::gaussianEliminationGF2() { +void Tableau::rref() { const size_t rows = tableau.size(); const size_t cols = tableau[0].size(); if (rows == 1) { @@ -585,11 +585,11 @@ bool Tableau::equivalentUpToStabilizer(const Tableau* t) const { Tableau tEliminated = Tableau(nQubits, hasDestabilizers()); tEliminated.tableau = tableau; - tEliminated.gaussianEliminationGF2(); + tEliminated.rref(); Tableau t2Eliminated = Tableau(nQubits, hasDestabilizers()); t2Eliminated.tableau = t->getTableau(); - t2Eliminated.gaussianEliminationGF2(); + t2Eliminated.rref(); return tEliminated == t2Eliminated; } } // namespace cs diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 6010e832b..01bdaf4a9 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -168,8 +168,8 @@ class SynthesisTest : public ::testing::TestWithParam { Tableau targetPrime = targetTableau.applyMapping(p); std::cout << "Target tableau with mapping:\n" << targetPrime; if (!targetPrime.hasDestabilizers()) { - targetPrime.gaussianEliminationGF2(); - resultTableau.gaussianEliminationGF2(); + targetPrime.rref(); + resultTableau.rref(); assert(targetPrime.equivalentUpToStabilizer(&resultTableau)); std::cout << "Target tableau with mapping and Gauss:\n" << targetPrime; std::cout << "Result tableau with mapping and Gauss:\n" << resultTableau; @@ -197,7 +197,7 @@ class SynthesisTest : public ::testing::TestWithParam { } std::cout << "Circuit Tableau :\n" << circuitTableau; if (!circuitTableau.hasDestabilizers()) { - circuitTableau.gaussianEliminationGF2(); + circuitTableau.rref(); std::cout << "Circuit Tableau with Gauss" << circuitTableau; } EXPECT_EQ(resultTableau, circuitTableau); From 0a476b2252f8c2716ed44634d9123f67d5fb00ab Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 10 Sep 2024 09:17:02 +0200 Subject: [PATCH 30/36] fix deprecation warning in test_cliffordsynthesis.py --- test/python/test_cliffordsynthesis.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py index 7ce2a9eea..ed45838a3 100644 --- a/test/python/test_cliffordsynthesis.py +++ b/test/python/test_cliffordsynthesis.py @@ -36,7 +36,10 @@ def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int, ...]) -> Qua permuted_circ = QuantumCircuit(circuit.num_qubits) qubit_map = {qubit: i for i, qubit in enumerate(circuit.qubits)} - for gate, qubits, clbits in circuit.data: + for d in circuit.data: + gate = d.operation + qubits = d.qubits + clbits = d.clbits new_qubits = [circuit.qubits[permutation[qubit_map[q]]] for q in qubits] permuted_circ.append(gate, new_qubits, clbits) From 5253d8c6b34a12f40a61375fcd69bd7f38bc32e9 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Tue, 10 Sep 2024 09:40:33 +0000 Subject: [PATCH 31/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- include/cliffordsynthesis/Results.hpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index bb04e0f3e..57b7ef9ec 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -66,17 +66,17 @@ class Results { void setResultCircuit(qc::QuantumComputation& qc); void setResultTableau(const Tableau& tableau); void setMapping(std::vector> p) { - std::ostringstream oss; - for (const auto& row : permutationVector) { - for (const bool val : row) { - oss << (val ? '1' : '0'); + std::ostringstream oss; + for (const auto& row : permutationVector) { + for (const bool val : row) { + oss << (val ? '1' : '0'); + } + oss << '\n'; } - oss << '\n'; + permutationString = oss.str(); + permutationVector = std::move(p); } - permutationString = oss.str(); - permutationVector = std::move(p); -} - + [[nodiscard]] bool sat() const { return getSolverResult() == logicbase::Result::SAT; } From 81dd844dc9fe1935a4ca15a7e49a425800fcd5b4 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 10 Sep 2024 11:46:06 +0200 Subject: [PATCH 32/36] fix include path in test_synthesis --- test/cliffordsynthesis/test_synthesis.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index ddcc882fc..5b7878c91 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -10,7 +10,7 @@ #include "cliffordsynthesis/TargetMetric.hpp" #include "ir/QuantumComputation.hpp" #include "ir/operations/Control.hpp" -#include "utils.hpp" +#include "sc/utils.hpp" #include #include From d8948c9cf396af06223d69e95f2a7ce84685d375 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 10 Sep 2024 11:59:02 +0200 Subject: [PATCH 33/36] fix include --- include/cliffordsynthesis/Results.hpp | 1 + 1 file changed, 1 insertion(+) diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index 57b7ef9ec..409f8167f 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -16,6 +16,7 @@ #include #include #include +#include namespace cs { class Results { From c78224ddc12cf58e75ab4b89ab12beadd60e2e78 Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 10 Sep 2024 12:28:52 +0200 Subject: [PATCH 34/36] add getFullyConnectedMap to CliffordSynthesizer --- include/cliffordsynthesis/CliffordSynthesizer.hpp | 11 +++++++++++ include/cliffordsynthesis/Results.hpp | 2 +- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 088161d65..55e2e299e 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -187,6 +187,17 @@ class CliffordSynthesizer { static void updateResults(const Configuration& config, const Results& newResults, Results& currentResults); void removeRedundantGates(); + + static CouplingMap getFullyConnectedMap(const std::uint16_t nQubits) { + CouplingMap result{}; + for (std::uint16_t q = 0; q < nQubits; ++q) { + for (std::uint16_t p = q + 1; p < nQubits; ++p) { + result.emplace(q, p); + result.emplace(p, q); + } + } + return result; + } }; } // namespace cs diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp index 409f8167f..3dcfbee12 100644 --- a/include/cliffordsynthesis/Results.hpp +++ b/include/cliffordsynthesis/Results.hpp @@ -13,10 +13,10 @@ #include #include #include +#include #include #include #include -#include namespace cs { class Results { From af662c3eedb21aa3714ee01b1ee229c550f84bcc Mon Sep 17 00:00:00 2001 From: Jakob Date: Tue, 10 Sep 2024 13:36:10 +0200 Subject: [PATCH 35/36] add path of utils.hpp to CMakeLists.txt --- include/cliffordsynthesis/CliffordSynthesizer.hpp | 10 ---------- src/cliffordsynthesis/CMakeLists.txt | 3 ++- src/cliffordsynthesis/CliffordSynthesizer.cpp | 4 ++++ 3 files changed, 6 insertions(+), 11 deletions(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 55e2e299e..44fb1fd1a 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -188,16 +188,6 @@ class CliffordSynthesizer { const Results& newResults, Results& currentResults); void removeRedundantGates(); - static CouplingMap getFullyConnectedMap(const std::uint16_t nQubits) { - CouplingMap result{}; - for (std::uint16_t q = 0; q < nQubits; ++q) { - for (std::uint16_t p = q + 1; p < nQubits; ++p) { - result.emplace(q, p); - result.emplace(p, q); - } - } - return result; - } }; } // namespace cs diff --git a/src/cliffordsynthesis/CMakeLists.txt b/src/cliffordsynthesis/CMakeLists.txt index 832ec3f11..977e7303d 100644 --- a/src/cliffordsynthesis/CMakeLists.txt +++ b/src/cliffordsynthesis/CMakeLists.txt @@ -10,11 +10,12 @@ if(NOT TARGET ${MQT_QMAP_CLIFFORD_SYNTHESIS_TARGET_NAME}) file(GLOB_RECURSE CLIFFORD_SYNTHESIS_HEADERS ${MQT_QMAP_INCLUDE_BUILD_DIR}/cliffordsynthesis/*.hpp) file(GLOB_RECURSE CLIFFORD_SYNTHESIS_SOURCES **.cpp) + list(APPEND CLIFFORD_SYNTHESIS_SOURCES "${CMAKE_SOURCE_DIR}/src/sc/utils.cpp") # add CliffordSynthesis Package library add_library(${MQT_QMAP_CLIFFORD_SYNTHESIS_TARGET_NAME} ${CLIFFORD_SYNTHESIS_HEADERS} ${CLIFFORD_SYNTHESIS_SOURCES}) - + message(${CLIFFORD_SYNTHESIS_SOURCES}) # set include directories target_include_directories(${MQT_QMAP_CLIFFORD_SYNTHESIS_TARGET_NAME} PUBLIC $) diff --git a/src/cliffordsynthesis/CliffordSynthesizer.cpp b/src/cliffordsynthesis/CliffordSynthesizer.cpp index e9e443da0..e78603e19 100644 --- a/src/cliffordsynthesis/CliffordSynthesizer.cpp +++ b/src/cliffordsynthesis/CliffordSynthesizer.cpp @@ -87,6 +87,7 @@ void CliffordSynthesizer::synthesize(const Configuration& config) { const auto [lowerBin, upperBin] = determineUpperBound(encoderConfig); lower = lowerBin; upper = upperBin; + PLOG_INFO << "Upper bound " << upperBin; // if the upper bound is 0, the solution does not require any gates and the // synthesis is done. @@ -97,7 +98,10 @@ void CliffordSynthesizer::synthesize(const Configuration& config) { } // Otherwise, the determined upper bound is used as an initial timestep // limit. + encoderConfig.timestepLimit = upper; + PLOG_INFO << "Upper bound " << encoderConfig.timestepLimit; + // Once a valid upper bound is found, the SAT problem is solved again with // the objective function encoded. switch (config.target) { From e189af99deaa8771281a17325edacd3a753f0a9c Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Tue, 10 Sep 2024 11:40:49 +0000 Subject: [PATCH 36/36] =?UTF-8?q?=F0=9F=8E=A8=20pre-commit=20fixes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- include/cliffordsynthesis/CliffordSynthesizer.hpp | 1 - 1 file changed, 1 deletion(-) diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp index 44fb1fd1a..088161d65 100644 --- a/include/cliffordsynthesis/CliffordSynthesizer.hpp +++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp @@ -187,7 +187,6 @@ class CliffordSynthesizer { static void updateResults(const Configuration& config, const Results& newResults, Results& currentResults); void removeRedundantGates(); - }; } // namespace cs