diff --git a/extern/LogicBlocks b/extern/LogicBlocks index 67c3bca43..4bb726be7 160000 --- a/extern/LogicBlocks +++ b/extern/LogicBlocks @@ -1 +1 @@ -Subproject commit 67c3bca43b378a9ea0d3a32433c92719903b29bf +Subproject commit 4bb726be710e39c5571a0eb7874fd8e897be09d6 diff --git a/extern/mqt-core b/extern/mqt-core index 8b6e1bf0a..b08aec75c 160000 --- a/extern/mqt-core +++ b/extern/mqt-core @@ -1 +1 @@ -Subproject commit 8b6e1bf0af908c93ccdfbf84623f405163bd0154 +Subproject commit b08aec75c28fe6fc558244d0ff4bd280df1d4522 diff --git a/include/cliffordsynthesis/Configuration.hpp b/include/cliffordsynthesis/Configuration.hpp index 47bdbd829..4e548d535 100644 --- a/include/cliffordsynthesis/Configuration.hpp +++ b/include/cliffordsynthesis/Configuration.hpp @@ -5,13 +5,16 @@ #pragma once +#include "GateSet.hpp" #include "TargetMetric.hpp" #include "nlohmann/json.hpp" +#include "operations/OpType.hpp" #include #include #include #include +#include namespace cs { @@ -48,6 +51,12 @@ struct Configuration { std::size_t splitSize = 5U; std::size_t nThreadsHeuristic = std::thread::hardware_concurrency(); + GateSet gateSet = {qc::OpType::None, qc::OpType::S, qc::OpType::Sdg, + qc::OpType::H, qc::OpType::X, qc::OpType::Y, + qc::OpType::Z}; + + bool delayPaulis = false; + [[nodiscard]] nlohmann::json json() const { nlohmann::json j; j["initial_timestep_limit"] = initialTimestepLimit; @@ -66,6 +75,8 @@ struct Configuration { j["heuristic"] = heuristic; j["split_size"] = splitSize; j["n_threads_heuristic"] = nThreadsHeuristic; + j["gate_set"] = gateSet.toString(); + j["delay_paulis"] = delayPaulis; if (!solverParameters.empty()) { nlohmann::json solverParametersJson; for (const auto& entry : solverParameters) { diff --git a/include/cliffordsynthesis/GateSet.hpp b/include/cliffordsynthesis/GateSet.hpp new file mode 100644 index 000000000..e0aed6611 --- /dev/null +++ b/include/cliffordsynthesis/GateSet.hpp @@ -0,0 +1,237 @@ +// +// This file is part of the MQT QMAP library released under the MIT license. +// See README.md or go to https://github.com/cda-tum/qmap for more information. +// + +#pragma once + +#include "operations/OpType.hpp" + +#include +#include +#include +#include + +namespace cs { +class GateSet { + static constexpr std::array SINGLE_QUBIT_CLIFFORDS = { + qc::OpType::I, qc::OpType::H, qc::OpType::X, qc::OpType::Y, + qc::OpType::Z, qc::OpType::S, qc::OpType::Sdg, qc::OpType::SX, + qc::OpType::SXdg, qc::OpType::None}; + + using iterator = typename std::vector::iterator; + using const_iterator = typename std::vector::const_iterator; + +private: + // Check if None is already contained and if not, append it + void appendNone() { + if (!containsGate(qc::OpType::None)) { + gates.push_back(qc::OpType::None); + } + } + std::vector gates{}; + +public: + GateSet() { appendNone(); }; + + explicit GateSet(std::vector gateSet) + : gates(std::move(gateSet)) { + appendNone(); + }; + + GateSet(const GateSet& gateSet) : gates(gateSet.gates) { appendNone(); }; + + GateSet(GateSet&& gateSet) noexcept : gates(std::move(gateSet.gates)) { + appendNone(); + }; + + GateSet(std::initializer_list gateSet) : gates(gateSet) { + appendNone(); + } + + GateSet& operator=(const GateSet& other) { + gates = other.gates; + appendNone(); + return *this; + } + + GateSet& operator=(GateSet&& other) noexcept { + gates = std::move(other.gates); + appendNone(); + return *this; + } + + GateSet& operator=(std::initializer_list other) { + gates = other; + appendNone(); + return *this; + } + + void removeGate(const qc::OpType& gate) { + gates.erase(std::remove(gates.begin(), gates.end(), gate), gates.end()); + } + + void removePaulis() { + gates.erase(std::remove_if(gates.begin(), gates.end(), + [](qc::OpType gate) { + return gate == qc::OpType::X || + gate == qc::OpType::Y || + gate == qc::OpType::Z || + gate == qc::OpType::None; + }), + gates.end()); + } + [[nodiscard]] bool containsGate(qc::OpType gate) const { + for (const auto& g : // NOLINT(readability-use-anyofallof) + gates) { + if (g == gate) { + return true; + } + } + return false; + } + [[nodiscard]] bool containsX() const { return containsGate(qc::OpType::X); } + [[nodiscard]] bool containsY() const { return containsGate(qc::OpType::Y); } + [[nodiscard]] bool containsZ() const { return containsGate(qc::OpType::Z); } + [[nodiscard]] bool containsH() const { return containsGate(qc::OpType::H); } + [[nodiscard]] bool containsS() const { return containsGate(qc::OpType::S); } + [[nodiscard]] bool containsSdg() const { + return containsGate(qc::OpType::Sdg); + } + [[nodiscard]] bool containsSX() const { return containsGate(qc::OpType::SX); } + [[nodiscard]] bool containsSXdg() const { + return containsGate(qc::OpType::SXdg); + } + [[nodiscard]] std::size_t gateToIndex(const qc::OpType type) const { + for (std::size_t i = 0; i < gates.size(); ++i) { + if (gates.at(i) == type) { + return i; + } + } + return 0; + } + + [[nodiscard]] GateSet paulis() const { + std::vector result; + for (const auto& g : gates) { + if (g == qc::OpType::X || g == qc::OpType::Y || g == qc::OpType::Z || + g == qc::OpType::I) { + result.push_back(g); + } + } + return GateSet(result); + } + + [[nodiscard]] bool isValidGateSet() const { + return std::all_of(gates.begin(), gates.end(), [](const auto& g) { + return std::find(SINGLE_QUBIT_CLIFFORDS.begin(), + SINGLE_QUBIT_CLIFFORDS.end(), + g) != SINGLE_QUBIT_CLIFFORDS.end(); + }); + } + + // Any single-qubit Clifford gate can be obtained from a product of PI/2 + // rotations around different axes. + [[nodiscard]] bool isComplete() const { + if (containsS() || containsSdg()) { + if (containsSX() || containsSXdg() || containsH()) { + return true; + } + } + + if (containsSX() || containsSXdg()) { + if (containsH()) { + return true; + } + } + return false; + } + + [[nodiscard]] std::string toString() const { + std::string result = "{"; + for (const auto& g : gates) { + result += qc::toString(g) + ", "; + } + result += "}"; + return result; + } + + const qc::OpType& operator[](std::size_t index) const { return gates[index]; } + /** + * Pass-Through + */ + + // Iterators (pass-through) + auto begin() noexcept { return gates.begin(); } + [[nodiscard]] auto begin() const noexcept { return gates.begin(); } + [[nodiscard]] auto cbegin() const noexcept { return gates.cbegin(); } + auto end() noexcept { return gates.end(); } + [[nodiscard]] auto end() const noexcept { return gates.end(); } + [[nodiscard]] auto cend() const noexcept { return gates.cend(); } + auto rbegin() noexcept { return gates.rbegin(); } + [[nodiscard]] auto rbegin() const noexcept { return gates.rbegin(); } + [[nodiscard]] auto crbegin() const noexcept { return gates.crbegin(); } + auto rend() noexcept { return gates.rend(); } + [[nodiscard]] auto rend() const noexcept { return gates.rend(); } + [[nodiscard]] auto crend() const noexcept { return gates.crend(); } + + // Capacity (pass-through) + [[nodiscard]] bool empty() const noexcept { return gates.empty(); } + [[nodiscard]] std::size_t size() const noexcept { return gates.size(); } + // NOLINTNEXTLINE(readability-identifier-naming) + [[nodiscard]] std::size_t max_size() const noexcept { + return gates.max_size(); + } + [[nodiscard]] std::size_t capacity() const noexcept { + return gates.capacity(); + } + + void reserve(const std::size_t newCap) { gates.reserve(newCap); } + // NOLINTNEXTLINE(readability-identifier-naming) + void shrink_to_fit() { gates.shrink_to_fit(); } + + // Modifiers (pass-through) + void clear() noexcept { gates.clear(); } + // NOLINTNEXTLINE(readability-identifier-naming) + void pop_back() { return gates.pop_back(); } + void resize(std::size_t count) { gates.resize(count); } + iterator erase(const_iterator pos) { return gates.erase(pos); } + iterator erase(const_iterator first, const_iterator last) { + return gates.erase(first, last); + } + + // NOLINTNEXTLINE(readability-identifier-naming) + void push_back(const qc::OpType& gate) { + if (!containsGate(gate)) { + gates.push_back(gate); + } + } + + // NOLINTNEXTLINE(readability-identifier-naming) + template void emplace_back(Args&&... args) { + gates.emplace_back(args...); + } + + // NOLINTNEXTLINE(readability-identifier-naming) + void emplace_back(qc::OpType& gate) { + if (!containsGate(gate)) { + gates.emplace_back(gate); + } + } + + // NOLINTNEXTLINE(readability-identifier-naming) + void emplace_back(qc::OpType&& gate) { + if (!containsGate(gate)) { + gates.emplace_back(gate); + } + } + + [[nodiscard]] const auto& at(const std::size_t i) const { + return gates.at(i); + } + [[nodiscard]] auto& at(const std::size_t i) { return gates.at(i); } + [[nodiscard]] const auto& front() const { return gates.front(); } + [[nodiscard]] const auto& back() const { return gates.back(); } +}; + +} // namespace cs diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp index 73ea850af..5b2d22b28 100644 --- a/include/cliffordsynthesis/Tableau.hpp +++ b/include/cliffordsynthesis/Tableau.hpp @@ -6,6 +6,7 @@ #pragma once #include "QuantumComputation.hpp" +#include "operations/OpType.hpp" #include "utils/logging.hpp" #include @@ -50,7 +51,7 @@ class Tableau { nQubits = tableau.size() / 2U; } - [[nodiscard]] RowType operator[](const std::size_t index) { + [[nodiscard]] RowType& operator[](const std::size_t index) { return tableau[index]; } [[nodiscard]] RowType operator[](const std::size_t index) const { @@ -98,6 +99,7 @@ class Tableau { } void applyGate(const qc::Operation* gate); + void applySingleQGate(const qc::OpType& gate, std::size_t target); void applyH(std::size_t target); void applyS(std::size_t target); void applySdag(std::size_t target); @@ -121,6 +123,19 @@ class Tableau { return !(lhs == rhs); } + [[nodiscard]] bool equalUpToPhase(const Tableau& rhs) const { + const auto& lhsTab = this->getTableau(); + const auto& rhsTab = rhs.getTableau(); + for (std::size_t i = 0; i < lhsTab.size(); ++i) { + for (std::size_t j = 0; j < lhsTab[i].size() - 1; ++j) { + if (lhsTab[i][j] != rhsTab[i][j]) { + return false; + } + } + } + return true; + } + [[nodiscard]] bool isIdentityTableau() const; void createDiagonalTableau(std::size_t nQ, bool includeDestabilizers = false); diff --git a/include/cliffordsynthesis/Utils.hpp b/include/cliffordsynthesis/Utils.hpp new file mode 100644 index 000000000..44621306f --- /dev/null +++ b/include/cliffordsynthesis/Utils.hpp @@ -0,0 +1,26 @@ +// +// This file is part of the MQT QMAP library released under the MIT license. +// See README.md or go to https://github.com/cda-tum/qmap for more information. +// + +#pragma once + +#include "cliffordsynthesis/GateSet.hpp" +#include "operations/OpType.hpp" + +namespace cs { + +const GateSet PAULIS{ + qc::OpType::None, + qc::OpType::X, + qc::OpType::Y, + qc::OpType::Z, +}; + +inline bool isPauli(const qc::OpType& gate) { + return PAULIS.containsGate(gate); +} + +qc::OpType multiplyPaulis(const GateSet& paulis); + +} // namespace cs diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp index d22b4182e..0055b691c 100644 --- a/include/cliffordsynthesis/encoding/GateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp @@ -5,13 +5,21 @@ #pragma once +#include "Definitions.hpp" #include "LogicBlock/LogicBlock.hpp" +#include "LogicTerm/LogicTerm.hpp" +#include "QuantumComputation.hpp" +#include "cliffordsynthesis/GateSet.hpp" #include "cliffordsynthesis/Results.hpp" +#include "cliffordsynthesis/Tableau.hpp" #include "cliffordsynthesis/encoding/TableauEncoder.hpp" #include "operations/OpType.hpp" +#include #include #include +#include +#include namespace cs::encoding { @@ -20,9 +28,20 @@ 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) + std::shared_ptr logicBlock, + GateSet singleQGates, Tableau initialTableau, + bool ignorePhase = false) : N(nQubits), S(tableauSize), T(timestepLimit), tvars(tableauVars), - lb(std::move(logicBlock)) {} + lb(std::move(logicBlock)), singleQubitGates(std::move(singleQGates)), + init(std::move(initialTableau)), ignoreRChanges(ignorePhase) { + if (!singleQubitGates.isValidGateSet()) { + throw qc::QFRException("Invalid gate set"); + } + if (!singleQubitGates.isComplete()) { + std::cerr << "Warning: The gate set " << singleQubitGates.toString() + << "is not complete. The synthesis might fail." << std::endl; + } + } virtual ~GateEncoder() = default; struct Variables { @@ -52,54 +71,11 @@ class GateEncoder { virtual void encodeSymmetryBreakingConstraints(); // extracting the circuit - void extractCircuitFromModel(Results& res, logicbase::Model& model); + qc::QuantumComputation extractCircuitFromModel(Results& res, + logicbase::Model& model); [[nodiscard]] auto* getVariables() { return &vars; } - static constexpr std::array SINGLE_QUBIT_GATES = { - qc::OpType::None, qc::OpType::X, qc::OpType::Y, qc::OpType::Z, - qc::OpType::H, qc::OpType::S, qc::OpType::Sdg}; - - [[nodiscard]] static constexpr std::size_t - gateToIndex(const qc::OpType type) { - for (std::size_t i = 0; i < SINGLE_QUBIT_GATES.size(); ++i) { - if (SINGLE_QUBIT_GATES.at(i) == type) { - return i; - } - } - return 0; - } - - template - [[nodiscard]] static constexpr bool containsGate() { - for (const auto& g : // NOLINT(readability-use-anyofallof) - SINGLE_QUBIT_GATES) { - if (g == Gate) { - return true; - } - } - return false; - } - - [[nodiscard]] static constexpr bool containsX() { - return containsGate(); - } - [[nodiscard]] static constexpr bool containsY() { - return containsGate(); - } - [[nodiscard]] static constexpr bool containsZ() { - return containsGate(); - } - [[nodiscard]] static constexpr bool containsH() { - return containsGate(); - } - [[nodiscard]] static constexpr bool containsS() { - return containsGate(); - } - [[nodiscard]] static constexpr bool containsSdag() { - return containsGate(); - } - protected: // number of qubits N std::size_t N{}; // NOLINT (readability-identifier-naming) @@ -117,19 +93,27 @@ class GateEncoder { // the logic block to use std::shared_ptr lb{}; + // the gates that are used + GateSet singleQubitGates; + + Tableau init{}; + bool ignoreRChanges{false}; + using TransformationFamily = std::pair>; using GateToTransformation = std::function; void assertExactlyOne(const logicbase::LogicVector& variables) const; + [[nodiscard]] logicbase::LogicTerm + createExactlyOne(const logicbase::LogicVector& variables) const; virtual void assertConsistency() const = 0; - virtual void assertGateConstraints() = 0; - virtual void assertSingleQubitGateConstraints(std::size_t pos) = 0; - virtual void assertTwoQubitGateConstraints(std::size_t pos) = 0; - [[nodiscard]] static std::vector + virtual void assertGateConstraints() = 0; + void assertSingleQubitGateConstraints(std::size_t pos); + void assertTwoQubitGateConstraints(std::size_t pos); + [[nodiscard]] std::vector collectGateTransformations(std::size_t pos, std::size_t qubit, const GateToTransformation& gateToTransformation); void assertGatesImplyTransform( @@ -141,14 +125,21 @@ class GateEncoder { [[nodiscard]] virtual logicbase::LogicTerm createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl, std::size_t trgt) = 0; + [[nodiscard]] virtual logicbase::LogicTerm + createTwoQubitRConstraint(std::size_t pos, std::size_t ctrl, + std::size_t trgt) = 0; void extractSingleQubitGatesFromModel(std::size_t pos, logicbase::Model& model, qc::QuantumComputation& qc, - std::size_t& nSingleQubitGates); + std::size_t& nSingleQubitGates, + std::vector& hasGate, + Tableau& intermediateTableau); void extractTwoQubitGatesFromModel(std::size_t pos, logicbase::Model& model, qc::QuantumComputation& qc, - std::size_t& nTwoQubitGates); + std::size_t& nTwoQubitGates, + std::vector& hasGate, + Tableau& intermediateTableau); virtual void assertSingleQubitGateSymmetryBreakingConstraints(std::size_t pos); diff --git a/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp b/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp index a1343c5b3..f4291cb04 100644 --- a/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp @@ -5,6 +5,7 @@ #pragma once +#include "LogicTerm/LogicTerm.hpp" #include "cliffordsynthesis/encoding/GateEncoder.hpp" #include @@ -23,11 +24,12 @@ class MultiGateEncoder : public GateEncoder { void assertConsistency() const override; void assertGateConstraints() override; void assertRConstraints(std::size_t pos, std::size_t qubit) override; - void assertSingleQubitGateConstraints(std::size_t pos) override; - void assertTwoQubitGateConstraints(std::size_t pos) override; [[nodiscard]] logicbase::LogicTerm createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl, std::size_t trgt) override; + [[nodiscard]] logicbase::LogicTerm + createTwoQubitRConstraint(std::size_t pos, std::size_t ctrl, + std::size_t trgt) override; void assertSingleQubitGateOrderConstraints(std::size_t pos, std::size_t qubit) override; diff --git a/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp b/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp index 5c8eab141..5f7c9448e 100644 --- a/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp +++ b/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp @@ -8,10 +8,12 @@ #include "cliffordsynthesis/TargetMetric.hpp" #include "cliffordsynthesis/encoding/GateEncoder.hpp" #include "cliffordsynthesis/encoding/TableauEncoder.hpp" +#include "operations/OpType.hpp" #include #include #include +#include namespace cs::encoding { @@ -19,8 +21,10 @@ class ObjectiveEncoder { public: ObjectiveEncoder(const std::size_t nQubits, const std::size_t timestepLimit, GateEncoder::Variables* vars, - std::shared_ptr logicBlock) - : N(nQubits), T(timestepLimit), gvars(vars), lb(std::move(logicBlock)) {} + std::shared_ptr logicBlock, + GateSet singleQGates) + : N(nQubits), T(timestepLimit), gvars(vars), lb(std::move(logicBlock)), + singleQubitGates(std::move(singleQGates)) {} template void limitGateCount(const std::size_t maxGateCount, Op op, @@ -51,19 +55,23 @@ class ObjectiveEncoder { // the logic block std::shared_ptr lb; + // the set of single-qubit gates + GateSet singleQubitGates; + [[nodiscard]] logicbase::LogicTerm collectGateCount(bool includeSingleQubitGates = true) const; template void collectSingleQubitGateTerms(std::size_t pos, logicbase::LogicTerm& terms, Op op) const { - const auto& singleQubitGates = gvars->gS[pos]; + const auto& singleQubitGateVars = gvars->gS[pos]; for (std::size_t q = 0U; q < N; ++q) { - for (const auto gate : GateEncoder::SINGLE_QUBIT_GATES) { + for (const auto gate : singleQubitGates) { if (gate == qc::OpType::None) { continue; } - terms = op(terms, singleQubitGates[GateEncoder::gateToIndex(gate)][q]); + terms = op(terms, + singleQubitGateVars[singleQubitGates.gateToIndex(gate)][q]); } } } diff --git a/include/cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp b/include/cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp new file mode 100644 index 000000000..e791c1328 --- /dev/null +++ b/include/cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp @@ -0,0 +1,62 @@ +// +// This file is part of the MQT QMAP library released under the MIT license. +// See README.md or go to https://github.com/cda-tum/qmap for more information. +// + +#pragma once + +#include "LogicBlock/LogicBlock.hpp" +#include "LogicTerm/Logic.hpp" +#include "LogicUtil/util_logicblock.hpp" +#include "cliffordsynthesis/Tableau.hpp" +#include "operations/OpType.hpp" + +#include +#include +#include + +namespace cs::encoding { +using namespace logicbase; +class PhaseCorrectionEncoder { +public: + PhaseCorrectionEncoder(const std::size_t nQubits, + const std::size_t tableauSize, + Tableau uncorrectedTableau, Tableau targetTableau) + : N{nQubits}, S{tableauSize}, uncorrected(std::move(uncorrectedTableau)), + target(std::move(targetTableau)), paulis{N} { + bool success = true; + lb = logicutil::getZ3LogicBlock(success, true); + if (!success) { + FATAL() << "Could not initialize solver engine."; + } + } + + std::vector phaseCorrection(); + +protected: + // number of qubits N + std::size_t N{}; // NOLINT (readability-identifier-naming) + // number of rows in the tableau S + std::size_t S{}; // NOLINT (readability-identifier-naming) + // the logic block to use + std::shared_ptr lb{}; + Tableau uncorrected{}; + Tableau target{}; + + logicbase::LogicMatrix paulis{}; // order: I, X, Y, Z + LogicVector initialPhase{}; + LogicVector targetPhase{}; + + LogicMatrix xorHelpers{}; + + void splitXorR(const LogicVector& changes); + + [[nodiscard]] LogicVector vectorFromBitset(const std::bitset<64>& bs) const; + + void encodePauliConstraints(); + + void createVariables(); + + std::vector extractResult(); +}; +} // namespace cs::encoding diff --git a/include/cliffordsynthesis/encoding/SATEncoder.hpp b/include/cliffordsynthesis/encoding/SATEncoder.hpp index e017fa69a..70800aa73 100644 --- a/include/cliffordsynthesis/encoding/SATEncoder.hpp +++ b/include/cliffordsynthesis/encoding/SATEncoder.hpp @@ -57,6 +57,10 @@ class SATEncoder { std::optional twoQubitGateLimit = std::nullopt; SolverParameterMap solverParameters = {}; + + GateSet gateSet = {}; + + bool ignoreRChanges = false; }; SATEncoder() = default; @@ -86,6 +90,8 @@ class SATEncoder { std::size_t N{}; // NOLINT (readability-identifier-naming) // timestep limit T std::size_t T{}; // NOLINT (readability-identifier-naming) + // number of rows in the tableau S + std::size_t S{}; // NOLINT (readability-identifier-naming) }; } // namespace cs::encoding diff --git a/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp b/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp index 7bb83497e..e391f454f 100644 --- a/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp +++ b/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp @@ -20,12 +20,13 @@ class SingleGateEncoder : public GateEncoder { protected: void assertConsistency() const override; void assertGateConstraints() override; - void assertSingleQubitGateConstraints(std::size_t pos) override; - void assertTwoQubitGateConstraints(std::size_t pos) override; void assertNoGateNoChangeConstraint(std::size_t pos); [[nodiscard]] logicbase::LogicTerm createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl, std::size_t trgt) override; + [[nodiscard]] logicbase::LogicTerm + createTwoQubitRConstraint(std::size_t pos, std::size_t ctrl, + std::size_t trgt) override; [[nodiscard]] logicbase::LogicTerm createNoChangeOnQubit(std::size_t pos, std::size_t q); diff --git a/include/cliffordsynthesis/encoding/TableauEncoder.hpp b/include/cliffordsynthesis/encoding/TableauEncoder.hpp index 40d16e745..b7f8588fe 100644 --- a/include/cliffordsynthesis/encoding/TableauEncoder.hpp +++ b/include/cliffordsynthesis/encoding/TableauEncoder.hpp @@ -19,9 +19,10 @@ class TableauEncoder { TableauEncoder() = default; TableauEncoder(const std::size_t nQubits, const std::size_t tableauSize, const std::size_t timestepLimit, - std::shared_ptr logicBlock) - : N(nQubits), S(tableauSize), T(timestepLimit), - lb(std::move(logicBlock)) {} + std::shared_ptr logicBlock, + bool ignorePhase = false) + : N(nQubits), S(tableauSize), T(timestepLimit), lb(std::move(logicBlock)), + ignoreR(ignorePhase) {} struct Variables { // variables for the X parts of the tableaus @@ -58,8 +59,8 @@ class TableauEncoder { void assertTableau(const Tableau& tableau, std::size_t t); // extracting the tableau - void extractTableauFromModel(Results& results, std::size_t t, - logicbase::Model& model) const; + Tableau extractTableauFromModel(Results& results, std::size_t t, + logicbase::Model& model) const; [[nodiscard]] auto* getVariables() { return &vars; } @@ -76,5 +77,7 @@ class TableauEncoder { // the logic block to use std::shared_ptr lb{}; + + bool ignoreR = false; }; } // namespace cs::encoding diff --git a/src/Architecture.cpp b/src/Architecture.cpp index c0f11473d..60084ed19 100644 --- a/src/Architecture.cpp +++ b/src/Architecture.cpp @@ -92,8 +92,8 @@ void Architecture::loadProperties(const std::string& filename) { } void Architecture::loadProperties(std::istream&& is) { - static const auto SINGLE_QUBIT_GATES = {"id", "u1", "u2", "u3", - "rz", "sx", "x"}; + static const auto singleQubitGates = {"id", "u1", "u2", "u3", + "rz", "sx", "x"}; properties.clear(); @@ -115,7 +115,7 @@ void Architecture::loadProperties(std::istream&& is) { properties.qubitFrequency.set(qubitNumber, std::stod(data.at(3U))); properties.readoutErrorRate.set(qubitNumber, std::stod(data.at(4U))); // csv file reports average single qubit fidelities - for (const auto& operation : SINGLE_QUBIT_GATES) { + for (const auto& operation : singleQubitGates) { properties.setSingleQubitErrorRate(qubitNumber, operation, std::stod(data.at(5))); } diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 65b087cb2..d2c1c0096 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -64,17 +64,22 @@ macro(ADD_SYNTHESIS_LIBRARY libname srcfile) ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/SATEncoder.hpp ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/TableauEncoder.hpp + ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/Results.hpp ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/Tableau.hpp ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/TargetMetric.hpp ${PROJECT_SOURCE_DIR}/include/utils.hpp + ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/GateSet.hpp + ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/Utils.hpp cliffordsynthesis/encoding/GateEncoder.cpp cliffordsynthesis/encoding/MultiGateEncoder.cpp cliffordsynthesis/encoding/ObjectiveEncoder.cpp cliffordsynthesis/encoding/SATEncoder.cpp cliffordsynthesis/encoding/SingleGateEncoder.cpp cliffordsynthesis/encoding/TableauEncoder.cpp + cliffordsynthesis/encoding/PhaseCorrectionEncoder.cpp cliffordsynthesis/Tableau.cpp + cliffordsynthesis/Utils.cpp utils.cpp) add_internal_library(${lib} ${srcfile}) diff --git a/src/cliffordsynthesis/CliffordSynthesizer.cpp b/src/cliffordsynthesis/CliffordSynthesizer.cpp index e8f3a6880..12cec1cfb 100644 --- a/src/cliffordsynthesis/CliffordSynthesizer.cpp +++ b/src/cliffordsynthesis/CliffordSynthesizer.cpp @@ -44,6 +44,8 @@ void CliffordSynthesizer::synthesize(const Configuration& config) { encoderConfig.solverParameters = configuration.solverParameters; encoderConfig.useMultiGateEncoding = requiresMultiGateEncoding(encoderConfig.targetMetric); + encoderConfig.gateSet = configuration.gateSet; + encoderConfig.ignoreRChanges = config.delayPaulis; if (configuration.heuristic) { if (initialCircuit->empty() && !targetTableau.isIdentityTableau()) { diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp index 132f4ccc7..9c48766e6 100644 --- a/src/cliffordsynthesis/Tableau.cpp +++ b/src/cliffordsynthesis/Tableau.cpp @@ -5,6 +5,7 @@ #include "cliffordsynthesis/Tableau.hpp" +#include "operations/OpType.hpp" #include "utils.hpp" namespace cs { @@ -48,6 +49,38 @@ void Tableau::import(std::istream& is) { } } +void Tableau::applySingleQGate(const qc::OpType& gate, std::size_t target) { + switch (gate) { + case qc::OpType::H: + applyH(target); + break; + case qc::OpType::S: + applyS(target); + break; + case qc::OpType::Sdg: + applySdag(target); + break; + case qc::OpType::SX: + applySx(target); + break; + case qc::OpType::SXdg: + applySxdag(target); + break; + case qc::OpType::X: + applyX(target); + break; + case qc::OpType::Y: + applyY(target); + break; + case qc::OpType::Z: + applyZ(target); + break; + default: + util::fatal("Tableau::applyGate: Unsupported non-controlled gate type " + + qc::toString(gate)); + } +} + void Tableau::applyGate(const qc::Operation* const gate) { if (gate->getNcontrols() > 1U) { util::fatal("Tableau::applyGate: Only operations with up to one control " @@ -60,28 +93,14 @@ void Tableau::applyGate(const qc::Operation* const gate) { if (!gate->isControlled()) { switch (gate->getType()) { case qc::OpType::H: - applyH(target); - break; case qc::OpType::S: - applyS(target); - break; case qc::OpType::Sdg: - applySdag(target); - break; case qc::OpType::SX: - applySx(target); - break; case qc::OpType::SXdg: - applySxdag(target); - break; case qc::OpType::X: - applyX(target); - break; case qc::OpType::Y: - applyY(target); - break; case qc::OpType::Z: - applyZ(target); + applySingleQGate(gate->getType(), target); break; case qc::OpType::SWAP: { const auto target2 = static_cast(gate->getTargets().at(1U)); diff --git a/src/cliffordsynthesis/Utils.cpp b/src/cliffordsynthesis/Utils.cpp new file mode 100644 index 000000000..a260e76ae --- /dev/null +++ b/src/cliffordsynthesis/Utils.cpp @@ -0,0 +1,32 @@ +#include "cliffordsynthesis/Utils.hpp" + +#include "operations/OpType.hpp" + +namespace cs { +qc::OpType multiplyPaulis(const GateSet& paulis) { + auto pauliCopy = paulis; + pauliCopy.removeGate(qc::OpType::None); + if (paulis.empty()) { + return qc::OpType::None; + } + + if (pauliCopy.size() == 1) { + return pauliCopy.at(0); + } + + if (pauliCopy.size() == 2) { + if (pauliCopy.containsX()) { + if (pauliCopy.containsY()) { + return qc::OpType::Z; + } + return qc::OpType::Y; + } + return qc::OpType::X; + } + + if (pauliCopy.size() == 3) { + return qc::OpType::None; + } + return qc::OpType::None; +}; +} // namespace cs diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp index aeff8fcf6..5710b0b5b 100644 --- a/src/cliffordsynthesis/encoding/GateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp @@ -5,9 +5,18 @@ #include "cliffordsynthesis/encoding/GateEncoder.hpp" +#include "Definitions.hpp" #include "Encodings/Encodings.hpp" +#include "LogicTerm/LogicTerm.hpp" +#include "QuantumComputation.hpp" +#include "cliffordsynthesis/GateSet.hpp" +#include "cliffordsynthesis/Tableau.hpp" +#include "cliffordsynthesis/Utils.hpp" +#include "operations/OpType.hpp" #include "utils/logging.hpp" +#include + namespace cs::encoding { using namespace logicbase; @@ -17,8 +26,8 @@ void GateEncoder::createSingleQubitGateVariables() { vars.gS.reserve(T); for (std::size_t t = 0U; t < T; ++t) { auto& timeStep = vars.gS.emplace_back(); - timeStep.reserve(SINGLE_QUBIT_GATES.size()); - for (const auto gate : SINGLE_QUBIT_GATES) { + timeStep.reserve(singleQubitGates.size()); + for (const auto gate : singleQubitGates) { auto& g = timeStep.emplace_back(); g.reserve(N); for (std::size_t q = 0U; q < N; ++q) { @@ -54,8 +63,8 @@ void GateEncoder::createTwoQubitGateVariables() { void GateEncoder::Variables::collectSingleQubitGateVariables( const std::size_t pos, const std::size_t qubit, LogicVector& variables) const { - const auto& singleQubitGates = gS[pos]; - for (const auto& gate : singleQubitGates) { + const auto& singleQubitGateVariables = gS[pos]; + for (const auto& gate : singleQubitGateVariables) { variables.emplace_back(gate[qubit]); } } @@ -77,10 +86,14 @@ void GateEncoder::Variables::collectTwoQubitGateVariables( } } -void GateEncoder::assertExactlyOne(const LogicVector& variables) const { +LogicTerm +GateEncoder::createExactlyOne(const logicbase::LogicVector& variables) const { const auto variableGrouping = encodings::groupVars(variables, 3U); - lb->assertFormula(encodings::exactlyOneCmdr(variableGrouping, - LogicTerm::noneTerm(), lb.get())); + return encodings::exactlyOneCmdr(variableGrouping, LogicTerm::noneTerm(), + lb.get()); +} +void GateEncoder::assertExactlyOne(const LogicVector& variables) const { + lb->assertFormula(createExactlyOne(variables)); } std::vector @@ -89,7 +102,7 @@ GateEncoder::collectGateTransformations( const GateToTransformation& gateToTransformation) { std::vector transformations; - for (const auto& gate : SINGLE_QUBIT_GATES) { + for (const auto& gate : singleQubitGates) { const auto& transformation = gateToTransformation(pos, qubit, gate); const auto& it = std::find_if( transformations.begin(), transformations.end(), [&](const auto& entry) { @@ -108,11 +121,12 @@ GateEncoder::collectGateTransformations( void GateEncoder::assertGatesImplyTransform( const std::size_t pos, const std::size_t qubit, const std::vector& transformations) { - const auto& singleQubitGates = vars.gS[pos]; + const auto& singleQubitGateVars = vars.gS[pos]; for (const auto& [transformation, gates] : transformations) { auto gateOr = LogicTerm(false); for (const auto& gate : gates) { - gateOr = gateOr || singleQubitGates[gateToIndex(gate)][qubit]; + gateOr = gateOr || + singleQubitGateVars[singleQubitGates.gateToIndex(gate)][qubit]; } lb->assertFormula(LogicTerm::implies(gateOr, transformation)); } @@ -160,36 +174,86 @@ void GateEncoder::assertRConstraints(const std::size_t pos, assertGatesImplyTransform(pos, qubit, gateTransformations); } -void GateEncoder::extractCircuitFromModel(Results& res, Model& model) { +qc::QuantumComputation GateEncoder::extractCircuitFromModel(Results& res, + Model& model) { std::size_t nSingleQubitGates = 0U; std::size_t nTwoQubitGates = 0U; + Tableau intermediateTableau = init; qc::QuantumComputation qc(N); for (std::size_t t = 0; t < T; ++t) { - extractSingleQubitGatesFromModel(t, model, qc, nSingleQubitGates); - extractTwoQubitGatesFromModel(t, model, qc, nTwoQubitGates); + std::vector hasGate(N, false); + extractSingleQubitGatesFromModel(t, model, qc, nSingleQubitGates, hasGate, + intermediateTableau); + extractTwoQubitGatesFromModel(t, model, qc, nTwoQubitGates, hasGate, + intermediateTableau); } res.setSingleQubitGates(nSingleQubitGates); res.setTwoQubitGates(nTwoQubitGates); res.setDepth(qc.getDepth()); res.setResultCircuit(qc); + return qc; +} + +void GateEncoder::assertSingleQubitGateConstraints(std::size_t pos) { + for (std::size_t q = 0U; q < N; ++q) { + DEBUG() << "Asserting gates on " << q; + assertZConstraints(pos, q); + assertXConstraints(pos, q); + if (!ignoreRChanges) { + assertRConstraints(pos, q); + } + } +} + +void GateEncoder::assertTwoQubitGateConstraints(std::size_t pos) { + const auto& twoQubitGates = vars.gC[pos]; + for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) { + for (std::size_t trgt = 0U; trgt < N; ++trgt) { + if (ctrl == trgt) { + continue; + } + auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt); + if (!ignoreRChanges) { + changes = changes && createTwoQubitRConstraint(pos, ctrl, trgt); + } + lb->assertFormula(LogicTerm::implies(twoQubitGates[ctrl][trgt], changes)); + DEBUG() << "Asserting CNOT on " << ctrl << " and " << trgt; + } + } } void GateEncoder::extractSingleQubitGatesFromModel( const std::size_t pos, Model& model, qc::QuantumComputation& qc, - std::size_t& nSingleQubitGates) { - const auto& singleQubitGates = vars.gS[pos]; + std::size_t& nSingleQubitGates, std::vector& hasGate, + Tableau& intermediateTableau) { + const auto& singleQubitGateVars = vars.gS[pos]; + auto validPaulis = singleQubitGates.paulis(); for (std::size_t q = 0U; q < N; ++q) { - for (const auto gate : SINGLE_QUBIT_GATES) { + if (hasGate[q]) { + continue; + } + for (const auto gate : singleQubitGates) { if (gate == qc::OpType::None) { continue; } - if (model.getBoolValue(singleQubitGates[gateToIndex(gate)][q], - lb.get())) { + + if (model.getBoolValue( + singleQubitGateVars[singleQubitGates.gateToIndex(gate)][q], + lb.get())) { + auto temp = intermediateTableau; + temp.applySingleQGate(gate, q); + if ((ignoreRChanges && intermediateTableau.equalUpToPhase(temp)) || + intermediateTableau == temp) { + continue; + } + intermediateTableau.applySingleQGate(gate, q); qc.emplace_back(N, q, gate); + hasGate[q] = true; ++nSingleQubitGates; DEBUG() << toString(gate) << "(" << q << ")"; + break; } } } @@ -198,17 +262,33 @@ void GateEncoder::extractSingleQubitGatesFromModel( void GateEncoder::extractTwoQubitGatesFromModel(const std::size_t pos, Model& model, qc::QuantumComputation& qc, - size_t& nTwoQubitGates) { + size_t& nTwoQubitGates, + std::vector& hasGate, + Tableau& intermediateTableau) { const auto& twoQubitGates = vars.gC[pos]; for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) { + if (hasGate[ctrl]) { + continue; + } for (std::size_t trgt = 0U; trgt < N; ++trgt) { - if (ctrl == trgt) { + if (hasGate[trgt] || ctrl == trgt) { continue; } const auto control = qc::Control{static_cast(ctrl), qc::Control::Type::Pos}; if (model.getBoolValue(twoQubitGates[ctrl][trgt], lb.get())) { + auto temp = intermediateTableau; + temp.applyCX(ctrl, trgt); + DEBUG() << temp.toString(); + DEBUG() << intermediateTableau.toString(); + if ((ignoreRChanges && intermediateTableau.equalUpToPhase(temp)) || + intermediateTableau == temp) { // gate doesn't do anything + continue; + } + intermediateTableau.applyCX(ctrl, trgt); qc.emplace_back(N, control, trgt, qc::OpType::X); + hasGate[ctrl] = true; + hasGate[trgt] = true; ++nTwoQubitGates; DEBUG() << "CX(" << ctrl << ", " << trgt << ")"; } @@ -237,33 +317,36 @@ void GateEncoder::assertSingleQubitGateCancellationConstraints( // Any Pauli must not be followed by another Pauli since -iXYZ = I. std::vector paulis{}; - if constexpr (containsX()) { + if (singleQubitGates.containsX()) { paulis.emplace_back(qc::OpType::X); } - if constexpr (containsY()) { + if (singleQubitGates.containsY()) { paulis.emplace_back(qc::OpType::Y); } - if constexpr (containsZ()) { + if (singleQubitGates.containsZ()) { paulis.emplace_back(qc::OpType::Z); } - constexpr bool containsPaulis = containsX() || containsY() || containsZ(); - if constexpr (containsPaulis) { - auto gates = gSNow[gateToIndex(paulis[0])][qubit]; - auto disallowed = !gSNext[gateToIndex(paulis[0])][qubit]; + const bool containsPaulis = singleQubitGates.containsX() || + singleQubitGates.containsY() || + singleQubitGates.containsZ(); + if (containsPaulis) { + auto gates = gSNow[singleQubitGates.gateToIndex(paulis[0])][qubit]; + auto disallowed = !gSNext[singleQubitGates.gateToIndex(paulis[0])][qubit]; for (std::size_t i = 1U; i < paulis.size(); ++i) { - gates = gates || gSNow[gateToIndex(paulis[i])][qubit]; - disallowed = disallowed && !gSNext[gateToIndex(paulis[i])][qubit]; + gates = gates || gSNow[singleQubitGates.gateToIndex(paulis[i])][qubit]; + disallowed = + disallowed && !gSNext[singleQubitGates.gateToIndex(paulis[i])][qubit]; } - if constexpr (containsH()) { + if (singleQubitGates.containsH()) { // -(X|Y|Z)-H- ~= -H-(Z|Y|X)- - constexpr auto gateIndex = gateToIndex(qc::OpType::H); - disallowed = disallowed && !gSNext[gateIndex][qubit]; + auto gateIndex = singleQubitGates.gateToIndex(qc::OpType::H); + disallowed = disallowed && !gSNext[gateIndex][qubit]; } - if constexpr (containsS() && containsSdag()) { - const auto gateIndexS = gateToIndex(qc::OpType::S); - const auto gateIndexSdg = gateToIndex(qc::OpType::Sdg); + if (singleQubitGates.containsS() && singleQubitGates.containsSdg()) { + const auto gateIndexS = singleQubitGates.gateToIndex(qc::OpType::S); + const auto gateIndexSdg = singleQubitGates.gateToIndex(qc::OpType::Sdg); // -X-(S|Sd)- ~= -(Sd|S)-X- // -Y-(S|Sd)- ~= -(Sd|S)-Y- @@ -276,24 +359,24 @@ void GateEncoder::assertSingleQubitGateCancellationConstraints( } // H is self-inverse - if constexpr (containsH()) { - constexpr auto gateIndex = gateToIndex(qc::OpType::H); + if (singleQubitGates.containsH()) { + auto gateIndex = singleQubitGates.gateToIndex(qc::OpType::H); lb->assertFormula( LogicTerm::implies(gSNow[gateIndex][qubit], !gSNext[gateIndex][qubit])); } - if constexpr (containsS()) { - constexpr auto gateIndexS = gateToIndex(qc::OpType::S); + if (singleQubitGates.containsS()) { + auto gateIndexS = singleQubitGates.gateToIndex(qc::OpType::S); - if constexpr (containsZ()) { - constexpr auto gateIndexZ = gateToIndex(qc::OpType::Z); + if (singleQubitGates.containsZ()) { + auto gateIndexZ = singleQubitGates.gateToIndex(qc::OpType::Z); // -S-S- = -Z- auto gates = gSNow[gateIndexS][qubit]; auto disallowed = !gSNext[gateIndexS][qubit]; - if constexpr (containsSdag()) { - constexpr auto gateIndexSdag = gateToIndex(qc::OpType::Sdg); + if (singleQubitGates.containsSdg()) { + auto gateIndexSdag = singleQubitGates.gateToIndex(qc::OpType::Sdg); // -Sd-Sd- = -Z- // -Sd-S- = -I- @@ -307,8 +390,8 @@ void GateEncoder::assertSingleQubitGateCancellationConstraints( lb->assertFormula(LogicTerm::implies(gates, disallowed)); } else { - if constexpr (containsSdag()) { - constexpr auto gateIndexSdag = gateToIndex(qc::OpType::Sdg); + if (singleQubitGates.containsSdg()) { + auto gateIndexSdag = singleQubitGates.gateToIndex(qc::OpType::Sdg); // -S-Sd- = -I- // -Sd-S- = -I- diff --git a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp index 1ee9a4d05..32717910c 100644 --- a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp @@ -5,9 +5,12 @@ #include "cliffordsynthesis/encoding/MultiGateEncoder.hpp" +#include "LogicTerm/Logic.hpp" #include "LogicTerm/LogicTerm.hpp" #include "utils/logging.hpp" +#include + namespace cs::encoding { using namespace logicbase; @@ -18,9 +21,11 @@ void encoding::MultiGateEncoder::assertConsistency() const { // asserting only a single gate is applied on each qubit. for (std::size_t q = 0U; q < N; ++q) { LogicVector gateVariables{}; + LogicVector trgtVariables{}; + LogicVector ctrlVariables{}; vars.collectSingleQubitGateVariables(t, q, gateVariables); - vars.collectTwoQubitGateVariables(t, q, true, gateVariables); - vars.collectTwoQubitGateVariables(t, q, false, gateVariables); + vars.collectTwoQubitGateVariables(t, q, true, trgtVariables); + vars.collectTwoQubitGateVariables(t, q, false, ctrlVariables); IF_PLOG(plog::verbose) { TRACE() << "Gate variables at time " << t << " and qubit " << q; @@ -28,8 +33,28 @@ void encoding::MultiGateEncoder::assertConsistency() const { TRACE() << var.getName(); } } + if (singleQubitGates.paulis().size() > + 1) { // if no Paulis are present we can relax the exactlyone + // constraint + // collect all variables into gateVariables + gateVariables.insert(gateVariables.end(), trgtVariables.begin(), + trgtVariables.end()); + gateVariables.insert(gateVariables.end(), ctrlVariables.begin(), + ctrlVariables.end()); + assertExactlyOne(gateVariables); + } else { + auto atLeastOneSingle = LogicTerm(false); + for (const auto& var : gateVariables) { + atLeastOneSingle = atLeastOneSingle || var; + } + auto consistency = atLeastOneSingle; + if (!trgtVariables.empty() && !ctrlVariables.empty()) { + consistency = consistency || createExactlyOne(trgtVariables) || + createExactlyOne(ctrlVariables); + } - assertExactlyOne(gateVariables); + lb->assertFormula(consistency); + } } } } @@ -39,51 +64,31 @@ void encoding::MultiGateEncoder::assertGateConstraints() { xorHelpers = logicbase::LogicMatrix{T}; for (std::size_t t = 0U; t < T; ++t) { TRACE() << "Asserting gate constraints at time " << t; - rChanges = tvars->r[t]; - splitXorR(tvars->r[t], t); + if (!ignoreRChanges) { + rChanges = tvars->r[t]; + splitXorR(tvars->r[t], t); + } assertSingleQubitGateConstraints(t); assertTwoQubitGateConstraints(t); TRACE() << "Asserting r changes at time " << t; - lb->assertFormula(tvars->r[t + 1] == xorHelpers[t].back()); - } -} -void encoding::MultiGateEncoder::assertSingleQubitGateConstraints( - const std::size_t pos) { - for (std::size_t q = 0U; q < N; ++q) { - assertZConstraints(pos, q); - assertXConstraints(pos, q); - assertRConstraints(pos, q); + if (!ignoreRChanges) { + lb->assertFormula(tvars->r[t + 1] == xorHelpers[t].back()); + } } } void MultiGateEncoder::assertRConstraints(const std::size_t pos, const std::size_t qubit) { - for (const auto gate : SINGLE_QUBIT_GATES) { + for (const auto gate : singleQubitGates) { const auto& change = - LogicTerm::ite(vars.gS[pos][gateToIndex(gate)][qubit], + LogicTerm::ite(vars.gS[pos][singleQubitGates.gateToIndex(gate)][qubit], tvars->singleQubitRChange(pos, qubit, gate), LogicTerm(0, static_cast(S))); splitXorR(change, pos); } } -void encoding::MultiGateEncoder::assertTwoQubitGateConstraints( - const std::size_t pos) { - const auto& twoQubitGates = vars.gC[pos]; - for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) { - for (std::size_t trgt = 0U; trgt < N; ++trgt) { - if (ctrl == trgt) { - continue; - } - const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt); - lb->assertFormula(LogicTerm::implies(twoQubitGates[ctrl][trgt], changes)); - - DEBUG() << "Asserting CNOT on " << ctrl << " and " << trgt; - } - } -} - LogicTerm encoding::MultiGateEncoder::createTwoQubitGateConstraint( std::size_t pos, std::size_t ctrl, std::size_t trgt) { auto changes = LogicTerm(true); @@ -95,11 +100,17 @@ LogicTerm encoding::MultiGateEncoder::createTwoQubitGateConstraint( changes = changes && (tvars->z[pos + 1][ctrl] == zCtrl); changes = changes && (tvars->z[pos + 1][trgt] == zTrgt); + return changes; +} + +[[nodiscard]] logicbase::LogicTerm +MultiGateEncoder::createTwoQubitRConstraint(std::size_t pos, std::size_t ctrl, + std::size_t trgt) { const auto& newRChanges = LogicTerm::ite( vars.gC[pos][ctrl][trgt], tvars->twoQubitRChange(pos, ctrl, trgt), LogicTerm(0, static_cast(S))); splitXorR(newRChanges, pos); - return changes; + return logicbase::LogicTerm(true); } void MultiGateEncoder::assertSingleQubitGateOrderConstraints( @@ -116,14 +127,16 @@ void MultiGateEncoder::assertSingleQubitGateOrderConstraints( // once no gate is applied to the considered qubit, no single qubit gate can // be applied to it in the next time step. auto noSingleQubitGate = LogicTerm(true); - for (const auto gate : SINGLE_QUBIT_GATES) { + for (const auto gate : singleQubitGates) { if (gate == qc::OpType::None) { continue; } - noSingleQubitGate = noSingleQubitGate && !gSNext[gateToIndex(gate)][qubit]; + noSingleQubitGate = + noSingleQubitGate && !gSNext[singleQubitGates.gateToIndex(gate)][qubit]; } lb->assertFormula(LogicTerm::implies( - gSNow[gateToIndex(qc::OpType::None)][qubit], noSingleQubitGate)); + gSNow[singleQubitGates.gateToIndex(qc::OpType::None)][qubit], + noSingleQubitGate)); } void MultiGateEncoder::assertTwoQubitGateOrderConstraints( @@ -147,16 +160,16 @@ void MultiGateEncoder::assertTwoQubitGateOrderConstraints( // hadamards on both qubits => no CNOT on them in the next time step (CNOT can // be conjugated with Hadamards) No Combination of Paulis on both Qubits // before a CNOT These gates can be just pushed through to the other side - constexpr auto noneIndex = gateToIndex(qc::OpType::None); - const auto noGate = gSNow[noneIndex][ctrl] && gSNow[noneIndex][trgt]; - const auto noFurtherCnot = !gCNext[ctrl][trgt] && !gCNext[trgt][ctrl]; - - constexpr auto hIndex = gateToIndex(qc::OpType::H); - constexpr auto xIndex = gateToIndex(qc::OpType::X); - constexpr auto zIndex = gateToIndex(qc::OpType::Z); - constexpr auto yIndex = gateToIndex(qc::OpType::Y); - const auto hh = gSNow[hIndex][ctrl] && gSNow[hIndex][trgt]; - const auto gateBeforeCtrl = + auto noneIndex = singleQubitGates.gateToIndex(qc::OpType::None); + const auto noGate = gSNow[noneIndex][ctrl] && gSNow[noneIndex][trgt]; + const auto noFurtherCnot = !gCNext[ctrl][trgt] && !gCNext[trgt][ctrl]; + + auto hIndex = singleQubitGates.gateToIndex(qc::OpType::H); + auto xIndex = singleQubitGates.gateToIndex(qc::OpType::X); + auto zIndex = singleQubitGates.gateToIndex(qc::OpType::Z); + auto yIndex = singleQubitGates.gateToIndex(qc::OpType::Y); + const auto hh = gSNow[hIndex][ctrl] && gSNow[hIndex][trgt]; + const auto gateBeforeCtrl = gSNow[zIndex][ctrl] || gSNow[xIndex][ctrl] || gSNow[yIndex][ctrl]; const auto gateBeforeTarget = gSNow[zIndex][trgt] || gSNow[xIndex][trgt] || gSNow[yIndex][ctrl]; diff --git a/src/cliffordsynthesis/encoding/ObjectiveEncoder.cpp b/src/cliffordsynthesis/encoding/ObjectiveEncoder.cpp index c2693a7f3..d49437276 100644 --- a/src/cliffordsynthesis/encoding/ObjectiveEncoder.cpp +++ b/src/cliffordsynthesis/encoding/ObjectiveEncoder.cpp @@ -9,6 +9,8 @@ #include "cliffordsynthesis/encoding/MultiGateEncoder.hpp" #include "utils/logging.hpp" +#include + namespace cs::encoding { using namespace logicbase; @@ -37,13 +39,20 @@ void ObjectiveEncoder::optimizeDepth() const { DEBUG() << "Optimizing depth"; auto* optimizer = dynamic_cast(lb.get()); - constexpr auto noGateIndex = GateEncoder::gateToIndex(qc::OpType::None); + auto noGateIndex = singleQubitGates.gateToIndex(qc::OpType::None); for (std::size_t t = 0U; t < T; ++t) { const auto& gS = gvars->gS[t]; auto noGate = LogicTerm(true); for (std::size_t q = 0U; q < N; ++q) { noGate = noGate && gS[noGateIndex][q]; + for (std::size_t tar = 0U; tar < N; ++tar) { + if (tar == q) { + continue; + } + noGate = noGate && !gvars->gC[t][q][tar]; + } } + optimizer->weightedTerm(!noGate, 1); } optimizer->makeMinimize(); diff --git a/src/cliffordsynthesis/encoding/PhaseCorrectionEncoder.cpp b/src/cliffordsynthesis/encoding/PhaseCorrectionEncoder.cpp new file mode 100644 index 000000000..86c7d1f8b --- /dev/null +++ b/src/cliffordsynthesis/encoding/PhaseCorrectionEncoder.cpp @@ -0,0 +1,148 @@ +#include "cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp" + +#include "LogicTerm/Logic.hpp" +#include "LogicTerm/LogicTerm.hpp" +#include "cliffordsynthesis/GateSet.hpp" +#include "cliffordsynthesis/Utils.hpp" +#include "utils/logging.hpp" + +#include +#include +#include +#include + +namespace cs::encoding { +using namespace logicbase; + +std::vector PhaseCorrectionEncoder::phaseCorrection() { + createVariables(); + encodePauliConstraints(); + lb->solve(); + return extractResult(); +} + +void PhaseCorrectionEncoder::createVariables() { + DEBUG() << "Creating phase correction gate variables."; + for (std::size_t i = 0U; i < N; ++i) { + paulis[i].reserve(4); + for (const auto& pauli : PAULIS) { + const std::string gName = + "g_" + std::to_string(i) + "_" + toString(pauli); + TRACE() << "Creating pauli variable " << gName; + paulis[i].emplace_back(lb->makeVariable(gName)); + } + } + + const std::bitset<64> init = uncorrected.getBVFrom(2 * N); + initialPhase = vectorFromBitset(init); + const std::bitset<64> tar = target.getBVFrom(2 * N); + targetPhase = vectorFromBitset(tar); +} + +void PhaseCorrectionEncoder::encodePauliConstraints() { + DEBUG() << "Encoding pauli constraints."; + splitXorR(initialPhase); + for (std::size_t q = 0U; q < N; ++q) { + const auto& xCol = vectorFromBitset(uncorrected.getBVFrom(q)); + const auto& zCol = vectorFromBitset(uncorrected.getBVFrom(N + q)); + + LogicVector iChange{}; + LogicVector xChange{}; + LogicVector zChange{}; + LogicVector yChange{}; + iChange.reserve(S); + xChange.reserve(S); + zChange.reserve(S); + yChange.reserve(S); + + for (std::size_t row = 0U; row < S; ++row) { + DEBUG() << "Encoding identity constraint."; + iChange.emplace_back(logicbase::LogicTerm::ite( + paulis[q][0], LogicTerm(false), LogicTerm(false))); + DEBUG() << "Encoding X constraint."; + xChange.emplace_back( + logicbase::LogicTerm::ite(paulis[q][1], zCol[row], LogicTerm(false))); + DEBUG() << "Encoding Y constraint."; + yChange.emplace_back(logicbase::LogicTerm::ite( + paulis[q][2], !(zCol[row] == xCol[row]), LogicTerm(false))); + DEBUG() << "Encoding Z constraint."; + zChange.emplace_back( + logicbase::LogicTerm::ite(paulis[q][3], xCol[row], LogicTerm(false))); + } + splitXorR(iChange); + splitXorR(xChange); + splitXorR(yChange); + splitXorR(zChange); + + // at least one gate per qubit + lb->assertFormula(paulis[q][0] || paulis[q][1] || paulis[q][2] || + paulis[q][3]); + } + DEBUG() << "Assert Phase."; + for (std::size_t row = 0U; row < S; ++row) { + lb->assertFormula(targetPhase[row] == xorHelpers.back()[row]); + } + DEBUG() << "Finished Phase Encoding."; +} + +void PhaseCorrectionEncoder::splitXorR(const LogicVector& changes) { + auto xorHelper = LogicVector{}; + xorHelper.reserve(S); + for (std::size_t row = 0U; row < S; ++row) { + const std::string hName = + "h_" + std::to_string(row) + "_" + std::to_string(xorHelpers.size()); + DEBUG() << "Creating helper variable for RChange XOR " << hName; + xorHelper.emplace_back(lb->makeVariable(hName)); + } + xorHelpers.emplace_back(xorHelper); + if (xorHelpers.size() == 1) { + for (std::size_t row = 0U; row < S; ++row) { + lb->assertFormula(xorHelpers[0][row] == changes[row]); + } + } else { + for (std::size_t row = 0U; row < S; ++row) { + lb->assertFormula( + xorHelpers.back()[row] == + (changes[row] != xorHelpers[xorHelpers.size() - 2][row])); + } + } +} + +LogicVector +PhaseCorrectionEncoder::vectorFromBitset(const std::bitset<64>& bs) const { + LogicVector result{}; + result.reserve(S); + for (std::size_t i = 0U; i < S; ++i) { + result.emplace_back(bs[i]); + } + return result; +} + +std::vector PhaseCorrectionEncoder::extractResult() { + const auto& model = lb->getModel(); + std::vector result{}; + result.reserve(N); + for (std::size_t q = 0U; q < N; ++q) { + GateSet pauliGates{}; + pauliGates.removePaulis(); + if (model->getBoolValue(paulis[q][0], lb.get())) { + pauliGates.emplace_back(qc::OpType::None); + DEBUG() << "Identity gate for qubit " << q; + } + if (model->getBoolValue(paulis[q][1], lb.get())) { + pauliGates.emplace_back(qc::OpType::X); + DEBUG() << "X gate for qubit " << q; + } + if (model->getBoolValue(paulis[q][2], lb.get())) { + pauliGates.emplace_back(qc::OpType::Y); + DEBUG() << "Y gate for qubit " << q; + } + if (model->getBoolValue(paulis[q][3], lb.get())) { + pauliGates.emplace_back(qc::OpType::Z); + DEBUG() << "Z gate for qubit " << q; + } + result.emplace_back(multiplyPaulis(pauliGates)); + } + return result; +} +} // namespace cs::encoding diff --git a/src/cliffordsynthesis/encoding/SATEncoder.cpp b/src/cliffordsynthesis/encoding/SATEncoder.cpp index 4fcbf4aaf..584325e81 100644 --- a/src/cliffordsynthesis/encoding/SATEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SATEncoder.cpp @@ -6,11 +6,16 @@ #include "cliffordsynthesis/encoding/SATEncoder.hpp" #include "LogicUtil/util_logicblock.hpp" +#include "cliffordsynthesis/Tableau.hpp" #include "cliffordsynthesis/encoding/MultiGateEncoder.hpp" +#include "cliffordsynthesis/encoding/PhaseCorrectionEncoder.hpp" #include "cliffordsynthesis/encoding/SingleGateEncoder.hpp" +#include "operations/OpType.hpp" #include "utils/logging.hpp" #include +#include +#include namespace cs::encoding { @@ -50,22 +55,30 @@ void SATEncoder::createFormulation() { const auto start = std::chrono::high_resolution_clock::now(); initializeSolver(); - const std::size_t s = config.targetTableau->hasDestabilizers() && - config.initialTableau->hasDestabilizers() - ? 2U * N - : N; + S = config.targetTableau->hasDestabilizers() && + config.initialTableau->hasDestabilizers() + ? 2U * N + : N; - tableauEncoder = std::make_shared(N, s, T, lb); + tableauEncoder = + std::make_shared(N, S, T, lb, config.ignoreRChanges); tableauEncoder->createTableauVariables(); tableauEncoder->assertTableau(*config.initialTableau, 0U); tableauEncoder->assertTableau(*config.targetTableau, T); + if (config.ignoreRChanges) { + config.gateSet.removePaulis(); + config.gateSet.emplace_back(qc::OpType::None); + } + if (config.useMultiGateEncoding) { gateEncoder = std::make_shared( - N, s, T, tableauEncoder->getVariables(), lb); + N, S, T, tableauEncoder->getVariables(), lb, config.gateSet, + *config.initialTableau, config.ignoreRChanges); } else { gateEncoder = std::make_shared( - N, s, T, tableauEncoder->getVariables(), lb); + N, S, T, tableauEncoder->getVariables(), lb, config.gateSet, + *config.initialTableau, config.ignoreRChanges); } gateEncoder->createSingleQubitGateVariables(); gateEncoder->createTwoQubitGateVariables(); @@ -75,8 +88,8 @@ void SATEncoder::createFormulation() { gateEncoder->encodeSymmetryBreakingConstraints(); } - objectiveEncoder = - std::make_shared(N, T, gateEncoder->getVariables(), lb); + objectiveEncoder = std::make_shared( + N, T, gateEncoder->getVariables(), lb, config.gateSet); if (config.gateLimit.has_value()) { objectiveEncoder->limitGateCount(*config.gateLimit, std::less_equal{}); @@ -114,7 +127,38 @@ Result SATEncoder::solve() const { void SATEncoder::extractResultsFromModel(Results& res) const { auto* const model = lb->getModel(); tableauEncoder->extractTableauFromModel(res, T, *model); - gateEncoder->extractCircuitFromModel(res, *model); + auto qc = gateEncoder->extractCircuitFromModel(res, *model); + if (config.ignoreRChanges) { + const auto start = std::chrono::high_resolution_clock::now(); + auto tab = *config.targetTableau; + auto qcTab = Tableau(qc, 0, std::numeric_limits::max(), + config.targetTableau->hasDestabilizers()); + for (std::size_t row = 0U; row < S; ++row) { + DEBUG() << "Row " << std::to_string(row); + tab[row][2 * N] = qcTab.at(row)[2 * N]; + } + PhaseCorrectionEncoder phaseCorrectionEncoder(N, S, tab, + *config.targetTableau); + auto paulis = phaseCorrectionEncoder.phaseCorrection(); + + for (std::size_t row = 0U; row < S; ++row) { + tab[row][2 * N] = config.targetTableau->at(row)[2 * N]; + } + + for (std::size_t q = 0U; q < N; ++q) { + if (paulis[q] != qc::OpType::None) { + DEBUG() << "Phase correction for qubit " << q << ": " + << qc::toString(paulis[q]); + qc.emplace_back(N, q, paulis[q]); + } + } + const auto end = std::chrono::high_resolution_clock::now(); + const auto runtime = std::chrono::duration(end - start); + res.setRuntime(res.getRuntime() + runtime.count()); + res.setResultCircuit(qc); + res.setResultTableau(tab); + res.setDepth(qc.getDepth()); + } } void SATEncoder::cleanup() const { diff --git a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp index 60f537398..04ac70452 100644 --- a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp +++ b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp @@ -14,7 +14,7 @@ using namespace logicbase; void SingleGateEncoder::assertConsistency() const { DEBUG() << "Asserting gate consistency"; LogicVector gateVariables{}; - gateVariables.reserve(N * (1 + SINGLE_QUBIT_GATES.size())); + gateVariables.reserve(N * (1 + singleQubitGates.size())); for (std::size_t t = 0U; t < T; ++t) { for (std::size_t q = 0U; q < N; ++q) { vars.collectSingleQubitGateVariables(t, q, gateVariables); @@ -49,31 +49,6 @@ void SingleGateEncoder::assertNoGateNoChangeConstraint(const std::size_t pos) { } } -void SingleGateEncoder::assertSingleQubitGateConstraints(std::size_t pos) { - for (std::size_t q = 0U; q < N; ++q) { - DEBUG() << "Asserting gates on " << q; - assertZConstraints(pos, q); - assertXConstraints(pos, q); - assertRConstraints(pos, q); - } -} - -void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) { - const auto& twoQubitGates = vars.gC[pos]; - for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) { - for (std::size_t trgt = 0U; trgt < N; ++trgt) { - if (ctrl == trgt) { - continue; - } - const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt); - - DEBUG() << "Asserting CNOT on " << ctrl << " and " << trgt; - - lb->assertFormula(LogicTerm::implies(twoQubitGates[ctrl][trgt], changes)); - } - } -} - LogicTerm SingleGateEncoder::createTwoQubitGateConstraint( const std::size_t pos, const std::size_t ctrl, const std::size_t trgt) { auto changes = LogicTerm(true); @@ -84,13 +59,17 @@ LogicTerm SingleGateEncoder::createTwoQubitGateConstraint( 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->r[pos + 1] == - (tvars->r[pos] ^ tvars->twoQubitRChange(pos, ctrl, trgt))); return changes; } +[[nodiscard]] logicbase::LogicTerm +SingleGateEncoder::createTwoQubitRConstraint(std::size_t pos, std::size_t ctrl, + std::size_t trgt) { + return (tvars->r[pos + 1] == + (tvars->r[pos] ^ tvars->twoQubitRChange(pos, ctrl, trgt))); +} + LogicTerm SingleGateEncoder::createNoChangeOnQubit(const std::size_t pos, const std::size_t q) { auto noChange = LogicTerm(true); @@ -101,13 +80,14 @@ LogicTerm SingleGateEncoder::createNoChangeOnQubit(const std::size_t pos, LogicTerm SingleGateEncoder::createNoGateOnQubit(const std::size_t pos, const std::size_t q) { - const auto& singleQubitGates = vars.gS[pos]; - auto noGate = LogicTerm(true); - for (const auto& gate : SINGLE_QUBIT_GATES) { + const auto& singleQubitGateVars = vars.gS[pos]; + auto noGate = LogicTerm(true); + for (const auto& gate : singleQubitGates) { if (gate == qc::OpType::None) { continue; } - noGate = noGate && !singleQubitGates[gateToIndex(gate)][q]; + noGate = + noGate && !singleQubitGateVars[singleQubitGates.gateToIndex(gate)][q]; } const auto& twoQubitGates = vars.gC[pos]; for (std::size_t i = 0; i < N; ++i) { @@ -134,12 +114,13 @@ void SingleGateEncoder::assertSingleQubitGateOrderConstraints( // collect variables of single-qubit gates that could be applied to `qubit` auto singleQubitGate = LogicTerm(false); - for (const auto& gate : SINGLE_QUBIT_GATES) { + for (const auto& gate : singleQubitGates) { if (gate == qc::OpType::None) { continue; } // any single-qubit gate on qubit q - singleQubitGate = singleQubitGate || gSNow[gateToIndex(gate)][qubit]; + singleQubitGate = + singleQubitGate || gSNow[singleQubitGates.gateToIndex(gate)][qubit]; } // collect gate variables of the next timestep that should not be applied. @@ -147,11 +128,12 @@ void SingleGateEncoder::assertSingleQubitGateOrderConstraints( // no single-qubit gate on a lower qubit for (std::size_t lower = 0U; lower < qubit; ++lower) { - for (const auto& gate : SINGLE_QUBIT_GATES) { + for (const auto& gate : singleQubitGates) { if (gate == qc::OpType::None) { continue; } - disallowed = disallowed && !gSNext[gateToIndex(gate)][lower]; + disallowed = + disallowed && !gSNext[singleQubitGates.gateToIndex(gate)][lower]; } } @@ -159,7 +141,7 @@ void SingleGateEncoder::assertSingleQubitGateOrderConstraints( // once no gate is applied, no other gate can be applied, i.e., in the next // timestep any of the `None` gate variables must be selected. - const auto noneIndex = gateToIndex(qc::OpType::None); + const auto noneIndex = singleQubitGates.gateToIndex(qc::OpType::None); auto noGate = LogicTerm(false); for (std::size_t q = 0U; q < N; ++q) { noGate = noGate || gSNext[noneIndex][q]; @@ -190,22 +172,26 @@ void SingleGateEncoder::assertTwoQubitGateOrderConstraints( if (q == control || q == target) { continue; } - for (const auto& gate : SINGLE_QUBIT_GATES) { + for (const auto& gate : singleQubitGates) { if (gate == qc::OpType::None) { continue; } - disallowed = disallowed && !gSNext[gateToIndex(gate)][q]; + disallowed = + disallowed && !gSNext[singleQubitGates.gateToIndex(gate)][q]; } } // no X gate may be placed on the target qubit since it would commute. - disallowed = disallowed && !gSNext[gateToIndex(qc::OpType::X)][target]; + disallowed = disallowed && + !gSNext[singleQubitGates.gateToIndex(qc::OpType::X)][target]; // no diagonal gate may be placed on the control qubit since it would // commute. - disallowed = disallowed && !gSNext[gateToIndex(qc::OpType::Z)][control] && - !gSNext[gateToIndex(qc::OpType::S)][control] && - !gSNext[gateToIndex(qc::OpType::Sdg)][control]; + disallowed = + disallowed && + !gSNext[singleQubitGates.gateToIndex(qc::OpType::Z)][control] && + !gSNext[singleQubitGates.gateToIndex(qc::OpType::S)][control] && + !gSNext[singleQubitGates.gateToIndex(qc::OpType::Sdg)][control]; // no CNOT with the same control and a lower target qubit may be placed. for (std::size_t t = 0U; t < target; ++t) { diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp index 12df965b4..4261b52c1 100644 --- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp +++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp @@ -5,6 +5,7 @@ #include "cliffordsynthesis/encoding/TableauEncoder.hpp" +#include "cliffordsynthesis/Tableau.hpp" #include "utils/logging.hpp" namespace cs::encoding { @@ -17,7 +18,9 @@ void TableauEncoder::createTableauVariables() { DEBUG() << "Creating tableau variables."; vars.x.reserve(T); vars.z.reserve(T); - vars.r.reserve(T); + if (!ignoreR) { + vars.r.reserve(T); + } for (std::size_t t = 0U; t <= T; ++t) { auto& x = vars.x.emplace_back(); auto& z = vars.z.emplace_back(); @@ -33,9 +36,11 @@ void TableauEncoder::createTableauVariables() { TRACE() << "Creating variable " << zName; z.emplace_back(lb->makeVariable(zName, CType::BITVECTOR, n)); } - const std::string rName = "r_" + std::to_string(t); - TRACE() << "Creating variable " << rName; - vars.r.emplace_back(lb->makeVariable(rName, CType::BITVECTOR, n)); + if (!ignoreR) { + const std::string rName = "r_" + std::to_string(t); + TRACE() << "Creating variable " << rName; + vars.r.emplace_back(lb->makeVariable(rName, CType::BITVECTOR, n)); + } } } @@ -53,13 +58,15 @@ void TableauEncoder::assertTableau(const Tableau& tableau, lb->assertFormula(vars.z[t][a] == LogicTerm(targetZ, n)); } - const auto targetR = tableau.getBVFrom(2U * N); - lb->assertFormula(vars.r[t] == LogicTerm(targetR, n)); + if (!ignoreR) { + const auto targetR = tableau.getBVFrom(2U * N); + lb->assertFormula(vars.r[t] == LogicTerm(targetR, n)); + } } -void TableauEncoder::extractTableauFromModel(Results& results, - const std::size_t t, - Model& model) const { +Tableau TableauEncoder::extractTableauFromModel(Results& results, + const std::size_t t, + Model& model) const { Tableau tableau(N, S > N); for (std::size_t i = 0; i < N; ++i) { const auto bvx = model.getBitvectorValue(vars.x[t][i], lb.get()); @@ -67,10 +74,12 @@ void TableauEncoder::extractTableauFromModel(Results& results, const auto bvz = model.getBitvectorValue(vars.z[t][i], lb.get()); tableau.populateTableauFrom(bvz, S, i + N); } - const auto bvr = model.getBitvectorValue(vars.r[t], lb.get()); - tableau.populateTableauFrom(bvr, S, 2 * N); - + if (!ignoreR) { + const auto bvr = model.getBitvectorValue(vars.r[t], lb.get()); + tableau.populateTableauFrom(bvr, S, 2 * N); + } results.setResultTableau(tableau); + return tableau; } LogicTerm diff --git a/src/python/bindings.cpp b/src/python/bindings.cpp index c3719f6d3..914ba51c5 100644 --- a/src/python/bindings.cpp +++ b/src/python/bindings.cpp @@ -4,17 +4,36 @@ // #include "cliffordsynthesis/CliffordSynthesizer.hpp" +#include "cliffordsynthesis/GateSet.hpp" #include "exact/ExactMapper.hpp" #include "heuristic/HeuristicMapper.hpp" #include "nlohmann/json.hpp" +#include "operations/OpType.hpp" #include "pybind11/pybind11.h" #include "pybind11/stl.h" #include "pybind11_json/pybind11_json.hpp" #include "python/qiskit/QuantumCircuit.hpp" +#include + namespace py = pybind11; using namespace pybind11::literals; +cs::GateSet loadGateSet(const py::object& circ) { + cs::GateSet gs{}; + if (py::isinstance(circ)) { + auto l = circ.cast(); + if (l.size() > 0) { + for (auto& gate : l) { + if (py::isinstance(gate)) { + gs.emplace_back(qc::opTypeFromString(gate.cast())); + } + } + } + } + return gs; +} + void loadQC(qc::QuantumComputation& qc, const py::object& circ) { try { if (py::isinstance(circ)) { @@ -504,6 +523,12 @@ PYBIND11_MODULE(pyqmap, m) { "n_threads_heuristic", &cs::Configuration::nThreadsHeuristic, "Maximum number of threads used for the heuristic optimizer. " "Defaults to the number of available threads on the system.") + .def_readwrite("gate_set", &cs::Configuration::gateSet, + "Gate Set to be used for the Synthesis. " + "Defaults to {H, S, Sdg, X, Y, Z, CX}.") + .def_readwrite("delay_paulis", &cs::Configuration::delayPaulis, + "Delay Pauli gates to the end of the circuit. " + "Defaults to `false`.") .def("json", &cs::Configuration::json, "Returns a JSON-style dictionary of all the information present in " "the :class:`.Configuration`") @@ -543,6 +568,11 @@ PYBIND11_MODULE(pyqmap, m) { .def("unsat", &cs::Results::unsat, "Returns `true` if the synthesis was unsuccessful."); + py::class_(m, "GateSet") + .def(py::init<>()) + .def(py::init(&loadGateSet)); + py::implicitly_convertible(); + auto tableau = py::class_( m, "Tableau", "A class for representing stabilizer tableaus."); tableau.def(py::init(), "n"_a, diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp index 6361b570c..47d63c665 100644 --- a/test/cliffordsynthesis/test_synthesis.cpp +++ b/test/cliffordsynthesis/test_synthesis.cpp @@ -353,6 +353,17 @@ TEST_P(SynthesisTest, TestDestabilizerTwoQubitGates) { } } +TEST_P(SynthesisTest, DepthDelayedPhase) { + config.target = TargetMetric::Depth; + config.linearSearch = true; + config.delayPaulis = true; + synthesizer.synthesize(config); + + results = synthesizer.getResults(); + + EXPECT_LE(results.getDepth(), test.expectedMinimalDepth + 1); +} + TEST(HeuristicTest, basic) { auto config = Configuration(); auto qc = qc::QuantumComputation(2);