monist_core/
graph.rs

1use crate::ast::{Atomic, Formula, FormulaArena, Var};
2use crate::eval::ExecutionLimits;
3use crate::budget::ResourceBudget;
4use std::collections::{HashMap, HashSet};
5
6#[derive(Debug, Clone, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
7pub struct ScopedVar(pub Var, pub usize);
8
9#[derive(Debug, Clone, PartialEq, Eq, Hash)]
10pub struct Constraint {
11    pub v1: ScopedVar,
12    pub v2: ScopedVar,
13    pub weight: i32,
14    pub in_comp: bool,
15}
16
17#[derive(Debug, Clone, PartialEq, Eq, Hash)]
18pub struct Edge {
19    pub source: ScopedVar,
20    pub target: ScopedVar,
21    pub weight: i32,
22    pub in_comp: bool,
23}
24
25impl From<Constraint> for Edge {
26    fn from(c: Constraint) -> Self {
27        Edge {
28            source: c.v1,
29            target: c.v2,
30            weight: c.weight,
31            in_comp: c.in_comp,
32        }
33    }
34}
35
36pub fn extract_atom_constraints(
37    atomic: &Atomic,
38    depth: usize,
39    in_comp: bool,
40    edge_count: &mut usize,
41) -> Vec<Constraint> {
42    let mut constraints = Vec::new();
43    match atomic {
44        Atomic::Eq(x, y) => {
45            let sx = ScopedVar(x.clone(), depth);
46            let sy = ScopedVar(y.clone(), depth);
47            constraints.push(Constraint {
48                v1: sx.clone(),
49                v2: sy.clone(),
50                weight: 0,
51                in_comp,
52            });
53            constraints.push(Constraint {
54                v1: sy,
55                v2: sx,
56                weight: 0,
57                in_comp,
58            });
59            *edge_count += 2;
60        }
61        Atomic::Mem(x, y) => {
62            let sx = ScopedVar(x.clone(), depth);
63            let sy = ScopedVar(y.clone(), depth);
64            constraints.push(Constraint {
65                v1: sx.clone(),
66                v2: sy.clone(),
67                weight: 1,
68                in_comp,
69            });
70            constraints.push(Constraint {
71                v1: sy,
72                v2: sx,
73                weight: -1,
74                in_comp,
75            });
76            *edge_count += 2;
77        }
78        Atomic::Lt(x, y) => {
79            let sx = ScopedVar(x.clone(), depth);
80            let sy = ScopedVar(y.clone(), depth);
81            constraints.push(Constraint {
82                v1: sy.clone(),
83                v2: sx.clone(),
84                weight: -1,
85                in_comp,
86            });
87            *edge_count += 1;
88        }
89        Atomic::QPair(p, x, y) => {
90            let sp = ScopedVar(p.clone(), depth);
91            let sx = ScopedVar(x.clone(), depth);
92            let sy = ScopedVar(y.clone(), depth);
93            constraints.push(Constraint { v1: sp.clone(), v2: sx.clone(), weight: 0, in_comp });
94            constraints.push(Constraint { v1: sx, v2: sp.clone(), weight: 0, in_comp });
95            constraints.push(Constraint { v1: sp.clone(), v2: sy.clone(), weight: 0, in_comp });
96            constraints.push(Constraint { v1: sy, v2: sp, weight: 0, in_comp });
97            *edge_count += 4;
98        }
99        Atomic::QProj1(x, p) => {
100            let sx = ScopedVar(x.clone(), depth);
101            let sp = ScopedVar(p.clone(), depth);
102            constraints.push(Constraint { v1: sx.clone(), v2: sp.clone(), weight: 0, in_comp });
103            constraints.push(Constraint { v1: sp, v2: sx, weight: 0, in_comp });
104            *edge_count += 2;
105        }
106        Atomic::QProj2(y, p) => {
107            let sy = ScopedVar(y.clone(), depth);
108            let sp = ScopedVar(p.clone(), depth);
109            constraints.push(Constraint { v1: sy.clone(), v2: sp.clone(), weight: 0, in_comp });
110            constraints.push(Constraint { v1: sp, v2: sy, weight: 0, in_comp });
111            *edge_count += 2;
112        }
113        Atomic::App(z, u, v) => {
114            let sz = ScopedVar(z.clone(), depth);
115            let su = ScopedVar(u.clone(), depth);
116            let sv = ScopedVar(v.clone(), depth);
117            constraints.push(Constraint { v1: sz.clone(), v2: sv.clone(), weight: 0, in_comp });
118            constraints.push(Constraint { v1: sv, v2: sz.clone(), weight: 0, in_comp });
119            constraints.push(Constraint { v1: sz.clone(), v2: su.clone(), weight: 0, in_comp });
120            constraints.push(Constraint { v1: su, v2: sz, weight: 0, in_comp });
121            *edge_count += 4;
122        }
123        Atomic::Lam(z, x, t) => {
124            let sz = ScopedVar(z.clone(), depth);
125            let sx = ScopedVar(x.clone(), depth);
126            let st = ScopedVar(t.clone(), depth);
127            constraints.push(Constraint { v1: sz.clone(), v2: st.clone(), weight: 0, in_comp });
128            constraints.push(Constraint { v1: st, v2: sz.clone(), weight: 0, in_comp });
129            constraints.push(Constraint { v1: sz.clone(), v2: sx.clone(), weight: 0, in_comp });
130            constraints.push(Constraint { v1: sx, v2: sz, weight: 0, in_comp });
131            *edge_count += 4;
132        }
133    }
134    constraints
135}
136
137pub fn extract_dnf_clauses(
138    arena: &FormulaArena,
139    formula_idx: usize,
140    depth: usize,
141    in_comp: bool,
142    budget: &ResourceBudget,
143    edge_count: &mut usize,
144) -> Vec<Vec<Constraint>> {
145    extract_dnf_clauses_aux(arena, formula_idx, false, depth, in_comp, budget, edge_count)
146}
147
148pub fn extract_dnf_clauses_aux(
149    arena: &FormulaArena,
150    formula_idx: usize,
151    is_negated: bool,
152    depth: usize,
153    in_comp: bool,
154    budget: &ResourceBudget,
155    edge_count: &mut usize,
156) -> Vec<Vec<Constraint>> {
157    if depth > budget.max_depth {
158        panic!("Graph Extraction Nesting Limit Exceeded");
159    }
160
161    let formula = match arena.get(formula_idx) {
162        Some(f) => f,
163        None => return vec![Vec::new()],
164    };
165
166    if !is_negated {
167        match formula {
168            Formula::Atom(atomic) => {
169                vec![extract_atom_constraints(atomic, depth, in_comp, edge_count)]
170            }
171            Formula::Neg(f_idx) => {
172                extract_dnf_clauses_aux(arena, *f_idx, true, depth, in_comp, budget, edge_count)
173            }
174            Formula::Conj(f1_idx, f2_idx) => {
175                let left_clauses = extract_dnf_clauses_aux(arena, *f1_idx, false, depth, in_comp, budget, edge_count);
176                let right_clauses = extract_dnf_clauses_aux(arena, *f2_idx, false, depth, in_comp, budget, edge_count);
177                let mut combined = Vec::new();
178                for lc in &left_clauses {
179                    for rc in &right_clauses {
180                        let mut merged = lc.clone();
181                        merged.extend(rc.clone());
182                        combined.push(merged);
183                    }
184                }
185                if combined.is_empty() {
186                    left_clauses
187                } else {
188                    combined
189                }
190            }
191            Formula::Disj(f1_idx, f2_idx) => {
192                let mut clauses = extract_dnf_clauses_aux(arena, *f1_idx, false, depth, in_comp, budget, edge_count);
193                clauses.extend(extract_dnf_clauses_aux(arena, *f2_idx, false, depth, in_comp, budget, edge_count));
194                clauses
195            }
196            Formula::Impl(f1_idx, f2_idx) => {
197                // A -> B => ~A \/ B
198                let mut clauses = extract_dnf_clauses_aux(arena, *f1_idx, true, depth, in_comp, budget, edge_count);
199                clauses.extend(extract_dnf_clauses_aux(arena, *f2_idx, false, depth, in_comp, budget, edge_count));
200                clauses
201            }
202            Formula::Univ(_, _, f_idx) | Formula::Exist(_, _, f_idx) => {
203                extract_dnf_clauses_aux(arena, *f_idx, false, depth + 1, in_comp, budget, edge_count)
204            }
205            Formula::Comp(_, _, f_idx) => {
206                extract_dnf_clauses_aux(arena, *f_idx, false, depth + 1, true, budget, edge_count)
207            }
208        }
209    } else {
210        // Negated formula branch
211        match formula {
212            Formula::Atom(atomic) => {
213                vec![extract_atom_constraints(atomic, depth, in_comp, edge_count)]
214            }
215            Formula::Neg(f_idx) => {
216                // Double negation: ~~A => A
217                extract_dnf_clauses_aux(arena, *f_idx, false, depth, in_comp, budget, edge_count)
218            }
219            Formula::Conj(f1_idx, f2_idx) => {
220                // De Morgan: ~(A /\ B) => ~A \/ ~B
221                let mut clauses = extract_dnf_clauses_aux(arena, *f1_idx, true, depth, in_comp, budget, edge_count);
222                clauses.extend(extract_dnf_clauses_aux(arena, *f2_idx, true, depth, in_comp, budget, edge_count));
223                clauses
224            }
225            Formula::Disj(f1_idx, f2_idx) => {
226                // De Morgan: ~(A \/ B) => ~A /\ ~B
227                let left_clauses = extract_dnf_clauses_aux(arena, *f1_idx, true, depth, in_comp, budget, edge_count);
228                let right_clauses = extract_dnf_clauses_aux(arena, *f2_idx, true, depth, in_comp, budget, edge_count);
229                let mut combined = Vec::new();
230                for lc in &left_clauses {
231                    for rc in &right_clauses {
232                        let mut merged = lc.clone();
233                        merged.extend(rc.clone());
234                        combined.push(merged);
235                    }
236                }
237                if combined.is_empty() {
238                    left_clauses
239                } else {
240                    combined
241                }
242            }
243            Formula::Impl(f1_idx, f2_idx) => {
244                // ~(A -> B) => A /\ ~B
245                let left_clauses = extract_dnf_clauses_aux(arena, *f1_idx, false, depth, in_comp, budget, edge_count);
246                let right_clauses = extract_dnf_clauses_aux(arena, *f2_idx, true, depth, in_comp, budget, edge_count);
247                let mut combined = Vec::new();
248                for lc in &left_clauses {
249                    for rc in &right_clauses {
250                        let mut merged = lc.clone();
251                        merged.extend(rc.clone());
252                        combined.push(merged);
253                    }
254                }
255                if combined.is_empty() {
256                    left_clauses
257                } else {
258                    combined
259                }
260            }
261            Formula::Univ(_, _, f_idx) | Formula::Exist(_, _, f_idx) => {
262                extract_dnf_clauses_aux(arena, *f_idx, true, depth + 1, in_comp, budget, edge_count)
263            }
264            Formula::Comp(_, _, f_idx) => {
265                extract_dnf_clauses_aux(arena, *f_idx, true, depth + 1, true, budget, edge_count)
266            }
267        }
268    }
269}
270
271pub fn extract_constraints_aux(
272    arena: &FormulaArena,
273    formula_idx: usize,
274    depth: usize,
275    in_comp: bool,
276    budget: &ResourceBudget,
277    edge_count: &mut usize,
278) -> Vec<Constraint> {
279    let clauses = extract_dnf_clauses(arena, formula_idx, depth, in_comp, budget, edge_count);
280    if let Some(first) = clauses.into_iter().next() {
281        first
282    } else {
283        Vec::new()
284    }
285}
286
287/// The GraphArena represents the CPU Geometry Layer in the hybrid pipeline.
288/// It translates the semantic interactions (from the `FormulaArena`) into a weighted directed graph
289/// using De Bruijn indexing and lexical depths, enabling purely structural verification.
290#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
291pub struct GraphArena {
292    pub vars: Vec<ScopedVar>,
293    pub var_to_idx: HashMap<ScopedVar, usize>,
294    pub edges: Vec<(usize, usize, i32, bool)>, // Added in_comp
295}
296
297impl GraphArena {
298    pub fn new() -> Self {
299        Self {
300            vars: Vec::new(),
301            var_to_idx: HashMap::new(),
302            edges: Vec::new(),
303        }
304    }
305
306    pub fn add_var(&mut self, var: ScopedVar) -> usize {
307        if let Some(&idx) = self.var_to_idx.get(&var) {
308            idx
309        } else {
310            let idx = self.vars.len();
311            self.vars.push(var.clone());
312            self.var_to_idx.insert(var, idx);
313            idx
314        }
315    }
316
317    pub fn from_constraints(constraints: &[Constraint]) -> Self {
318        let mut arena = Self::new();
319        for c in constraints {
320            let u = arena.add_var(c.v1.clone());
321            let v = arena.add_var(c.v2.clone());
322            arena.edges.push((u, v, c.weight, c.in_comp));
323        }
324        arena
325    }
326
327    pub fn collapse_scc_0_weight(&mut self) {
328        // Obsolete: SCC flattening is now handled natively within evaluate_topology using tarjan_scc.
329        // This is kept strictly for CLI compatibility to avoid refactoring the CLI arguments at this moment.
330    }
331
332    /// Returns Strongly Connected Components for 0-weight edges using Tarjan's single-pass algorithm.
333    pub fn tarjan_scc(&self) -> Vec<Vec<usize>> {
334        let n = self.vars.len();
335        if n == 0 {
336            return Vec::new();
337        }
338
339        let mut adj = vec![Vec::new(); n];
340        for &(u, v, w, _) in &self.edges {
341            if w == 0 {
342                adj[u].push(v);
343            }
344        }
345
346        let mut dfn = vec![None; n];
347        let mut low = vec![0; n];
348        let mut on_stack = vec![false; n];
349        let mut stack = Vec::new();
350        let mut timer = 0;
351        let mut sccs = Vec::new();
352
353        fn dfs(
354            u: usize,
355            adj: &[Vec<usize>],
356            dfn: &mut [Option<usize>],
357            low: &mut [usize],
358            on_stack: &mut [bool],
359            stack: &mut Vec<usize>,
360            timer: &mut usize,
361            sccs: &mut Vec<Vec<usize>>,
362        ) {
363            dfn[u] = Some(*timer);
364            low[u] = *timer;
365            *timer += 1;
366            stack.push(u);
367            on_stack[u] = true;
368
369            for &v in &adj[u] {
370                if dfn[v].is_none() {
371                    dfs(v, adj, dfn, low, on_stack, stack, timer, sccs);
372                    low[u] = low[u].min(low[v]);
373                } else if on_stack[v] {
374                    low[u] = low[u].min(dfn[v].unwrap());
375                }
376            }
377
378            if low[u] == dfn[u].unwrap() {
379                let mut scc = Vec::new();
380                while let Some(v) = stack.pop() {
381                    on_stack[v] = false;
382                    scc.push(v);
383                    if v == u {
384                        break;
385                    }
386                }
387                sccs.push(scc);
388            }
389        }
390
391        for i in 0..n {
392            if dfn[i].is_none() {
393                dfs(i, &adj, &mut dfn, &mut low, &mut on_stack, &mut stack, &mut timer, &mut sccs);
394            }
395        }
396
397        sccs
398    }
399
400    /// Alias to tarjan_scc for backwards compatibility
401    pub fn kosaraju_scc(&self) -> Vec<Vec<usize>> {
402        self.tarjan_scc()
403    }
404
405    pub fn contract_graph(&self, sccs: &[Vec<usize>]) -> (Vec<usize>, Vec<(usize, usize, i32)>, Vec<usize>) {
406        let n = self.vars.len();
407        let mut rep = vec![0; n];
408        for scc in sccs {
409            let r = *scc.iter().min().unwrap_or(&0);
410            for &u in scc {
411                rep[u] = r;
412            }
413        }
414
415        let mut c_vars = Vec::new();
416        let mut c_vars_set = std::collections::HashSet::new();
417        for &r in &rep {
418            if c_vars_set.insert(r) {
419                c_vars.push(r);
420            }
421        }
422
423        let mut c_edges = std::collections::HashSet::new();
424        for &(u, v, w, _) in &self.edges {
425            let ru = rep[u];
426            let rv = rep[v];
427            if ru != rv || w != 0 {
428                c_edges.insert((ru, rv, w));
429            }
430        }
431
432        (c_vars, c_edges.into_iter().collect(), rep)
433    }
434
435    /// Continuous daemon that isolates Strongly Cantorian (ZFC-compliant) bedrock
436    /// by scanning for subgraphs satisfying the x = T(x) constraint (topological self-loops)
437    /// and severing their outgoing +1 offset edges to reduce computational load.
438    pub fn isolate_sc_bedrock(&mut self) -> Vec<String> {
439        let mut sc_nodes = HashSet::new();
440
441        // Detect x = T(x) constraints: nodes that have a +1 or -1 weight self-loop.
442        // We strictly enforce that Comprehension boundaries are respected:
443        // if the self-loop is part of a Comprehension (in_comp == true), it is an
444        // unstratifiable paradox and MUST NOT be isolated as Strongly Cantorian bedrock.
445        for &(u, v, w, in_comp) in &self.edges {
446            if u == v && w != 0 && !in_comp {
447                sc_nodes.insert(u);
448            }
449        }
450
451        if sc_nodes.is_empty() {
452            return Vec::new();
453        }
454
455        let mut actions = Vec::new();
456        let mut new_edges = HashSet::new();
457
458        for &(u, v, w, in_comp) in &self.edges {
459            if u == v && w != 0 && !in_comp {
460                actions.push(format!(
461                    "Neutralized SC defining self-loop on {}",
462                    self.var_name(u)
463                ));
464                continue;
465            }
466            // Only sever connections if they are NOT inside a Comprehension
467            if sc_nodes.contains(&u) && w == 1 && !in_comp {
468                actions.push(format!(
469                    "Severed outgoing +1 offset edge from SC bedrock node {} to {}",
470                    self.var_name(u),
471                    self.var_name(v)
472                ));
473                continue;
474            }
475            if sc_nodes.contains(&v) && w == -1 && !in_comp {
476                actions.push(format!(
477                    "Severed incoming -1 offset edge to SC bedrock node {} from {}",
478                    self.var_name(v),
479                    self.var_name(u)
480                ));
481                continue;
482            }
483            new_edges.insert((u, v, w, in_comp));
484        }
485        self.edges = new_edges.into_iter().collect();
486
487        // Remove duplicates and return
488        let mut unique_actions: Vec<String> = actions
489            .into_iter()
490            .collect::<HashSet<_>>()
491            .into_iter()
492            .collect();
493        unique_actions.sort();
494        unique_actions
495    }
496
497    fn var_name(&self, u: usize) -> String {
498        let var = &self.vars[u];
499        let name = match &var.0 {
500            crate::ast::Var::Free(n) => n.clone(),
501            crate::ast::Var::Bound(idx) => format!("b{}", idx),
502        };
503        format!("{}_{}", name, var.1)
504    }
505
506
507    pub fn topological_sort(&self) -> Option<Vec<usize>> {
508        let n = self.vars.len();
509        let mut in_degree = vec![0; n];
510        let mut adj = vec![Vec::new(); n];
511
512        for &(u, v, _, _) in &self.edges {
513            adj[u].push(v);
514            in_degree[v] += 1;
515        }
516
517        let mut queue = std::collections::VecDeque::new();
518        for i in 0..n {
519            if in_degree[i] == 0 {
520                queue.push_back(i);
521            }
522        }
523
524        let mut order = Vec::new();
525        while let Some(u) = queue.pop_front() {
526            order.push(u);
527            for &v in &adj[u] {
528                in_degree[v] -= 1;
529                if in_degree[v] == 0 {
530                    queue.push_back(v);
531                }
532            }
533        }
534
535        if order.len() == n {
536            Some(order)
537        } else {
538            None
539        }
540    }
541
542    pub fn classify_subsystems(&self, d: &[i32]) -> (bool, bool) {
543        let mut base_weight = i32::MIN;
544        for (i, var) in self.vars.iter().enumerate() {
545            if let crate::ast::Var::Free(_) = var.0 {
546                if d[i] > base_weight {
547                    base_weight = d[i];
548                }
549            }
550        }
551
552        if base_weight == i32::MIN {
553            for &w in d {
554                if w > base_weight {
555                    base_weight = w;
556                }
557            }
558            if base_weight == i32::MIN {
559                base_weight = 0;
560            }
561        }
562
563        let mut is_nfi = true;
564        let mut is_nfp = true;
565
566        for (i, var) in self.vars.iter().enumerate() {
567            let weight = d[i];
568            
569            if weight > base_weight + 1 {
570                is_nfi = false;
571            }
572
573            match var.0 {
574                crate::ast::Var::Free(_) => {
575                    if weight > base_weight + 1 {
576                        is_nfp = false;
577                    }
578                }
579                crate::ast::Var::Bound(_) => {
580                    if weight > base_weight {
581                        is_nfp = false;
582                    }
583                }
584            }
585        }
586
587        (is_nfp, is_nfi)
588    }
589
590    /// Evaluates the topological structure using a hybrid approach.
591    /// It attempts a fast O(V+E) DAG Shortest Path evaluation first. If the graph contains 
592    /// cycles, it falls back to the O(V*E) Bellman-Ford algorithm to detect negative-weight cycles
593    /// (Extensionality Collisions).
594    pub fn evaluate_topology(&mut self) -> Result<(Vec<i32>, Vec<String>, bool, bool), String> {
595        // Run the continuous daemon to dynamically sever outgoing +1 offset edges from SC bedrock
596        let sc_actions = self.isolate_sc_bedrock();
597
598        let n = self.vars.len();
599        if n == 0 {
600            return Ok((Vec::new(), sc_actions, true, true));
601        }
602
603        let sccs = self.tarjan_scc();
604        let (c_vars, c_edges, reps) = self.contract_graph(&sccs);
605
606        let mut in_degree = HashMap::new();
607        for &u in &c_vars {
608            in_degree.insert(u, 0);
609        }
610        let mut adj = HashMap::new();
611        for &(u, v, w) in &c_edges {
612            adj.entry(u).or_insert_with(Vec::new).push((v, w));
613            *in_degree.entry(v).or_insert(0) += 1;
614        }
615
616        let mut queue = std::collections::VecDeque::new();
617        for (&u, &deg) in &in_degree {
618            if deg == 0 {
619                queue.push_back(u);
620            }
621        }
622
623        let mut order = Vec::new();
624        while let Some(u) = queue.pop_front() {
625            order.push(u);
626            if let Some(neighbors) = adj.get(&u) {
627                for &(v, _) in neighbors {
628                    if let Some(deg) = in_degree.get_mut(&v) {
629                        *deg -= 1;
630                        if *deg == 0 {
631                            queue.push_back(v);
632                        }
633                    }
634                }
635            }
636        }
637
638        // Fast-path: O(V+E) DAG Shortest Path on Contracted Graph
639        if order.len() == c_vars.len() {
640            let mut c_d = HashMap::new();
641            for &u in &c_vars {
642                c_d.insert(u, 0);
643            }
644            for &u in &order {
645                let du = *c_d.get(&u).unwrap();
646                if let Some(neighbors) = adj.get(&u) {
647                    for &(v, w) in neighbors {
648                        let dv = *c_d.get(&v).unwrap();
649                        if du + w < dv {
650                            c_d.insert(v, du + w);
651                        }
652                    }
653                }
654            }
655
656            let mut d = vec![0; n];
657            for i in 0..n {
658                d[i] = *c_d.get(&reps[i]).unwrap();
659            }
660
661            let (is_nfp, is_nfi) = self.classify_subsystems(&d);
662            return Ok((d, sc_actions, is_nfp, is_nfi));
663        }
664
665        // Fallback: O(V*E) Bellman-Ford
666        let mut d = vec![0; n];
667        let mut p: Vec<Option<(usize, i32)>> = vec![None; n];
668
669        // Relax edges n-1 times
670        for _ in 0..n {
671            let mut changed = false;
672            for &(u, v, w, _) in &self.edges {
673                if d[u] + w < d[v] {
674                    d[v] = d[u] + w;
675                    p[v] = Some((u, w));
676                    changed = true;
677                }
678            }
679            if !changed {
680                break;
681            }
682        }
683
684        // Final pass for negative weight cycles
685        let mut collision_vertex = None;
686        for &(u, v, w, _) in &self.edges {
687            if d[u] + w < d[v] {
688                collision_vertex = Some(v);
689                p[v] = Some((u, w));
690                break;
691            }
692        }
693
694        if let Some(mut curr) = collision_vertex {
695            let lambda_star = match ExecutionLimits::compute_for_graph(self) {
696                Some(limits) => limits.mcm,
697                None => f64::NEG_INFINITY,
698            };
699
700            for _ in 0..n {
701                curr = p[curr].unwrap().0;
702            }
703
704            let cycle_start = curr;
705            let mut cycle = Vec::new();
706
707            loop {
708                let (prev, w) = p[curr].unwrap();
709                cycle.push((prev, curr, w));
710                curr = prev;
711                if curr == cycle_start {
712                    break;
713                }
714            }
715
716            cycle.reverse();
717
718            let mut result = String::new();
719            result.push_str(&format!("Extensionality Collision: Negative-weight cycle detected (μ* = {:.4})!\n", lambda_star));
720            result.push_str("Engine halted safely (K_ITERATION_HALT)\n");
721            result.push_str("Topological Trace: ");
722
723            let mut sum_str = Vec::new();
724            let mut total_weight = 0;
725            for (u, v, w) in &cycle {
726                let u_var = &self.vars[*u];
727                let v_var = &self.vars[*v];
728
729                let u_name = match &u_var.0 {
730                    crate::ast::Var::Free(name) => name.clone(),
731                    crate::ast::Var::Bound(idx) => format!("b{}", idx),
732                };
733                let v_name = match &v_var.0 {
734                    crate::ast::Var::Free(name) => name.clone(),
735                    crate::ast::Var::Bound(idx) => format!("b{}", idx),
736                };
737
738                let u_str = format!("{}_{}", u_name, u_var.1);
739                let v_str = format!("{}_{}", v_name, v_var.1);
740
741                sum_str.push(format!("{} -> {} ({})", u_str, v_str, w));
742                total_weight += w;
743            }
744
745            result.push_str(&sum_str.join(" + "));
746            result.push_str(&format!(" = {}", total_weight));
747
748            return Err(result);
749        }
750
751        let (is_nfp, is_nfi) = self.classify_subsystems(&d);
752        Ok((d, sc_actions, is_nfp, is_nfi))
753    }
754
755    /// Extract Minimal Conflict Clauses for Vector Superposition (IDL Masking)
756    /// When Bellman-Ford flags a negative-weight cycle, this identifies the nodes
757    /// involved so the upper ingestion layer can translate them into a hyperdimensional 
758    /// destructive interference mask.
759    pub fn extract_conflict_clauses(&mut self) -> Vec<Vec<usize>> {
760        let n = self.vars.len();
761        let mut d = vec![0; n];
762        let mut p: Vec<Option<(usize, i32)>> = vec![None; n];
763        
764        // Relax edges
765        for _ in 0..n {
766            for &(u, v, w, _) in &self.edges {
767                if d[u] + w < d[v] {
768                    d[v] = d[u] + w;
769                    p[v] = Some((u, w));
770                }
771            }
772        }
773        
774        let mut conflict_clauses = Vec::new();
775        // Detect cycle
776        for &(u, v, w, _) in &self.edges {
777            if d[u] + w < d[v] {
778                // We found a node 'v' in a negative weight cycle
779                let mut curr = v;
780                for _ in 0..n {
781                    if let Some((prev, _)) = p[curr] {
782                        curr = prev;
783                    }
784                }
785                
786                let cycle_start = curr;
787                let mut cycle = Vec::new();
788                
789                loop {
790                    if let Some((prev, _)) = p[curr] {
791                        cycle.push(curr);
792                        curr = prev;
793                        if curr == cycle_start {
794                            break;
795                        }
796                    } else {
797                        break;
798                    }
799                }
800                cycle.reverse();
801                
802                // Only add if not already present
803                let mut sorted_cycle = cycle.clone();
804                sorted_cycle.sort();
805                
806                let is_duplicate = conflict_clauses.iter().any(|c: &Vec<usize>| {
807                    let mut sc = c.clone();
808                    sc.sort();
809                    sc == sorted_cycle
810                });
811                
812                if !is_duplicate {
813                    conflict_clauses.push(cycle);
814                }
815            }
816        }
817        
818        conflict_clauses
819    }
820
821    /// Evaluates a formula in Disjunctive Normal Form (DNF) across all extracted clauses.
822    /// Stratification succeeds if at least one DNF clause forms an acyclic/valid topological graph.
823    pub fn evaluate_dnf_formula(
824        arena: &FormulaArena,
825        formula_idx: usize,
826        budget: &ResourceBudget,
827    ) -> Result<(Vec<i32>, Vec<String>, bool, bool), String> {
828        let mut edge_count = 0;
829        let clauses = extract_dnf_clauses(arena, formula_idx, 0, false, budget, &mut edge_count);
830        let mut last_err = String::from("No DNF clauses generated");
831        for clause in clauses {
832            let mut graph = GraphArena::from_constraints(&clause);
833            match graph.evaluate_topology() {
834                Ok(res) => return Ok(res),
835                Err(e) => last_err = e,
836            }
837        }
838        Err(last_err)
839    }
840}
monist_core/graph.rs

monist_core/
graph.rs
