🔊 Allow to dump intermediate synthesis results (#243)

Author: burgholzer

include/cliffordsynthesis/Configuration.hpp

@@ -15,11 +15,13 @@ struct Configuration {
   Configuration() = default;
 
   /// General configuration for the synthesis algorithm
-  std::size_t    initialTimestepLimit = 0U;
-  bool           useMaxSAT            = false;
-  TargetMetric   target               = TargetMetric::Gates;
-  bool           useSymmetryBreaking  = true;
-  plog::Severity verbosity            = plog::Severity::warning;
+  std::size_t    initialTimestepLimit    = 0U;
+  bool           useMaxSAT               = false;
+  TargetMetric   target                  = TargetMetric::Gates;
+  bool           useSymmetryBreaking     = true;
+  bool           dumpIntermediateResults = false;
+  std::string    intermediateResultsPath = "./";
+  plog::Severity verbosity               = plog::Severity::warning;
 
   /// Settings for the SAT solver
   std::size_t nThreads = 1U;

mqt/qmap/bindings.cpp

@@ -421,6 +421,15 @@ PYBIND11_MODULE(pyqmap, m) {
                      &cs::Configuration::useSymmetryBreaking,
                      "Use symmetry breaking clauses to speed up the synthesis "
                      "process. Defaults to `true`.")
+      .def_readwrite("dump_intermediate_results",
+                     &cs::Configuration::dumpIntermediateResults,
+                     "Dump intermediate results of the synthesis process. "
+                     "Defaults to `false`.")
+      .def_readwrite("intermediate_results_path",
+                     &cs::Configuration::intermediateResultsPath,
+                     "Path to the directory where intermediate results should "
+                     "be dumped. Defaults to `./`. The path needs to include a "
+                     "path separator at the end.")
       .def_readwrite(
           "verbosity", &cs::Configuration::verbosity,
           "Verbosity level for the synthesis process. Defaults to 'warning'.")

mqt/qmap/pyqmap.pyi

@@ -321,8 +321,10 @@ class Verbosity:
     def value(self) -> int: ...
 
 class SynthesisConfiguration:
+    dump_intermediate_results: bool
     gate_limit_factor: float
     initial_timestep_limit: int
+    intermediate_results_path: str
     minimize_gates_after_depth_optimization: bool
     minimize_gates_after_two_qubit_gate_optimization: bool
     n_threads: int

src/cliffordsynthesis/CliffordSynthesizer.cpp

@@ -9,6 +9,7 @@
 #include "utils/logging.hpp"
 
 #include <chrono>
+#include <fstream>
 
 namespace cs {
 
@@ -345,8 +346,18 @@ void CliffordSynthesizer::runMaxSAT(const EncoderConfig& config) {
 
 Results CliffordSynthesizer::callSolver(const EncoderConfig& config) {
   ++solverCalls;
-  auto encoder = encoding::SATEncoder(config);
-  return encoder.run();
+  auto       encoder = encoding::SATEncoder(config);
+  const auto res     = encoder.run();
+  if (configuration.dumpIntermediateResults && res.sat()) {
+    const auto filename = configuration.intermediateResultsPath +
+                          "intermediate_" + std::to_string(solverCalls) +
+                          ".qasm";
+    INFO() << "Dumping circuit to " << filename;
+    std::ofstream file(filename);
+    file << res.getResultCircuit();
+    file.close();
+  }
+  return res;
 }
 
 void CliffordSynthesizer::updateResults(const Configuration& config,

test/cliffordsynthesis/test_synthesis.cpp

@@ -87,8 +87,9 @@ class SynthesisTest : public ::testing::TestWithParam<TestConfiguration> {
     }
     std::cout << "Target tableau:\n" << targetTableau;
 
-    config           = Configuration();
-    config.verbosity = plog::Severity::verbose;
+    config                         = Configuration();
+    config.verbosity               = plog::Severity::verbose;
+    config.dumpIntermediateResults = true;
   }
 
   void TearDown() override {