♻️ vendor logicblocks

.clang-tidy

@@ -14,6 +14,8 @@ Checks: |
   -cppcoreguidelines-special-member-functions,
   -cppcoreguidelines-avoid-magic-numbers,
   -cppcoreguidelines-macro-usage,
+  -cppcoreguidelines-pro-type-reinterpret-cast,
+  -cppcoreguidelines-pro-bounds-array-to-pointer-decay,
   google-*,
   -google-readability-todo,
   -google-build-using-namespace,

.gitmodules

@@ -2,7 +2,3 @@
 	path = extern/mqt-core
 	url = https://github.com/cda-tum/mqt-core.git
 	branch = main
-[submodule "extern/LogicBlocks"]
-	path = extern/LogicBlocks
-	url = https://github.com/cda-tum/LogicBlocks.git
-    branch = main

cmake/ExternalDependencies.cmake

@@ -6,7 +6,8 @@ set(FETCH_PACKAGES "")
 # search for Z3
 find_package(Z3 4.8.15)
 if(NOT Z3_FOUND)
-  message(WARNING "Did not find Z3. Exact library and other depending target will not be available")
+  message(
+    WARNING "Did not find Z3. Exact mapper and Clifford synthesis libraries will not be available")
 endif()
 
 if(BUILD_MQT_QMAP_BINDINGS)
@@ -52,20 +53,20 @@ else()
   endif()
 endif()
 
