Added new class for handling the encoding for phase correction.

include/cliffordsynthesis/Utils.hpp

@@ -1,3 +1,8 @@
+//
+// 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/cliffordsynthesis/encoding/GateEncoder.hpp

@@ -26,9 +26,10 @@ class GateEncoder {
               const std::size_t                      timestepLimit,
               TableauEncoder::Variables*             tableauVars,
               std::shared_ptr<logicbase::LogicBlock> logicBlock,
-              GateSet                                singleQGates)
+              GateSet                                singleQGates,
+              bool                                  ignorePhase = false)
       : N(nQubits), S(tableauSize), T(timestepLimit), tvars(tableauVars),
-        lb(std::move(logicBlock)), singleQubitGates(std::move(singleQGates)) {
+        lb(std::move(logicBlock)), singleQubitGates(std::move(singleQGates)), ignoreRChanges(ignorePhase) {
     if (!singleQGates.isValidGateSet()) {
       throw qc::QFRException("Invalid gate set");
     }
@@ -90,7 +91,7 @@ class GateEncoder {
   // the gates that are used
   GateSet singleQubitGates;
 
-  bool 
+  bool ignoreRChanges{false};
 
   using TransformationFamily =
       std::pair<logicbase::LogicTerm, std::vector<qc::OpType>>;

include/cliffordsynthesis/encoding/SATEncoder.hpp

@@ -59,6 +59,8 @@ class SATEncoder {
     SolverParameterMap solverParameters = {};
 
     GateSet gateSet = {};
+
+    bool ignoreRChanges = false;
   };
 
   SATEncoder() = default;

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<logicbase::LogicBlock> logicBlock)
+                 std::shared_ptr<logicbase::LogicBlock> logicBlock,
+                 bool ignorePhase=false)
       : N(nQubits), S(tableauSize), T(timestepLimit),
-        lb(std::move(logicBlock)) {}
+        lb(std::move(logicBlock)), ignoreR(ignorePhase) {}
 
   struct Variables {
     // variables for the X parts of the tableaus
@@ -76,5 +77,7 @@ class TableauEncoder {
 
   // the logic block to use
   std::shared_ptr<logicbase::LogicBlock> lb{};
+
+  bool ignoreR = false;
 };
 } // namespace cs::encoding

src/cliffordsynthesis/encoding/GateEncoder.cpp

@@ -189,7 +189,9 @@ void GateEncoder::assertSingleQubitGateConstraints(std::size_t pos) {
     DEBUG() << "Asserting gates on " << q;
     assertZConstraints(pos, q);
     assertXConstraints(pos, q);
+    if (! ignoreRChanges){
     assertRConstraints(pos, q);
+    }
   }
 }
 
@@ -200,8 +202,10 @@ void GateEncoder::assertTwoQubitGateConstraints(std::size_t pos) {
       if (ctrl == trgt) {
         continue;
       }
-      const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt) &&
-                           createTwoQubitRConstraint(pos, ctrl, trgt);
+      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;
     }

src/cliffordsynthesis/encoding/MultiGateEncoder.cpp

@@ -49,12 +49,18 @@ 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());
+
+    if(!ignoreRChanges){
+      lb->assertFormula(tvars->r[t + 1] == xorHelpers[t].back());
+    }
+
   }
 }
 

src/cliffordsynthesis/encoding/SATEncoder.cpp

@@ -55,17 +55,17 @@ void SATEncoder::createFormulation() {
                             ? 2U * N
                             : N;
 
-  tableauEncoder = std::make_shared<TableauEncoder>(N, s, T, lb);
+  tableauEncoder = std::make_shared<TableauEncoder>(N, s, T, lb, config.ignoreRChanges);
   tableauEncoder->createTableauVariables();
   tableauEncoder->assertTableau(*config.initialTableau, 0U);
   tableauEncoder->assertTableau(*config.targetTableau, T);
 
   if (config.useMultiGateEncoding) {
     gateEncoder = std::make_shared<MultiGateEncoder>(
-        N, s, T, tableauEncoder->getVariables(), lb, config.gateSet);
+                                                     N, s, T, tableauEncoder->getVariables(), lb, config.gateSet, config.ignoreRChanges);
   } else {
     gateEncoder = std::make_shared<SingleGateEncoder>(
-        N, s, T, tableauEncoder->getVariables(), lb, config.gateSet);
+                                                      N, s, T, tableauEncoder->getVariables(), lb, config.gateSet, config.ignoreRChanges);
   }
   gateEncoder->createSingleQubitGateVariables();
   gateEncoder->createTwoQubitGateVariables();
@@ -76,7 +76,7 @@ void SATEncoder::createFormulation() {
   }
 
   objectiveEncoder = std::make_shared<ObjectiveEncoder>(
-      N, T, gateEncoder->getVariables(), lb, config.gateSet);
+                                                        N, T, gateEncoder->getVariables(), lb, config.gateSet);
 
   if (config.gateLimit.has_value()) {
     objectiveEncoder->limitGateCount(*config.gateLimit, std::less_equal{});

src/cliffordsynthesis/encoding/TableauEncoder.cpp

@@ -17,7 +17,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 +35,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,8 +57,10 @@ 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,
@@ -67,9 +73,10 @@ 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);
 }