CegWorkbook — a thin wrapper that suppresses phantom #CIRC errors from mutually-exclusive IF branches

[VTO-AhmedHassan]

CegWorkbook — a thin wrapper that suppresses phantom #CIRC errors from mutually-exclusive IF branches

@VTO-AhmedHassan @ahah43 @DrRoot85

Abstract

formualizer correctly raises #CIRC when two cells reference each other — but not all such cycles are real. When the cross-references sit inside mutually-exclusive IF branches, the cycle exists in the static dependency graph yet can never execute at runtime. This project introduces a Conditional Edge Graph (CEG) layer that annotates each dependency edge with the condition under which it fires (WhenTrue(guard), WhenFalse(guard), or Always), detects cycles whose edges are provably contradictory, and evaluates those cells lazily using short-circuit IF semantics — suppressing the phantom #CIRC without touching formualizer internals. Phantom detection uses backtracking DFS over the SCC sub-graph to test the satisfiability of every simple cycle's condition conjunction, handling chains of any length. Real cycles are preserved. The implementation wraps Workbook via Deref, so the calling code changes by exactly one word.

---

The problem

Consider this valid spreadsheet pattern:

A1 = TRUE
A2 = =IF(A1, 555, A3)   ← references A3 only in the FALSE branch
A3 = =IF(A1, A2, 999)   ← references A2 only in the TRUE branch

When A1 = TRUE, A2 takes its true branch (555) and A3 follows A2. When A1 = FALSE, A3 takes its false branch (999) and A2 follows A3. At runtime, only one direction of the A2↔A3 reference is ever active — the other is dead code for that value of A1. The spreadsheet is mathematically sound.

formualizer's cycle detector, however, sees the flat dependency graph: A2→A3 and A3→A2. It raises #CIRC for both cells regardless of A1's value.

---

The idea: Conditional Edge Graph (CEG)

Instead of a flat graph, annotate each dependency edge with the condition under which it is active:

• A2→A3 is WhenFalse(A1) — only active when A1 is false
• A3→A2 is WhenTrue(A1) — only active when A1 is true

A cycle made entirely of edges whose conditions contradict each other (WhenTrue vs WhenFalse on the same guard cell) can never execute at runtime. It is a phantom cycle — real in the static graph, impossible at runtime.

The CEG layer:

1. Parses every formula's AST (via formualizer-parse) and walks it, annotating edges inside IF branches as WhenTrue(guard) / WhenFalse(guard) and everything else as Always
2. Runs Tarjan's SCC on the full edge set and the unconditional-only edge set separately; SCCs that appear only in the full graph and whose internal edges are all contradictory are marked phantom
3. Evaluates phantom cells lazily with short-circuit IF semantics, never calling evaluate_cell on them (so formualizer never sees the phantom dependency)

---

Usage — nearly identical to Workbook

CegWorkbook implements Deref<Target = Workbook> and DerefMut, so every Workbook method is available directly. The CEG-aware methods (set_formula, evaluate_cell) shadow the inner versions automatically.

// ── Before (formualizer) ─────────────────────────────────────────────────────
let mut wb = Workbook::new();
wb.add_sheet("Sheet1")?;
wb.set_value("Sheet1", 1, 1, LiteralValue::Boolean(true))?;
wb.set_formula("Sheet1", 2, 1, "=IF(A1, 555, A3)")?;
wb.set_formula("Sheet1", 3, 1, "=IF(A1, A2, 999)")?;
let val = wb.evaluate_cell("Sheet1", 2, 1)?;  // → #CIRC!

// ── After (CegWorkbook) ──────────────────────────────────────────────────────
let mut wb = CegWorkbook::new();               // only this line changes
wb.add_sheet("Sheet1")?;
wb.set_value("Sheet1", 1, 1, LiteralValue::Boolean(true))?;
wb.set_formula("Sheet1", 2, 1, "=IF(A1, 555, A3)")?;
wb.set_formula("Sheet1", 3, 1, "=IF(A1, A2, 999)")?;
let val = wb.evaluate_cell("Sheet1", 2, 1);   // → 555  ✓

Wrapping an existing workbook loaded from XLSX is one line:

let mut wb = CegWorkbook::wrap(Workbook::from_reader(adapter, config, LoadStrategy::EagerSheet)?);

---

Demo output

Running three cases side by side — phantom cycle, real cycle, and a normal chain — produces:

════════════════════════════════════════════════════════════════════════
  CASE 1 — Phantom / Guarded Cycle  (A2 ↔ A3 behind opposite IF branches)
════════════════════════════════════════════════════════════════════════
  [CEG] 1 phantom cycle(s) — cells involved: Phantom!A2, Phantom!A3
        conditions are mutually exclusive → #CIRC suppressed

  ┄ A1 = TRUE  →  A2 enters TRUE branch (555); A3 enters TRUE branch (→ A2 = 555)

  Cell             Formula / Value              CEG result             Original formualizer
  ──────────────   ──────────────────────────   ────────────────────   ────────────────────
  Phantom!A1       (value = TRUE)               TRUE                   TRUE
  Phantom!A2       =IF(A1, 555, A3)             555                    #CIRC!
  Phantom!A3       =IF(A1, A2, 999)             555                    #CIRC!

  ┄ A1 = FALSE →  A2 enters FALSE branch (→ A3 = 999); A3 enters FALSE branch (999)

  Cell             Formula / Value              CEG result             Original formualizer
  ──────────────   ──────────────────────────   ────────────────────   ────────────────────
  Phantom!A1       (value = FALSE)              FALSE                  FALSE
  Phantom!A2       =IF(A1, 555, A3)             999                    #CIRC!
  Phantom!A3       =IF(A1, A2, 999)             999                    #CIRC!

════════════════════════════════════════════════════════════════════════
  CASE 2 — Real Circular Reference  (B1 ↔ B2, unconditional edges)
════════════════════════════════════════════════════════════════════════
  [CEG] 1 real cycle(s) — cells involved: RealCirc!B1, RealCirc!B2
        unconditional dependency → #CIRC preserved (correct)

  Cell             Formula / Value              CEG result             Original formualizer
  ──────────────   ──────────────────────────   ────────────────────   ────────────────────
  RealCirc!B1      =B2+1                        #CIRC!                 #CIRC!
  RealCirc!B2      =B1+1                        #CIRC!                 #CIRC!

════════════════════════════════════════════════════════════════════════
  CASE 3 — Normal Cells  (linear dependency chain, no circularity)
════════════════════════════════════════════════════════════════════════
  [CEG] no cycles detected → plain delegation to formualizer

  Cell             Formula / Value              CEG result             Original formualizer
  ──────────────   ──────────────────────────   ────────────────────   ────────────────────
  Normal!A1        (value = 10)                 10                     10
  Normal!A2        =A1*3                        30                     30
  Normal!A3        =A2-5                        25                     25