-set(BUILD_LB_TESTS
-    OFF
-    CACHE BOOL "Build LogicBlocks tests")
-set(FETCHCONTENT_SOURCE_DIR_LOGICBLOCKS
-    ${PROJECT_SOURCE_DIR}/extern/LogicBlocks
-    CACHE
-      PATH
-      "Path to the source directory of the LogicBlocks library. This variable is used by FetchContent to download the library if it is not already available."
-)
-FetchContent_Declare(
-  LogicBlocks
-  GIT_REPOSITORY https://github.com/cda-tum/LogicBlocks.git
-  GIT_TAG main)
-list(APPEND FETCH_PACKAGES LogicBlocks)
+set(PLOG_VERSION
+    1.1.10
+    CACHE STRING "Plog version")
+set(PLOG_URL https://github.com/SergiusTheBest/plog/archive/refs/tags/${PLOG_VERSION}.tar.gz)
+if(CMAKE_VERSION VERSION_GREATER_EQUAL 3.24)
+  FetchContent_Declare(plog URL ${PLOG_URL} FIND_PACKAGE_ARGS ${PLOG_VERSION})
+  list(APPEND FETCH_PACKAGES plog)
+else()
+  find_package(plog ${PLOG_VERSION} QUIET)
+  if(NOT plog_FOUND)
+    FetchContent_Declare(plog URL ${PLOG_URL})
+    list(APPEND FETCH_PACKAGES plog)
+  endif()
+endif()
 
 if(BUILD_MQT_QMAP_TESTS)
   set(gtest_force_shared_crt

include/cliffordsynthesis/CliffordSynthesizer.hpp

@@ -10,10 +10,13 @@
 #include "cliffordsynthesis/Results.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
 #include "cliffordsynthesis/encoding/SATEncoder.hpp"
+#include "plog/Log.h"
 
 #include <cstddef>
-#include <optional>
+#include <limits>
+#include <memory>
 #include <sstream>
+#include <utility>
 
 namespace cs {
 
@@ -103,47 +106,47 @@ class CliffordSynthesizer {
   template <typename T>
   void runBinarySearch(T& value, T lowerBound, T upperBound,
                        const EncoderConfig& config) {
-    INFO() << "Running binary search in range [" << lowerBound << ", "
-           << upperBound << ")";
+    PLOG_INFO << "Running binary search in range [" << lowerBound << ", "
+              << upperBound << ")";
 
     while (lowerBound != upperBound) {
       value = (lowerBound + upperBound) / 2;
-      INFO() << "Trying value " << value << " in range [" << lowerBound << ", "
-             << upperBound << ")";
+      PLOG_INFO << "Trying value " << value << " in range [" << lowerBound
+                << ", " << upperBound << ")";
       const auto r = callSolver(config);
       updateResults(configuration, r, results);
       if (r.sat()) {
         upperBound = value;
-        INFO() << "Found solution. New upper bound is " << upperBound;
+        PLOG_INFO << "Found solution. New upper bound is " << upperBound;
       } else {
         lowerBound = value + 1;
-        INFO() << "No solution found. New lower bound is " << lowerBound;
+        PLOG_INFO << "No solution found. New lower bound is " << lowerBound;
       }
     }
-    INFO() << "Found optimum: " << lowerBound;
+    PLOG_INFO << "Found optimum: " << lowerBound;
   }
 
   template <typename T>
   void runLinearSearch(T& value, T lowerBound, T upperBound,
                        const EncoderConfig& config) {
-    INFO() << "Running linear search in range [" << lowerBound << ", "
-           << upperBound << ")";
+    PLOG_INFO << "Running linear search in range [" << lowerBound << ", "
+              << upperBound << ")";
 
     if (upperBound == 0U) {
       upperBound = std::numeric_limits<std::size_t>::max();
     }
     for (value = lowerBound; value < upperBound; ++value) {
-      INFO() << "Trying value " << value << " in range [" << lowerBound << ", "
-             << upperBound << ")";
+      PLOG_INFO << "Trying value " << value << " in range [" << lowerBound
+                << ", " << upperBound << ")";
       const auto r = callSolver(config);
       updateResults(configuration, r, results);
       if (r.sat()) {
-        INFO() << "Found optimum " << value;
+        PLOG_INFO << "Found optimum " << value;
         return;
       }
-      INFO() << "No solution found. Trying next value.";
+      PLOG_INFO << "No solution found. Trying next value.";
     }
-    INFO() << "No solution found in given interval.";
+    PLOG_INFO << "No solution found in given interval.";
   }
 
   static std::shared_ptr<qc::QuantumComputation>

include/cliffordsynthesis/Results.hpp

@@ -6,8 +6,8 @@
 #pragma once
 
 #include "CircuitOptimizer.hpp"
-#include "LogicTerm/Logic.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
+#include "logicblocks/Logic.hpp"
 
 #include <nlohmann/json.hpp>
 #include <sstream>

include/cliffordsynthesis/Tableau.hpp

@@ -6,7 +6,7 @@
 #pragma once
 
 #include "QuantumComputation.hpp"
-#include "utils/logging.hpp"
+#include "plog/Log.h"
 
 #include <cstdint>
 #include <fstream>

include/cliffordsynthesis/encoding/GateEncoder.hpp

@@ -5,9 +5,9 @@
 
 #pragma once
 
-#include "LogicBlock/LogicBlock.hpp"
 #include "cliffordsynthesis/Results.hpp"
 #include "cliffordsynthesis/encoding/TableauEncoder.hpp"
+#include "logicblocks/LogicBlock.hpp"
 #include "operations/OpType.hpp"
 
 #include <cstddef>

include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp

@@ -25,8 +25,8 @@ class ObjectiveEncoder {
   template <class Op>
   void limitGateCount(const std::size_t maxGateCount, Op op,
                       const bool includeSingleQubitGates = true) const {
-    DEBUG() << "Limiting gate count to at most " << maxGateCount
-            << (includeSingleQubitGates ? "" : " two-qubit") << " gate(s)";
+    PLOG_DEBUG << "Limiting gate count to at most " << maxGateCount
+               << (includeSingleQubitGates ? "" : " two-qubit") << " gate(s)";
 
     const auto cost = collectGateCount(includeSingleQubitGates);
     lb->assertFormula(

include/cliffordsynthesis/encoding/SATEncoder.hpp

@@ -5,13 +5,13 @@
 
 #pragma once
 
-#include "LogicBlock/LogicBlock.hpp"
 #include "cliffordsynthesis/Configuration.hpp"
 #include "cliffordsynthesis/Results.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
 #include "cliffordsynthesis/encoding/GateEncoder.hpp"
 #include "cliffordsynthesis/encoding/ObjectiveEncoder.hpp"
 #include "cliffordsynthesis/encoding/TableauEncoder.hpp"
+#include "logicblocks/LogicBlock.hpp"
 #include "operations/OpType.hpp"
 
 #include <cstddef>

include/cliffordsynthesis/encoding/TableauEncoder.hpp

@@ -5,9 +5,9 @@
 
 #pragma once
 
-#include "LogicBlock/LogicBlock.hpp"
 #include "cliffordsynthesis/Results.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
+#include "logicblocks/LogicBlock.hpp"
 
 #include <cstddef>
 #include <memory>

include/configuration/Configuration.hpp

@@ -102,7 +102,6 @@ struct Configuration {
   bool          enableSwapLimits = true;
   SwapReduction swapReduction    = SwapReduction::CouplingLimit;
   std::size_t   swapLimit        = 0;
-  bool          useBDD           = false;
 
   [[nodiscard]] nlohmann::json json() const;
   [[nodiscard]] std::string    toString() const { return json().dump(2); }

include/logicblocks/Encodings.hpp

@@ -0,0 +1,67 @@
+#pragma once
+
+#include "LogicBlock.hpp"
+#include "LogicTerm.hpp"
+
+#include <cmath>
+#include <cstddef>
+#include <cstdint>
+#include <set>
+#include <utility>
+#include <vector>
+
+namespace encodings {
+
+using namespace logicbase;
+
+struct NestedVar {
+  explicit NestedVar(const LogicTerm& v) : var(v){};
+  NestedVar(const LogicTerm& v, std::vector<NestedVar> l)
+      : var(v), list(std::move(l)) {}
+  LogicTerm              var = LogicTerm::noneTerm();
+  std::vector<NestedVar> list;
+};
+
+struct WeightedVar {
+  WeightedVar(const LogicTerm& v, const int w) : var(v), weight(w) {}
+  LogicTerm var    = LogicTerm::noneTerm();
+  int       weight = 0;
+};
+inline bool operator<(const WeightedVar& rhs, const WeightedVar& lhs) {
+  return rhs.weight < lhs.weight;
+}
+inline bool operator==(const WeightedVar& rhs, const WeightedVar& lhs) {
+  return rhs.weight == lhs.weight && rhs.var.getID() == lhs.var.getID();
+}
+
+enum class Type : uint8_t { Uninitialized, AuxVar, ProgramVar };
+struct SavedLit {
+  SavedLit() : var(LogicTerm::noneTerm()) {}
+  SavedLit(Type t, const LogicTerm& v) : type(t), var(v) {}
+  Type      type = Type::Uninitialized;
+  LogicTerm var  = LogicTerm::noneTerm();
+};
+
+LogicTerm atMostOneCmdr(const std::vector<NestedVar>& subords,
+                        const LogicTerm& cmdrVar, LogicBlock* logic);
+
+LogicTerm exactlyOneCmdr(const std::vector<NestedVar>& subords,
+                         const LogicTerm& cmdrVar, LogicBlock* logic);
+
+LogicTerm naiveExactlyOne(const std::vector<LogicTerm>& clauseVars);
+
+LogicTerm naiveAtMostOne(const std::vector<LogicTerm>& clauseVars);
+
+LogicTerm naiveAtLeastOne(const std::vector<LogicTerm>& clauseVars);
+
+LogicTerm atMostOneBiMander(const std::vector<LogicTerm>& vars,
+                            LogicBlock*                   logic);
+
+std::vector<NestedVar> groupVars(const std::vector<LogicTerm>& vars,
+                                 std::size_t                   maxSize);
+std::vector<NestedVar> groupVarsAux(const std::vector<NestedVar>& vars,
+                                    std::size_t                   maxSize);
+
+std::vector<std::vector<LogicTerm>>
+groupVarsBimander(const std::vector<LogicTerm>& vars, std::size_t groupCount);
+} // namespace encodings