monist_core/
eval.rs

1use crate::graph::{Edge, GraphArena, ScopedVar};
2
3#[derive(Debug, Clone, PartialEq, Eq)]
4pub enum EvalResult {
5    Success(Vec<(ScopedVar, i32)>),
6    NegativeCycle,
7    NumericOverflow,
8}
9
10pub fn evaluate_clause(edges: &[Edge]) -> EvalResult {
11    let mut vertices = Vec::new();
12    for edge in edges {
13        if !vertices.contains(&edge.source) {
14            vertices.push(edge.source.clone());
15        }
16        if !vertices.contains(&edge.target) {
17            vertices.push(edge.target.clone());
18        }
19    }
20
21    let v_count = vertices.len();
22    if v_count == 0 {
23        return EvalResult::Success(Vec::new());
24    }
25
26    let mut dist: Vec<i64> = vec![0; v_count];
27    let get_idx = |v: &ScopedVar| vertices.iter().position(|x| x == v).unwrap();
28
29    let indexed_edges: Vec<(usize, usize, i64)> = edges
30        .iter()
31        .map(|e| (get_idx(&e.source), get_idx(&e.target), e.weight as i64))
32        .collect();
33
34    for _ in 0..(v_count - 1) {
35        let mut updated = false;
36        for &(u, v, weight) in &indexed_edges {
37            if let Some(new_dist) = dist[u].checked_add(weight) {
38                if new_dist < dist[v] {
39                    dist[v] = new_dist;
40                    updated = true;
41                }
42            } else {
43                return EvalResult::NumericOverflow;
44            }
45        }
46        if !updated {
47            break;
48        }
49    }
50
51    for &(u, v, weight) in &indexed_edges {
52        if let Some(new_dist) = dist[u].checked_add(weight) {
53            if new_dist < dist[v] {
54                return EvalResult::NegativeCycle;
55            }
56        } else {
57            return EvalResult::NumericOverflow;
58        }
59    }
60
61    let final_dist = vertices.into_iter().zip(dist.into_iter().map(|d| d as i32)).collect();
62    EvalResult::Success(final_dist)
63}
64
65#[derive(Debug, Clone)]
66pub struct ExecutionLimits {
67    pub max_k_iterations: usize,
68    pub mcm: f64,
69}
70
71impl ExecutionLimits {
72    pub fn compute_for_graph(graph: &GraphArena) -> Option<Self> {
73        let n = graph.vars.len();
74        if n == 0 {
75            return None;
76        }
77
78        const INF: i64 = i64::MAX / 2;
79
80        // Karp's Minimum Cycle Mean (MCM) Algorithm
81        // DP array: dp[k][v] = min weight of path of length k to v
82        let mut dp = vec![vec![INF; n]; n + 1];
83        for v in 0..n {
84            dp[0][v] = 0;
85        }
86
87        for k in 1..=n {
88            for &(u, v, w, _) in &graph.edges {
89                if dp[k - 1][u] == INF {
90                    continue;
91                }
92                if let Some(new_dist) = dp[k - 1][u].checked_add(w as i64) {
93                    if new_dist < dp[k][v] {
94                        dp[k][v] = new_dist;
95                    }
96                } else {
97                    return None; // numeric overflow
98                }
99            }
100        }
101
102        let mut mcm: f64 = f64::INFINITY;
103        let mut has_cycle = false;
104
105        for v in 0..n {
106            if dp[n][v] == INF {
107                continue;
108            }
109            let mut min_val: f64 = f64::NEG_INFINITY;
110            for k in 0..n {
111                if dp[k][v] == INF {
112                    continue;
113                }
114                let val = (dp[n][v] - dp[k][v]) as f64 / (n - k) as f64;
115                if val > min_val {
116                    min_val = val;
117                }
118            }
119            if min_val < mcm {
120                mcm = min_val;
121                has_cycle = true;
122            }
123        }
124
125        if !has_cycle {
126            mcm = 0.0;
127        }
128
129        // K-Iteration based on Pigeonhole Principle
130        let max_iterations = if mcm < 0.0 {
131            // Negative cycle indicates Extensionality Collision, halt early.
132            0
133        } else {
134            // Safe geometric limits
135            n * 2
136        };
137
138        Some(ExecutionLimits {
139            max_k_iterations: max_iterations,
140            mcm,
141        })
142    }
143}
monist_core/eval.rs

monist_core/
eval.rs