Real cycles are preserved correctly (Case 2). Normal cells are unaffected (Case 3). Only phantom cycles are suppressed (Case 1).

---

Current scope and known limits

• Simple guards handled well: IF(cell, …) and IF(AND(cell1, cell2), …) — guards that reduce to concrete cell references
• Complex guards treated conservatively: conditions like IF(VLOOKUP(…)>0, …) produce Always edges (no suppression, no false positives)
• Cycles of any length supported: phantom detection uses backtracking DFS to enumerate all simple cycles and tests the condition conjunction of each path for satisfiability — works for 2-cell, 3-cell, and longer chains alike
• No changes to formualizer internals required — the CEG sits entirely outside as a pre-evaluation layer

---

Open questions for the authors

Would something like this be worth building natively into formualizer's cycle detector — perhaps as an opt-in pass that annotates edges during set_formula? Or is the current design intentional (strict cycle detection, leave suppression to the caller)? Happy to discuss the approach or refine the implementation based on your feedback.

---

The Implementation Code

// =============================================================================
// conditional_edge_graph.rs
//
// Conditional Edge Graph (CEG) — a pre-evaluation layer that sits between
// your formula-loading code and formualizer's cycle detector.
//
// PROBLEM:
//   formualizer builds a flat dependency graph from formula text and runs
//   Tarjan's SCC on it. It sees B1→C1 and C1→B1 and raises #CIRC.
//   But those edges are inside mutually-exclusive IF branches — the cycle
//   can never actually execute at runtime.
//
// SOLUTION (the CEG approach):
//   1. Parse every formula's AST yourself (using formualizer-parse).
//   2. Walk the AST. When you encounter IF(cond, true_expr, false_expr),
//      annotate the edges from true_expr as WhenTrue(cond_cell) and edges
//      from false_expr as WhenFalse(cond_cell). Everything else is Always.
//   3. Before handing formulas to formualizer, run is_phantom_cycle() over
//      any detected cycle. If ALL edges in the cycle carry conditions that
//      are mutually contradictory, the cycle is phantom — suppress the error.
//   4. Optionally: feed formualizer only the Always edges for cycle detection,
//      while keeping the full edge set for dirty-propagation (recalc).
//
// HOW TO INTEGRATE (two-step):
//   Step A — Before set_formula() calls:
//     let mut ceg = ConditionalEdgeGraph::new();
//     ceg.add_formula("Sheet1", row, col, formula_text)?;
//     // repeat for all cells
//     ceg.analyze();  // populates phantom_cycles
//
//   Step B — Guarded set_formula() calls:
//     for (sheet, row, col, formula) in formulas {
//         if ceg.would_cause_phantom_circ(&sheet, row, col) {
//             // skip formualizer's set_formula, evaluate with CEG runtime
//             // OR call wb.set_formula() but override the result if #CIRC
//         } else {
//             wb.set_formula(&sheet, row, col, &formula)?;
//         }
//     }
//
// CRATE DEPENDENCIES (add to Cargo.toml):
//   formualizer-parse = "*"
//   formualizer-common = "*"
//   formualizer-workbook = "*"   # for the integration harness at bottom
// =============================================================================

use std::collections::{HashMap, HashSet};
use std::ops::{Deref, DerefMut};

use formualizer_common::LiteralValue as FormLiteralValue;
use formualizer_parse::parser::ReferenceType;
use formualizer_parse::{parse, ASTNode, ASTNodeType};
use formualizer_workbook::{Workbook, WorkbookConfig, WorkbookMode};

// ---------------------------------------------------------------------------
// 1. Core types
// ---------------------------------------------------------------------------

/// Identifies a cell by sheet + (row, col) — 1-based to match formualizer.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct CellCoord {
    pub sheet: String,
    pub row: u32,
    pub col: u32,
}

impl CellCoord {
    pub fn new(sheet: impl Into<String>, row: u32, col: u32) -> Self {
        CellCoord {
            sheet: sheet.into(),
            row,
            col,
        }
    }

    /// Human-readable label like "Sheet1!B1"
    pub fn label(&self) -> String {
        format!("{}!{}{}", self.sheet, col_to_letter(self.col), self.row)
    }
}

/// Convert 1-based column index to Excel letter(s): 1→A, 26→Z, 27→AA …
fn col_to_letter(col: u32) -> String {
    let mut n = col;
    let mut result = String::new();
    while n > 0 {
        n -= 1;
        result.insert(0, (b'A' + (n % 26) as u8) as char);
        n /= 26;
    }
    result
}

// ---------------------------------------------------------------------------
// 2. Edge condition — the heart of the CEG idea
// ---------------------------------------------------------------------------

/// The condition under which a dependency edge is active.
///
/// Two conditions are *contradictory* if one requires a cell to be TRUE
/// while the other requires it to be FALSE simultaneously. A cycle built
/// entirely from contradictory edge-pairs can never execute → phantom cycle.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum EdgeCondition {
    /// This edge is always traversed (not inside any IF branch).
    Always,

    /// Edge is traversed only when `guard` evaluates to TRUE.
    /// Produced by: the true-branch of IF(guard, …, …).
    WhenTrue(CellCoord),

    /// Edge is traversed only when `guard` evaluates to FALSE.
    /// Produced by: the false-branch of IF(guard, …, …).
    WhenFalse(CellCoord),

    /// Edge sits inside nested IFs. All inner conditions must hold together.
    /// e.g. IF(A1, IF(B1, X, Y), Z) → X has condition [WhenTrue(A1), WhenTrue(B1)]
    Conjunction(Vec<EdgeCondition>),
}

impl EdgeCondition {
    /// Returns true if `self` and `other` can NEVER both be satisfied at once.
    ///
    /// Simple cases:
    ///   WhenTrue(A1)  vs  WhenFalse(A1)  → contradictory ✓
    ///   WhenTrue(A1)  vs  WhenTrue(A1)   → compatible    (same branch)
    ///   Always        vs  anything        → compatible    (always fires)
    ///
    /// For Conjunctions, check whether any pair of sub-conditions is
    /// contradictory, or whether the conjunction has an internal contradiction.
    pub fn contradicts(&self, other: &EdgeCondition) -> bool {
        use EdgeCondition::*;
        match (self, other) {
            (Always, _) | (_, Always) => false,

            (WhenTrue(a), WhenFalse(b)) | (WhenFalse(a), WhenTrue(b)) => a == b,

            (WhenTrue(_), WhenTrue(_)) | (WhenFalse(_), WhenFalse(_)) => false,

            // Conjunction: contradicts if ANY element contradicts the other side
            (Conjunction(parts), other) | (other, Conjunction(parts)) => {
                // Check if 'other' contradicts any element in the conjunction
                parts.iter().any(|p| p.contradicts(other))
            }
        }
    }

