From bd7b7fde25cb0e5eb4fdcbf898f76b4790b68d41 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Tue, 7 Oct 2025 02:41:39 +0200
Subject: [PATCH 01/21] Main

---
 .../Support/BooleanLogic/ReadOnceBDD.h        | 113 +++++++
 .../lib/Support/BooleanLogic/CMakeLists.txt   |   1 +
 .../lib/Support/BooleanLogic/ReadOnceBDD.cpp  | 254 +++++++++++++++
 .../lib/Support/FtdImplementation.cpp         | 307 +++++++++++++++++-
 4 files changed, 666 insertions(+), 9 deletions(-)
 create mode 100644 experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
 create mode 100644 experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp

diff --git a/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h b/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
new file mode 100644
index 0000000000..6e72d6923a
--- /dev/null
+++ b/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
@@ -0,0 +1,113 @@
+//===--------- ReadOnceBDD.h - Read-once BDD --------------------*- C++ -*-===//
+//
+// Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a lightweight **Read-Once Binary Decision Diagram (BDD)**
+// builder and basic analysis utilities. It constructs a decision diagram for a
+// minimized boolean expression following a user-provided variable order. Each
+// internal node corresponds to one boolean variable with two outgoing edges
+// (false/true). Two terminal nodes (0 and 1) are always appended at the end.
+//
+// The class provides:
+//   * Construction from a minimized BoolExpression.
+//   * Traversal of a subgraph defined by a root and two designated sinks.
+//   * Enumeration of all 2-vertex cuts in that subgraph.
+//
+// This implementation assumes the expression is already minimized and
+// read-once compatible (no variable reused along any path).
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef EXPERIMENTAL_SUPPORT_BOOLEANLOGIC_READONCEBDD_H
+#define EXPERIMENTAL_SUPPORT_BOOLEANLOGIC_READONCEBDD_H
+
+#include <string>
+#include <utility>
+#include <vector>
+
+#include "experimental/Support/BooleanLogic/BDD.h"
+#include "experimental/Support/BooleanLogic/BoolExpression.h"
+#include "mlir/Support/LogicalResult.h"
+
+namespace dynamatic {
+namespace experimental {
+namespace boolean {
+
+/// One node of a read-once BDD.
+/// - `var`       : variable name (empty string for terminal nodes)
+/// - `falseSucc` : index of the successor if the variable evaluates to false
+/// - `trueSucc`  : index of the successor if the variable evaluates to true
+struct BDDNode {
+  std::string var;
+  unsigned falseSucc;
+  unsigned trueSucc;
+};
+
+/// Container for a Read-Once BDD.
+/// Each internal node is indexed by its position in the user-defined variable
+/// order. Two additional nodes at the end are the 0 and 1 terminals.
+class ReadOnceBDD {
+public:
+  /// Create an empty BDD.
+  ReadOnceBDD();
+
+  /// Build the BDD from a minimized boolean expression and a variable order.
+  /// Variables in `varOrder` that do not appear in the expression are ignored.
+  /// Returns `success()` on success, or `failure()` if the input is invalid.
+  mlir::LogicalResult
+  buildFromExpression(BoolExpression *expr,
+                      const std::vector<std::string> &varOrder);
+
+  /// Traverse the subgraph reachable from `root` until either `tTrue` or
+  /// `tFalse` (treated as local sinks). Aborts if any path reaches the global
+  /// 0/1 terminals prematurely. Returns the list of node indices in the
+  /// subgraph (sorted ascending, always including `root`, `tTrue`, `tFalse`).
+  std::vector<unsigned> collectSubgraph(unsigned root, unsigned tTrue,
+                                        unsigned tFalse) const;
+
+  /// Enumerate all 2-vertex cuts within the subgraph defined by
+  /// (root, tTrue, tFalse). Returns pairs sorted lexicographically
+  /// (first ascending, then second ascending).
+  std::vector<std::pair<unsigned, unsigned>>
+  listTwoVertexCuts(unsigned root, unsigned tTrue, unsigned tFalse) const;
+
+  /// Accessors
+  const std::vector<BDDNode> &getnodes() const { return nodes; }
+  unsigned root() const { return rootIndex; }
+  unsigned one() const { return oneIndex; }
+  unsigned zero() const { return zeroIndex; }
+
+private:
+  /// All nodes of the BDD: internal nodes first (following `order`),
+  /// then the 0 terminal, then the 1 terminal.
+  std::vector<BDDNode> nodes;
+
+  /// Variable order actually used to build the diagram (minimized & filtered).
+  std::vector<std::string> order;
+
+  /// Index of the BDD root node.
+  unsigned rootIndex = 0;
+  /// Index of the constant 0 terminal.
+  unsigned zeroIndex = 0;
+  /// Index of the constant 1 terminal.
+  unsigned oneIndex = 0;
+
+  /// Recursively expand edges for a node according to Shannon decomposition.
+  /// Avoids duplicating nodes by reusing existing indices.
+  void expandFrom(unsigned idx, BoolExpression *residual,
+                  std::vector<char> &expanded);
+
+  /// Helper: test whether banning nodes `a` and `b` disconnects both sinks.
+  bool sinksUnreachableIfBan(unsigned root, unsigned tTrue, unsigned tFalse,
+                             unsigned a, unsigned b) const;
+};
+
+} // namespace boolean
+} // namespace experimental
+} // namespace dynamatic
+
+#endif // EXPERIMENTAL_SUPPORT_BOOLEANLOGIC_READONCEBDD_H
\ No newline at end of file
diff --git a/experimental/lib/Support/BooleanLogic/CMakeLists.txt b/experimental/lib/Support/BooleanLogic/CMakeLists.txt
index c59e616dc0..92fdbeeaad 100644
--- a/experimental/lib/Support/BooleanLogic/CMakeLists.txt
+++ b/experimental/lib/Support/BooleanLogic/CMakeLists.txt
@@ -3,6 +3,7 @@ add_dynamatic_library(DynamaticExperimentalSupportBooleanLogic
   Lexer.cpp
   Parser.cpp
   BDD.cpp
+  ReadOnceBDD.cpp
 
   LINK_LIBS PRIVATE
   DynamaticSupportEspresso
diff --git a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
new file mode 100644
index 0000000000..df609a07aa
--- /dev/null
+++ b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
@@ -0,0 +1,254 @@
+//===- ReadOnceBDD.cpp - Read-Once BDD Implementation -----------*- C++ -*-===//
+//
+// Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file implements the construction and basic analysis of a **Read-Once
+// Binary Decision Diagram (BDD)**. It provides:
+//
+//  * Building a read-once BDD from a minimized BoolExpression and a user-
+//    defined variable order.
+//  * Traversing a subgraph defined by a root and two designated sink nodes.
+//  * Enumerating all 2-vertex cut pairs in the subgraph.
+//
+// Each internal node corresponds to a variable in the provided order. Two
+// terminal nodes (0 and 1) are always appended at the end. The implementation
+// assumes the boolean expression is already minimized and read-once compatible.
+//
+//===----------------------------------------------------------------------===//
+
+#include <algorithm>
+#include <functional>
+#include <set>
+#include <string>
+#include <vector>
+
+#include "experimental/Support/BooleanLogic/BDD.h"
+#include "experimental/Support/BooleanLogic/BoolExpression.h"
+#include "experimental/Support/BooleanLogic/ReadOnceBDD.h"
+#include "mlir/Support/LogicalResult.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace dynamatic::experimental::boolean;
+using namespace llvm;
+using namespace mlir;
+
+ReadOnceBDD::ReadOnceBDD() {
+  nodes.clear();
+  order.clear();
+  rootIndex = zeroIndex = oneIndex = 0;
+}
+
+LogicalResult
+ReadOnceBDD::buildFromExpression(BoolExpression *expr,
+                                 const std::vector<std::string> &varOrder) {
+  nodes.clear();
+  order.clear();
+  rootIndex = zeroIndex = oneIndex = 0;
+
+  if (!expr) {
+    llvm::errs() << "ReadOnceBDD: null expression\n";
+    return failure();
+  }
+
+  // Minimize the whole expression once before starting.
+  BoolExpression *rootExpr = expr->boolMinimize();
+
+  // If the expression itself is constant, build only two terminals.
+  if (rootExpr->type == ExpressionType::Zero ||
+      rootExpr->type == ExpressionType::One) {
+    nodes.resize(2);
+    zeroIndex = 0;
+    oneIndex = 1;
+    nodes[zeroIndex] = {"", zeroIndex, zeroIndex};
+    nodes[oneIndex] = {"", oneIndex, oneIndex};
+    rootIndex = (rootExpr->type == ExpressionType::One) ? oneIndex : zeroIndex;
+    return success();
+  }
+
+  // Keep only variables that still appear after minimization and respect
+  // the order provided by the user.
+  {
+    std::set<std::string> present = rootExpr->getVariables();
+    for (const auto &v : varOrder)
+      if (present.find(v) != present.end())
+        order.push_back(v);
+  }
+
+  // Pre-allocate all internal nodes; initially connect them to the terminals.
+  const unsigned n = (unsigned)order.size();
+  nodes.resize(n + 2);
+  zeroIndex = n;
+  oneIndex = n + 1;
+  for (unsigned i = 0; i < n; ++i)
+    nodes[i] = BDDNode{order[i], zeroIndex, oneIndex};
+  nodes[zeroIndex] = {"", zeroIndex, zeroIndex};
+  nodes[oneIndex] = {"", oneIndex, oneIndex};
+
+  // Root is always the first internal node (smallest variable index).
+  rootIndex = 0;
+
+  // Recursively expand edges from the root; mark each expanded node to
+  // avoid rebuilding the same subgraph.
+  std::vector<char> expanded(nodes.size(), 0);
+  expandFrom(rootIndex, rootExpr, expanded);
+
+  return success();
+}
+
+void ReadOnceBDD::expandFrom(unsigned idx, BoolExpression *residual,
+                             std::vector<char> &expanded) {
+  if (idx >= order.size() || expanded[idx])
+    return;
+
+  const std::string &var = order[idx];
+
+  // Perform Shannon decomposition for the current variable.
+  BoolExpression *f0 = residual->deepCopy();
+  restrict(f0, var, false);
+  f0 = f0->boolMinimize();
+  BoolExpression *f1 = residual->deepCopy();
+  restrict(f1, var, true);
+  f1 = f1->boolMinimize();
+
+  // Decide the next node index for each branch.
+  auto decideNext = [&](BoolExpression *f, unsigned &succ) {
+    if (!f) {
+      succ = zeroIndex;
+      return;
+    }
+    if (f->type == ExpressionType::Zero) {
+      succ = zeroIndex;
+      return;
+    }
+    if (f->type == ExpressionType::One) {
+      succ = oneIndex;
+      return;
+    }
+
+    // Find the earliest variable in the current order that appears in f.
+    auto vars = f->getVariables();
+    size_t vpos = order.size();
+    for (size_t i = 0; i < order.size(); ++i)
+      if (vars.find(order[i]) != vars.end()) {
+        vpos = i;
+        break;
+      }
+
+    succ = static_cast<unsigned>(vpos);
+  };
+
+  unsigned fSucc = zeroIndex, tSucc = oneIndex;
+  decideNext(f0, fSucc);
+  decideNext(f1, tSucc);
+
+  // Connect edges for the current node.
+  nodes[idx].falseSucc = fSucc;
+  nodes[idx].trueSucc = tSucc;
+
+  expanded[idx] = 1;
+
+  // Recurse only on unexplored internal successors.
+  if (fSucc < zeroIndex && !expanded[fSucc])
+    expandFrom(fSucc, f0, expanded);
+  if (tSucc < zeroIndex && !expanded[tSucc])
+    expandFrom(tSucc, f1, expanded);
+}
+
+std::vector<unsigned> ReadOnceBDD::collectSubgraph(unsigned root, unsigned t1,
+                                                   unsigned t0) const {
+  std::vector<char> vis(nodes.size(), 0);
+  std::vector<unsigned> st{root};
+  std::vector<unsigned> subgraph;
+
+  while (!st.empty()) {
+    unsigned u = st.back();
+    st.pop_back();
+    if (u >= nodes.size() || vis[u])
+      continue;
+    vis[u] = 1;
+    subgraph.push_back(u);
+
+    // Stop expansion at the designated local sinks.
+    if (u == t1 || u == t0)
+      continue;
+
+    // Abort if we accidentally reach the global terminals.
+    if (u == zeroIndex || u == oneIndex) {
+      llvm::errs() << "Illegal subgraph: reached global terminal\n";
+      std::abort();
+    }
+
+    const auto &nd = nodes[u];
+    st.push_back(nd.falseSucc);
+    st.push_back(nd.trueSucc);
+  }
+
+  // Ensure both sinks appear in the final list.
+  if (std::find(subgraph.begin(), subgraph.end(), t1) == subgraph.end())
+    subgraph.push_back(t1);
+  if (std::find(subgraph.begin(), subgraph.end(), t0) == subgraph.end())
+    subgraph.push_back(t0);
+
+  std::sort(subgraph.begin(), subgraph.end());
+  return subgraph;
+}
+
+bool ReadOnceBDD::sinksUnreachableIfBan(unsigned root, unsigned t1, unsigned t0,
+                                        unsigned a, unsigned b) const {
+  std::vector<char> vis(nodes.size(), 0);
+  std::vector<unsigned> st{root};
+
+  auto push = [&](unsigned v) {
+    if (v == a || v == b)
+      return; // skip banned nodes
+    if (v < nodes.size() && !vis[v])
+      st.push_back(v);
+  };
+
+  while (!st.empty()) {
+    unsigned u = st.back();
+    st.pop_back();
+    if (u >= nodes.size() || vis[u] || u == a || u == b)
+      continue;
+    vis[u] = 1;
+
+    // Reaching either sink means the cut fails.
+    if (u == t1 || u == t0)
+      return false;
+
+    const auto &nd = nodes[u];
+    push(nd.falseSucc);
+    push(nd.trueSucc);
+  }
+  // Neither sink reachable → valid cut.
+  return true;
+}
+
+std::vector<std::pair<unsigned, unsigned>>
+ReadOnceBDD::listTwoVertexCuts(unsigned root, unsigned t1, unsigned t0) const {
+  // Collect and validate the subgraph (sorted, includes root/t1/t0).
+  std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
+  std::vector<std::pair<unsigned, unsigned>> cuts;
+
+  // Scan all pairs in ascending order.
+  for (size_t i = 1; i < cand.size() - 2; ++i) {
+    for (size_t j = i + 1; j < cand.size(); ++j) {
+      if (sinksUnreachableIfBan(root, t1, t0, cand[i], cand[j])) {
+        cuts.emplace_back(cand[i], cand[j]);
+      }
+    }
+  }
+
+  // Sort lexicographically by (first, second).
+  std::sort(cuts.begin(), cuts.end(), [](const auto &a, const auto &b) {
+    if (a.first != b.first)
+      return a.first < b.first;
+    return a.second < b.second;
+  });
+
+  return cuts;
+}
\ No newline at end of file
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index c7ca948a71..4548f07fe0 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -17,6 +17,7 @@
 #include "dynamatic/Support/Backedge.h"
 #include "experimental/Support/BooleanLogic/BDD.h"
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
+#include "experimental/Support/BooleanLogic/ReadOnceBDD.h"
 #include "experimental/Support/FtdSupport.h"
 #include "mlir/Analysis/CFGLoopInfo.h"
 #include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h"
@@ -291,7 +292,7 @@ static BoolExpression *getBlockLoopExitCondition(Block *loopExit, CFGLoop *loop,
 /// Run the Cytron algorithm to determine, give a set of values, in which blocks
 /// should we add a merge in order for those values to be merged
 static DenseSet<Block *>
-runCrytonAlgorithm(Region &funcRegion, DenseMap<Block *, Value> &inputBlocks) {
+runCytronAlgorithm(Region &funcRegion, DenseMap<Block *, Value> &inputBlocks) {
   // Get dominance frontier
   auto dominanceFrontier = getDominanceFrontier(funcRegion);
 
@@ -394,7 +395,7 @@ LogicalResult experimental::ftd::createPhiNetwork(
 
   // In which block a new phi is necessary
   DenseSet<Block *> blocksToAddPhi =
-      runCrytonAlgorithm(funcRegion, inputBlocks);
+      runCytronAlgorithm(funcRegion, inputBlocks);
 
   // A backedge is created for each block in `blocksToAddPhi`, and it will
   // contain the value used as placeholder for the phi
@@ -766,6 +767,275 @@ static bool isWhileLoop(CFGLoop *loop) {
          !llvm::is_contained(latchBlocks, headerBlock);
 }
 
+// Build a mux tree for a BDD sub-region (start → {trueSink,falseSink}).
+// - Validate the region (must not hit global 0/1 before the two sinks).
+// - Enumerate 2-vertex-cuts (sorted asc).
+// - Build a mux chain: select of mux[i] = output of mux[i-1]; mux[0] uses
+//   the `start` condition. Pair placement:
+//     * terminal endpoint -> constant 0/1;
+//     * if u→v (or v→u) then successor side is constant (true/false edge);
+//     * else use the largest common predecessor P: P.trueSucc goes to true.
+//       If no common predecessor, place min→false, max→true.
+// - Recurse for non-constant inputs; the sinks for recursion are the next
+//   pair’s two original endpoints (constants mapped to global Z/O).
+static Value
+buildMuxTree(PatternRewriter &rewriter, Block *block,
+             const ftd::BlockIndexing &bi,
+             const dynamatic::experimental::boolean::ReadOnceBDD &bdd,
+             unsigned startIdx, unsigned trueSinkIdx, unsigned falseSinkIdx) {
+
+  const auto &nodes = bdd.getnodes();
+  const unsigned N = (unsigned)nodes.size();
+  const unsigned Z = bdd.zero(), O = bdd.one();
+
+  auto valid = [&](unsigned x) { return x < N; };
+  if (!valid(startIdx) || !valid(trueSinkIdx) || !valid(falseSinkIdx)) {
+    llvm::errs() << "BddToCircuit: invalid region indices.\n";
+    return nullptr;
+  }
+
+  // Map a variable to its selection value (channelified i1).
+  auto getSel = [&](const std::string &varName) -> Value {
+    auto condBlkOpt = bi.getBlockFromCondition(varName);
+    if (!condBlkOpt.has_value()) {
+      llvm::errs() << "BddToCircuit: cannot map condition '" << varName
+                   << "'.\n";
+      return nullptr;
+    }
+    Value s = condBlkOpt.value()->getTerminator()->getOperand(0);
+    s.setType(ftd::channelifyType(s.getType()));
+    return s;
+  };
+
+  // Channelified i1 constants.
+  auto makeConst = [&](bool v) -> Value {
+    rewriter.setInsertionPointToStart(block);
+    auto src = rewriter.create<handshake::SourceOp>(
+        block->getOperations().front().getLoc());
+    auto i1 = rewriter.getIntegerType(1);
+    auto cst = rewriter.create<handshake::ConstantOp>(
+        block->getOperations().front().getLoc(),
+        rewriter.getIntegerAttr(i1, v ? 1 : 0), src.getResult());
+    cst->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr());
+    return cst.getResult();
+  };
+
+  // Optional inversion for a selection.
+  auto maybeNot = [&](Value sel, bool invert) -> Value {
+    if (!invert)
+      return sel;
+    rewriter.setInsertionPointToStart(block);
+    auto notOp = rewriter.create<handshake::NotOp>(
+        block->getOperations().front().getLoc(),
+        ftd::channelifyType(sel.getType()), sel);
+    notOp->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr());
+    return notOp.getResult();
+  };
+
+  // Region validation: treat (trueSink,falseSink) as local sinks.
+  auto validateSub = [&]() -> bool {
+    std::vector<char> vis(N, 0);
+    std::vector<unsigned> st{startIdx};
+    while (!st.empty()) {
+      unsigned u = st.back();
+      st.pop_back();
+      if (!valid(u) || vis[u])
+        continue;
+      vis[u] = 1;
+      if (u == trueSinkIdx || u == falseSinkIdx)
+        continue;
+      if (u == Z || u == O) {
+        llvm::errs() << "Illegal subgraph: hit global terminal before sinks.\n";
+        return false;
+      }
+      st.push_back(nodes[u].falseSucc);
+      st.push_back(nodes[u].trueSucc);
+    }
+    return true;
+  };
+  if (!validateSub())
+    std::abort();
+
+  // Predecessor lists for placement decisions.
+  auto preds = [&]() {
+    std::vector<std::vector<unsigned>> p(N);
+    for (unsigned i = 0; i < N; ++i) {
+      const auto &n = nodes[i];
+      if (n.falseSucc < N)
+        p[n.falseSucc].push_back(i);
+      if (n.trueSucc < N && n.trueSucc != n.falseSucc)
+        p[n.trueSucc].push_back(i);
+    }
+    return p;
+  }();
+
+  struct InputSpec {
+    bool isConst = false, constVal = false;
+    unsigned nodeIdx = 0;
+  };
+
+  auto decideInputsForPair =
+      [&](unsigned u, unsigned v) -> std::pair<InputSpec, InputSpec> {
+    auto nodeToSpec = [&](unsigned idx) -> InputSpec {
+      if (idx == Z)
+        return {true, false, 0};
+      if (idx == O)
+        return {true, true, 0};
+      return {false, false, idx};
+    };
+    auto edge = [&](unsigned a, unsigned b) -> int {
+      if (nodes[a].trueSucc == b)
+        return +1;
+      if (nodes[a].falseSucc == b)
+        return 0;
+      return -1;
+    };
+
+    InputSpec A = nodeToSpec(u), B = nodeToSpec(v);
+
+    // Direct edge → successor becomes constant (true/false edge).
+    if (!A.isConst && !B.isConst) {
+      int uv = edge(u, v), vu = edge(v, u);
+      if (uv != -1 && vu == -1) {
+        B.isConst = true;
+        B.constVal = (uv == +1);
+      } else if (vu != -1 && uv == -1) {
+        A.isConst = true;
+        A.constVal = (vu == +1);
+      }
+    }
+
+    // Largest common predecessor decides who goes to true.
+    unsigned chosenP = (unsigned)-1;
+    for (unsigned pu : preds[u])
+      for (unsigned pv : preds[v])
+        if (pu == pv && (chosenP == (unsigned)-1 || pu > chosenP))
+          chosenP = pu;
+
+    InputSpec inF, inT;
+    if (chosenP != (unsigned)-1) {
+      if (!A.isConst && nodes[chosenP].trueSucc == A.nodeIdx)
+        inT = A, inF = B;
+      else if (!B.isConst && nodes[chosenP].trueSucc == B.nodeIdx)
+        inT = B, inF = A;
+      else {
+        if (u < v)
+          inF = A, inT = B;
+        else
+          inF = B, inT = A;
+      }
+    } else {
+      if (u < v)
+        inF = A, inT = B;
+      else
+        inF = B, inT = A;
+    }
+    return {inF, inT};
+  };
+
+  // 2-cut pairs (sorted).
+  auto pairs = bdd.listTwoVertexCuts(startIdx, trueSinkIdx, falseSinkIdx);
+
+  // No pair → no mux; return `start` condition (maybe inverted).
+  if (pairs.empty()) {
+    bool dir = (nodes[startIdx].trueSucc == trueSinkIdx &&
+                nodes[startIdx].falseSucc == falseSinkIdx);
+    bool inv = (nodes[startIdx].trueSucc == falseSinkIdx &&
+                nodes[startIdx].falseSucc == trueSinkIdx);
+    if (!dir && !inv) {
+      llvm::errs() << "BddToCircuit: no pair but start doesn't map to sinks.\n";
+      return nullptr;
+    }
+    Value sel = getSel(nodes[startIdx].var);
+    if (!sel)
+      return nullptr;
+    return maybeNot(sel, inv);
+  }
+
+  Value c0 = makeConst(false);
+  Value c1 = makeConst(true);
+
+  struct MuxSpec {
+    unsigned u, v;
+    InputSpec inF, inT;
+    Value select, out;
+    Operation *op = nullptr;
+  };
+  std::vector<MuxSpec> chain;
+  chain.reserve(pairs.size());
+
+  for (auto [u, v] : pairs) {
+    auto [inF, inT] = decideInputsForPair(u, v);
+    chain.push_back(
+        MuxSpec{u, v, inF, inT, /*select*/ nullptr, /*out*/ nullptr, nullptr});
+  }
+
+  // First select = start condition; others chain from previous out.
+  chain[0].select = getSel(nodes[startIdx].var);
+  if (!chain[0].select)
+    return nullptr;
+
+  for (size_t i = 0; i < chain.size(); ++i) {
+    if (i > 0)
+      chain[i].select = chain[i - 1].out;
+
+    Value inF = chain[i].inF.isConst ? (chain[i].inF.constVal ? c1 : c0)
+                                     : c0; // placeholder
+    Value inT = chain[i].inT.isConst ? (chain[i].inT.constVal ? c1 : c0)
+                                     : c0; // placeholder
+
+    rewriter.setInsertionPointToStart(block);
+    auto mux = rewriter.create<handshake::MuxOp>(
+        block->getOperations().front().getLoc(), c0.getType(), chain[i].select,
+        ValueRange{inF, inT});
+    mux->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr());
+
+    chain[i].op = mux.getOperation();
+    chain[i].out = mux.getResult();
+  }
+
+  // Fill variable inputs by recursion; sinks come from the next pair.
+  auto setOpnd = [&](Operation *op, int pos, Value v) {
+    op->setOperand(pos, v);
+  };
+
+  for (size_t i = 0; i < chain.size(); ++i) {
+    unsigned subF = falseSinkIdx, subT = trueSinkIdx;
+    if (i + 1 < chain.size()) {
+      subF = chain[i + 1].inF.isConst ? (chain[i + 1].inF.constVal ? O : Z)
+                                      : chain[i + 1].inF.nodeIdx;
+      subT = chain[i + 1].inT.isConst ? (chain[i + 1].inT.constVal ? O : Z)
+                                      : chain[i + 1].inT.nodeIdx;
+    }
+
+    if (!chain[i].inF.isConst) {
+      unsigned s = chain[i].inF.nodeIdx;
+      Value sub = buildMuxTree(rewriter, block, bi, bdd, s, subT, subF);
+      if (!sub)
+        return nullptr;
+      setOpnd(chain[i].op, /*1:false*/ 1, sub);
+    }
+    if (!chain[i].inT.isConst) {
+      unsigned s = chain[i].inT.nodeIdx;
+      Value sub = buildMuxTree(rewriter, block, bi, bdd, s, subT, subF);
+      if (!sub)
+        return nullptr;
+      setOpnd(chain[i].op, /*2:true*/ 2, sub);
+    }
+  }
+
+  return chain.back().out;
+}
+
+// Top-level: full BDD (root → {1,0}).
+static Value
+ReadOnceBDDToCircuit(PatternRewriter &rewriter, Block *block,
+                     const ftd::BlockIndexing &bi,
+                     const dynamatic::experimental::boolean::ReadOnceBDD &bdd) {
+  return buildMuxTree(rewriter, block, bi, bdd, bdd.root(), bdd.one(),
+                      bdd.zero());
+}
+
 using PairOperandConsumer = std::pair<Value, Operation *>;
 
 /// Insert a branch to the correct position, taking into account whether it
@@ -826,12 +1096,21 @@ static Value addSuppressionInLoop(PatternRewriter &rewriter, CFGLoop *loop,
     // Sort the cofactors alphabetically
     std::sort(cofactorList.begin(), cofactorList.end());
 
-    // Apply a BDD expansion to the loop exit expression and the list of
-    // cofactors
-    BDD *bdd = buildBDD(fLoopExit, cofactorList);
+    // // Apply a BDD expansion to the loop exit expression and the list of
+    // // cofactors
+    // BDD *bdd = buildBDD(fLoopExit, cofactorList);
+
+    // // Convert the boolean expression obtained through BDD to a circuit
+    // Value branchCond = bddToCircuit(rewriter, bdd, loopExit, bi);
 
-    // Convert the boolean expression obtained through BDD to a circuit
-    Value branchCond = bddToCircuit(rewriter, bdd, loopExit, bi);
+    // Build read-once BDD on the loop-exit condition and lower to mux chain
+    ReadOnceBDD ro;
+    if (failed(ro.buildFromExpression(fLoopExit, cofactorList))) {
+      llvm::errs() << "ReadOnceBDD: buildFromExpression failed in "
+                      "addSuppressionInLoop.\n";
+      std::abort();
+    }
+    Value branchCond = ReadOnceBDDToCircuit(rewriter, loopExit, bi, ro);
 
     Operation *loopTerminator = loopExit->getTerminator();
     assert(isa<cf::CondBranchOp>(loopTerminator) &&
@@ -936,8 +1215,18 @@ static void insertDirectSuppression(
     std::set<std::string> blocks = fSup->getVariables();
 
     std::vector<std::string> cofactorList(blocks.begin(), blocks.end());
-    BDD *bdd = buildBDD(fSup, cofactorList);
-    Value branchCond = bddToCircuit(rewriter, bdd, consumer->getBlock(), bi);
+    // BDD *bdd = buildBDD(fSup, cofactorList);
+    // Value branchCond = bddToCircuit(rewriter, bdd, consumer->getBlock(), bi);
+
+    // Build read-once BDD and lower to mux tree
+    ReadOnceBDD ro;
+    if (failed(ro.buildFromExpression(fSup, cofactorList))) {
+      llvm::errs() << "ReadOnceBDD: buildFromExpression failed in "
+                      "insertDirectSuppression.\n";
+      std::abort();
+    }
+    Value branchCond =
+        ReadOnceBDDToCircuit(rewriter, consumer->getBlock(), bi, ro);
 
     rewriter.setInsertionPointToStart(consumer->getBlock());
     auto branchOp = rewriter.create<handshake::ConditionalBranchOp>(

From ea2ec1b105e3de6e705cc867591f0ed11fe160a8 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Wed, 8 Oct 2025 01:11:09 +0200
Subject: [PATCH 02/21] Main Update

---
 .../Support/BooleanLogic/ReadOnceBDD.h        |   5 +
 .../lib/Support/BooleanLogic/ReadOnceBDD.cpp  |  24 +-
 .../lib/Support/FtdImplementation.cpp         | 245 ++++++++----------
 3 files changed, 130 insertions(+), 144 deletions(-)

diff --git a/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h b/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
index 6e72d6923a..db0e894341 100644
--- a/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
+++ b/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
@@ -41,10 +41,12 @@ namespace boolean {
 /// - `var`       : variable name (empty string for terminal nodes)
 /// - `falseSucc` : index of the successor if the variable evaluates to false
 /// - `trueSucc`  : index of the successor if the variable evaluates to true
+/// - `preds`     : indices of all predecessor nodes that point to this node
 struct BDDNode {
   std::string var;
   unsigned falseSucc;
   unsigned trueSucc;
+  std::vector<unsigned> preds;
 };
 
 /// Container for a Read-Once BDD.
@@ -77,6 +79,9 @@ class ReadOnceBDD {
 
   /// Accessors
   const std::vector<BDDNode> &getnodes() const { return nodes; }
+  const std::vector<unsigned> &getpreds(unsigned idx) const {
+    return nodes[idx].preds;
+  }
   unsigned root() const { return rootIndex; }
   unsigned one() const { return oneIndex; }
   unsigned zero() const { return zeroIndex; }
diff --git a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
index df609a07aa..6c625854df 100644
--- a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
@@ -42,9 +42,8 @@ ReadOnceBDD::ReadOnceBDD() {
   rootIndex = zeroIndex = oneIndex = 0;
 }
 
-LogicalResult
-ReadOnceBDD::buildFromExpression(BoolExpression *expr,
-                                 const std::vector<std::string> &varOrder) {
+LogicalResult ReadOnceBDD::buildFromExpression(BoolExpression *expr,
+                           const std::vector<std::string> &varOrder) {
   nodes.clear();
   order.clear();
   rootIndex = zeroIndex = oneIndex = 0;
@@ -84,9 +83,9 @@ ReadOnceBDD::buildFromExpression(BoolExpression *expr,
   zeroIndex = n;
   oneIndex = n + 1;
   for (unsigned i = 0; i < n; ++i)
-    nodes[i] = BDDNode{order[i], zeroIndex, oneIndex};
-  nodes[zeroIndex] = {"", zeroIndex, zeroIndex};
-  nodes[oneIndex] = {"", oneIndex, oneIndex};
+    nodes[i] = BDDNode{order[i], zeroIndex, oneIndex, {}};
+  nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
+  nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
 
   // Root is always the first internal node (smallest variable index).
   rootIndex = 0;
@@ -95,6 +94,14 @@ ReadOnceBDD::buildFromExpression(BoolExpression *expr,
   // avoid rebuilding the same subgraph.
   std::vector<char> expanded(nodes.size(), 0);
   expandFrom(rootIndex, rootExpr, expanded);
+  
+  // After the BDD is fully built, clean up each node's predecessor list:
+  // sort in ascending order and remove any duplicates.
+  for (auto &nd : nodes) {
+    auto &ps = nd.preds;
+    std::sort(ps.begin(), ps.end());
+    ps.erase(std::unique(ps.begin(), ps.end()), ps.end());
+  }
 
   return success();
 }
@@ -149,6 +156,11 @@ void ReadOnceBDD::expandFrom(unsigned idx, BoolExpression *residual,
   nodes[idx].falseSucc = fSucc;
   nodes[idx].trueSucc = tSucc;
 
+  // While expanding the BDD, record the current node `idx`
+  // as a predecessor of each of its false/true successors.
+  nodes[fSucc].preds.push_back(idx);
+  nodes[tSucc].preds.push_back(idx);
+
   expanded[idx] = 1;
 
   // Recurse only on unexplored internal successors.
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 4548f07fe0..566337b4a6 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -767,34 +767,30 @@ static bool isWhileLoop(CFGLoop *loop) {
          !llvm::is_contained(latchBlocks, headerBlock);
 }
 
-// Build a mux tree for a BDD sub-region (start → {trueSink,falseSink}).
-// - Validate the region (must not hit global 0/1 before the two sinks).
-// - Enumerate 2-vertex-cuts (sorted asc).
-// - Build a mux chain: select of mux[i] = output of mux[i-1]; mux[0] uses
-//   the `start` condition. Pair placement:
-//     * terminal endpoint -> constant 0/1;
-//     * if u→v (or v→u) then successor side is constant (true/false edge);
-//     * else use the largest common predecessor P: P.trueSucc goes to true.
-//       If no common predecessor, place min→false, max→true.
-// - Recurse for non-constant inputs; the sinks for recursion are the next
-//   pair’s two original endpoints (constants mapped to global Z/O).
-static Value
-buildMuxTree(PatternRewriter &rewriter, Block *block,
-             const ftd::BlockIndexing &bi,
-             const dynamatic::experimental::boolean::ReadOnceBDD &bdd,
+/// Build a MUX tree for a read-once BDD subgraph delimited by
+///   startIdx  ->  {trueSinkIdx, falseSinkIdx}.
+/// Strategy:
+///   1) Enumerate all start–{true,false} two-vertex cuts (u,v) in ascending order,
+///      each cut instantiates one MUX stage.
+///   2) Input placement per pair (u,v):
+///        • Choose the largest common predecessor P of {u,v}.
+///          Whichever endpoint equals P.trueSucc goes to the TRUE input;
+///          the other goes to FALSE.
+///        • If u and v are adjacent, the latter one's input is a terminal constant
+///          (true-edge -> 1, false-edge -> 0).
+///   3) Chain the MUXes: select(mux[0]) is the start condition; for i>0,
+///      select(mux[i]) = out(mux[i-1]).
+///   4) For non-constant inputs, recurse on the corresponding sub-region;
+///      the recursion’s sinks are the next vertex-cut pair or the subgraph's sinks.
+static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
+             const ftd::BlockIndexing &bi, const ReadOnceBDD &bdd,
              unsigned startIdx, unsigned trueSinkIdx, unsigned falseSinkIdx) {
 
   const auto &nodes = bdd.getnodes();
-  const unsigned N = (unsigned)nodes.size();
-  const unsigned Z = bdd.zero(), O = bdd.one();
+  const unsigned numNodes = (unsigned)nodes.size();
 
-  auto valid = [&](unsigned x) { return x < N; };
-  if (!valid(startIdx) || !valid(trueSinkIdx) || !valid(falseSinkIdx)) {
-    llvm::errs() << "BddToCircuit: invalid region indices.\n";
-    return nullptr;
-  }
-
-  // Map a variable to its selection value (channelified i1).
+  // Look up the boolean signal for a given condition variable name and
+  // return it as the select input of a mux (converted to a handshake channel).
   auto getSel = [&](const std::string &varName) -> Value {
     auto condBlkOpt = bi.getBlockFromCondition(varName);
     if (!condBlkOpt.has_value()) {
@@ -807,7 +803,8 @@ buildMuxTree(PatternRewriter &rewriter, Block *block,
     return s;
   };
 
-  // Channelified i1 constants.
+  // Create a handshake boolean constant (0 or 1) as a channel signal.
+  // The returned Value can be connected directly to a mux input.
   auto makeConst = [&](bool v) -> Value {
     rewriter.setInsertionPointToStart(block);
     auto src = rewriter.create<handshake::SourceOp>(
@@ -832,57 +829,29 @@ buildMuxTree(PatternRewriter &rewriter, Block *block,
     return notOp.getResult();
   };
 
-  // Region validation: treat (trueSink,falseSink) as local sinks.
-  auto validateSub = [&]() -> bool {
-    std::vector<char> vis(N, 0);
-    std::vector<unsigned> st{startIdx};
-    while (!st.empty()) {
-      unsigned u = st.back();
-      st.pop_back();
-      if (!valid(u) || vis[u])
-        continue;
-      vis[u] = 1;
-      if (u == trueSinkIdx || u == falseSinkIdx)
-        continue;
-      if (u == Z || u == O) {
-        llvm::errs() << "Illegal subgraph: hit global terminal before sinks.\n";
-        return false;
-      }
-      st.push_back(nodes[u].falseSucc);
-      st.push_back(nodes[u].trueSucc);
-    }
-    return true;
-  };
-  if (!validateSub())
-    std::abort();
-
-  // Predecessor lists for placement decisions.
-  auto preds = [&]() {
-    std::vector<std::vector<unsigned>> p(N);
-    for (unsigned i = 0; i < N; ++i) {
-      const auto &n = nodes[i];
-      if (n.falseSucc < N)
-        p[n.falseSucc].push_back(i);
-      if (n.trueSucc < N && n.trueSucc != n.falseSucc)
-        p[n.trueSucc].push_back(i);
-    }
-    return p;
-  }();
-
+  // Describes one mux data input:
+  //  - isConst  : true if this input is a boolean constant
+  //  - constVal : value of the constant if isConst == true
+  //  - nodeIdx  : BDD node index if this input is driven by a variable
   struct InputSpec {
     bool isConst = false, constVal = false;
     unsigned nodeIdx = 0;
   };
 
+  // Decide how to connect the two endpoints (u, v) of a cut pair
+  // to the false/true inputs of a mux.
   auto decideInputsForPair =
       [&](unsigned u, unsigned v) -> std::pair<InputSpec, InputSpec> {
+    
+    // Convert a BDD node index to an InputSpec.
     auto nodeToSpec = [&](unsigned idx) -> InputSpec {
-      if (idx == Z)
-        return {true, false, 0};
-      if (idx == O)
-        return {true, true, 0};
       return {false, false, idx};
     };
+
+    // Check whether there is a direct edge from node a to node b:
+    //  +1 if a.trueSucc == b (true edge)
+    //   0 if a.falseSucc == b (false edge)
+    //  -1 if no direct edge from a to b
     auto edge = [&](unsigned a, unsigned b) -> int {
       if (nodes[a].trueSucc == b)
         return +1;
@@ -891,49 +860,42 @@ buildMuxTree(PatternRewriter &rewriter, Block *block,
       return -1;
     };
 
+    // Wrap the two cut endpoints into InputSpec objects.
     InputSpec A = nodeToSpec(u), B = nodeToSpec(v);
 
-    // Direct edge → successor becomes constant (true/false edge).
-    if (!A.isConst && !B.isConst) {
-      int uv = edge(u, v), vu = edge(v, u);
-      if (uv != -1 && vu == -1) {
-        B.isConst = true;
-        B.constVal = (uv == +1);
-      } else if (vu != -1 && uv == -1) {
-        A.isConst = true;
-        A.constVal = (vu == +1);
-      }
+    // Direct edge -> successor becomes constant.
+    int uv = edge(u, v), vu = edge(v, u);
+    if (uv != -1 && vu == -1) {
+      B.isConst = true;
+      B.constVal = (uv == +1);
+    } else if (vu != -1 && uv == -1) {
+      A.isConst = true;
+      A.constVal = (vu == +1);
     }
 
     // Largest common predecessor decides who goes to true.
-    unsigned chosenP = (unsigned)-1;
-    for (unsigned pu : preds[u])
-      for (unsigned pv : preds[v])
-        if (pu == pv && (chosenP == (unsigned)-1 || pu > chosenP))
-          chosenP = pu;
-
-    InputSpec inF, inT;
-    if (chosenP != (unsigned)-1) {
-      if (!A.isConst && nodes[chosenP].trueSucc == A.nodeIdx)
-        inT = A, inF = B;
-      else if (!B.isConst && nodes[chosenP].trueSucc == B.nodeIdx)
-        inT = B, inF = A;
-      else {
-        if (u < v)
-          inF = A, inT = B;
-        else
-          inF = B, inT = A;
+    // nodes[].preds are already sorted in ascending order.
+    unsigned chosenP = 0;
+    const auto &predU = nodes[u].preds;
+    const auto &predV = nodes[v].preds;
+    size_t iu = 0, iv = 0;
+    while (iu < predU.size() && iv < predV.size()) {
+      if (predU[iu] == predV[iv]) {
+        if (predU[iu] > chosenP) 
+          chosenP = predU[iu];
+        ++iu; ++iv;
+      } else if (predU[iu] < predV[iv]) {
+        ++iu;
+      } else {
+        ++iv;
       }
-    } else {
-      if (u < v)
-        inF = A, inT = B;
-      else
-        inF = B, inT = A;
     }
-    return {inF, inT};
+
+    return (nodes[chosenP].trueSucc == B.nodeIdx) ? std::pair{A,B}
+                                                  : std::pair{B,A};
   };
 
-  // 2-cut pairs (sorted).
+  // 2-vertex-cut pairs (sorted).
   auto pairs = bdd.listTwoVertexCuts(startIdx, trueSinkIdx, falseSinkIdx);
 
   // No pair → no mux; return `start` condition (maybe inverted).
@@ -943,7 +905,7 @@ buildMuxTree(PatternRewriter &rewriter, Block *block,
     bool inv = (nodes[startIdx].trueSucc == falseSinkIdx &&
                 nodes[startIdx].falseSucc == trueSinkIdx);
     if (!dir && !inv) {
-      llvm::errs() << "BddToCircuit: no pair but start doesn't map to sinks.\n";
+      llvm::errs() << "BddToCircuit: start node doesn't map to sinks.\n";
       return nullptr;
     }
     Value sel = getSel(nodes[startIdx].var);
@@ -952,86 +914,93 @@ buildMuxTree(PatternRewriter &rewriter, Block *block,
     return maybeNot(sel, inv);
   }
 
+  // Create handshake constants for Boolean false and true
   Value c0 = makeConst(false);
   Value c1 = makeConst(true);
 
+  // Specification of one Mux stage
   struct MuxSpec {
-    unsigned u, v;
     InputSpec inF, inT;
     Value select, out;
     Operation *op = nullptr;
   };
-  std::vector<MuxSpec> chain;
-  chain.reserve(pairs.size());
+
+  // Build the list of mux stages from the given vertex-cut pairs
+  std::vector<MuxSpec> muxChain;
+  muxChain.reserve(pairs.size());
 
   for (auto [u, v] : pairs) {
     auto [inF, inT] = decideInputsForPair(u, v);
-    chain.push_back(
-        MuxSpec{u, v, inF, inT, /*select*/ nullptr, /*out*/ nullptr, nullptr});
+    muxChain.push_back(MuxSpec{inF, inT, nullptr, nullptr, nullptr});
   }
 
-  // First select = start condition; others chain from previous out.
-  chain[0].select = getSel(nodes[startIdx].var);
-  if (!chain[0].select)
+  // The first mux select signal comes from the starting variable
+  // Later muxes will use the previous mux output as select
+  muxChain[0].select = getSel(nodes[startIdx].var);
+  if (!muxChain[0].select)
     return nullptr;
 
-  for (size_t i = 0; i < chain.size(); ++i) {
+  // Create each mux with partial inputs; real variable inputs will be filled later
+  for (size_t i = 0; i < muxChain.size(); ++i) {
     if (i > 0)
-      chain[i].select = chain[i - 1].out;
+      muxChain[i].select = muxChain[i - 1].out;
 
-    Value inF = chain[i].inF.isConst ? (chain[i].inF.constVal ? c1 : c0)
-                                     : c0; // placeholder
-    Value inT = chain[i].inT.isConst ? (chain[i].inT.constVal ? c1 : c0)
-                                     : c0; // placeholder
+    Value inF = muxChain[i].inF.isConst ? (muxChain[i].inF.constVal ? c1 : c0)
+                                        : c0; // placeholder
+    Value inT = muxChain[i].inT.isConst ? (muxChain[i].inT.constVal ? c1 : c0)
+                                        : c0; // placeholder
 
     rewriter.setInsertionPointToStart(block);
     auto mux = rewriter.create<handshake::MuxOp>(
-        block->getOperations().front().getLoc(), c0.getType(), chain[i].select,
-        ValueRange{inF, inT});
+        block->getOperations().front().getLoc(), c0.getType(),
+        muxChain[i].select, ValueRange{inF, inT});
     mux->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr());
 
-    chain[i].op = mux.getOperation();
-    chain[i].out = mux.getResult();
+    muxChain[i].op = mux.getOperation();
+    muxChain[i].out = mux.getResult();
   }
 
-  // Fill variable inputs by recursion; sinks come from the next pair.
+  // Helper lambda to set an operand of an operation at the given position
   auto setOpnd = [&](Operation *op, int pos, Value v) {
     op->setOperand(pos, v);
   };
 
-  for (size_t i = 0; i < chain.size(); ++i) {
+  // Fill real inputs for each mux by recursion
+  // False/true sinks default to global sinks; if there is a next mux, use its inputs
+  for (size_t i = 0; i < muxChain.size(); ++i) {
     unsigned subF = falseSinkIdx, subT = trueSinkIdx;
-    if (i + 1 < chain.size()) {
-      subF = chain[i + 1].inF.isConst ? (chain[i + 1].inF.constVal ? O : Z)
-                                      : chain[i + 1].inF.nodeIdx;
-      subT = chain[i + 1].inT.isConst ? (chain[i + 1].inT.constVal ? O : Z)
-                                      : chain[i + 1].inT.nodeIdx;
+    if (i + 1 < muxChain.size()) {
+      subF = muxChain[i + 1].inF.nodeIdx;
+      subT = muxChain[i + 1].inT.nodeIdx;
     }
 
-    if (!chain[i].inF.isConst) {
-      unsigned s = chain[i].inF.nodeIdx;
+    if (!muxChain[i].inF.isConst) {
+      unsigned s = muxChain[i].inF.nodeIdx;
       Value sub = buildMuxTree(rewriter, block, bi, bdd, s, subT, subF);
       if (!sub)
         return nullptr;
-      setOpnd(chain[i].op, /*1:false*/ 1, sub);
+      // operand index 1 = false
+      setOpnd(muxChain[i].op, 1, sub);
     }
-    if (!chain[i].inT.isConst) {
-      unsigned s = chain[i].inT.nodeIdx;
+    if (!muxChain[i].inT.isConst) {
+      unsigned s = muxChain[i].inT.nodeIdx;
       Value sub = buildMuxTree(rewriter, block, bi, bdd, s, subT, subF);
       if (!sub)
         return nullptr;
-      setOpnd(chain[i].op, /*2:true*/ 2, sub);
+      // operand index 2 = true
+      setOpnd(muxChain[i].op, 2, sub);
     }
   }
 
-  return chain.back().out;
+  // Return the output of the last mux in the chain
+  return muxChain.back().out;
 }
 
-// Top-level: full BDD (root → {1,0}).
-static Value
-ReadOnceBDDToCircuit(PatternRewriter &rewriter, Block *block,
-                     const ftd::BlockIndexing &bi,
-                     const dynamatic::experimental::boolean::ReadOnceBDD &bdd) {
+/// Convert the entire read-once BDD into a circuit by invoking buildMuxTree
+/// on the BDD root with terminal nodes {one, zero}. The result is a MUX tree
+/// in which each variable appears exactly once.
+static Value ReadOnceBDDToCircuit(PatternRewriter &rewriter, Block *block,
+                      const ftd::BlockIndexing &bi, const ReadOnceBDD &bdd) {
   return buildMuxTree(rewriter, block, bi, bdd, bdd.root(), bdd.one(),
                       bdd.zero());
 }

From 2a21222407c8e2c2ca5dece3fd2938d6cf1d17cd Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Wed, 8 Oct 2025 01:13:24 +0200
Subject: [PATCH 03/21] Main Update

---
 .../lib/Support/BooleanLogic/ReadOnceBDD.cpp  |  7 ++--
 .../lib/Support/FtdImplementation.cpp         | 33 +++++++++++--------
 2 files changed, 24 insertions(+), 16 deletions(-)

diff --git a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
index 6c625854df..9d9717a798 100644
--- a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
@@ -42,8 +42,9 @@ ReadOnceBDD::ReadOnceBDD() {
   rootIndex = zeroIndex = oneIndex = 0;
 }
 
-LogicalResult ReadOnceBDD::buildFromExpression(BoolExpression *expr,
-                           const std::vector<std::string> &varOrder) {
+LogicalResult
+ReadOnceBDD::buildFromExpression(BoolExpression *expr,
+                                 const std::vector<std::string> &varOrder) {
   nodes.clear();
   order.clear();
   rootIndex = zeroIndex = oneIndex = 0;
@@ -94,7 +95,7 @@ LogicalResult ReadOnceBDD::buildFromExpression(BoolExpression *expr,
   // avoid rebuilding the same subgraph.
   std::vector<char> expanded(nodes.size(), 0);
   expandFrom(rootIndex, rootExpr, expanded);
-  
+
   // After the BDD is fully built, clean up each node's predecessor list:
   // sort in ascending order and remove any duplicates.
   for (auto &nd : nodes) {
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 566337b4a6..dfdbaa55e3 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -770,21 +770,25 @@ static bool isWhileLoop(CFGLoop *loop) {
 /// Build a MUX tree for a read-once BDD subgraph delimited by
 ///   startIdx  ->  {trueSinkIdx, falseSinkIdx}.
 /// Strategy:
-///   1) Enumerate all start–{true,false} two-vertex cuts (u,v) in ascending order,
+///   1) Enumerate all start–{true,false} two-vertex cuts (u,v) in ascending
+///   order,
 ///      each cut instantiates one MUX stage.
 ///   2) Input placement per pair (u,v):
 ///        • Choose the largest common predecessor P of {u,v}.
 ///          Whichever endpoint equals P.trueSucc goes to the TRUE input;
 ///          the other goes to FALSE.
-///        • If u and v are adjacent, the latter one's input is a terminal constant
+///        • If u and v are adjacent, the latter one's input is a terminal
+///        constant
 ///          (true-edge -> 1, false-edge -> 0).
 ///   3) Chain the MUXes: select(mux[0]) is the start condition; for i>0,
 ///      select(mux[i]) = out(mux[i-1]).
 ///   4) For non-constant inputs, recurse on the corresponding sub-region;
-///      the recursion’s sinks are the next vertex-cut pair or the subgraph's sinks.
+///      the recursion’s sinks are the next vertex-cut pair or the subgraph's
+///      sinks.
 static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
-             const ftd::BlockIndexing &bi, const ReadOnceBDD &bdd,
-             unsigned startIdx, unsigned trueSinkIdx, unsigned falseSinkIdx) {
+                          const ftd::BlockIndexing &bi, const ReadOnceBDD &bdd,
+                          unsigned startIdx, unsigned trueSinkIdx,
+                          unsigned falseSinkIdx) {
 
   const auto &nodes = bdd.getnodes();
   const unsigned numNodes = (unsigned)nodes.size();
@@ -842,7 +846,6 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   // to the false/true inputs of a mux.
   auto decideInputsForPair =
       [&](unsigned u, unsigned v) -> std::pair<InputSpec, InputSpec> {
-    
     // Convert a BDD node index to an InputSpec.
     auto nodeToSpec = [&](unsigned idx) -> InputSpec {
       return {false, false, idx};
@@ -881,9 +884,10 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     size_t iu = 0, iv = 0;
     while (iu < predU.size() && iv < predV.size()) {
       if (predU[iu] == predV[iv]) {
-        if (predU[iu] > chosenP) 
+        if (predU[iu] > chosenP)
           chosenP = predU[iu];
-        ++iu; ++iv;
+        ++iu;
+        ++iv;
       } else if (predU[iu] < predV[iv]) {
         ++iu;
       } else {
@@ -891,8 +895,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
       }
     }
 
-    return (nodes[chosenP].trueSucc == B.nodeIdx) ? std::pair{A,B}
-                                                  : std::pair{B,A};
+    return (nodes[chosenP].trueSucc == B.nodeIdx) ? std::pair{A, B}
+                                                  : std::pair{B, A};
   };
 
   // 2-vertex-cut pairs (sorted).
@@ -940,7 +944,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   if (!muxChain[0].select)
     return nullptr;
 
-  // Create each mux with partial inputs; real variable inputs will be filled later
+  // Create each mux with partial inputs; real variable inputs will be filled
+  // later
   for (size_t i = 0; i < muxChain.size(); ++i) {
     if (i > 0)
       muxChain[i].select = muxChain[i - 1].out;
@@ -966,7 +971,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   };
 
   // Fill real inputs for each mux by recursion
-  // False/true sinks default to global sinks; if there is a next mux, use its inputs
+  // False/true sinks default to global sinks; if there is a next mux, use its
+  // inputs
   for (size_t i = 0; i < muxChain.size(); ++i) {
     unsigned subF = falseSinkIdx, subT = trueSinkIdx;
     if (i + 1 < muxChain.size()) {
@@ -1000,7 +1006,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
 /// on the BDD root with terminal nodes {one, zero}. The result is a MUX tree
 /// in which each variable appears exactly once.
 static Value ReadOnceBDDToCircuit(PatternRewriter &rewriter, Block *block,
-                      const ftd::BlockIndexing &bi, const ReadOnceBDD &bdd) {
+                                  const ftd::BlockIndexing &bi,
+                                  const ReadOnceBDD &bdd) {
   return buildMuxTree(rewriter, block, bi, bdd, bdd.root(), bdd.one(),
                       bdd.zero());
 }

From 24c9af293d14118d0b30b418b59e64b6ac51e118 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Wed, 8 Oct 2025 01:32:48 +0200
Subject: [PATCH 04/21] Main Update

---
 .../experimental/Support/BooleanLogic/ReadOnceBDD.h       | 2 +-
 experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp     | 8 ++++----
 experimental/lib/Support/FtdImplementation.cpp            | 1 -
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h b/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
index db0e894341..d70e3a2f30 100644
--- a/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
+++ b/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
@@ -101,7 +101,7 @@ class ReadOnceBDD {
   /// Index of the constant 1 terminal.
   unsigned oneIndex = 0;
 
-  /// Recursively expand edges for a node according to Shannon decomposition.
+  /// Recursively expand edges for a node according to Shannon expansion.
   /// Avoids duplicating nodes by reusing existing indices.
   void expandFrom(unsigned idx, BoolExpression *residual,
                   std::vector<char> &expanded);
diff --git a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
index 9d9717a798..4671096ef8 100644
--- a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
@@ -63,8 +63,8 @@ ReadOnceBDD::buildFromExpression(BoolExpression *expr,
     nodes.resize(2);
     zeroIndex = 0;
     oneIndex = 1;
-    nodes[zeroIndex] = {"", zeroIndex, zeroIndex};
-    nodes[oneIndex] = {"", oneIndex, oneIndex};
+    nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
+    nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
     rootIndex = (rootExpr->type == ExpressionType::One) ? oneIndex : zeroIndex;
     return success();
   }
@@ -114,7 +114,7 @@ void ReadOnceBDD::expandFrom(unsigned idx, BoolExpression *residual,
 
   const std::string &var = order[idx];
 
-  // Perform Shannon decomposition for the current variable.
+  // Perform Shannon expansion for the current variable.
   BoolExpression *f0 = residual->deepCopy();
   restrict(f0, var, false);
   f0 = f0->boolMinimize();
@@ -237,7 +237,7 @@ bool ReadOnceBDD::sinksUnreachableIfBan(unsigned root, unsigned t1, unsigned t0,
     push(nd.falseSucc);
     push(nd.trueSucc);
   }
-  // Neither sink reachable → valid cut.
+  // Neither sink reachable -> valid cut.
   return true;
 }
 
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index dfdbaa55e3..a4a0ccbf67 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -791,7 +791,6 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
                           unsigned falseSinkIdx) {
 
   const auto &nodes = bdd.getnodes();
-  const unsigned numNodes = (unsigned)nodes.size();
 
   // Look up the boolean signal for a given condition variable name and
   // return it as the select input of a mux (converted to a handshake channel).

From ae15fb36c9724c8db25f98a79f2a1c7930e014c5 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Wed, 8 Oct 2025 01:52:53 +0200
Subject: [PATCH 05/21] Update

---
 experimental/lib/Support/FtdImplementation.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index a4a0ccbf67..6ee817e781 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -777,9 +777,8 @@ static bool isWhileLoop(CFGLoop *loop) {
 ///        • Choose the largest common predecessor P of {u,v}.
 ///          Whichever endpoint equals P.trueSucc goes to the TRUE input;
 ///          the other goes to FALSE.
-///        • If u and v are adjacent, the latter one's input is a terminal
-///        constant
-///          (true-edge -> 1, false-edge -> 0).
+///        • If u and v are adjacent, the successive one's input is a terminal
+///        constant (true-edge -> 1, false-edge -> 0).
 ///   3) Chain the MUXes: select(mux[0]) is the start condition; for i>0,
 ///      select(mux[i]) = out(mux[i-1]).
 ///   4) For non-constant inputs, recurse on the corresponding sub-region;

From c9422bd71eaff72d38fbe2616781d9ffc977748e Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Wed, 8 Oct 2025 23:23:29 +0200
Subject: [PATCH 06/21] Fix Bug

---
 experimental/lib/Support/FtdImplementation.cpp | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 6ee817e781..d7b8548cab 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -953,6 +953,20 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     Value inT = muxChain[i].inT.isConst ? (muxChain[i].inT.constVal ? c1 : c0)
                                         : c0; // placeholder
 
+    // Override constants for the last mux if an input is exactly a terminal
+    // node. This ignores inF/inT.constVal and uses the terminal identity
+    // instead.
+    if (i + 1 == muxChain.size()) {
+      if (muxChain[i].inF.nodeIdx == bdd.one())
+        inF = c1;
+      else if (muxChain[i].inF.nodeIdx == bdd.zero())
+        inF = c0;
+      if (muxChain[i].inT.nodeIdx == bdd.one())
+        inT = c1;
+      else if (muxChain[i].inT.nodeIdx == bdd.zero())
+        inT = c0;
+    }
+
     rewriter.setInsertionPointToStart(block);
     auto mux = rewriter.create<handshake::MuxOp>(
         block->getOperations().front().getLoc(), c0.getType(),

From f96fe31a96fb074a611ee85ae2c9699e8a1b625e Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Thu, 9 Oct 2025 18:52:33 +0200
Subject: [PATCH 07/21] Add condition

---
 experimental/lib/Support/FtdImplementation.cpp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index d7b8548cab..1b57f0495c 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -902,14 +902,29 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
 
   // No pair → no mux; return `start` condition (maybe inverted).
   if (pairs.empty()) {
+    // Root is a terminal: return constant value 1/0.
+    if (startIdx == trueSinkIdx)
+      return makeConst(true);
+    if (startIdx == falseSinkIdx)
+      return makeConst(false);
+
     bool dir = (nodes[startIdx].trueSucc == trueSinkIdx &&
                 nodes[startIdx].falseSucc == falseSinkIdx);
     bool inv = (nodes[startIdx].trueSucc == falseSinkIdx &&
                 nodes[startIdx].falseSucc == trueSinkIdx);
+
     if (!dir && !inv) {
       llvm::errs() << "BddToCircuit: start node doesn't map to sinks.\n";
+      llvm::errs() << "  Summary\n";
+      llvm::errs() << "    nodes.size = " << nodes.size() << "\n";
+      llvm::errs() << "    startIdx   = " << startIdx << "\n";
+      llvm::errs() << "    trueSinkIdx  = " << trueSinkIdx  << "\n";
+      llvm::errs() << "    falseSinkIdx = " << falseSinkIdx << "\n";
+      llvm::errs() << "    trueSucc  = " << nodes[startIdx].trueSucc << "\n";
+      llvm::errs() << "    falseSucc = " << nodes[startIdx].falseSucc << "\n";
       return nullptr;
     }
+
     Value sel = getSel(nodes[startIdx].var);
     if (!sel)
       return nullptr;

From 7119233983b48c2cbc99bd3c486d9e06781154a9 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Thu, 9 Oct 2025 19:04:55 +0200
Subject: [PATCH 08/21] Update

---
 experimental/lib/Support/FtdImplementation.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 1b57f0495c..0a51208505 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -918,7 +918,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
       llvm::errs() << "  Summary\n";
       llvm::errs() << "    nodes.size = " << nodes.size() << "\n";
       llvm::errs() << "    startIdx   = " << startIdx << "\n";
-      llvm::errs() << "    trueSinkIdx  = " << trueSinkIdx  << "\n";
+      llvm::errs() << "    trueSinkIdx  = " << trueSinkIdx << "\n";
       llvm::errs() << "    falseSinkIdx = " << falseSinkIdx << "\n";
       llvm::errs() << "    trueSucc  = " << nodes[startIdx].trueSucc << "\n";
       llvm::errs() << "    falseSucc = " << nodes[startIdx].falseSucc << "\n";

From 75fb8f109008e2581398fce721f7a6f5342e99c8 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Tue, 4 Nov 2025 22:03:24 +0100
Subject: [PATCH 09/21] Merge BDD files

---
 .../experimental/Support/BooleanLogic/BDD.h   | 129 +++++--
 .../Support/BooleanLogic/ReadOnceBDD.h        | 118 -------
 experimental/lib/Support/BooleanLogic/BDD.cpp | 333 ++++++++++++++++--
 .../lib/Support/BooleanLogic/CMakeLists.txt   |   1 -
 .../lib/Support/BooleanLogic/ReadOnceBDD.cpp  | 267 --------------
 .../lib/Support/FtdImplementation.cpp         |  93 +----
 6 files changed, 422 insertions(+), 519 deletions(-)
 delete mode 100644 experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
 delete mode 100644 experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp

diff --git a/experimental/include/experimental/Support/BooleanLogic/BDD.h b/experimental/include/experimental/Support/BooleanLogic/BDD.h
index 52c7fffc88..12a0013359 100644
--- a/experimental/include/experimental/Support/BooleanLogic/BDD.h
+++ b/experimental/include/experimental/Support/BooleanLogic/BDD.h
@@ -1,4 +1,4 @@
-//===- BDD.h - BDD Decomposition for Bool Expressions --*-- C++ -*-===//
+//===- BDD.h - BDD construction and analysis --------------------*- C++ -*-===//
 //
 // Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,46 +6,123 @@
 //
 //===----------------------------------------------------------------------===//
 //
-// This file defines the functions for performing a BDD decomposition on
-// boolean logic expression, following a specific order of variables.
+// This file provides a Binary Decision Diagram (BDD) builder and
+// basic analysis utilities. A user-specified variable
+// order is respected.
+//
+// Provided functionality:
+//   * Construction from a minimized BoolExpression and a variable order.
+//   * Reduction to a canonical Reduced Ordered BDD (ROBDD).
+//   * Traversal of a subgraph with a designated root and two designated sinks.
+//   * Enumeration of every vertex pair that covers all paths from the root to
+//     either sink inside that subgraph.
+//
+// This implementation assumes the expression is already minimized.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef DYNAMATIC_SUPPORT_BDD_H
 #define DYNAMATIC_SUPPORT_BDD_H
 
+#include <string>
+#include <utility>
+#include <vector>
+
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
-#include <optional>
+#include "mlir/Support/LogicalResult.h"
 
 namespace dynamatic {
 namespace experimental {
 namespace boolean {
 
-/// A BDD is a tree which represents a boolean expression by considering all the
-/// outcomes of the expression as a decision tree, with two edges (positive and
-/// negative) for each non terminal node. Each node is charaterized by a boolean
-/// variable and possibly 2 subsequent nodes, stored into `successors`
-struct BDD {
-  // First element is the `negative` branch; second is the `positive` branch
-  std::optional<std::pair<BDD *, BDD *>> successors;
-  BoolExpression *boolVariable;
-
-  /// Build a BDD node with two descendents
-  BDD(BDD *ni, BDD *pi, BoolExpression *bv)
-      : successors({ni, pi}), boolVariable(bv) {}
-
-  /// Build a leaf
-  BDD(BoolExpression *bv) : boolVariable(bv) {}
-};
-
-/// Replaces a boolean variable in a boolean expression with the specified truth
-/// value
+/// Replaces a boolean variable in a boolean expression with a truth value.
 void restrict(BoolExpression *exp, const std::string &var,
               bool expressionValue);
 
-/// Build a BDD out of an expression, by relying on the order of variables
-/// provided
-BDD *buildBDD(BoolExpression *exp, std::vector<std::string> variableList);
+/// One node of a reduced ordered BDD (ROBDD).
+/// var       : variable name (empty for terminals)
+/// falseSucc : successor index when var evaluates to false
+/// trueSucc  : successor index when var evaluates to true
+/// preds     : indices of all predecessor nodes that point to this node
+struct BDDNode {
+  std::string var;
+  unsigned falseSucc;
+  unsigned trueSucc;
+  std::vector<unsigned> preds;
+};
+
+/// Container for a reduced ordered BDD built from a BoolExpression.
+/// Each internal node is indexed by its position in the user-defined variable
+/// order. Two additional nodes at the end are the 0 and 1 terminals.
+class BDD {
+public:
+  /// Create an empty BDD.
+  BDD();
+
+  /// Build a tree-structured ordered BDD reflecting Shannon expansion from a
+  /// minimized boolean expression and a variable order. Variables in `varOrder`
+  /// that do not appear in the expression are ignored. Returns `success()` on
+  /// success, or `failure()` if the input is invalid.
+  mlir::LogicalResult
+  buildOBDDTreeFromExpression(BoolExpression *expr,
+                              const std::vector<std::string> &varOrder);
+
+  /// Build an ROBDD from a minimized boolean expression and a variable order.
+  /// Variables in `varOrder` that do not appear in the expression are ignored.
+  /// Returns `success()` on success, or `failure()` if the input is invalid.
+  ///
+  /// This is a simple method that assumes each variable appears only once in
+  /// the BDD, which matches the case of checking whether a basic block in the
+  /// CFG can be reached.
+  mlir::LogicalResult
+  buildROBDDFromExpression(BoolExpression *expr,
+                           const std::vector<std::string> &varOrder);
+
+  /// Traverse the subgraph reachable from `root` until either `tTrue` or
+  /// `tFalse` (treated as local sinks). Aborts if any path reaches the global
+  /// 0/1 terminals prematurely. Returns the list of node indices in the
+  /// subgraph (sorted ascending, always including `root`, `tTrue`, `tFalse`).
+  std::vector<unsigned> collectSubgraph(unsigned root, unsigned tTrue,
+                                        unsigned tFalse) const;
+
+  /// Enumerate all pairs of vertices that cover all paths within the subgraph
+  /// defined by (root, tTrue, tFalse). Returns pairs sorted lexicographically
+  /// (first ascending, then second ascending).
+  std::vector<std::pair<unsigned, unsigned>>
+  listPathCoveringPairs(unsigned root, unsigned tTrue, unsigned tFalse) const;
+
+  /// Accessors.
+  const std::vector<BDDNode> &getnodes() const { return nodes; }
+  const std::vector<unsigned> &getpreds(unsigned idx) const {
+    return nodes[idx].preds;
+  }
+  unsigned root() const { return rootIndex; }
+  unsigned one() const { return oneIndex; }
+  unsigned zero() const { return zeroIndex; }
+  const std::vector<std::string> &getOrder() const { return order; }
+
+private:
+  /// Storage: internal nodes first, then terminals zeroIndex and oneIndex.
+  std::vector<BDDNode> nodes;
+
+  /// Variable order used to build the diagram (minimized & filtered).
+  std::vector<std::string> order;
+
+  /// Index of the BDD root node.
+  unsigned rootIndex = 0;
+  /// Index of the constant 0 terminal.
+  unsigned zeroIndex = 0;
+  /// Index of the constant 1 terminal.
+  unsigned oneIndex = 0;
+
+  /// Build an OBDD via Shannon expansion per the filtered order.
+  void expandFrom(unsigned idx, BoolExpression *residual,
+                  std::vector<char> &expanded);
+
+  /// Helper: test whether nodes `a` and `b` cover all paths.
+  bool pairCoverAllPaths(unsigned root, unsigned tTrue, unsigned tFalse,
+                         unsigned a, unsigned b) const;
+};
 
 } // namespace boolean
 } // namespace experimental
diff --git a/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h b/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
deleted file mode 100644
index d70e3a2f30..0000000000
--- a/experimental/include/experimental/Support/BooleanLogic/ReadOnceBDD.h
+++ /dev/null
@@ -1,118 +0,0 @@
-//===--------- ReadOnceBDD.h - Read-once BDD --------------------*- C++ -*-===//
-//
-// Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-//
-// This file defines a lightweight **Read-Once Binary Decision Diagram (BDD)**
-// builder and basic analysis utilities. It constructs a decision diagram for a
-// minimized boolean expression following a user-provided variable order. Each
-// internal node corresponds to one boolean variable with two outgoing edges
-// (false/true). Two terminal nodes (0 and 1) are always appended at the end.
-//
-// The class provides:
-//   * Construction from a minimized BoolExpression.
-//   * Traversal of a subgraph defined by a root and two designated sinks.
-//   * Enumeration of all 2-vertex cuts in that subgraph.
-//
-// This implementation assumes the expression is already minimized and
-// read-once compatible (no variable reused along any path).
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef EXPERIMENTAL_SUPPORT_BOOLEANLOGIC_READONCEBDD_H
-#define EXPERIMENTAL_SUPPORT_BOOLEANLOGIC_READONCEBDD_H
-
-#include <string>
-#include <utility>
-#include <vector>
-
-#include "experimental/Support/BooleanLogic/BDD.h"
-#include "experimental/Support/BooleanLogic/BoolExpression.h"
-#include "mlir/Support/LogicalResult.h"
-
-namespace dynamatic {
-namespace experimental {
-namespace boolean {
-
-/// One node of a read-once BDD.
-/// - `var`       : variable name (empty string for terminal nodes)
-/// - `falseSucc` : index of the successor if the variable evaluates to false
-/// - `trueSucc`  : index of the successor if the variable evaluates to true
-/// - `preds`     : indices of all predecessor nodes that point to this node
-struct BDDNode {
-  std::string var;
-  unsigned falseSucc;
-  unsigned trueSucc;
-  std::vector<unsigned> preds;
-};
-
-/// Container for a Read-Once BDD.
-/// Each internal node is indexed by its position in the user-defined variable
-/// order. Two additional nodes at the end are the 0 and 1 terminals.
-class ReadOnceBDD {
-public:
-  /// Create an empty BDD.
-  ReadOnceBDD();
-
-  /// Build the BDD from a minimized boolean expression and a variable order.
-  /// Variables in `varOrder` that do not appear in the expression are ignored.
-  /// Returns `success()` on success, or `failure()` if the input is invalid.
-  mlir::LogicalResult
-  buildFromExpression(BoolExpression *expr,
-                      const std::vector<std::string> &varOrder);
-
-  /// Traverse the subgraph reachable from `root` until either `tTrue` or
-  /// `tFalse` (treated as local sinks). Aborts if any path reaches the global
-  /// 0/1 terminals prematurely. Returns the list of node indices in the
-  /// subgraph (sorted ascending, always including `root`, `tTrue`, `tFalse`).
-  std::vector<unsigned> collectSubgraph(unsigned root, unsigned tTrue,
-                                        unsigned tFalse) const;
-
-  /// Enumerate all 2-vertex cuts within the subgraph defined by
-  /// (root, tTrue, tFalse). Returns pairs sorted lexicographically
-  /// (first ascending, then second ascending).
-  std::vector<std::pair<unsigned, unsigned>>
-  listTwoVertexCuts(unsigned root, unsigned tTrue, unsigned tFalse) const;
-
-  /// Accessors
-  const std::vector<BDDNode> &getnodes() const { return nodes; }
-  const std::vector<unsigned> &getpreds(unsigned idx) const {
-    return nodes[idx].preds;
-  }
-  unsigned root() const { return rootIndex; }
-  unsigned one() const { return oneIndex; }
-  unsigned zero() const { return zeroIndex; }
-
-private:
-  /// All nodes of the BDD: internal nodes first (following `order`),
-  /// then the 0 terminal, then the 1 terminal.
-  std::vector<BDDNode> nodes;
-
-  /// Variable order actually used to build the diagram (minimized & filtered).
-  std::vector<std::string> order;
-
-  /// Index of the BDD root node.
-  unsigned rootIndex = 0;
-  /// Index of the constant 0 terminal.
-  unsigned zeroIndex = 0;
-  /// Index of the constant 1 terminal.
-  unsigned oneIndex = 0;
-
-  /// Recursively expand edges for a node according to Shannon expansion.
-  /// Avoids duplicating nodes by reusing existing indices.
-  void expandFrom(unsigned idx, BoolExpression *residual,
-                  std::vector<char> &expanded);
-
-  /// Helper: test whether banning nodes `a` and `b` disconnects both sinks.
-  bool sinksUnreachableIfBan(unsigned root, unsigned tTrue, unsigned tFalse,
-                             unsigned a, unsigned b) const;
-};
-
-} // namespace boolean
-} // namespace experimental
-} // namespace dynamatic
-
-#endif // EXPERIMENTAL_SUPPORT_BOOLEANLOGIC_READONCEBDD_H
\ No newline at end of file
diff --git a/experimental/lib/Support/BooleanLogic/BDD.cpp b/experimental/lib/Support/BooleanLogic/BDD.cpp
index 6135b0b311..3686a3695e 100644
--- a/experimental/lib/Support/BooleanLogic/BDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/BDD.cpp
@@ -1,4 +1,4 @@
-//===- BDD.cpp - BDD Decomposition for Bool Expressions -----*----- C++ -*-===//
+//===- BDD.cpp - BDD construction and analysis ------------------*- C++ -*-===//
 //
 // Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,20 +6,37 @@
 //
 //===----------------------------------------------------------------------===//
 //
-// This file implements the functions for performing a BDD decomposition on
-// boolean logic expression, following a specific order of variables.
+// This file implements construction of a Binary Decision Diagram (BDD) from a
+// BoolExpression and basic analysis utilities. It provides:
+//
+//  * Building a reduced ordered BDD from a minimized BoolExpression and a user-
+//    defined variable order.
+//  * Traversing a subgraph defined by a designated root and two designated
+//    sinks.
+//  * Enumerating every vertex pair that covers all paths in the subgraph.
+//
+// Each internal node corresponds to a variable in the provided order. Two
+// terminal nodes (0 and 1) are always appended at the end. The implementation
+// assumes the boolean expression is already minimized and read-once compatible.
 //
 //===----------------------------------------------------------------------===//
 
 #include "experimental/Support/BooleanLogic/BDD.h"
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
 
-#include <iterator>
+#include <algorithm>
+#include <functional>
+#include <set>
 #include <string>
+#include <unordered_map>
 #include <vector>
 
+#include "mlir/Support/LogicalResult.h"
+#include "llvm/Support/raw_ostream.h"
+
 using namespace dynamatic::experimental::boolean;
 using namespace llvm;
+using namespace mlir;
 
 void dynamatic::experimental::boolean::restrict(BoolExpression *exp,
                                                 const std::string &var,
@@ -52,33 +69,295 @@ void dynamatic::experimental::boolean::restrict(BoolExpression *exp,
   }
 }
 
-BDD *dynamatic::experimental::boolean::buildBDD(
-    BoolExpression *exp, std::vector<std::string> variableList) {
-  if (exp->type == ExpressionType::Variable ||
-      exp->type == ExpressionType::Zero || exp->type == ExpressionType::One)
-    return new BDD(exp);
+BDD::BDD() {
+  nodes.clear();
+  order.clear();
+  rootIndex = zeroIndex = oneIndex = 0;
+}
+
+LogicalResult
+BDD::buildOBDDTreeFromExpression(BoolExpression *expr,
+                                 const std::vector<std::string> &varOrder) {
+  nodes.clear();
+  order = varOrder;
+  rootIndex = 0;
+
+  if (!expr) {
+    llvm::errs() << "BDD: null expression\n";
+    return failure();
+  }
+
+  auto createNode =
+      [&](auto &&self, BoolExpression *exp,
+          const std::vector<std::string> &variableList) -> unsigned {
+    if (exp->type == ExpressionType::Variable ||
+        exp->type == ExpressionType::Zero || exp->type == ExpressionType::One) {
+      unsigned idx = nodes.size();
+      std::string leafVar;
+      if (exp->type == ExpressionType::Variable) {
+        leafVar = exp->toString();
+      } else if (exp->type == ExpressionType::Zero) {
+        leafVar = "0";
+      } else {
+        leafVar = "1";
+      }
+      nodes.emplace_back(BDDNode{leafVar, idx, idx, {}});
+      return idx;
+    }
 
-  // Get the next variable to expand
-  const std::string &var = variableList[0];
+    // Assume variableList is not empty
+    const std::string &var = variableList[0];
+    std::vector<std::string> subList(std::next(variableList.begin()),
+                                     variableList.end());
 
-  // Get a boolean expression in which `var` is substituted with false
-  BoolExpression *restrictedNegative = exp->deepCopy();
-  restrict(restrictedNegative, var, false);
-  restrictedNegative = restrictedNegative->boolMinimize();
+    BoolExpression *restrictedNegative = exp->deepCopy();
+    restrict(restrictedNegative, var, false);
+    restrictedNegative = restrictedNegative->boolMinimize();
 
-  // Get a boolean expression in which `var` is substituted with true
-  BoolExpression *restrictedPositive = exp->deepCopy();
-  restrict(restrictedPositive, var, true);
-  restrictedPositive = restrictedPositive->boolMinimize();
+    BoolExpression *restrictedPositive = exp->deepCopy();
+    restrict(restrictedPositive, var, true);
+    restrictedPositive = restrictedPositive->boolMinimize();
 
-  // Get a list of the next variables to expand
-  std::vector<std::string> subList(std::next(variableList.begin()),
-                                   variableList.end());
+    unsigned negativeInput = self(self, restrictedNegative, subList);
+    unsigned positiveInput = self(self, restrictedPositive, subList);
 
-  // Recursively build the left and right sub-trees
-  BDD *negativeInput = buildBDD(restrictedNegative, subList);
-  BDD *positiveInput = buildBDD(restrictedPositive, subList);
-  auto *condition = new SingleCond(ExpressionType::Variable, var);
+    unsigned idx = nodes.size();
+    nodes.emplace_back(BDDNode{var, negativeInput, positiveInput, {}});
 
-  return new BDD(negativeInput, positiveInput, condition);
+    nodes[negativeInput].preds.push_back(idx);
+    nodes[positiveInput].preds.push_back(idx);
+
+    delete restrictedNegative;
+    delete restrictedPositive;
+
+    return idx;
+  };
+
+  rootIndex = createNode(createNode, expr, order);
+  return success();
 }
+
+LogicalResult
+BDD::buildROBDDFromExpression(BoolExpression *expr,
+                              const std::vector<std::string> &varOrder) {
+  nodes.clear();
+  order.clear();
+  rootIndex = zeroIndex = oneIndex = 0;
+
+  if (!expr) {
+    llvm::errs() << "BDD: null expression\n";
+    return failure();
+  }
+
+  // Minimize the whole expression once before starting.
+  BoolExpression *rootExpr = expr->boolMinimize();
+
+  // If the expression itself is constant, build only two terminals.
+  if (rootExpr->type == ExpressionType::Zero ||
+      rootExpr->type == ExpressionType::One) {
+    nodes.resize(2);
+    zeroIndex = 0;
+    oneIndex = 1;
+    nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
+    nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
+    rootIndex = (rootExpr->type == ExpressionType::One) ? oneIndex : zeroIndex;
+    return success();
+  }
+
+  // Keep only variables that still appear after minimization and respect
+  // the order provided by the user.
+  {
+    std::set<std::string> present = rootExpr->getVariables();
+    for (const auto &v : varOrder)
+      if (present.find(v) != present.end())
+        order.push_back(v);
+  }
+
+  // Pre-allocate all internal nodes; initially connect them to the terminals.
+  const unsigned n = (unsigned)order.size();
+  nodes.resize(n + 2);
+  zeroIndex = n;
+  oneIndex = n + 1;
+  for (unsigned i = 0; i < n; ++i)
+    nodes[i] = BDDNode{order[i], zeroIndex, oneIndex, {}};
+  nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
+  nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
+
+  // Root is always the first internal node (smallest variable index).
+  rootIndex = 0;
+
+  // Recursively expand edges from the root; mark each expanded node to
+  // avoid rebuilding the same subgraph.
+  std::vector<char> expanded(nodes.size(), 0);
+  expandFrom(rootIndex, rootExpr, expanded);
+
+  // After the BDD is fully built, clean up each node's predecessor list:
+  // sort in ascending order and remove any duplicates.
+  for (auto &nd : nodes) {
+    auto &ps = nd.preds;
+    std::sort(ps.begin(), ps.end());
+    ps.erase(std::unique(ps.begin(), ps.end()), ps.end());
+  }
+
+  return success();
+}
+
+void BDD::expandFrom(unsigned idx, BoolExpression *residual,
+                     std::vector<char> &expanded) {
+  if (idx >= order.size() || expanded[idx])
+    return;
+
+  const std::string &var = order[idx];
+
+  // Perform Shannon expansion for the current variable.
+  BoolExpression *f0 = residual->deepCopy();
+  restrict(f0, var, false);
+  f0 = f0->boolMinimize();
+  BoolExpression *f1 = residual->deepCopy();
+  restrict(f1, var, true);
+  f1 = f1->boolMinimize();
+
+  // Decide the next node index for each branch.
+  auto decideNext = [&](BoolExpression *f, unsigned &succ) {
+    if (!f) {
+      succ = zeroIndex;
+      return;
+    }
+    if (f->type == ExpressionType::Zero) {
+      succ = zeroIndex;
+      return;
+    }
+    if (f->type == ExpressionType::One) {
+      succ = oneIndex;
+      return;
+    }
+
+    // Find the earliest variable in the current order that appears in f.
+    auto vars = f->getVariables();
+    size_t vpos = order.size();
+    for (size_t i = 0; i < order.size(); ++i)
+      if (vars.find(order[i]) != vars.end()) {
+        vpos = i;
+        break;
+      }
+
+    succ = static_cast<unsigned>(vpos);
+  };
+
+  unsigned fSucc = zeroIndex, tSucc = oneIndex;
+  decideNext(f0, fSucc);
+  decideNext(f1, tSucc);
+
+  // Connect edges for the current node.
+  nodes[idx].falseSucc = fSucc;
+  nodes[idx].trueSucc = tSucc;
+
+  // While expanding the BDD, record the current node `idx`
+  // as a predecessor of each of its false/true successors.
+  nodes[fSucc].preds.push_back(idx);
+  nodes[tSucc].preds.push_back(idx);
+
+  expanded[idx] = 1;
+
+  // Recurse only on unexplored internal successors.
+  if (fSucc < zeroIndex && !expanded[fSucc])
+    expandFrom(fSucc, f0, expanded);
+  if (tSucc < zeroIndex && !expanded[tSucc])
+    expandFrom(tSucc, f1, expanded);
+}
+
+std::vector<unsigned> ReadOnceBDD::collectSubgraph(unsigned root, unsigned t1,
+                                                   unsigned t0) const {
+  std::vector<char> vis(nodes.size(), 0);
+  std::vector<unsigned> st{root};
+  std::vector<unsigned> subgraph;
+
+  while (!st.empty()) {
+    unsigned u = st.back();
+    st.pop_back();
+    if (u >= nodes.size() || vis[u])
+      continue;
+    vis[u] = 1;
+    subgraph.push_back(u);
+
+    // Stop expansion at the designated local sinks.
+    if (u == t1 || u == t0)
+      continue;
+
+    // Abort if we accidentally reach the global terminals.
+    if (u == zeroIndex || u == oneIndex) {
+      llvm::errs() << "Illegal subgraph: reached global terminal\n";
+      std::abort();
+    }
+
+    const auto &nd = nodes[u];
+    st.push_back(nd.falseSucc);
+    st.push_back(nd.trueSucc);
+  }
+
+  // Ensure both sinks appear in the final list.
+  if (std::find(subgraph.begin(), subgraph.end(), t1) == subgraph.end())
+    subgraph.push_back(t1);
+  if (std::find(subgraph.begin(), subgraph.end(), t0) == subgraph.end())
+    subgraph.push_back(t0);
+
+  std::sort(subgraph.begin(), subgraph.end());
+  return subgraph;
+}
+
+bool BDD::pairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
+                            unsigned b) const {
+  std::vector<char> vis(nodes.size(), 0);
+  std::vector<unsigned> st{root};
+
+  auto push = [&](unsigned v) {
+    if (v == a || v == b)
+      return; // skip banned nodes
+    if (v < nodes.size() && !vis[v])
+      st.push_back(v);
+  };
+
+  while (!st.empty()) {
+    unsigned u = st.back();
+    st.pop_back();
+    if (u >= nodes.size() || vis[u] || u == a || u == b)
+      continue;
+    vis[u] = 1;
+
+    // Reaching either sink means not covering all paths.
+    if (u == t1 || u == t0)
+      return false;
+
+    const auto &nd = nodes[u];
+    push(nd.falseSucc);
+    push(nd.trueSucc);
+  }
+  // Neither sink reachable -> covering all paths.
+  return true;
+}
+
+std::vector<std::pair<unsigned, unsigned>>
+BDD::listPathCoveringPairs(unsigned root, unsigned t1, unsigned t0) const {
+  // Collect and validate the subgraph (sorted, includes root/t1/t0).
+  std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
+  std::vector<std::pair<unsigned, unsigned>> coverPairs;
+
+  // Scan all pairs in ascending order.
+  for (size_t i = 1; i < cand.size() - 2; ++i) {
+    for (size_t j = i + 1; j < cand.size(); ++j) {
+      if (pairCoverAllPaths(root, t1, t0, cand[i], cand[j])) {
+        coverPairs.emplace_back(cand[i], cand[j]);
+      }
+    }
+  }
+
+  // Sort lexicographically by (first, second).
+  std::sort(coverPairs.begin(), coverPairs.end(),
+            [](const auto &a, const auto &b) {
+              if (a.first != b.first)
+                return a.first < b.first;
+              return a.second < b.second;
+            });
+
+  return coverPairs;
+}
\ No newline at end of file
diff --git a/experimental/lib/Support/BooleanLogic/CMakeLists.txt b/experimental/lib/Support/BooleanLogic/CMakeLists.txt
index 92fdbeeaad..c59e616dc0 100644
--- a/experimental/lib/Support/BooleanLogic/CMakeLists.txt
+++ b/experimental/lib/Support/BooleanLogic/CMakeLists.txt
@@ -3,7 +3,6 @@ add_dynamatic_library(DynamaticExperimentalSupportBooleanLogic
   Lexer.cpp
   Parser.cpp
   BDD.cpp
-  ReadOnceBDD.cpp
 
   LINK_LIBS PRIVATE
   DynamaticSupportEspresso
diff --git a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp b/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
deleted file mode 100644
index 4671096ef8..0000000000
--- a/experimental/lib/Support/BooleanLogic/ReadOnceBDD.cpp
+++ /dev/null
@@ -1,267 +0,0 @@
-//===- ReadOnceBDD.cpp - Read-Once BDD Implementation -----------*- C++ -*-===//
-//
-// Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-//
-// This file implements the construction and basic analysis of a **Read-Once
-// Binary Decision Diagram (BDD)**. It provides:
-//
-//  * Building a read-once BDD from a minimized BoolExpression and a user-
-//    defined variable order.
-//  * Traversing a subgraph defined by a root and two designated sink nodes.
-//  * Enumerating all 2-vertex cut pairs in the subgraph.
-//
-// Each internal node corresponds to a variable in the provided order. Two
-// terminal nodes (0 and 1) are always appended at the end. The implementation
-// assumes the boolean expression is already minimized and read-once compatible.
-//
-//===----------------------------------------------------------------------===//
-
-#include <algorithm>
-#include <functional>
-#include <set>
-#include <string>
-#include <vector>
-
-#include "experimental/Support/BooleanLogic/BDD.h"
-#include "experimental/Support/BooleanLogic/BoolExpression.h"
-#include "experimental/Support/BooleanLogic/ReadOnceBDD.h"
-#include "mlir/Support/LogicalResult.h"
-#include "llvm/Support/raw_ostream.h"
-
-using namespace dynamatic::experimental::boolean;
-using namespace llvm;
-using namespace mlir;
-
-ReadOnceBDD::ReadOnceBDD() {
-  nodes.clear();
-  order.clear();
-  rootIndex = zeroIndex = oneIndex = 0;
-}
-
-LogicalResult
-ReadOnceBDD::buildFromExpression(BoolExpression *expr,
-                                 const std::vector<std::string> &varOrder) {
-  nodes.clear();
-  order.clear();
-  rootIndex = zeroIndex = oneIndex = 0;
-
-  if (!expr) {
-    llvm::errs() << "ReadOnceBDD: null expression\n";
-    return failure();
-  }
-
-  // Minimize the whole expression once before starting.
-  BoolExpression *rootExpr = expr->boolMinimize();
-
-  // If the expression itself is constant, build only two terminals.
-  if (rootExpr->type == ExpressionType::Zero ||
-      rootExpr->type == ExpressionType::One) {
-    nodes.resize(2);
-    zeroIndex = 0;
-    oneIndex = 1;
-    nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
-    nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
-    rootIndex = (rootExpr->type == ExpressionType::One) ? oneIndex : zeroIndex;
-    return success();
-  }
-
-  // Keep only variables that still appear after minimization and respect
-  // the order provided by the user.
-  {
-    std::set<std::string> present = rootExpr->getVariables();
-    for (const auto &v : varOrder)
-      if (present.find(v) != present.end())
-        order.push_back(v);
-  }
-
-  // Pre-allocate all internal nodes; initially connect them to the terminals.
-  const unsigned n = (unsigned)order.size();
-  nodes.resize(n + 2);
-  zeroIndex = n;
-  oneIndex = n + 1;
-  for (unsigned i = 0; i < n; ++i)
-    nodes[i] = BDDNode{order[i], zeroIndex, oneIndex, {}};
-  nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
-  nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
-
-  // Root is always the first internal node (smallest variable index).
-  rootIndex = 0;
-
-  // Recursively expand edges from the root; mark each expanded node to
-  // avoid rebuilding the same subgraph.
-  std::vector<char> expanded(nodes.size(), 0);
-  expandFrom(rootIndex, rootExpr, expanded);
-
-  // After the BDD is fully built, clean up each node's predecessor list:
-  // sort in ascending order and remove any duplicates.
-  for (auto &nd : nodes) {
-    auto &ps = nd.preds;
-    std::sort(ps.begin(), ps.end());
-    ps.erase(std::unique(ps.begin(), ps.end()), ps.end());
-  }
-
-  return success();
-}
-
-void ReadOnceBDD::expandFrom(unsigned idx, BoolExpression *residual,
-                             std::vector<char> &expanded) {
-  if (idx >= order.size() || expanded[idx])
-    return;
-
-  const std::string &var = order[idx];
-
-  // Perform Shannon expansion for the current variable.
-  BoolExpression *f0 = residual->deepCopy();
-  restrict(f0, var, false);
-  f0 = f0->boolMinimize();
-  BoolExpression *f1 = residual->deepCopy();
-  restrict(f1, var, true);
-  f1 = f1->boolMinimize();
-
-  // Decide the next node index for each branch.
-  auto decideNext = [&](BoolExpression *f, unsigned &succ) {
-    if (!f) {
-      succ = zeroIndex;
-      return;
-    }
-    if (f->type == ExpressionType::Zero) {
-      succ = zeroIndex;
-      return;
-    }
-    if (f->type == ExpressionType::One) {
-      succ = oneIndex;
-      return;
-    }
-
-    // Find the earliest variable in the current order that appears in f.
-    auto vars = f->getVariables();
-    size_t vpos = order.size();
-    for (size_t i = 0; i < order.size(); ++i)
-      if (vars.find(order[i]) != vars.end()) {
-        vpos = i;
-        break;
-      }
-
-    succ = static_cast<unsigned>(vpos);
-  };
-
-  unsigned fSucc = zeroIndex, tSucc = oneIndex;
-  decideNext(f0, fSucc);
-  decideNext(f1, tSucc);
-
-  // Connect edges for the current node.
-  nodes[idx].falseSucc = fSucc;
-  nodes[idx].trueSucc = tSucc;
-
-  // While expanding the BDD, record the current node `idx`
-  // as a predecessor of each of its false/true successors.
-  nodes[fSucc].preds.push_back(idx);
-  nodes[tSucc].preds.push_back(idx);
-
-  expanded[idx] = 1;
-
-  // Recurse only on unexplored internal successors.
-  if (fSucc < zeroIndex && !expanded[fSucc])
-    expandFrom(fSucc, f0, expanded);
-  if (tSucc < zeroIndex && !expanded[tSucc])
-    expandFrom(tSucc, f1, expanded);
-}
-
-std::vector<unsigned> ReadOnceBDD::collectSubgraph(unsigned root, unsigned t1,
-                                                   unsigned t0) const {
-  std::vector<char> vis(nodes.size(), 0);
-  std::vector<unsigned> st{root};
-  std::vector<unsigned> subgraph;
-
-  while (!st.empty()) {
-    unsigned u = st.back();
-    st.pop_back();
-    if (u >= nodes.size() || vis[u])
-      continue;
-    vis[u] = 1;
-    subgraph.push_back(u);
-
-    // Stop expansion at the designated local sinks.
-    if (u == t1 || u == t0)
-      continue;
-
-    // Abort if we accidentally reach the global terminals.
-    if (u == zeroIndex || u == oneIndex) {
-      llvm::errs() << "Illegal subgraph: reached global terminal\n";
-      std::abort();
-    }
-
-    const auto &nd = nodes[u];
-    st.push_back(nd.falseSucc);
-    st.push_back(nd.trueSucc);
-  }
-
-  // Ensure both sinks appear in the final list.
-  if (std::find(subgraph.begin(), subgraph.end(), t1) == subgraph.end())
-    subgraph.push_back(t1);
-  if (std::find(subgraph.begin(), subgraph.end(), t0) == subgraph.end())
-    subgraph.push_back(t0);
-
-  std::sort(subgraph.begin(), subgraph.end());
-  return subgraph;
-}
-
-bool ReadOnceBDD::sinksUnreachableIfBan(unsigned root, unsigned t1, unsigned t0,
-                                        unsigned a, unsigned b) const {
-  std::vector<char> vis(nodes.size(), 0);
-  std::vector<unsigned> st{root};
-
-  auto push = [&](unsigned v) {
-    if (v == a || v == b)
-      return; // skip banned nodes
-    if (v < nodes.size() && !vis[v])
-      st.push_back(v);
-  };
-
-  while (!st.empty()) {
-    unsigned u = st.back();
-    st.pop_back();
-    if (u >= nodes.size() || vis[u] || u == a || u == b)
-      continue;
-    vis[u] = 1;
-
-    // Reaching either sink means the cut fails.
-    if (u == t1 || u == t0)
-      return false;
-
-    const auto &nd = nodes[u];
-    push(nd.falseSucc);
-    push(nd.trueSucc);
-  }
-  // Neither sink reachable -> valid cut.
-  return true;
-}
-
-std::vector<std::pair<unsigned, unsigned>>
-ReadOnceBDD::listTwoVertexCuts(unsigned root, unsigned t1, unsigned t0) const {
-  // Collect and validate the subgraph (sorted, includes root/t1/t0).
-  std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
-  std::vector<std::pair<unsigned, unsigned>> cuts;
-
-  // Scan all pairs in ascending order.
-  for (size_t i = 1; i < cand.size() - 2; ++i) {
-    for (size_t j = i + 1; j < cand.size(); ++j) {
-      if (sinksUnreachableIfBan(root, t1, t0, cand[i], cand[j])) {
-        cuts.emplace_back(cand[i], cand[j]);
-      }
-    }
-  }
-
-  // Sort lexicographically by (first, second).
-  std::sort(cuts.begin(), cuts.end(), [](const auto &a, const auto &b) {
-    if (a.first != b.first)
-      return a.first < b.first;
-    return a.second < b.second;
-  });
-
-  return cuts;
-}
\ No newline at end of file
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 0a51208505..e0e08bb706 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -17,7 +17,6 @@
 #include "dynamatic/Support/Backedge.h"
 #include "experimental/Support/BooleanLogic/BDD.h"
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
-#include "experimental/Support/BooleanLogic/ReadOnceBDD.h"
 #include "experimental/Support/FtdSupport.h"
 #include "mlir/Analysis/CFGLoopInfo.h"
 #include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h"
@@ -693,62 +692,6 @@ static Value boolVariableToCircuit(PatternRewriter &rewriter,
   return condition;
 }
 
-/// Get a circuit out a boolean expression, depending on the different kinds
-/// of expressions you might have.
-static Value boolExpressionToCircuit(PatternRewriter &rewriter,
-                                     BoolExpression *expr, Block *block,
-                                     const ftd::BlockIndexing &bi) {
-
-  // Variable case
-  if (expr->type == ExpressionType::Variable)
-    return boolVariableToCircuit(rewriter, expr, block, bi);
-
-  // Constant case (either 0 or 1)
-  rewriter.setInsertionPointToStart(block);
-  auto sourceOp = rewriter.create<handshake::SourceOp>(
-      block->getOperations().front().getLoc());
-  Value cnstTrigger = sourceOp.getResult();
-
-  auto intType = rewriter.getIntegerType(1);
-  auto cstAttr = rewriter.getIntegerAttr(
-      intType, (expr->type == ExpressionType::One ? 1 : 0));
-
-  auto constOp = rewriter.create<handshake::ConstantOp>(
-      block->getOperations().front().getLoc(), cstAttr, cnstTrigger);
-
-  constOp->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr());
-
-  return constOp.getResult();
-}
-
-/// Convert a `BDD` object as obtained from the bdd expansion to a
-/// circuit
-static Value bddToCircuit(PatternRewriter &rewriter, BDD *bdd, Block *block,
-                          const ftd::BlockIndexing &bi) {
-  if (!bdd->successors.has_value())
-    return boolExpressionToCircuit(rewriter, bdd->boolVariable, block, bi);
-
-  rewriter.setInsertionPointToStart(block);
-
-  // Get the two operands by recursively calling `bddToCircuit` (it possibly
-  // creates other muxes in a hierarchical way)
-  SmallVector<Value> muxOperands;
-  muxOperands.push_back(
-      bddToCircuit(rewriter, bdd->successors.value().first, block, bi));
-  muxOperands.push_back(
-      bddToCircuit(rewriter, bdd->successors.value().second, block, bi));
-  Value muxCond =
-      boolExpressionToCircuit(rewriter, bdd->boolVariable, block, bi);
-
-  // Create the multiplxer and add it to the rest of the circuit
-  auto muxOp = rewriter.create<handshake::MuxOp>(
-      block->getOperations().front().getLoc(), muxOperands[0].getType(),
-      muxCond, muxOperands);
-  muxOp->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr());
-
-  return muxOp.getResult();
-}
-
 // Returns true if loop is a while loop, detected by the loop header being
 // also a loop exit and not a loop latch
 static bool isWhileLoop(CFGLoop *loop) {
@@ -785,7 +728,7 @@ static bool isWhileLoop(CFGLoop *loop) {
 ///      the recursion’s sinks are the next vertex-cut pair or the subgraph's
 ///      sinks.
 static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
-                          const ftd::BlockIndexing &bi, const ReadOnceBDD &bdd,
+                          const ftd::BlockIndexing &bi, const BDD &bdd,
                           unsigned startIdx, unsigned trueSinkIdx,
                           unsigned falseSinkIdx) {
 
@@ -1032,9 +975,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
 /// Convert the entire read-once BDD into a circuit by invoking buildMuxTree
 /// on the BDD root with terminal nodes {one, zero}. The result is a MUX tree
 /// in which each variable appears exactly once.
-static Value ReadOnceBDDToCircuit(PatternRewriter &rewriter, Block *block,
-                                  const ftd::BlockIndexing &bi,
-                                  const ReadOnceBDD &bdd) {
+static Value BDDToCircuit(PatternRewriter &rewriter, Block *block,
+                          const ftd::BlockIndexing &bi, const BDD &bdd) {
   return buildMuxTree(rewriter, block, bi, bdd, bdd.root(), bdd.one(),
                       bdd.zero());
 }
@@ -1099,21 +1041,14 @@ static Value addSuppressionInLoop(PatternRewriter &rewriter, CFGLoop *loop,
     // Sort the cofactors alphabetically
     std::sort(cofactorList.begin(), cofactorList.end());
 
-    // // Apply a BDD expansion to the loop exit expression and the list of
-    // // cofactors
-    // BDD *bdd = buildBDD(fLoopExit, cofactorList);
-
-    // // Convert the boolean expression obtained through BDD to a circuit
-    // Value branchCond = bddToCircuit(rewriter, bdd, loopExit, bi);
-
-    // Build read-once BDD on the loop-exit condition and lower to mux chain
-    ReadOnceBDD ro;
-    if (failed(ro.buildFromExpression(fLoopExit, cofactorList))) {
-      llvm::errs() << "ReadOnceBDD: buildFromExpression failed in "
+    // Build BDD on the loop-exit condition and lower to mux chain
+    BDD robdd;
+    if (failed(robdd.buildFromExpression(fLoopExit, cofactorList))) {
+      llvm::errs() << "BDD: buildFromExpression failed in "
                       "addSuppressionInLoop.\n";
       std::abort();
     }
-    Value branchCond = ReadOnceBDDToCircuit(rewriter, loopExit, bi, ro);
+    Value branchCond = BDDToCircuit(rewriter, loopExit, bi, robdd);
 
     Operation *loopTerminator = loopExit->getTerminator();
     assert(isa<cf::CondBranchOp>(loopTerminator) &&
@@ -1218,18 +1153,16 @@ static void insertDirectSuppression(
     std::set<std::string> blocks = fSup->getVariables();
 
     std::vector<std::string> cofactorList(blocks.begin(), blocks.end());
-    // BDD *bdd = buildBDD(fSup, cofactorList);
-    // Value branchCond = bddToCircuit(rewriter, bdd, consumer->getBlock(), bi);
 
-    // Build read-once BDD and lower to mux tree
-    ReadOnceBDD ro;
-    if (failed(ro.buildFromExpression(fSup, cofactorList))) {
-      llvm::errs() << "ReadOnceBDD: buildFromExpression failed in "
+    // Build BDD and lower to mux tree
+    BDD robdd;
+    if (failed(robdd.buildFromExpression(fSup, cofactorList))) {
+      llvm::errs() << "BDD: buildFromExpression failed in "
                       "insertDirectSuppression.\n";
       std::abort();
     }
     Value branchCond =
-        ReadOnceBDDToCircuit(rewriter, consumer->getBlock(), bi, ro);
+        BDDToCircuit(rewriter, consumer->getBlock(), bi, robdd);
 
     rewriter.setInsertionPointToStart(consumer->getBlock());
     auto branchOp = rewriter.create<handshake::ConditionalBranchOp>(

From 14b047c003f2d61201fab97fef9f1556ec7e6caa Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Tue, 4 Nov 2025 23:06:10 +0100
Subject: [PATCH 10/21] Update

---
 .../experimental/Support/BooleanLogic/BDD.h   | 22 ++----
 experimental/lib/Support/BooleanLogic/BDD.cpp | 78 +------------------
 .../lib/Support/FtdImplementation.cpp         | 42 +++++-----
 3 files changed, 28 insertions(+), 114 deletions(-)

diff --git a/experimental/include/experimental/Support/BooleanLogic/BDD.h b/experimental/include/experimental/Support/BooleanLogic/BDD.h
index 12a0013359..4fcadcc121 100644
--- a/experimental/include/experimental/Support/BooleanLogic/BDD.h
+++ b/experimental/include/experimental/Support/BooleanLogic/BDD.h
@@ -7,18 +7,15 @@
 //===----------------------------------------------------------------------===//
 //
 // This file provides a Binary Decision Diagram (BDD) builder and
-// basic analysis utilities. A user-specified variable
-// order is respected.
+// basic analysis utilities. A user-specified variable order is respected.
 //
 // Provided functionality:
-//   * Construction from a minimized BoolExpression and a variable order.
-//   * Reduction to a canonical Reduced Ordered BDD (ROBDD).
-//   * Traversal of a subgraph with a designated root and two designated sinks.
+//   * BDD Construction from a minimized BoolExpression and a variable order.
+//   * Traversal of a BDD subgraph with a designated root and two designated
+//     sinks.
 //   * Enumeration of every vertex pair that covers all paths from the root to
 //     either sink inside that subgraph.
 //
-// This implementation assumes the expression is already minimized.
-//
 //===----------------------------------------------------------------------===//
 
 #ifndef DYNAMATIC_SUPPORT_BDD_H
@@ -59,14 +56,6 @@ class BDD {
   /// Create an empty BDD.
   BDD();
 
-  /// Build a tree-structured ordered BDD reflecting Shannon expansion from a
-  /// minimized boolean expression and a variable order. Variables in `varOrder`
-  /// that do not appear in the expression are ignored. Returns `success()` on
-  /// success, or `failure()` if the input is invalid.
-  mlir::LogicalResult
-  buildOBDDTreeFromExpression(BoolExpression *expr,
-                              const std::vector<std::string> &varOrder);
-
   /// Build an ROBDD from a minimized boolean expression and a variable order.
   /// Variables in `varOrder` that do not appear in the expression are ignored.
   /// Returns `success()` on success, or `failure()` if the input is invalid.
@@ -89,7 +78,7 @@ class BDD {
   /// defined by (root, tTrue, tFalse). Returns pairs sorted lexicographically
   /// (first ascending, then second ascending).
   std::vector<std::pair<unsigned, unsigned>>
-  listPathCoveringPairs(unsigned root, unsigned tTrue, unsigned tFalse) const;
+  pairCoverAllPathsList(unsigned root, unsigned tTrue, unsigned tFalse) const;
 
   /// Accessors.
   const std::vector<BDDNode> &getnodes() const { return nodes; }
@@ -99,7 +88,6 @@ class BDD {
   unsigned root() const { return rootIndex; }
   unsigned one() const { return oneIndex; }
   unsigned zero() const { return zeroIndex; }
-  const std::vector<std::string> &getOrder() const { return order; }
 
 private:
   /// Storage: internal nodes first, then terminals zeroIndex and oneIndex.
diff --git a/experimental/lib/Support/BooleanLogic/BDD.cpp b/experimental/lib/Support/BooleanLogic/BDD.cpp
index 3686a3695e..d49cb1b9d7 100644
--- a/experimental/lib/Support/BooleanLogic/BDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/BDD.cpp
@@ -7,17 +7,7 @@
 //===----------------------------------------------------------------------===//
 //
 // This file implements construction of a Binary Decision Diagram (BDD) from a
-// BoolExpression and basic analysis utilities. It provides:
-//
-//  * Building a reduced ordered BDD from a minimized BoolExpression and a user-
-//    defined variable order.
-//  * Traversing a subgraph defined by a designated root and two designated
-//    sinks.
-//  * Enumerating every vertex pair that covers all paths in the subgraph.
-//
-// Each internal node corresponds to a variable in the provided order. Two
-// terminal nodes (0 and 1) are always appended at the end. The implementation
-// assumes the boolean expression is already minimized and read-once compatible.
+// BoolExpression and basic analysis utilities.
 //
 //===----------------------------------------------------------------------===//
 
@@ -75,68 +65,6 @@ BDD::BDD() {
   rootIndex = zeroIndex = oneIndex = 0;
 }
 
-LogicalResult
-BDD::buildOBDDTreeFromExpression(BoolExpression *expr,
-                                 const std::vector<std::string> &varOrder) {
-  nodes.clear();
-  order = varOrder;
-  rootIndex = 0;
-
-  if (!expr) {
-    llvm::errs() << "BDD: null expression\n";
-    return failure();
-  }
-
-  auto createNode =
-      [&](auto &&self, BoolExpression *exp,
-          const std::vector<std::string> &variableList) -> unsigned {
-    if (exp->type == ExpressionType::Variable ||
-        exp->type == ExpressionType::Zero || exp->type == ExpressionType::One) {
-      unsigned idx = nodes.size();
-      std::string leafVar;
-      if (exp->type == ExpressionType::Variable) {
-        leafVar = exp->toString();
-      } else if (exp->type == ExpressionType::Zero) {
-        leafVar = "0";
-      } else {
-        leafVar = "1";
-      }
-      nodes.emplace_back(BDDNode{leafVar, idx, idx, {}});
-      return idx;
-    }
-
-    // Assume variableList is not empty
-    const std::string &var = variableList[0];
-    std::vector<std::string> subList(std::next(variableList.begin()),
-                                     variableList.end());
-
-    BoolExpression *restrictedNegative = exp->deepCopy();
-    restrict(restrictedNegative, var, false);
-    restrictedNegative = restrictedNegative->boolMinimize();
-
-    BoolExpression *restrictedPositive = exp->deepCopy();
-    restrict(restrictedPositive, var, true);
-    restrictedPositive = restrictedPositive->boolMinimize();
-
-    unsigned negativeInput = self(self, restrictedNegative, subList);
-    unsigned positiveInput = self(self, restrictedPositive, subList);
-
-    unsigned idx = nodes.size();
-    nodes.emplace_back(BDDNode{var, negativeInput, positiveInput, {}});
-
-    nodes[negativeInput].preds.push_back(idx);
-    nodes[positiveInput].preds.push_back(idx);
-
-    delete restrictedNegative;
-    delete restrictedPositive;
-
-    return idx;
-  };
-
-  rootIndex = createNode(createNode, expr, order);
-  return success();
-}
-
 LogicalResult
 BDD::buildROBDDFromExpression(BoolExpression *expr,
                               const std::vector<std::string> &varOrder) {
@@ -266,7 +194,7 @@ void BDD::expandFrom(unsigned idx, BoolExpression *residual,
     expandFrom(tSucc, f1, expanded);
 }
 
-std::vector<unsigned> ReadOnceBDD::collectSubgraph(unsigned root, unsigned t1,
+std::vector<unsigned> BDD::collectSubgraph(unsigned root, unsigned t1,
                                                    unsigned t0) const {
   std::vector<char> vis(nodes.size(), 0);
   std::vector<unsigned> st{root};
@@ -337,7 +265,7 @@ bool BDD::pairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
 }
 
 std::vector<std::pair<unsigned, unsigned>>
-BDD::listPathCoveringPairs(unsigned root, unsigned t1, unsigned t0) const {
+BDD::pairCoverAllPathsList(unsigned root, unsigned t1, unsigned t0) const {
   // Collect and validate the subgraph (sorted, includes root/t1/t0).
   std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
   std::vector<std::pair<unsigned, unsigned>> coverPairs;
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index e0e08bb706..60136a2671 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -710,13 +710,12 @@ static bool isWhileLoop(CFGLoop *loop) {
          !llvm::is_contained(latchBlocks, headerBlock);
 }
 
-/// Build a MUX tree for a read-once BDD subgraph delimited by
+/// Build a MUX tree for an ROBDD subgraph delimited by
 ///   startIdx  ->  {trueSinkIdx, falseSinkIdx}.
 /// Strategy:
-///   1) Enumerate all start–{true,false} two-vertex cuts (u,v) in ascending
-///   order,
-///      each cut instantiates one MUX stage.
-///   2) Input placement per pair (u,v):
+///   1) Enumerate all start–{true,false} all-paths-covering pairs (u,v) in
+///   ascending order, each pair instantiates one MUX stage. 2) Input placement
+///   per pair (u,v):
 ///        • Choose the largest common predecessor P of {u,v}.
 ///          Whichever endpoint equals P.trueSucc goes to the TRUE input;
 ///          the other goes to FALSE.
@@ -725,8 +724,8 @@ static bool isWhileLoop(CFGLoop *loop) {
 ///   3) Chain the MUXes: select(mux[0]) is the start condition; for i>0,
 ///      select(mux[i]) = out(mux[i-1]).
 ///   4) For non-constant inputs, recurse on the corresponding sub-region;
-///      the recursion’s sinks are the next vertex-cut pair or the subgraph's
-///      sinks.
+///      the recursion’s sinks are the next all-paths-covering pair or the
+///      subgraph's sinks.
 static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
                           const ftd::BlockIndexing &bi, const BDD &bdd,
                           unsigned startIdx, unsigned trueSinkIdx,
@@ -783,8 +782,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     unsigned nodeIdx = 0;
   };
 
-  // Decide how to connect the two endpoints (u, v) of a cut pair
-  // to the false/true inputs of a mux.
+  // Decide how to connect the two vertices (u, v) of a pair to the false/true
+  // inputs of a mux.
   auto decideInputsForPair =
       [&](unsigned u, unsigned v) -> std::pair<InputSpec, InputSpec> {
     // Convert a BDD node index to an InputSpec.
@@ -804,7 +803,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
       return -1;
     };
 
-    // Wrap the two cut endpoints into InputSpec objects.
+    // Wrap the two vertices in the pair into InputSpec objects.
     InputSpec A = nodeToSpec(u), B = nodeToSpec(v);
 
     // Direct edge -> successor becomes constant.
@@ -840,8 +839,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
                                                   : std::pair{B, A};
   };
 
-  // 2-vertex-cut pairs (sorted).
-  auto pairs = bdd.listTwoVertexCuts(startIdx, trueSinkIdx, falseSinkIdx);
+  // List all-paths-covering pairs (sorted).
+  auto pairs = bdd.pairCoverAllPathsList(startIdx, trueSinkIdx, falseSinkIdx);
 
   // No pair → no mux; return `start` condition (maybe inverted).
   if (pairs.empty()) {
@@ -885,7 +884,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     Operation *op = nullptr;
   };
 
-  // Build the list of mux stages from the given vertex-cut pairs
+  // Build the list of mux stages from the given all-paths-covering pairs
   std::vector<MuxSpec> muxChain;
   muxChain.reserve(pairs.size());
 
@@ -972,9 +971,9 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   return muxChain.back().out;
 }
 
-/// Convert the entire read-once BDD into a circuit by invoking buildMuxTree
-/// on the BDD root with terminal nodes {one, zero}. The result is a MUX tree
-/// in which each variable appears exactly once.
+/// Convert the entire ROBDD into a circuit by invoking buildMuxTree on the BDD
+/// root with terminal nodes {one, zero}. The result is a MUX tree in which each
+/// variable appears exactly once.
 static Value BDDToCircuit(PatternRewriter &rewriter, Block *block,
                           const ftd::BlockIndexing &bi, const BDD &bdd) {
   return buildMuxTree(rewriter, block, bi, bdd, bdd.root(), bdd.one(),
@@ -1043,8 +1042,8 @@ static Value addSuppressionInLoop(PatternRewriter &rewriter, CFGLoop *loop,
 
     // Build BDD on the loop-exit condition and lower to mux chain
     BDD robdd;
-    if (failed(robdd.buildFromExpression(fLoopExit, cofactorList))) {
-      llvm::errs() << "BDD: buildFromExpression failed in "
+    if (failed(robdd.buildROBDDFromExpression(fLoopExit, cofactorList))) {
+      llvm::errs() << "BDD: buildROBDDFromExpression failed in "
                       "addSuppressionInLoop.\n";
       std::abort();
     }
@@ -1156,13 +1155,12 @@ static void insertDirectSuppression(
 
     // Build BDD and lower to mux tree
     BDD robdd;
-    if (failed(robdd.buildFromExpression(fSup, cofactorList))) {
-      llvm::errs() << "BDD: buildFromExpression failed in "
+    if (failed(robdd.buildROBDDFromExpression(fSup, cofactorList))) {
+      llvm::errs() << "BDD: buildROBDDFromExpression failed in "
                       "insertDirectSuppression.\n";
       std::abort();
     }
-    Value branchCond =
-        BDDToCircuit(rewriter, consumer->getBlock(), bi, robdd);
+    Value branchCond = BDDToCircuit(rewriter, consumer->getBlock(), bi, robdd);
 
     rewriter.setInsertionPointToStart(consumer->getBlock());
     auto branchOp = rewriter.create<handshake::ConditionalBranchOp>(

From 0bf710c763bb4c3c6269ece9d001ad69de600abb Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 21:39:05 +0100
Subject: [PATCH 11/21] change name to robdd

---
 .../Support/BooleanLogic/{BDD.h => ROBDD.h}   | 32 +++++-----
 experimental/lib/Analysis/GSAAnalysis.cpp     |  2 +-
 .../lib/Support/BooleanLogic/CMakeLists.txt   |  2 +-
 .../BooleanLogic/{BDD.cpp => ROBDD.cpp}       | 24 ++++----
 .../lib/Support/FtdImplementation.cpp         | 58 +++++++++----------
 5 files changed, 59 insertions(+), 59 deletions(-)
 rename experimental/include/experimental/Support/BooleanLogic/{BDD.h => ROBDD.h} (83%)
 rename experimental/lib/Support/BooleanLogic/{BDD.cpp => ROBDD.cpp} (91%)

diff --git a/experimental/include/experimental/Support/BooleanLogic/BDD.h b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
similarity index 83%
rename from experimental/include/experimental/Support/BooleanLogic/BDD.h
rename to experimental/include/experimental/Support/BooleanLogic/ROBDD.h
index 4fcadcc121..18cf77ba75 100644
--- a/experimental/include/experimental/Support/BooleanLogic/BDD.h
+++ b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
@@ -1,4 +1,4 @@
-//===- BDD.h - BDD construction and analysis --------------------*- C++ -*-===//
+//===- ROBDD.h - ROBDD construction and analysis ----------------*- C++ -*-===//
 //
 // Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,20 +6,20 @@
 //
 //===----------------------------------------------------------------------===//
 //
-// This file provides a Binary Decision Diagram (BDD) builder and
-// basic analysis utilities. A user-specified variable order is respected.
+// This file provides a Reduced Ordered Binary Decision Diagram (ROBDD) builder
+// and basic analysis utilities. A user-specified variable order is respected.
 //
 // Provided functionality:
-//   * BDD Construction from a minimized BoolExpression and a variable order.
-//   * Traversal of a BDD subgraph with a designated root and two designated
+//   * ROBDD Construction from a minimized BoolExpression and a variable order.
+//   * Traversal of an ROBDD subgraph with a designated root and two designated
 //     sinks.
 //   * Enumeration of every vertex pair that covers all paths from the root to
 //     either sink inside that subgraph.
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef DYNAMATIC_SUPPORT_BDD_H
-#define DYNAMATIC_SUPPORT_BDD_H
+#ifndef DYNAMATIC_SUPPORT_ROBDD_H
+#define DYNAMATIC_SUPPORT_ROBDD_H
 
 #include <string>
 #include <utility>
@@ -41,20 +41,20 @@ void restrict(BoolExpression *exp, const std::string &var,
 /// falseSucc : successor index when var evaluates to false
 /// trueSucc  : successor index when var evaluates to true
 /// preds     : indices of all predecessor nodes that point to this node
-struct BDDNode {
+struct ROBDDNode {
   std::string var;
   unsigned falseSucc;
   unsigned trueSucc;
   std::vector<unsigned> preds;
 };
 
-/// Container for a reduced ordered BDD built from a BoolExpression.
+/// Container for a reduced ordered BDD (ROBDD) built from a BoolExpression.
 /// Each internal node is indexed by its position in the user-defined variable
 /// order. Two additional nodes at the end are the 0 and 1 terminals.
-class BDD {
+class ROBDD {
 public:
-  /// Create an empty BDD.
-  BDD();
+  /// Create an empty ROBDD.
+  ROBDD();
 
   /// Build an ROBDD from a minimized boolean expression and a variable order.
   /// Variables in `varOrder` that do not appear in the expression are ignored.
@@ -81,7 +81,7 @@ class BDD {
   pairCoverAllPathsList(unsigned root, unsigned tTrue, unsigned tFalse) const;
 
   /// Accessors.
-  const std::vector<BDDNode> &getnodes() const { return nodes; }
+  const std::vector<ROBDDNode> &getnodes() const { return nodes; }
   const std::vector<unsigned> &getpreds(unsigned idx) const {
     return nodes[idx].preds;
   }
@@ -91,12 +91,12 @@ class BDD {
 
 private:
   /// Storage: internal nodes first, then terminals zeroIndex and oneIndex.
-  std::vector<BDDNode> nodes;
+  std::vector<ROBDDNode> nodes;
 
   /// Variable order used to build the diagram (minimized & filtered).
   std::vector<std::string> order;
 
-  /// Index of the BDD root node.
+  /// Index of the ROBDD root node.
   unsigned rootIndex = 0;
   /// Index of the constant 0 terminal.
   unsigned zeroIndex = 0;
@@ -116,4 +116,4 @@ class BDD {
 } // namespace experimental
 } // namespace dynamatic
 
-#endif // DYNAMATIC_SUPPORT_BDD_H
+#endif // DYNAMATIC_SUPPORT_ROBDD_H
diff --git a/experimental/lib/Analysis/GSAAnalysis.cpp b/experimental/lib/Analysis/GSAAnalysis.cpp
index 1afdc9a5eb..c89d657e59 100644
--- a/experimental/lib/Analysis/GSAAnalysis.cpp
+++ b/experimental/lib/Analysis/GSAAnalysis.cpp
@@ -13,7 +13,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "experimental/Analysis/GSAAnalysis.h"
-#include "experimental/Support/BooleanLogic/BDD.h"
+#include "experimental/Support/BooleanLogic/ROBDD.h"
 #include "experimental/Support/FtdSupport.h"
 #include "mlir/Analysis/CFGLoopInfo.h"
 #include "mlir/Dialect/Func/IR/FuncOps.h"
diff --git a/experimental/lib/Support/BooleanLogic/CMakeLists.txt b/experimental/lib/Support/BooleanLogic/CMakeLists.txt
index c59e616dc0..cb1b839196 100644
--- a/experimental/lib/Support/BooleanLogic/CMakeLists.txt
+++ b/experimental/lib/Support/BooleanLogic/CMakeLists.txt
@@ -2,7 +2,7 @@ add_dynamatic_library(DynamaticExperimentalSupportBooleanLogic
   BoolExpression.cpp
   Lexer.cpp
   Parser.cpp
-  BDD.cpp
+  ROBDD.cpp
 
   LINK_LIBS PRIVATE
   DynamaticSupportEspresso
diff --git a/experimental/lib/Support/BooleanLogic/BDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
similarity index 91%
rename from experimental/lib/Support/BooleanLogic/BDD.cpp
rename to experimental/lib/Support/BooleanLogic/ROBDD.cpp
index d49cb1b9d7..166a8669e1 100644
--- a/experimental/lib/Support/BooleanLogic/BDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -1,4 +1,4 @@
-//===- BDD.cpp - BDD construction and analysis ------------------*- C++ -*-===//
+//===- ROBDD.cpp - ROBDD construction and analysis --------------*- C++ -*-===//
 //
 // Dynamatic is under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,12 +6,12 @@
 //
 //===----------------------------------------------------------------------===//
 //
-// This file implements construction of a Binary Decision Diagram (BDD) from a
-// BoolExpression and basic analysis utilities.
+// This file implements construction of a Reduced Ordered Binary Decision 
+// Diagram (ROBDD) from a BoolExpression and basic analysis utilities.
 //
 //===----------------------------------------------------------------------===//
 
-#include "experimental/Support/BooleanLogic/BDD.h"
+#include "experimental/Support/BooleanLogic/ROBDD.h"
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
 
 #include <algorithm>
@@ -59,21 +59,21 @@ void dynamatic::experimental::boolean::restrict(BoolExpression *exp,
   }
 }
 
-BDD::BDD() {
+ROBDD::ROBDD() {
   nodes.clear();
   order.clear();
   rootIndex = zeroIndex = oneIndex = 0;
 }
 
 LogicalResult
-BDD::buildROBDDFromExpression(BoolExpression *expr,
+ROBDD::buildROBDDFromExpression(BoolExpression *expr,
                               const std::vector<std::string> &varOrder) {
   nodes.clear();
   order.clear();
   rootIndex = zeroIndex = oneIndex = 0;
 
   if (!expr) {
-    llvm::errs() << "BDD: null expression\n";
+    llvm::errs() << "ROBDD: null expression\n";
     return failure();
   }
 
@@ -107,7 +107,7 @@ BDD::buildROBDDFromExpression(BoolExpression *expr,
   zeroIndex = n;
   oneIndex = n + 1;
   for (unsigned i = 0; i < n; ++i)
-    nodes[i] = BDDNode{order[i], zeroIndex, oneIndex, {}};
+    nodes[i] = ROBDDNode{order[i], zeroIndex, oneIndex, {}};
   nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
   nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
 
@@ -130,7 +130,7 @@ BDD::buildROBDDFromExpression(BoolExpression *expr,
   return success();
 }
 
-void BDD::expandFrom(unsigned idx, BoolExpression *residual,
+void ROBDD::expandFrom(unsigned idx, BoolExpression *residual,
                      std::vector<char> &expanded) {
   if (idx >= order.size() || expanded[idx])
     return;
@@ -194,7 +194,7 @@ void BDD::expandFrom(unsigned idx, BoolExpression *residual,
     expandFrom(tSucc, f1, expanded);
 }
 
-std::vector<unsigned> BDD::collectSubgraph(unsigned root, unsigned t1,
+std::vector<unsigned> ROBDD::collectSubgraph(unsigned root, unsigned t1,
                                                    unsigned t0) const {
   std::vector<char> vis(nodes.size(), 0);
   std::vector<unsigned> st{root};
@@ -233,7 +233,7 @@ std::vector<unsigned> BDD::collectSubgraph(unsigned root, unsigned t1,
   return subgraph;
 }
 
-bool BDD::pairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
+bool ROBDD::pairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
                             unsigned b) const {
   std::vector<char> vis(nodes.size(), 0);
   std::vector<unsigned> st{root};
@@ -265,7 +265,7 @@ bool BDD::pairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
 }
 
 std::vector<std::pair<unsigned, unsigned>>
-BDD::pairCoverAllPathsList(unsigned root, unsigned t1, unsigned t0) const {
+ROBDD::pairCoverAllPathsList(unsigned root, unsigned t1, unsigned t0) const {
   // Collect and validate the subgraph (sorted, includes root/t1/t0).
   std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
   std::vector<std::pair<unsigned, unsigned>> coverPairs;
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 60136a2671..cd2b02706d 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -15,7 +15,7 @@
 #include "experimental/Support/FtdImplementation.h"
 #include "dynamatic/Analysis/ControlDependenceAnalysis.h"
 #include "dynamatic/Support/Backedge.h"
-#include "experimental/Support/BooleanLogic/BDD.h"
+#include "experimental/Support/BooleanLogic/ROBDD.h"
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
 #include "experimental/Support/FtdSupport.h"
 #include "mlir/Analysis/CFGLoopInfo.h"
@@ -727,18 +727,18 @@ static bool isWhileLoop(CFGLoop *loop) {
 ///      the recursion’s sinks are the next all-paths-covering pair or the
 ///      subgraph's sinks.
 static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
-                          const ftd::BlockIndexing &bi, const BDD &bdd,
+                          const ftd::BlockIndexing &bi, const ROBDD &robdd,
                           unsigned startIdx, unsigned trueSinkIdx,
                           unsigned falseSinkIdx) {
 
-  const auto &nodes = bdd.getnodes();
+  const auto &nodes = robdd.getnodes();
 
   // Look up the boolean signal for a given condition variable name and
   // return it as the select input of a mux (converted to a handshake channel).
   auto getSel = [&](const std::string &varName) -> Value {
     auto condBlkOpt = bi.getBlockFromCondition(varName);
     if (!condBlkOpt.has_value()) {
-      llvm::errs() << "BddToCircuit: cannot map condition '" << varName
+      llvm::errs() << "convertRobddToCircuit: cannot map condition '" << varName
                    << "'.\n";
       return nullptr;
     }
@@ -776,7 +776,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   // Describes one mux data input:
   //  - isConst  : true if this input is a boolean constant
   //  - constVal : value of the constant if isConst == true
-  //  - nodeIdx  : BDD node index if this input is driven by a variable
+  //  - nodeIdx  : ROBDD node index if this input is driven by a variable
   struct InputSpec {
     bool isConst = false, constVal = false;
     unsigned nodeIdx = 0;
@@ -786,7 +786,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   // inputs of a mux.
   auto decideInputsForPair =
       [&](unsigned u, unsigned v) -> std::pair<InputSpec, InputSpec> {
-    // Convert a BDD node index to an InputSpec.
+    // Convert a ROBDD node index to an InputSpec.
     auto nodeToSpec = [&](unsigned idx) -> InputSpec {
       return {false, false, idx};
     };
@@ -840,7 +840,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   };
 
   // List all-paths-covering pairs (sorted).
-  auto pairs = bdd.pairCoverAllPathsList(startIdx, trueSinkIdx, falseSinkIdx);
+  auto pairs = robdd.pairCoverAllPathsList(startIdx, trueSinkIdx, falseSinkIdx);
 
   // No pair → no mux; return `start` condition (maybe inverted).
   if (pairs.empty()) {
@@ -856,7 +856,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
                 nodes[startIdx].falseSucc == trueSinkIdx);
 
     if (!dir && !inv) {
-      llvm::errs() << "BddToCircuit: start node doesn't map to sinks.\n";
+      llvm::errs() << "convertRobddToCircuit: start node doesn't map to sinks.\n";
       llvm::errs() << "  Summary\n";
       llvm::errs() << "    nodes.size = " << nodes.size() << "\n";
       llvm::errs() << "    startIdx   = " << startIdx << "\n";
@@ -914,13 +914,13 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     // node. This ignores inF/inT.constVal and uses the terminal identity
     // instead.
     if (i + 1 == muxChain.size()) {
-      if (muxChain[i].inF.nodeIdx == bdd.one())
+      if (muxChain[i].inF.nodeIdx == robdd.one())
         inF = c1;
-      else if (muxChain[i].inF.nodeIdx == bdd.zero())
+      else if (muxChain[i].inF.nodeIdx == robdd.zero())
         inF = c0;
-      if (muxChain[i].inT.nodeIdx == bdd.one())
+      if (muxChain[i].inT.nodeIdx == robdd.one())
         inT = c1;
-      else if (muxChain[i].inT.nodeIdx == bdd.zero())
+      else if (muxChain[i].inT.nodeIdx == robdd.zero())
         inT = c0;
     }
 
@@ -951,7 +951,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
 
     if (!muxChain[i].inF.isConst) {
       unsigned s = muxChain[i].inF.nodeIdx;
-      Value sub = buildMuxTree(rewriter, block, bi, bdd, s, subT, subF);
+      Value sub = buildMuxTree(rewriter, block, bi, robdd, s, subT, subF);
       if (!sub)
         return nullptr;
       // operand index 1 = false
@@ -959,7 +959,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     }
     if (!muxChain[i].inT.isConst) {
       unsigned s = muxChain[i].inT.nodeIdx;
-      Value sub = buildMuxTree(rewriter, block, bi, bdd, s, subT, subF);
+      Value sub = buildMuxTree(rewriter, block, bi, robdd, s, subT, subF);
       if (!sub)
         return nullptr;
       // operand index 2 = true
@@ -971,13 +971,13 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   return muxChain.back().out;
 }
 
-/// Convert the entire ROBDD into a circuit by invoking buildMuxTree on the BDD
+/// Convert the entire ROBDD into a circuit by invoking buildMuxTree on the ROBDD
 /// root with terminal nodes {one, zero}. The result is a MUX tree in which each
 /// variable appears exactly once.
-static Value BDDToCircuit(PatternRewriter &rewriter, Block *block,
-                          const ftd::BlockIndexing &bi, const BDD &bdd) {
-  return buildMuxTree(rewriter, block, bi, bdd, bdd.root(), bdd.one(),
-                      bdd.zero());
+static Value convertRobddToCircuit(PatternRewriter &rewriter, Block *block,
+                          const ftd::BlockIndexing &bi, const ROBDD &robdd) {
+  return buildMuxTree(rewriter, block, bi, robdd, robdd.root(), robdd.one(),
+                      robdd.zero());
 }
 
 using PairOperandConsumer = std::pair<Value, Operation *>;
@@ -1040,14 +1040,14 @@ static Value addSuppressionInLoop(PatternRewriter &rewriter, CFGLoop *loop,
     // Sort the cofactors alphabetically
     std::sort(cofactorList.begin(), cofactorList.end());
 
-    // Build BDD on the loop-exit condition and lower to mux chain
-    BDD robdd;
+    // Build ROBDD on the loop-exit condition and lower to mux chain
+    ROBDD robdd;
     if (failed(robdd.buildROBDDFromExpression(fLoopExit, cofactorList))) {
-      llvm::errs() << "BDD: buildROBDDFromExpression failed in "
+      llvm::errs() << "ROBDD: buildROBDDFromExpression failed in "
                       "addSuppressionInLoop.\n";
       std::abort();
     }
-    Value branchCond = BDDToCircuit(rewriter, loopExit, bi, robdd);
+    Value branchCond = convertRobddToCircuit(rewriter, loopExit, bi, robdd);
 
     Operation *loopTerminator = loopExit->getTerminator();
     assert(isa<cf::CondBranchOp>(loopTerminator) &&
@@ -1153,14 +1153,14 @@ static void insertDirectSuppression(
 
     std::vector<std::string> cofactorList(blocks.begin(), blocks.end());
 
-    // Build BDD and lower to mux tree
-    BDD robdd;
+    // Build ROBDD and lower to mux tree
+    ROBDD robdd;
     if (failed(robdd.buildROBDDFromExpression(fSup, cofactorList))) {
-      llvm::errs() << "BDD: buildROBDDFromExpression failed in "
+      llvm::errs() << "ROBDD: buildROBDDFromExpression failed in "
                       "insertDirectSuppression.\n";
       std::abort();
     }
-    Value branchCond = BDDToCircuit(rewriter, consumer->getBlock(), bi, robdd);
+    Value branchCond = convertRobddToCircuit(rewriter, consumer->getBlock(), bi, robdd);
 
     rewriter.setInsertionPointToStart(consumer->getBlock());
     auto branchOp = rewriter.create<handshake::ConditionalBranchOp>(
@@ -1192,7 +1192,7 @@ void ftd::addSuppOperandConsumer(PatternRewriter &rewriter,
   auto cda = ControlDependenceAnalysis(region).getAllBlockDeps();
 
   // Skip the prod-cons if the producer is part of the operations related to
-  // the BDD expansion or INIT merges
+  // the ROBDD expansion or INIT merges
   if (consumerOp->hasAttr(FTD_OP_TO_SKIP) ||
       consumerOp->hasAttr(FTD_INIT_MERGE))
     return;
@@ -1226,7 +1226,7 @@ void ftd::addSuppOperandConsumer(PatternRewriter &rewriter,
       return;
 
     // Skip the prod-cons if the consumer is part of the operations
-    // related to the BDD expansion or INIT merges
+    // related to the ROBDD expansion or INIT merges
     if (producerOp->hasAttr(FTD_OP_TO_SKIP) ||
         producerOp->hasAttr(FTD_INIT_MERGE))
       return;

From 0ad744c2911cd26ddf1d6b4670fc94de976ae5ff Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 22:12:45 +0100
Subject: [PATCH 12/21] review changes

---
 .../experimental/Support/BooleanLogic/ROBDD.h | 29 ++++++++++---------
 .../lib/Support/BooleanLogic/ROBDD.cpp        |  6 ++--
 .../lib/Support/FtdImplementation.cpp         |  2 +-
 3 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/experimental/include/experimental/Support/BooleanLogic/ROBDD.h b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
index 18cf77ba75..9766051753 100644
--- a/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
+++ b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
@@ -56,13 +56,15 @@ class ROBDD {
   /// Create an empty ROBDD.
   ROBDD();
 
-  /// Build an ROBDD from a minimized boolean expression and a variable order.
-  /// Variables in `varOrder` that do not appear in the expression are ignored.
-  /// Returns `success()` on success, or `failure()` if the input is invalid.
+  /// Build a lightweight ROBDD for CFG reachability analysis.
   ///
-  /// This is a simple method that assumes each variable appears only once in
-  /// the BDD, which matches the case of checking whether a basic block in the
-  /// CFG can be reached.
+  /// Unlike a general ROBDD which may have multiple nodes for the same variable
+  /// (representing different sub-functions), this specialized implementation
+  /// enforces a **one-node-per-variable** constraint.
+  ///
+  /// This design exploits the specific structure of CFG path conditions, allowing
+  /// for a simplified, linear-sized construction without the need for a global
+  /// unique-table for node deduplication.
   mlir::LogicalResult
   buildROBDDFromExpression(BoolExpression *expr,
                            const std::vector<std::string> &varOrder);
@@ -70,15 +72,16 @@ class ROBDD {
   /// Traverse the subgraph reachable from `root` until either `tTrue` or
   /// `tFalse` (treated as local sinks). Aborts if any path reaches the global
   /// 0/1 terminals prematurely. Returns the list of node indices in the
-  /// subgraph (sorted ascending, always including `root`, `tTrue`, `tFalse`).
+  /// subgraph (sorted in ascending order, always including `root`, `tTrue`, `tFalse`).
   std::vector<unsigned> collectSubgraph(unsigned root, unsigned tTrue,
                                         unsigned tFalse) const;
-
-  /// Enumerate all pairs of vertices that cover all paths within the subgraph
-  /// defined by (root, tTrue, tFalse). Returns pairs sorted lexicographically
-  /// (first ascending, then second ascending).
+  
+  /// Enumerates all non-trivial pairs of vertices that cover all paths within
+  /// the subgraph defined by (root, tTrue, tFalse). Trivial covers (e.g., those containing the root node or both terminals) are explicitly excluded from the results.
+  ///
+  /// Returns pairs sorted lexicographically (first ascending, then second ascending).
   std::vector<std::pair<unsigned, unsigned>>
-  pairCoverAllPathsList(unsigned root, unsigned tTrue, unsigned tFalse) const;
+  findPairsCoveringAllPaths(unsigned root, unsigned tTrue, unsigned tFalse) const;
 
   /// Accessors.
   const std::vector<ROBDDNode> &getnodes() const { return nodes; }
@@ -108,7 +111,7 @@ class ROBDD {
                   std::vector<char> &expanded);
 
   /// Helper: test whether nodes `a` and `b` cover all paths.
-  bool pairCoverAllPaths(unsigned root, unsigned tTrue, unsigned tFalse,
+  bool doesPairCoverAllPaths(unsigned root, unsigned tTrue, unsigned tFalse,
                          unsigned a, unsigned b) const;
 };
 
diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
index 166a8669e1..fbeaf61701 100644
--- a/experimental/lib/Support/BooleanLogic/ROBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -233,7 +233,7 @@ std::vector<unsigned> ROBDD::collectSubgraph(unsigned root, unsigned t1,
   return subgraph;
 }
 
-bool ROBDD::pairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
+bool ROBDD::doesPairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
                             unsigned b) const {
   std::vector<char> vis(nodes.size(), 0);
   std::vector<unsigned> st{root};
@@ -265,7 +265,7 @@ bool ROBDD::pairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned
 }
 
 std::vector<std::pair<unsigned, unsigned>>
-ROBDD::pairCoverAllPathsList(unsigned root, unsigned t1, unsigned t0) const {
+ROBDD::findPairsCoveringAllPaths(unsigned root, unsigned t1, unsigned t0) const {
   // Collect and validate the subgraph (sorted, includes root/t1/t0).
   std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
   std::vector<std::pair<unsigned, unsigned>> coverPairs;
@@ -273,7 +273,7 @@ ROBDD::pairCoverAllPathsList(unsigned root, unsigned t1, unsigned t0) const {
   // Scan all pairs in ascending order.
   for (size_t i = 1; i < cand.size() - 2; ++i) {
     for (size_t j = i + 1; j < cand.size(); ++j) {
-      if (pairCoverAllPaths(root, t1, t0, cand[i], cand[j])) {
+      if (doesPairCoverAllPaths(root, t1, t0, cand[i], cand[j])) {
         coverPairs.emplace_back(cand[i], cand[j]);
       }
     }
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index cd2b02706d..18612a1cda 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -840,7 +840,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   };
 
   // List all-paths-covering pairs (sorted).
-  auto pairs = robdd.pairCoverAllPathsList(startIdx, trueSinkIdx, falseSinkIdx);
+  auto pairs = robdd.findPairsCoveringAllPaths(startIdx, trueSinkIdx, falseSinkIdx);
 
   // No pair → no mux; return `start` condition (maybe inverted).
   if (pairs.empty()) {

From 5d32285aa0267e66e5c3c0a7e71c6375c99d3208 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 22:15:04 +0100
Subject: [PATCH 13/21] clang-format

---
 .../experimental/Support/BooleanLogic/ROBDD.h | 23 +++++++++++--------
 .../lib/Support/BooleanLogic/ROBDD.cpp        | 15 ++++++------
 .../lib/Support/FtdImplementation.cpp         | 20 +++++++++-------
 3 files changed, 34 insertions(+), 24 deletions(-)

diff --git a/experimental/include/experimental/Support/BooleanLogic/ROBDD.h b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
index 9766051753..197c46386d 100644
--- a/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
+++ b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h
@@ -62,9 +62,9 @@ class ROBDD {
   /// (representing different sub-functions), this specialized implementation
   /// enforces a **one-node-per-variable** constraint.
   ///
-  /// This design exploits the specific structure of CFG path conditions, allowing
-  /// for a simplified, linear-sized construction without the need for a global
-  /// unique-table for node deduplication.
+  /// This design exploits the specific structure of CFG path conditions,
+  /// allowing for a simplified, linear-sized construction without the need for
+  /// a global unique-table for node deduplication.
   mlir::LogicalResult
   buildROBDDFromExpression(BoolExpression *expr,
                            const std::vector<std::string> &varOrder);
@@ -72,16 +72,21 @@ class ROBDD {
   /// Traverse the subgraph reachable from `root` until either `tTrue` or
   /// `tFalse` (treated as local sinks). Aborts if any path reaches the global
   /// 0/1 terminals prematurely. Returns the list of node indices in the
-  /// subgraph (sorted in ascending order, always including `root`, `tTrue`, `tFalse`).
+  /// subgraph (sorted in ascending order, always including `root`, `tTrue`,
+  /// `tFalse`).
   std::vector<unsigned> collectSubgraph(unsigned root, unsigned tTrue,
                                         unsigned tFalse) const;
-  
+
   /// Enumerates all non-trivial pairs of vertices that cover all paths within
-  /// the subgraph defined by (root, tTrue, tFalse). Trivial covers (e.g., those containing the root node or both terminals) are explicitly excluded from the results.
+  /// the subgraph defined by (root, tTrue, tFalse). Trivial covers (e.g., those
+  /// containing the root node or both terminals) are explicitly excluded from
+  /// the results.
   ///
-  /// Returns pairs sorted lexicographically (first ascending, then second ascending).
+  /// Returns pairs sorted lexicographically (first ascending, then second
+  /// ascending).
   std::vector<std::pair<unsigned, unsigned>>
-  findPairsCoveringAllPaths(unsigned root, unsigned tTrue, unsigned tFalse) const;
+  findPairsCoveringAllPaths(unsigned root, unsigned tTrue,
+                            unsigned tFalse) const;
 
   /// Accessors.
   const std::vector<ROBDDNode> &getnodes() const { return nodes; }
@@ -112,7 +117,7 @@ class ROBDD {
 
   /// Helper: test whether nodes `a` and `b` cover all paths.
   bool doesPairCoverAllPaths(unsigned root, unsigned tTrue, unsigned tFalse,
-                         unsigned a, unsigned b) const;
+                             unsigned a, unsigned b) const;
 };
 
 } // namespace boolean
diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
index fbeaf61701..6a0da848cd 100644
--- a/experimental/lib/Support/BooleanLogic/ROBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -6,7 +6,7 @@
 //
 //===----------------------------------------------------------------------===//
 //
-// This file implements construction of a Reduced Ordered Binary Decision 
+// This file implements construction of a Reduced Ordered Binary Decision
 // Diagram (ROBDD) from a BoolExpression and basic analysis utilities.
 //
 //===----------------------------------------------------------------------===//
@@ -67,7 +67,7 @@ ROBDD::ROBDD() {
 
 LogicalResult
 ROBDD::buildROBDDFromExpression(BoolExpression *expr,
-                              const std::vector<std::string> &varOrder) {
+                                const std::vector<std::string> &varOrder) {
   nodes.clear();
   order.clear();
   rootIndex = zeroIndex = oneIndex = 0;
@@ -131,7 +131,7 @@ ROBDD::buildROBDDFromExpression(BoolExpression *expr,
 }
 
 void ROBDD::expandFrom(unsigned idx, BoolExpression *residual,
-                     std::vector<char> &expanded) {
+                       std::vector<char> &expanded) {
   if (idx >= order.size() || expanded[idx])
     return;
 
@@ -195,7 +195,7 @@ void ROBDD::expandFrom(unsigned idx, BoolExpression *residual,
 }
 
 std::vector<unsigned> ROBDD::collectSubgraph(unsigned root, unsigned t1,
-                                                   unsigned t0) const {
+                                             unsigned t0) const {
   std::vector<char> vis(nodes.size(), 0);
   std::vector<unsigned> st{root};
   std::vector<unsigned> subgraph;
@@ -233,8 +233,8 @@ std::vector<unsigned> ROBDD::collectSubgraph(unsigned root, unsigned t1,
   return subgraph;
 }
 
-bool ROBDD::doesPairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsigned a,
-                            unsigned b) const {
+bool ROBDD::doesPairCoverAllPaths(unsigned root, unsigned t1, unsigned t0,
+                                  unsigned a, unsigned b) const {
   std::vector<char> vis(nodes.size(), 0);
   std::vector<unsigned> st{root};
 
@@ -265,7 +265,8 @@ bool ROBDD::doesPairCoverAllPaths(unsigned root, unsigned t1, unsigned t0, unsig
 }
 
 std::vector<std::pair<unsigned, unsigned>>
-ROBDD::findPairsCoveringAllPaths(unsigned root, unsigned t1, unsigned t0) const {
+ROBDD::findPairsCoveringAllPaths(unsigned root, unsigned t1,
+                                 unsigned t0) const {
   // Collect and validate the subgraph (sorted, includes root/t1/t0).
   std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
   std::vector<std::pair<unsigned, unsigned>> coverPairs;
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 18612a1cda..fca896b217 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -15,8 +15,8 @@
 #include "experimental/Support/FtdImplementation.h"
 #include "dynamatic/Analysis/ControlDependenceAnalysis.h"
 #include "dynamatic/Support/Backedge.h"
-#include "experimental/Support/BooleanLogic/ROBDD.h"
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
+#include "experimental/Support/BooleanLogic/ROBDD.h"
 #include "experimental/Support/FtdSupport.h"
 #include "mlir/Analysis/CFGLoopInfo.h"
 #include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h"
@@ -840,7 +840,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   };
 
   // List all-paths-covering pairs (sorted).
-  auto pairs = robdd.findPairsCoveringAllPaths(startIdx, trueSinkIdx, falseSinkIdx);
+  auto pairs =
+      robdd.findPairsCoveringAllPaths(startIdx, trueSinkIdx, falseSinkIdx);
 
   // No pair → no mux; return `start` condition (maybe inverted).
   if (pairs.empty()) {
@@ -856,7 +857,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
                 nodes[startIdx].falseSucc == trueSinkIdx);
 
     if (!dir && !inv) {
-      llvm::errs() << "convertRobddToCircuit: start node doesn't map to sinks.\n";
+      llvm::errs()
+          << "convertRobddToCircuit: start node doesn't map to sinks.\n";
       llvm::errs() << "  Summary\n";
       llvm::errs() << "    nodes.size = " << nodes.size() << "\n";
       llvm::errs() << "    startIdx   = " << startIdx << "\n";
@@ -971,11 +973,12 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   return muxChain.back().out;
 }
 
-/// Convert the entire ROBDD into a circuit by invoking buildMuxTree on the ROBDD
-/// root with terminal nodes {one, zero}. The result is a MUX tree in which each
-/// variable appears exactly once.
+/// Convert the entire ROBDD into a circuit by invoking buildMuxTree on the
+/// ROBDD root with terminal nodes {one, zero}. The result is a MUX tree in
+/// which each variable appears exactly once.
 static Value convertRobddToCircuit(PatternRewriter &rewriter, Block *block,
-                          const ftd::BlockIndexing &bi, const ROBDD &robdd) {
+                                   const ftd::BlockIndexing &bi,
+                                   const ROBDD &robdd) {
   return buildMuxTree(rewriter, block, bi, robdd, robdd.root(), robdd.one(),
                       robdd.zero());
 }
@@ -1160,7 +1163,8 @@ static void insertDirectSuppression(
                       "insertDirectSuppression.\n";
       std::abort();
     }
-    Value branchCond = convertRobddToCircuit(rewriter, consumer->getBlock(), bi, robdd);
+    Value branchCond =
+        convertRobddToCircuit(rewriter, consumer->getBlock(), bi, robdd);
 
     rewriter.setInsertionPointToStart(consumer->getBlock());
     auto branchOp = rewriter.create<handshake::ConditionalBranchOp>(

From e08ba8b5c26a90f70293946b2b38774f6ee307b3 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 22:29:29 +0100
Subject: [PATCH 14/21] give meaningful names

---
 .../lib/Support/BooleanLogic/ROBDD.cpp        | 84 +++++++++++--------
 1 file changed, 50 insertions(+), 34 deletions(-)

diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
index 6a0da848cd..510fbb0192 100644
--- a/experimental/lib/Support/BooleanLogic/ROBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -233,60 +233,76 @@ std::vector<unsigned> ROBDD::collectSubgraph(unsigned root, unsigned t1,
   return subgraph;
 }
 
-bool ROBDD::doesPairCoverAllPaths(unsigned root, unsigned t1, unsigned t0,
-                                  unsigned a, unsigned b) const {
-  std::vector<char> vis(nodes.size(), 0);
-  std::vector<unsigned> st{root};
+bool ROBDD::doesPairCoverAllPaths(unsigned rootNode, unsigned trueTerminal,
+                                  unsigned falseTerminal, unsigned coverNodeA,
+                                  unsigned coverNodeB) const {
+  // Use a visited array to avoid cycles and redundant processing.
+  std::vector<char> visited(nodes.size(), 0);
+  std::vector<unsigned> workStack{rootNode};
+
+  // Helper to push valid successors to the stack.
+  auto pushToStack = [&](unsigned v) {
+    // If we hit either of the covering nodes, the path is "blocked" or
+    // "covered" by them, so we stop traversing this path (effectively treating
+    // them as sinks).
+    if (v == coverNodeA || v == coverNodeB)
+      return;
 
-  auto push = [&](unsigned v) {
-    if (v == a || v == b)
-      return; // skip banned nodes
-    if (v < nodes.size() && !vis[v])
-      st.push_back(v);
+    if (v < nodes.size() && !visited[v])
+      workStack.push_back(v);
   };
 
-  while (!st.empty()) {
-    unsigned u = st.back();
-    st.pop_back();
-    if (u >= nodes.size() || vis[u] || u == a || u == b)
+  while (!workStack.empty()) {
+    unsigned u = workStack.back();
+    workStack.pop_back();
+
+    // Standard DFS checks: bounds, visited, or hitting the cover nodes (double
+    // check).
+    if (u >= nodes.size() || visited[u] || u == coverNodeA || u == coverNodeB)
       continue;
-    vis[u] = 1;
+    visited[u] = 1;
 
-    // Reaching either sink means not covering all paths.
-    if (u == t1 || u == t0)
+    // If we managed to reach either terminal without hitting coverNodeA or
+    // coverNodeB, then the pair does NOT cover all paths.
+    if (u == trueTerminal || u == falseTerminal)
       return false;
 
     const auto &nd = nodes[u];
-    push(nd.falseSucc);
-    push(nd.trueSucc);
+    pushToStack(nd.falseSucc);
+    pushToStack(nd.trueSucc);
   }
-  // Neither sink reachable -> covering all paths.
+
+  // If the stack is empty and we never reached a terminal,
+  // all paths were covered by the pair.
   return true;
 }
 
 std::vector<std::pair<unsigned, unsigned>>
-ROBDD::findPairsCoveringAllPaths(unsigned root, unsigned t1,
-                                 unsigned t0) const {
-  // Collect and validate the subgraph (sorted, includes root/t1/t0).
-  std::vector<unsigned> cand = collectSubgraph(root, t1, t0);
-  std::vector<std::pair<unsigned, unsigned>> coverPairs;
+ROBDD::findPairsCoveringAllPaths(unsigned rootNode, unsigned trueTerminal,
+                                 unsigned falseTerminal) const {
+  // Collect and validate the subgraph (sorted, includes root, trueTerminal,
+  // falseTerminal).
+  std::vector<unsigned> candidates =
+      collectSubgraph(rootNode, trueTerminal, falseTerminal);
+  std::vector<std::pair<unsigned, unsigned>> coveringPairs;
 
   // Scan all pairs in ascending order.
-  for (size_t i = 1; i < cand.size() - 2; ++i) {
-    for (size_t j = i + 1; j < cand.size(); ++j) {
-      if (doesPairCoverAllPaths(root, t1, t0, cand[i], cand[j])) {
-        coverPairs.emplace_back(cand[i], cand[j]);
+  for (size_t i = 1; i < candidates.size() - 2; ++i) {
+    for (size_t j = i + 1; j < candidates.size(); ++j) {
+      if (doesPairCoverAllPaths(rootNode, trueTerminal, falseTerminal,
+                                candidates[i], candidates[j])) {
+        coveringPairs.emplace_back(candidates[i], candidates[j]);
       }
     }
   }
 
   // Sort lexicographically by (first, second).
-  std::sort(coverPairs.begin(), coverPairs.end(),
-            [](const auto &a, const auto &b) {
-              if (a.first != b.first)
-                return a.first < b.first;
-              return a.second < b.second;
+  std::sort(coveringPairs.begin(), coveringPairs.end(),
+            [](const auto &lhs, const auto &rhs) {
+              if (lhs.first != rhs.first)
+                return lhs.first < rhs.first;
+              return lhs.second < rhs.second;
             });
 
-  return coverPairs;
+  return coveringPairs;
 }
\ No newline at end of file

From 3f024cec3eff5e55dc1532817bb9751c793bfdf8 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 22:40:47 +0100
Subject: [PATCH 15/21] leaf nodes update

---
 experimental/lib/Support/BooleanLogic/ROBDD.cpp | 10 ++++++++--
 experimental/lib/Support/FtdImplementation.cpp  |  4 ++--
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
index 510fbb0192..afeb257e03 100644
--- a/experimental/lib/Support/BooleanLogic/ROBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -15,6 +15,7 @@
 #include "experimental/Support/BooleanLogic/BoolExpression.h"
 
 #include <algorithm>
+#include <climits>
 #include <functional>
 #include <set>
 #include <string>
@@ -86,8 +87,13 @@ ROBDD::buildROBDDFromExpression(BoolExpression *expr,
     nodes.resize(2);
     zeroIndex = 0;
     oneIndex = 1;
-    nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
-    nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
+
+    // Terminals have no variables and no successors (indicated by specific
+    // sentinel values like UINT_MAX). Note: We create BOTH terminals to
+    // maintain valid zeroIndex/oneIndex invariants for the class, even if one
+    // of them is unreachable in this specific trivial graph.
+    nodes[zeroIndex] = {"", UINT_MAX, UINT_MAX, {}};
+    nodes[oneIndex] = {"", UINT_MAX, UINT_MAX, {}};
     rootIndex = (rootExpr->type == ExpressionType::One) ? oneIndex : zeroIndex;
     return success();
   }
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index fca896b217..a9dfffa42b 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -340,7 +340,7 @@ runCytronAlgorithm(Region &funcRegion, DenseMap<Block *, Value> &inputBlocks) {
 
 LogicalResult experimental::ftd::createPhiNetwork(
     Region &funcRegion, PatternRewriter &rewriter, SmallVector<Value> &vals,
-    SmallVector<OpOperand *> &toSubstitue) {
+    SmallVector<OpOperand *> &toSubstitute) {
 
   if (vals.empty()) {
     llvm::errs() << "Input of \"createPhiNetwork\" is empty";
@@ -478,7 +478,7 @@ LogicalResult experimental::ftd::createPhiNetwork(
     inputPerBlock[&bb] = foundValue;
   }
 
-  for (auto &op : toSubstitue)
+  for (auto &op : toSubstitute)
     op->set(inputPerBlock[op->getOwner()->getBlock()]);
 
   return success();

From 0304305a51ab0abb01544d2617a52ab526f656f3 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 22:55:38 +0100
Subject: [PATCH 16/21] name polishment and remove brackets

---
 .../lib/Support/BooleanLogic/ROBDD.cpp        | 48 ++++++++++---------
 1 file changed, 25 insertions(+), 23 deletions(-)

diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
index afeb257e03..cc451b4641 100644
--- a/experimental/lib/Support/BooleanLogic/ROBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -100,12 +100,10 @@ ROBDD::buildROBDDFromExpression(BoolExpression *expr,
 
   // Keep only variables that still appear after minimization and respect
   // the order provided by the user.
-  {
-    std::set<std::string> present = rootExpr->getVariables();
-    for (const auto &v : varOrder)
-      if (present.find(v) != present.end())
-        order.push_back(v);
-  }
+  std::set<std::string> present = rootExpr->getVariables();
+  for (const auto &v : varOrder)
+    if (present.find(v) != present.end())
+      order.push_back(v);
 
   // Pre-allocate all internal nodes; initially connect them to the terminals.
   const unsigned n = (unsigned)order.size();
@@ -200,22 +198,26 @@ void ROBDD::expandFrom(unsigned idx, BoolExpression *residual,
     expandFrom(tSucc, f1, expanded);
 }
 
-std::vector<unsigned> ROBDD::collectSubgraph(unsigned root, unsigned t1,
-                                             unsigned t0) const {
-  std::vector<char> vis(nodes.size(), 0);
-  std::vector<unsigned> st{root};
+std::vector<unsigned> ROBDD::collectSubgraph(unsigned rootNode,
+                                             unsigned trueTerminal,
+                                             unsigned falseTerminal) const {
+  std::vector<char> visited(nodes.size(), 0);
+  std::vector<unsigned> workStack{rootNode};
   std::vector<unsigned> subgraph;
 
-  while (!st.empty()) {
-    unsigned u = st.back();
-    st.pop_back();
-    if (u >= nodes.size() || vis[u])
+  while (!workStack.empty()) {
+    unsigned u = workStack.back();
+    workStack.pop_back();
+
+    // Bounds check and visited check
+    if (u >= nodes.size() || visited[u])
       continue;
-    vis[u] = 1;
+    
+    visited[u] = 1;
     subgraph.push_back(u);
 
     // Stop expansion at the designated local sinks.
-    if (u == t1 || u == t0)
+    if (u == trueTerminal || u == falseTerminal)
       continue;
 
     // Abort if we accidentally reach the global terminals.
@@ -225,15 +227,15 @@ std::vector<unsigned> ROBDD::collectSubgraph(unsigned root, unsigned t1,
     }
 
     const auto &nd = nodes[u];
-    st.push_back(nd.falseSucc);
-    st.push_back(nd.trueSucc);
+    workStack.push_back(nd.falseSucc);
+    workStack.push_back(nd.trueSucc);
   }
 
-  // Ensure both sinks appear in the final list.
-  if (std::find(subgraph.begin(), subgraph.end(), t1) == subgraph.end())
-    subgraph.push_back(t1);
-  if (std::find(subgraph.begin(), subgraph.end(), t0) == subgraph.end())
-    subgraph.push_back(t0);
+  // Ensure both designated sinks appear in the final list (if they weren't reached).
+  if (std::find(subgraph.begin(), subgraph.end(), trueTerminal) == subgraph.end())
+    subgraph.push_back(trueTerminal);
+  if (std::find(subgraph.begin(), subgraph.end(), falseTerminal) == subgraph.end())
+    subgraph.push_back(falseTerminal);
 
   std::sort(subgraph.begin(), subgraph.end());
   return subgraph;

From 1956b9bd6d6eb656a41d655ff36fe1de3a761825 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 23:05:03 +0100
Subject: [PATCH 17/21] initialization update

---
 experimental/lib/Support/BooleanLogic/ROBDD.cpp | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
index cc451b4641..f1359e3d72 100644
--- a/experimental/lib/Support/BooleanLogic/ROBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -105,15 +105,20 @@ ROBDD::buildROBDDFromExpression(BoolExpression *expr,
     if (present.find(v) != present.end())
       order.push_back(v);
 
-  // Pre-allocate all internal nodes; initially connect them to the terminals.
+  // Pre-allocate all internal nodes.
+  // Note: We initialize successors to UINT_MAX to indicate they are currently
+  // unconnected/dummies. These fields will be overwritten with actual indices
+  // during the expansion phase.
   const unsigned n = (unsigned)order.size();
   nodes.resize(n + 2);
   zeroIndex = n;
   oneIndex = n + 1;
+
   for (unsigned i = 0; i < n; ++i)
-    nodes[i] = ROBDDNode{order[i], zeroIndex, oneIndex, {}};
-  nodes[zeroIndex] = {"", zeroIndex, zeroIndex, {}};
-  nodes[oneIndex] = {"", oneIndex, oneIndex, {}};
+    nodes[i] = ROBDDNode{order[i], UINT_MAX, UINT_MAX, {}};
+
+  nodes[zeroIndex] = {"", UINT_MAX, UINT_MAX, {}};
+  nodes[oneIndex] = {"", UINT_MAX, UINT_MAX, {}};
 
   // Root is always the first internal node (smallest variable index).
   rootIndex = 0;
@@ -212,7 +217,7 @@ std::vector<unsigned> ROBDD::collectSubgraph(unsigned rootNode,
     // Bounds check and visited check
     if (u >= nodes.size() || visited[u])
       continue;
-    
+
     visited[u] = 1;
     subgraph.push_back(u);
 

From 21be2ded900503a675f0045e4af3a44c3ef6b082 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 23:27:09 +0100
Subject: [PATCH 18/21] polishment

---
 experimental/lib/Support/BooleanLogic/ROBDD.cpp | 9 ++++++---
 experimental/lib/Support/FtdImplementation.cpp  | 4 ++--
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
index f1359e3d72..ee92fa38e2 100644
--- a/experimental/lib/Support/BooleanLogic/ROBDD.cpp
+++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp
@@ -236,10 +236,13 @@ std::vector<unsigned> ROBDD::collectSubgraph(unsigned rootNode,
     workStack.push_back(nd.trueSucc);
   }
 
-  // Ensure both designated sinks appear in the final list (if they weren't reached).
-  if (std::find(subgraph.begin(), subgraph.end(), trueTerminal) == subgraph.end())
+  // Ensure both designated sinks appear in the final list (if they weren't
+  // reached).
+  if (std::find(subgraph.begin(), subgraph.end(), trueTerminal) ==
+      subgraph.end())
     subgraph.push_back(trueTerminal);
-  if (std::find(subgraph.begin(), subgraph.end(), falseTerminal) == subgraph.end())
+  if (std::find(subgraph.begin(), subgraph.end(), falseTerminal) ==
+      subgraph.end())
     subgraph.push_back(falseTerminal);
 
   std::sort(subgraph.begin(), subgraph.end());
diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index a9dfffa42b..20ff4c090f 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -806,7 +806,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     // Wrap the two vertices in the pair into InputSpec objects.
     InputSpec A = nodeToSpec(u), B = nodeToSpec(v);
 
-    // Direct edge -> successor becomes constant.
+    // If there's a direct edge connecting u and v -> successor becomes constant.
     int uv = edge(u, v), vu = edge(v, u);
     if (uv != -1 && vu == -1) {
       B.isConst = true;
@@ -816,7 +816,7 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
       A.constVal = (vu == +1);
     }
 
-    // Largest common predecessor decides who goes to true.
+    // The largest common predecessor decides who goes to true.
     // nodes[].preds are already sorted in ascending order.
     unsigned chosenP = 0;
     const auto &predU = nodes[u].preds;

From cc37d959b37b7edcb8de2b1c3105a94bef986d4d Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Sun, 7 Dec 2025 23:34:50 +0100
Subject: [PATCH 19/21] polish naming and comment in buildmuxtree

---
 experimental/lib/Support/FtdImplementation.cpp | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 20ff4c090f..34db9a9046 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -804,16 +804,18 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
     };
 
     // Wrap the two vertices in the pair into InputSpec objects.
-    InputSpec A = nodeToSpec(u), B = nodeToSpec(v);
+    InputSpec specU = nodeToSpec(u);
+    InputSpec specV = nodeToSpec(v);
 
-    // If there's a direct edge connecting u and v -> successor becomes constant.
+    // If there's a direct edge connecting u and v -> successor becomes
+    // constant.
     int uv = edge(u, v), vu = edge(v, u);
     if (uv != -1 && vu == -1) {
-      B.isConst = true;
-      B.constVal = (uv == +1);
+      specV.isConst = true;
+      specV.constVal = (uv == +1);
     } else if (vu != -1 && uv == -1) {
-      A.isConst = true;
-      A.constVal = (vu == +1);
+      specU.isConst = true;
+      specU.constVal = (vu == +1);
     }
 
     // The largest common predecessor decides who goes to true.
@@ -835,8 +837,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
       }
     }
 
-    return (nodes[chosenP].trueSucc == B.nodeIdx) ? std::pair{A, B}
-                                                  : std::pair{B, A};
+    return (nodes[chosenP].trueSucc == specV.nodeIdx) ? std::pair{specU, specV}
+                                                      : std::pair{specV, specU};
   };
 
   // List all-paths-covering pairs (sorted).

From 32a73ee66d36e43c1b654c226b9f135831feedd2 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Mon, 8 Dec 2025 00:15:15 +0100
Subject: [PATCH 20/21] update comment

---
 experimental/lib/Support/FtdImplementation.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 34db9a9046..957fc6cb45 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -889,6 +889,12 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   };
 
   // Build the list of mux stages from the given all-paths-covering pairs
+  //
+  // NOTE: The vector contains a sequence of path-covering vertex pairs
+  // sorted topologically from the root towards the sinks. Each pair represents
+  // a sequential stage in the decomposition. We construct a chain of Muxes
+  // where the i-th Mux corresponds to the i-th pair, and its selection is
+  // driven by the output of the (i-1)-th Mux (or the root variable for i=0).
   std::vector<MuxSpec> muxChain;
   muxChain.reserve(pairs.size());
 

From 885ba25795636896ab2f829b20c6f915122a96e5 Mon Sep 17 00:00:00 2001
From: QinYuan2000 <qinyuan123123@gmail.com>
Date: Mon, 8 Dec 2025 00:55:12 +0100
Subject: [PATCH 21/21] small polishment

---
 experimental/lib/Support/FtdImplementation.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp
index 957fc6cb45..0a42f5a84f 100644
--- a/experimental/lib/Support/FtdImplementation.cpp
+++ b/experimental/lib/Support/FtdImplementation.cpp
@@ -845,7 +845,8 @@ static Value buildMuxTree(PatternRewriter &rewriter, Block *block,
   auto pairs =
       robdd.findPairsCoveringAllPaths(startIdx, trueSinkIdx, falseSinkIdx);
 
-  // No pair → no mux; return `start` condition (maybe inverted).
+  // No pair -> no mux; return `start` condition with a possible Boolean
+  // negation.
   if (pairs.empty()) {
     // Root is a terminal: return constant value 1/0.
     if (startIdx == trueSinkIdx)