rmpca 0.1.1

//! Implementation of Hierholzers algorithm for finding Eulerian circuits.
//!
//! // Aligns with Lean4: theorem `hierholzer_finds_eulerian_circuit`

use crate::optimizer::error::RouteError;
use petgraph::graph::{DiGraph, NodeIndex};
use petgraph::visit::EdgeRef;
use std::collections::HashMap;

/// Find an Eulerian circuit in a directed graph using Hierholzers algorithm.
///
/// # Errors
/// Returns `RouteError::NotEulerian` if any node has mismatched in/out degree.
/// Returns `RouteError::EmptyGraph` if the graph has no nodes.
///
/// # Panics
/// May panic if internal invariants are violated (e.g., stack unexpectedly empty
/// during circuit construction).
// Aligns with Lean4: theorem eulerian_circuit_exists_iff_balanced
pub fn directed_eulerian_circuit<N, E: Clone>(
    graph: &DiGraph<N, E>,
    start_node: NodeIndex,
) -> Result<Vec<NodeIndex>, RouteError> {
    if graph.node_count() == 0 {
        return Ok(vec![]);
    }

    // Check if the graph is Eulerian (in-degree == out-degree for all nodes)
    for node in graph.node_indices() {
        let in_degree = graph.edges_directed(node, petgraph::Direction::Incoming).count();
        let out_degree = graph.edges_directed(node, petgraph::Direction::Outgoing).count();
        if in_degree != out_degree {
            return Err(RouteError::NotEulerian {
                node_id: format!("{node:?}"),
                in_degree,
                out_degree,
            });
        }
    }

    // Keep track of unused edges
    let mut edge_counts: HashMap<NodeIndex, Vec<NodeIndex>> = HashMap::new();
    for node in graph.node_indices() {
        let targets: Vec<NodeIndex> = graph.edges_directed(node, petgraph::Direction::Outgoing)
            .map(|e| e.target())
            .collect();
        edge_counts.insert(node, targets);
    }

    let mut circuit = Vec::new();
    let mut stack = vec![start_node];

    while let Some(u) = stack.last().copied() {
        if let Some(targets) = edge_counts.get_mut(&u) {
            if let Some(v) = targets.pop() {
                stack.push(v);
            } else {
                // SAFETY: stack.last() returned Some(&u), so stack is non-empty.
                // Popping u which we just verified has no remaining targets.
                circuit.push(
                    stack.pop().expect("stack non-empty: just verified last element exists")
                );
            }
        } else {
            // SAFETY: u came from stack.last(), so stack is non-empty.
            circuit.push(
                stack.pop().expect("stack non-empty: u came from stack.last()")
            );
        }
    }

    circuit.reverse();
    Ok(circuit)
}