    /// Merge two conditions (deepen nesting for nested IFs).
    pub fn and(self, other: EdgeCondition) -> EdgeCondition {
        use EdgeCondition::*;
        match (self, other) {
            (Always, x) | (x, Always) => x,
            (Conjunction(mut a), Conjunction(b)) => {
                a.extend(b);
                Conjunction(a)
            }
            (Conjunction(mut a), x) | (x, Conjunction(mut a)) => {
                a.push(x);
                Conjunction(a)
            }
            (a, b) => Conjunction(vec![a, b]),
        }
    }
}

// ---------------------------------------------------------------------------
// 3. A single annotated dependency edge
// ---------------------------------------------------------------------------

#[derive(Debug, Clone)]
pub struct DepEdge {
    pub from: CellCoord,
    pub to: CellCoord,
    pub condition: EdgeCondition,
}

// ---------------------------------------------------------------------------
// 4. AST walker — extract conditional edges from a formula
// ---------------------------------------------------------------------------

/// Recursively walk a formualizer-parse ASTNode, accumulating DepEdges.
///
/// `owner`       — the cell whose formula we are walking
/// `outer_cond`  — the EdgeCondition inherited from any enclosing IF branch
/// `edges_out`   — output vector to push edges into
pub fn walk_ast_if(
    owner: &CellCoord,
    node: &ASTNode,
    outer_cond: EdgeCondition,
    edges_out: &mut Vec<DepEdge>,
) {
    match &node.node_type {
        // ── A reference to another cell: emit one edge ──────────────────────
        ASTNodeType::Reference {
            reference: ReferenceType::Cell {
                sheet, row, col, ..
            },
            ..
        } => {
            let target = CellCoord::new(
                sheet.clone().unwrap_or_else(|| owner.sheet.clone()),
                *row,
                *col,
            );
            edges_out.push(DepEdge {
                from: owner.clone(),
                to: target,
                condition: outer_cond,
            });
        }

        // ── IF(condition, true_branch, false_branch) — the KEY case ─────────
        ASTNodeType::Function { name, args } if name.eq_ignore_ascii_case("IF") => {
            if args.len() < 2 {
                // Malformed IF — walk it as unconditional
                for arg in args {
                    walk_ast_if(owner, arg, outer_cond.clone(), edges_out);
                }
                return;
            }
            let cond_node = &args[0];
            let true_node = &args[1];
            let false_node = args.get(2); // optional (IF with 2 args)

            // The CONDITION itself is always evaluated — unconditional edges
            walk_ast_if(owner, cond_node, outer_cond.clone(), edges_out);

            // Extract the guard cell(s) from the condition.
            // Simple case: condition IS a single cell reference.
            // Complex case: AND(A1,B1)>0, VLOOKUP(…) — treat as opaque Always
            // (conservative: won't suppress phantom cycles, but won't false-positive either)
            let guard_cells = extract_guard_cells(cond_node, &owner.sheet);

            // ── TRUE branch ──────────────────────────────────────────────────
            // Edges from the true branch fire only when ALL guard cells are TRUE
            let true_cond = guard_cells.iter().fold(outer_cond.clone(), |acc, g| {
                acc.and(EdgeCondition::WhenTrue(g.clone()))
            });
            walk_ast_if(owner, true_node, true_cond, edges_out);

            // ── FALSE branch ─────────────────────────────────────────────────
            // Edges from the false branch fire only when ALL guard cells are FALSE
            if let Some(false_node) = false_node {
                let false_cond = guard_cells.iter().fold(outer_cond.clone(), |acc, g| {
                    acc.and(EdgeCondition::WhenFalse(g.clone()))
                });
                walk_ast_if(owner, false_node, false_cond, edges_out);
            }
        }

        // ── Any other function: walk all args with same outer condition ───────
        ASTNodeType::Function { args, .. } => {
            for arg in args {
                walk_ast_if(owner, arg, outer_cond.clone(), edges_out);
            }
        }

        // ── LAMBDA/Call: walk callee and all args ────────────────────────────
        ASTNodeType::Call { callee, args } => {
            walk_ast_if(owner, callee, outer_cond.clone(), edges_out);
            for arg in args {
                walk_ast_if(owner, arg, outer_cond.clone(), edges_out);
            }
        }

        // ── Binary / unary ops: descend ──────────────────────────────────────
        ASTNodeType::BinaryOp { left, right, .. } => {
            walk_ast_if(owner, left, outer_cond.clone(), edges_out);
            walk_ast_if(owner, right, outer_cond, edges_out);
        }
        ASTNodeType::UnaryOp { expr, .. } => {
            walk_ast_if(owner, expr, outer_cond, edges_out);
        }

        // ── Range references: expand to individual cell edges ────────────────
        ASTNodeType::Reference {
            reference:
                ReferenceType::Range {
                    sheet,
                    start_row,
                    start_col,
                    end_row,
                    end_col,
                    ..
                },
            ..
        } => {
            // Only emit edges when all four bounds are concrete (not whole-row/col refs)
            if let (Some(r1), Some(c1), Some(r2), Some(c2)) =
                (start_row, start_col, end_row, end_col)
            {
                let s = sheet.clone().unwrap_or_else(|| owner.sheet.clone());
                for r in *r1..=*r2 {
                    for c in *c1..=*c2 {
                        edges_out.push(DepEdge {
                            from: owner.clone(),
                            to: CellCoord::new(s.clone(), r, c),
                            condition: outer_cond.clone(),
                        });
                    }
                }
            }
        }

        // ── Literals, named ranges, arrays, 3D refs — no local deps ─────────
        _ => {}
    }
}

/// Extract cell references that serve as the IF guard.
/// Only handles the simple case: a single CellRef as the condition.
/// Returns empty vec for complex conditions (treated as opaque/Always).
fn extract_guard_cells(cond_node: &ASTNode, default_sheet: &str) -> Vec<CellCoord> {
    match &cond_node.node_type {
        ASTNodeType::Reference {
            reference: ReferenceType::Cell {
                sheet, row, col, ..
            },
            ..
        } => {
            vec![CellCoord::new(
                sheet.clone().unwrap_or_else(|| default_sheet.to_string()),
                *row,
                *col,
            )]
        }
        // AND(A1, B1) → both must be TRUE for the true branch
        ASTNodeType::Function { name, args } if name.eq_ignore_ascii_case("AND") => args
            .iter()
            .flat_map(|a| extract_guard_cells(a, default_sheet))
            .collect(),
        // OR is not cleanly decomposable → treat as opaque
        _ => vec![],
    }
}

// ---------------------------------------------------------------------------
// 5. The Conditional Edge Graph itself
// ---------------------------------------------------------------------------

pub struct ConditionalEdgeGraph {
    /// All annotated edges, keyed by source cell.
    pub edges: HashMap<CellCoord, Vec<DepEdge>>,

    /// Cycles detected by the unconditional-only DFS (real cycles).
    pub real_cycles: Vec<Vec<CellCoord>>,

    /// Cycles detected only when including conditional edges (phantom cycles).
    /// These are safe to suppress.
    pub phantom_cycles: Vec<Vec<CellCoord>>,
}

impl ConditionalEdgeGraph {
    pub fn new() -> Self {
        ConditionalEdgeGraph {
            edges: HashMap::new(),
            real_cycles: Vec::new(),
            phantom_cycles: Vec::new(),
        }
    }

    /// Scan every formula cell in `wb`, build and analyze a CEG in one shot.
    ///
    /// Returns the analyzed graph plus a `CellCoord → formula text` map for
    /// every formula cell found (needed by `eval_smart` for phantom cells).
    ///
    /// This is the normal entry point when wrapping an existing Workbook:
    /// ```ignore
    /// let (ceg, formulas) = ConditionalEdgeGraph::from_workbook(&wb);
    /// // then in your eval loop:
    /// let val = eval_smart(&mut wb, &ceg, &formulas, sheet, row, col);
    /// ```
    fn from_workbook(wb: &Workbook) -> (Self, HashMap<CellCoord, String>) {
        let mut ceg = Self::new();
        let mut all_formulas: HashMap<CellCoord, String> = HashMap::new();

        for sheet in wb.sheet_names() {
            let Some((rows, cols)) = wb.sheet_dimensions(&sheet) else {
                continue;
            };
            for row in 1..=rows {
                for col in 1..=cols {
                    let Some(formula) = wb.get_formula(&sheet, row, col) else {
                        continue;
                    };
                    let Ok(ast) = parse(&formula) else { continue };
                    let coord = CellCoord::new(sheet.clone(), row, col);
                    ceg.add_formula(coord.clone(), &ast);
                    all_formulas.insert(coord, formula);
                }
            }
        }

        ceg.analyze();
        (ceg, all_formulas)
    }

    /// Register a formula for a cell. Call this for every formula cell
    /// BEFORE calling `analyze()`.
    ///
    /// `ast` is the parsed formula root node — produce it with:
    ///   `formualizer_parse::parse(formula_text)?`
    pub fn add_formula(&mut self, owner: CellCoord, ast: &ASTNode) {
        let mut edges = Vec::new();
        walk_ast_if(&owner, ast, EdgeCondition::Always, &mut edges);
        self.edges.insert(owner, edges);
    }

    /// Run cycle analysis. Populates `real_cycles` and `phantom_cycles`.
    /// Call once after all formulas have been added.
    pub fn analyze(&mut self) {
        // Clear previous analysis results before re-running
        self.real_cycles.clear();
        self.phantom_cycles.clear();

        // Build two adjacency maps:
        //   unconditional_adj — only Always edges (for "real" cycle detection)
        //   full_adj          — all edges (for "phantom" cycle detection)
        let unconditional_adj = self.build_adj(|e| e.condition == EdgeCondition::Always);
        let full_adj = self.build_adj(|_| true);

        let unconditional_sccs = tarjan_scc(&unconditional_adj);
        let full_sccs = tarjan_scc(&full_adj);

        // Cycles in full graph but NOT in unconditional graph → phantom
        let real_cycle_sets: HashSet<Vec<CellCoord>> = unconditional_sccs
            .iter()
            .filter(|scc| scc.len() > 1)
            .cloned()
            .collect();

        for scc in &full_sccs {
            if scc.len() <= 1 {
                continue;
            }
            let sorted = sorted_scc(scc);
            if real_cycle_sets.contains(&sorted) {
                self.real_cycles.push(scc.clone());
            } else {
                // Extra check: verify all edges in this SCC are contradictory
                if self.scc_is_phantom_by_contradiction(scc) {
                    self.phantom_cycles.push(scc.clone());
                } else {
                    // Couldn't confirm phantom — treat as real (safe default)
                    self.real_cycles.push(scc.clone());
                }
            }
        }
    }

    /// True if the given cell is part of a phantom-only cycle
    /// (safe to load into formualizer without triggering #CIRC).
    pub fn is_phantom_participant(&self, cell: &CellCoord) -> bool {
        self.phantom_cycles.iter().any(|cyc| cyc.contains(cell))
    }

    // ── Private helpers ─────────────────────────────────────────────────────

    fn build_adj<F>(&self, edge_filter: F) -> HashMap<CellCoord, Vec<CellCoord>>
    where
        F: Fn(&DepEdge) -> bool,
    {
        let mut adj: HashMap<CellCoord, Vec<CellCoord>> = HashMap::new();
        for (owner, edges) in &self.edges {
            let neighbors: Vec<CellCoord> = edges
                .iter()
                .filter(|e| edge_filter(e))
                .map(|e| e.to.clone())
                .collect();
            adj.entry(owner.clone()).or_default().extend(neighbors);
        }
        adj
    }

    /// An SCC is phantom if and only if every simple cycle through it has a
    /// contradictory condition conjunction — i.e. no closed path can ever
    /// execute at runtime.
    ///
    /// We enumerate all simple cycles via backtracking DFS from every node in
    /// the SCC.  If even one cycle is satisfiable the SCC is real.  This
    /// handles chains of any length, not just direct 2-cell back-edge pairs.
    fn scc_is_phantom_by_contradiction(&self, scc: &[CellCoord]) -> bool {
        let scc_set: HashSet<&CellCoord> = scc.iter().collect();

        // Build the internal sub-graph; bail immediately on any Always edge.
        let mut adj: HashMap<&CellCoord, Vec<(&CellCoord, &EdgeCondition)>> = HashMap::new();
        for cell in scc {
            if let Some(edges) = self.edges.get(cell) {
                for e in edges {
                    if scc_set.contains(&e.to) {
                        if e.condition == EdgeCondition::Always {
                            return false; // Unconditional edge → real cycle
                        }
                        adj.entry(cell).or_default().push((&e.to, &e.condition));
                    }
                }
            }
        }

        // Starting DFS from every node guarantees every simple cycle is visited
        // at least once (each cycle is found when `start` is the first node on it).
        for start in scc {
            let mut visited: HashSet<&CellCoord> = HashSet::from([start]);
            let mut path: Vec<&EdgeCondition> = Vec::new();
            if cycle_has_satisfiable_path(start, start, &adj, &mut visited, &mut path) {
                return false; // Found an executable cycle → not phantom
            }
        }
        true
    }
}

// ---------------------------------------------------------------------------
// 6. Phantom-cycle helpers — path satisfiability via backtracking DFS
// ---------------------------------------------------------------------------

/// DFS from `current`, looking for simple cycles back to `start`.
/// Returns `true` as soon as one cycle with a satisfiable (non-contradictory)
/// condition conjunction is found.  Explores ALL simple paths, so it handles
/// cycles of any length.
fn cycle_has_satisfiable_path<'a>(
    start: &'a CellCoord,
    current: &'a CellCoord,
    adj: &HashMap<&'a CellCoord, Vec<(&'a CellCoord, &'a EdgeCondition)>>,
    visited: &mut HashSet<&'a CellCoord>,
    path: &mut Vec<&'a EdgeCondition>,
) -> bool {
    let Some(neighbors) = adj.get(current) else {
        return false;
    };
    for (next, cond) in neighbors {
        path.push(cond);
        if *next == start {
            // Closed a cycle — satisfiable means the cycle can actually fire.
            if !path_is_contradictory(path) {
                return true;
            }
        } else if !visited.contains(next) {
            visited.insert(next);
            if cycle_has_satisfiable_path(start, next, adj, visited, path) {
                return true;
            }
            visited.remove(next);
        }
        path.pop();
    }
    false
}

/// A path's condition conjunction is contradictory — and therefore can never
/// execute — when any guard cell appears as both `WhenTrue` and `WhenFalse`.
fn path_is_contradictory(conds: &[&EdgeCondition]) -> bool {
    let mut true_guards: HashSet<&CellCoord> = HashSet::new();
    let mut false_guards: HashSet<&CellCoord> = HashSet::new();
    for cond in conds {
        collect_guards(cond, &mut true_guards, &mut false_guards);
    }
    true_guards.iter().any(|g| false_guards.contains(g))
}

/// Recursively flatten an `EdgeCondition` into its constituent guard cells,
/// accumulating them into the `true_guards` / `false_guards` sets.
fn collect_guards<'a>(
    cond: &'a EdgeCondition,
    true_guards: &mut HashSet<&'a CellCoord>,
    false_guards: &mut HashSet<&'a CellCoord>,
) {
    match cond {
        EdgeCondition::WhenTrue(g) => {
            true_guards.insert(g);
        }
        EdgeCondition::WhenFalse(g) => {
            false_guards.insert(g);
        }
        EdgeCondition::Conjunction(parts) => {
            for p in parts {
                collect_guards(p, true_guards, false_guards);
            }
        }
        EdgeCondition::Always => {}
    }
}

// ---------------------------------------------------------------------------
// 8. Tarjan's SCC — iterative implementation, works on CellCoord keys
// ---------------------------------------------------------------------------
//
// Uses a (node, next-neighbor-index) work stack so the SCC root check fires
// only AFTER all neighbors of a node have been fully explored.  The previous
// frame-enum approach checked for root inside the back-edge branch, which
// fired prematurely for DAG edges (e.g. A3→A2 in a linear chain where A2
// had no further neighbors), producing false multi-node SCCs.

fn tarjan_scc(adj: &HashMap<CellCoord, Vec<CellCoord>>) -> Vec<Vec<CellCoord>> {
    let nodes: Vec<&CellCoord> = adj.keys().collect();
    let n = nodes.len();
    let index_map: HashMap<&CellCoord, usize> =
        nodes.iter().enumerate().map(|(i, &nd)| (nd, i)).collect();

    // Pre-build integer-indexed adjacency so inner loop is O(1) per edge.
    let mut adj_idx: Vec<Vec<usize>> = vec![vec![]; n];
    for (k, vs) in adj {
        if let Some(&ki) = index_map.get(k) {
            adj_idx[ki] = vs
                .iter()
                .filter_map(|v| index_map.get(v).copied())
                .collect();
        }
    }

    let mut index_counter = 0usize;
    let mut stack: Vec<usize> = Vec::new();
    let mut on_stack: Vec<bool> = vec![false; n];
    let mut indices: Vec<Option<usize>> = vec![None; n];
    let mut lowlinks: Vec<usize> = vec![0; n];
    let mut sccs: Vec<Vec<CellCoord>> = Vec::new();

    for start in 0..n {
        if indices[start].is_some() {
            continue;
        }

        // Discover the start node
        indices[start] = Some(index_counter);
        lowlinks[start] = index_counter;
        index_counter += 1;
        stack.push(start);
        on_stack[start] = true;

        // work: (v, index of the next neighbor to process)
        let mut work: Vec<(usize, usize)> = vec![(start, 0)];

        while !work.is_empty() {
            let (v, ni) = *work.last().unwrap();

            if ni < adj_idx[v].len() {
                // Advance the neighbor pointer before any recursive push so
                // we resume at the next neighbor when we return to v.
                work.last_mut().unwrap().1 += 1;
                let w = adj_idx[v][ni];

                if indices[w].is_none() {
                    // Tree edge — discover w and push it onto the work stack.
                    indices[w] = Some(index_counter);
                    lowlinks[w] = index_counter;
                    index_counter += 1;
                    stack.push(w);
                    on_stack[w] = true;
                    work.push((w, 0));
                } else if on_stack[w] {
                    // Back edge (w is an ancestor on the current path).
                    lowlinks[v] = lowlinks[v].min(indices[w].unwrap());
                }
                // Cross/forward edges (on_stack[w] == false, already finalized) are ignored.
            } else {
                // All neighbors of v have been processed — finalize v.
                work.pop();

                // Propagate lowlink upward to the parent.
                if let Some(&(parent, _)) = work.last() {
                    lowlinks[parent] = lowlinks[parent].min(lowlinks[v]);
                }

                // If v is the root of its SCC, pop the SCC off the Tarjan stack.
                if Some(lowlinks[v]) == indices[v] {
                    let mut scc = Vec::new();
                    while let Some(node) = stack.pop() {
                        on_stack[node] = false;
                        scc.push(nodes[node].clone());
                        if node == v {
                            break;
                        }
                    }
                    sccs.push(scc);
                }
            }
        }
    }
    sccs
}

fn sorted_scc(scc: &[CellCoord]) -> Vec<CellCoord> {
    let mut s = scc.to_vec();
    s.sort_by(|a, b| a.label().cmp(&b.label()));
    s
}

// ---------------------------------------------------------------------------
// 9. Workbook evaluation helpers (generic, project-independent)
// ---------------------------------------------------------------------------
//
// These three functions are the runtime complement to ConditionalEdgeGraph.
// Drop them into any project that loads a Workbook and wants phantom-#CIRC
// suppression — no changes needed for different sheet names or cell layouts.

/// Evaluate a cell, routing phantom participants through the lazy CEG
/// evaluator and delegating everything else to formualizer as normal.
///
/// Because phantom cells are intercepted **before** `evaluate_cell` is
/// called, formualizer never sees the phantom dependency and never raises
/// `#CIRC`.
///
/// Typical usage in an eval loop:
/// ```ignore
/// let (ceg, formulas) = ConditionalEdgeGraph::from_workbook(&wb);
/// let val = eval_smart(&mut wb, &ceg, &formulas, "Sheet1", row, col);
/// ```
pub fn eval_smart(
    wb: &mut Workbook,
    ceg: &ConditionalEdgeGraph,
    all_formulas: &HashMap<CellCoord, String>,
    sheet: &str,
    row: u32,
    col: u32,
) -> FormLiteralValue {
    let coord = CellCoord::new(sheet, row, col);
    if ceg.is_phantom_participant(&coord) {
        // Clone formula text before parse+eval so we don't hold a borrow on
        // all_formulas across the &mut wb calls inside eval_ast_lazy.
        let formula = match all_formulas.get(&coord) {
            Some(f) => f.clone(),
            None => return FormLiteralValue::Empty,
        };
        match parse(&formula) {
            Ok(ast) => eval_ast_lazy(wb, ceg, all_formulas, &ast, &coord),
            Err(e) => {
                eprintln!("[CEG] parse error for {}: {e}", coord.label());
                FormLiteralValue::Empty
            }
        }
    } else {
        wb.evaluate_cell(sheet, row, col)
            .unwrap_or(FormLiteralValue::Empty)
    }
}

/// Recursively evaluate an AST node with lazy IF short-circuit semantics.
///
/// Only the taken branch of every `IF` is traversed — the phantom back-edge
/// is never followed at runtime. Cell references recurse through `eval_smart`,
/// preserving the phantom vs. non-phantom routing at every level.
fn eval_ast_lazy(
    wb: &mut Workbook,
    ceg: &ConditionalEdgeGraph,
    all_formulas: &HashMap<CellCoord, String>,
    node: &ASTNode,
    ctx: &CellCoord,
) -> FormLiteralValue {
    match &node.node_type {
        ASTNodeType::Literal(lv) => lv.clone(),

        ASTNodeType::Reference {
            reference: ReferenceType::Cell {
                sheet, row, col, ..
            },
            ..
        } => {
            let s = sheet.clone().unwrap_or_else(|| ctx.sheet.clone());
            eval_smart(wb, ceg, all_formulas, &s, *row, *col)
        }

        ASTNodeType::Function { name, args } if name.eq_ignore_ascii_case("IF") => {
            if args.is_empty() {
                return FormLiteralValue::Empty;
            }
            let cond = eval_ast_lazy(wb, ceg, all_formulas, &args[0], ctx);
            if lit_is_truthy(&cond) {
                args.get(1)
                    .map(|n| eval_ast_lazy(wb, ceg, all_formulas, n, ctx))
                    .unwrap_or(FormLiteralValue::Boolean(true))
            } else {
                args.get(2)
                    .map(|n| eval_ast_lazy(wb, ceg, all_formulas, n, ctx))
                    .unwrap_or(FormLiteralValue::Boolean(false))
            }
        }

        // For other functions inside a phantom cell's formula, fall back to
        // whatever value formualizer cached from the XLSX load.
        _ => wb
            .get_value(&ctx.sheet, ctx.row, ctx.col)
            .unwrap_or(FormLiteralValue::Empty),
    }
}

fn lit_is_truthy(lv: &FormLiteralValue) -> bool {
    match lv {
        FormLiteralValue::Boolean(b) => *b,
        FormLiteralValue::Int(n) => *n != 0,
        FormLiteralValue::Number(n) => *n != 0.0,
        FormLiteralValue::Text(s) => !s.is_empty(),
        _ => false,
    }
}

// ---------------------------------------------------------------------------
// 10. Integration harness — the public-facing façade
// ---------------------------------------------------------------------------

/// Extends `Workbook` with a Conditional Edge Graph layer that suppresses
/// phantom `#CIRC` errors caused by mutually-exclusive `IF` branches.
///
/// `CegWorkbook` implements `Deref<Target = Workbook>` and `DerefMut`, so
/// every `Workbook` method is callable directly — `wb.get_formula(...)`,
/// `wb.sheet_names()`, `wb.add_sheet(...)`, `wb.set_value(...)`, etc.
/// CEG-aware methods (`set_formula`, `evaluate_cell`) shadow the inner
/// versions automatically; the raw inner workbook is still accessible via
/// `wb.inner` when needed.
///
/// **Incremental (build from scratch):**
/// ```ignore
/// let mut wb = CegWorkbook::new();
/// wb.add_sheet("Sheet1")?;                                    // via Deref
/// wb.set_value("Sheet1", 1, 1, LiteralValue::Boolean(true))?; // via Deref
/// wb.set_formula("Sheet1", 1, 2, "=IF(A1, 55, C1)")?;
/// wb.set_formula("Sheet1", 1, 3, "=IF(A1, B1, 99)")?;
/// println!("{:?}", wb.evaluate_cell("Sheet1", 1, 2));         // → 55, no #CIRC
/// println!("{:?}", wb.get_formula("Sheet1", 1, 2));           // via Deref
/// ```
///
/// **Wrap an existing workbook (e.g. loaded from XLSX):**
/// ```ignore
/// let mut wb = CegWorkbook::wrap(Workbook::from_reader(adapter, ...)?);
/// let val = wb.evaluate_cell("Design", row, col);
/// ```
pub struct CegWorkbook {
    pub inner: Workbook,
    pub ceg: ConditionalEdgeGraph,
    /// Formula text for every cell registered via `set_formula`.
    /// Includes both phantom and non-phantom cells; needed by `eval_smart`
    /// to lazily evaluate phantom cells without calling `inner.evaluate_cell`.
    all_formulas: HashMap<CellCoord, String>,
}

impl CegWorkbook {
    /// Create an empty workbook with default config (`WorkbookMode::Interactive`).
    pub fn new() -> Self {
        Self::new_with_mode(WorkbookMode::Interactive)
    }

    /// Create an empty workbook with a specific `WorkbookMode`.
    ///
    /// `WorkbookMode::Ephemeral` disables the changelog and deferred graph
    /// building — useful for batch processing where you don't need undo history.
    /// `WorkbookMode::Interactive` is the default (changelog + deferred graph).
    pub fn new_with_mode(mode: WorkbookMode) -> Self {
        CegWorkbook {
            inner: Workbook::new_with_mode(mode),
            ceg: ConditionalEdgeGraph::new(),
            all_formulas: HashMap::new(),
        }
    }

    /// Create an empty workbook with a fully customised `WorkbookConfig`.
    ///
    /// This is the lowest-level constructor and gives full control over the
    /// evaluation engine, changelog, and ingest limits — the same levers
    /// exposed by `Workbook::new_with_config`.
    ///
    /// ```ignore
    /// use formualizer_workbook::{WorkbookConfig, WorkbookMode};
    ///
    /// let mut wb = CegWorkbook::new_with_config(WorkbookConfig::ephemeral());
    /// // or build a fully custom config:
    /// let cfg = WorkbookConfig::interactive();
    /// let mut wb = CegWorkbook::new_with_config(cfg);
    /// ```
    pub fn new_with_config(config: WorkbookConfig) -> Self {
        CegWorkbook {
            inner: Workbook::new_with_config(config),
            ceg: ConditionalEdgeGraph::new(),
            all_formulas: HashMap::new(),
        }
    }

    /// Wrap an existing `Workbook` (e.g. loaded from XLSX).
    ///
    /// Scans every formula cell, builds and analyzes the CEG in one pass.
    /// Takes ownership so all three pieces live together.
    pub fn wrap(wb: Workbook) -> Self {
        let (ceg, all_formulas) = ConditionalEdgeGraph::from_workbook(&wb);
        CegWorkbook {
            inner: wb,
            ceg,
            all_formulas,
        }
    }

    /// Register a formula. Parses it, updates the CEG, and forwards it to the
    /// inner workbook.
    ///
    /// `set_formula` on a raw `Workbook` never raises `#CIRC` — that error only
    /// surfaces at evaluation time. So we safely forward every formula (including
    /// phantom-cycle participants) to the inner workbook; `eval_smart` intercepts
    /// phantom cells before `evaluate_cell` is ever called for them.
    ///
    /// Shadows `Workbook::set_formula`.
    pub fn set_formula(
        &mut self,
        sheet: &str,
        row: u32,
        col: u32,
        formula: &str,
    ) -> Result<(), CegError> {
        let coord = CellCoord::new(sheet, row, col);
        let ast = parse(formula).map_err(|e| CegError::ParseError(e.to_string()))?;

        self.ceg.add_formula(coord.clone(), &ast);
        self.ceg.analyze();
        self.all_formulas.insert(coord, formula.to_string());

        if !self.inner.has_sheet(sheet) {
            self.inner
                .add_sheet(sheet)
                .map_err(|e| CegError::WorkbookError(e.to_string()))?;
        }
        self.inner
            .set_formula(sheet, row, col, formula)
            .map_err(|e| CegError::WorkbookError(e.to_string()))
    }

    /// CEG-aware evaluation — phantom cells are routed through the lazy IF
    /// evaluator; all others delegate to `inner.evaluate_cell`.
    ///
    /// Shadows `Workbook::evaluate_cell` so callers never accidentally hit the
    /// raw version (which can return `#CIRC` for phantom cells).
    /// Use `wb.inner.evaluate_cell(...)` to bypass CEG if you ever need the
    /// raw `Result<LiteralValue, _>` form.
    pub fn evaluate_cell(&mut self, sheet: &str, row: u32, col: u32) -> FormLiteralValue {
        eval_smart(
            &mut self.inner,
            &self.ceg,
            &self.all_formulas,
            sheet,
            row,
            col,
        )
    }

    /// Synonym for `evaluate_cell` — kept for backwards compatibility.
    pub fn eval_smart(&mut self, sheet: &str, row: u32, col: u32) -> FormLiteralValue {
        self.evaluate_cell(sheet, row, col)
    }
}

impl Deref for CegWorkbook {
    type Target = Workbook;
    fn deref(&self) -> &Workbook {
        &self.inner
    }
}

impl DerefMut for CegWorkbook {
    fn deref_mut(&mut self) -> &mut Workbook {
        &mut self.inner
    }
}

// ---------------------------------------------------------------------------
// 11. Error type
// ---------------------------------------------------------------------------

#[derive(Debug)]
pub enum CegError {
    ParseError(String),
    WorkbookError(String),
}

impl std::fmt::Display for CegError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            CegError::ParseError(s) => write!(f, "CEG parse error: {s}"),
            CegError::WorkbookError(s) => write!(f, "CEG workbook error: {s}"),
        }
    }
}

impl std::error::Error for CegError {}

// ---------------------------------------------------------------------------
// 12. Tests
// ---------------------------------------------------------------------------

#[cfg(test)]
mod tests {
    use super::*;

    fn sheet1_cell(col: u32, row: u32) -> CellCoord {
        CellCoord::new("Sheet1", row, col)
    }

    #[test]
    fn test_edge_condition_contradicts() {
        let a1 = sheet1_cell(1, 1);
        let wt = EdgeCondition::WhenTrue(a1.clone());
        let wf = EdgeCondition::WhenFalse(a1.clone());
        let al = EdgeCondition::Always;

        assert!(
            wt.contradicts(&wf),
            "WhenTrue vs WhenFalse should contradict"
        );
        assert!(
            wf.contradicts(&wt),
            "WhenFalse vs WhenTrue should contradict"
        );
        assert!(
            !wt.contradicts(&wt),
            "WhenTrue vs WhenTrue should NOT contradict"
        );
        assert!(!al.contradicts(&wf), "Always never contradicts");
        assert!(!wf.contradicts(&al), "Always never contradicts (reversed)");
    }

    #[test]
    fn test_phantom_cycle_detected() {
        // A1=TRUE, B1=IF(A1, 55, C1), C1=IF(A1, B1, 99)
        // Static graph: B1→C1 (false branch) and C1→B1 (true branch)
        // Conditions: WhenFalse(A1) and WhenTrue(A1) → contradictory → phantom
        let b1 = sheet1_cell(2, 1);
        let c1 = sheet1_cell(3, 1);

        let mut ceg = ConditionalEdgeGraph::new();

        // B1: =IF(A1, 55, C1)
        let b1_ast = parse("=IF(A1, 55, C1)").unwrap();
        ceg.add_formula(b1.clone(), &b1_ast);

        // C1: =IF(A1, B1, 99)
        let c1_ast = parse("=IF(A1, B1, 99)").unwrap();
        ceg.add_formula(c1.clone(), &c1_ast);

        ceg.analyze();

        assert!(
            ceg.real_cycles.is_empty(),
            "Should be NO real cycles, got: {:?}",
            ceg.real_cycles
        );
        assert!(
            !ceg.phantom_cycles.is_empty(),
            "Should have detected phantom cycle"
        );
        assert!(ceg.is_phantom_participant(&b1));
        assert!(ceg.is_phantom_participant(&c1));
    }

    #[test]
    fn test_real_cycle_not_suppressed() {
        // B1=C1+1, C1=B1+1 — genuine cycle, no IF guards
        let b1 = sheet1_cell(2, 1);
        let c1 = sheet1_cell(3, 1);

        // Build a simple unconditional cycle manually
        let mut ceg = ConditionalEdgeGraph::new();
        ceg.edges.insert(
            b1.clone(),
            vec![DepEdge {
                from: b1.clone(),
                to: c1.clone(),
                condition: EdgeCondition::Always,
            }],
        );
        ceg.edges.insert(
            c1.clone(),
            vec![DepEdge {
                from: c1.clone(),
                to: b1.clone(),
                condition: EdgeCondition::Always,
            }],
        );
        ceg.analyze();

        assert!(
            !ceg.real_cycles.is_empty(),
            "Should have detected real cycle"
        );
        assert!(
            ceg.phantom_cycles.is_empty(),
            "Should NOT be a phantom cycle"
        );
    }

    #[test]
    fn test_ceg_workbook_evaluates_phantom() {
        // End-to-end: A1=TRUE, B1=IF(A1,55,C1), C1=IF(A1,B1,99)
        // Expected: B1 evaluates to 55, C1 evaluates to 55 (follows B1)
        let mut wb = CegWorkbook::new();

        // Register formulas — both end up phantom after analysis
        wb.set_formula("Sheet1", 1, 2, "=IF(A1, 55, C1)").unwrap(); // B1
        wb.set_formula("Sheet1", 1, 3, "=IF(A1, B1, 99)").unwrap(); // C1

        let b1 = CellCoord::new("Sheet1", 1, 2);
        let c1 = CellCoord::new("Sheet1", 1, 3);
        assert!(wb.ceg.is_phantom_participant(&b1), "B1 should be phantom");
        assert!(wb.ceg.is_phantom_participant(&c1), "C1 should be phantom");
    }

    #[test]
    fn test_three_cell_phantom_cycle_detected() {
        // 3-cell phantom cycle guarded by the same cell (A1):
        //   B1 = IF(A1, C1, 0)   →  B1→C1 : WhenTrue(A1)
        //   C1 = IF(A1, D1, 0)   →  C1→D1 : WhenTrue(A1)
        //   D1 = IF(A1, 0, B1)   →  D1→B1 : WhenFalse(A1)
        //
        // The only closed path B1→C1→D1→B1 requires
        //   WhenTrue(A1) ∧ WhenTrue(A1) ∧ WhenFalse(A1)  — unsatisfiable.
        // The pair-level check would miss this; the path-DFS catches it.
        let b1 = CellCoord::new("Sheet1", 1, 2); // B1
        let c1 = CellCoord::new("Sheet1", 1, 3); // C1
        let d1 = CellCoord::new("Sheet1", 1, 4); // D1

        let mut ceg = ConditionalEdgeGraph::new();
        ceg.add_formula(b1.clone(), &parse("=IF(A1, C1, 0)").unwrap());
        ceg.add_formula(c1.clone(), &parse("=IF(A1, D1, 0)").unwrap());
        ceg.add_formula(d1.clone(), &parse("=IF(A1, 0, B1)").unwrap());
        ceg.analyze();

        assert!(
            ceg.real_cycles.is_empty(),
            "Should be NO real cycles, got: {:?}",
            ceg.real_cycles
        );
        assert!(
            !ceg.phantom_cycles.is_empty(),
            "Should have detected phantom cycle"
        );
        assert!(ceg.is_phantom_participant(&b1), "B1 should be phantom");
        assert!(ceg.is_phantom_participant(&c1), "C1 should be phantom");
        assert!(ceg.is_phantom_participant(&d1), "D1 should be phantom");
    }
}

[PSU3D0]

Thanks for writing this up, this is a really useful breakdown of the failure mode.

I think the core diagnosis is right: IF already short-circuits at eval time, but our dependency extraction is still basically a flat AST walk. So the graph sees both branches, Tarjan finds the SCC, and then evaluation never gets the chance to prove that only one branch is live. That mismatch is probably the main thing to fix.

One thing that would help a lot before we choose the exact shape: do you have a sanitized workbook, or even just a few representative real formulas, where this comes up? I'm especially curious whether the guards are mostly simple flags like:

=IF(A1, ..., ...)

or more like:

=IF(A1>0, ..., ...)
=IF(ISNUMBER(XLOOKUP(...)), ..., ...)
=IFS(...)
=CHOOSE(...)

That difference matters quite a bit. A bare flag-cell case is much easier to reason about than arbitrary predicates, and I would rather not design around the toy example if the real workbooks are doing something broader.

My current instinct is that there are two related but separate things here.

First, there is a nearer-term Formualizer-native fix around control-flow-aware dependencies. The places for that are probably engine/graph/formula_analysis.rs, where we currently collect formula deps, and engine/scheduler.rs, where we decide which SCCs are hard cycles. Instead of treating every branch reference as an unconditional edge, dependency extraction could tag edges that come from short-circuit-only branches of functions like IF, IFS, IFERROR, IFNA, CHOOSE, and SWITCH.

Then the scheduler does not need to solve the whole boolean satisfiability problem up front. It can treat unconditional cycles as hard #CIRC, but defer SCCs that only become cyclic through guarded/control-flow edges. At eval time the existing lazy function machinery decides which branch is actually taken. If evaluation really does re-enter a cell through a live guarded path, then we still report #CIRC. If the back-edge is in a dead branch, we never touch it.

That seems preferable to making the planner prove "this cycle is impossible" statically. It also handles cases where the guard is not just a bare cell reference, or where the guard changes between recalcs. We already have the SHORT_CIRCUIT capability flag on functions, so there is probably a reasonable native design here without asking every function implementation to invent a second dependency model.

Second, there is the bigger Excel-parity topic of iterative calculation. Excel's normal answer for circular models is "enable iterative calculation" with max-iterations and tolerance. Formualizer doesn't have that yet. That would cover real fixed-point cycles too, not just phantom branch cycles. Finance models with circular interest, debt sweeps, depreciation/tax feedback loops, etc. tend to live in that world. But that is a larger feature and probably deserves its own design issue because it raises questions about convergence policy, previous-iteration values, arrays/spills, volatiles, and so on.

So I think we should open two issues:

1. branch-aware / control-flow-aware dependency edges plus deferred cycle handling
2. iterative calculation support

The first one is likely the right starting point for this specific IF phantom-cycle case. The second one is the larger compatibility feature.

Very open to contributors here. We'd just want to keep the work aligned with that split so we don't end up with a parallel wrapper/interpreter path that is hard to keep consistent with the engine. The CEG prototype is still useful though, especially as a concrete explanation of the branch-guarded-cycle shape and as a source of test cases.

[VTO-AhmedHassan]

Real Case: "Routing Switch" Dependency Cycles in our Engineering Models

To anchor this in actual production behavior, this problem heavily impacts our engineering design workflows. We maintain a highly adaptable spreadsheet designed to model various simulation scenarios. Because VBA was not an option for our environment, we rely on "guard cells" to dynamically steer the calculation logic.
As a simple example of the pattern causing the issue: we have a sequential calculation flow where the directional dependency of the cells is toggled by a TRUE/FALSE drop-down cell. Even though only one path is ever active at a time, Formualizer’s flat dependency walk flags it as a hard cycle.

[VTO-AhmedHassan]

My initial thought for a fix was actually something akin to "branching" —where the engine splits into separate routes on each condition, evaluates them independently, and then merges them back into the main flow once the remaining steps align.
But i think this would be a major change to the available code base, so i went with this "wrapping" way.

[VTO-AhmedHassan]

sorry for the late response but i will give it more time on the weekend :)