Skip to main content

trit_core/
limits.rs

1//! 库级资源预算:AST 深度/节点数/枚举变量数。
2//!
3//! CLI 与各引擎入口共用同一套 `Limits`;默认值对交互式使用足够宽,
4//! 调用方可以按场景收紧(例如 WASM 页面只允许 10 个变量)。
5
6use crate::ast::Expr;
7
8/// 资源预算。
9#[derive(Debug, Clone, Copy, PartialEq, Eq)]
10pub struct Limits {
11    /// AST 最大深度(根为 1)。
12    pub max_depth: usize,
13    /// AST 最大节点数。
14    pub max_nodes: usize,
15    /// 允许做 `3^n` 枚举的变量数上限。
16    pub max_vars: usize,
17    /// 一次枚举允许生成的最大行数。
18    pub max_rows: usize,
19}
20
21impl Default for Limits {
22    fn default() -> Self {
23        Self {
24            max_depth: 256,
25            max_nodes: 100_000,
26            max_vars: 12,
27            max_rows: 1_000_000,
28        }
29    }
30}
31
32/// 预算超限。
33#[derive(Debug, Clone, PartialEq, Eq, thiserror::Error)]
34pub enum LimitError {
35    /// 深度超限。
36    #[error("表达式深度超过 {limit} 层")]
37    Depth {
38        /// 上限。
39        limit: usize,
40    },
41    /// 节点数超限。
42    #[error("表达式节点数超过 {limit}")]
43    Nodes {
44        /// 上限。
45        limit: usize,
46    },
47    /// 变量数超出枚举预算。
48    #[error("表达式变量数超过 {limit}(3^n 枚举不可行)")]
49    Vars {
50        /// 上限。
51        limit: usize,
52    },
53    /// 赋值空间 `3^n` 超出 `u64` 可表示范围。
54    #[error("赋值空间 3^{vars} 超出 u64 容量")]
55    CountOverflow {
56        /// 变量数。
57        vars: usize,
58    },
59    /// 枚举行数超出预算。
60    #[error("枚举行数超过 {limit}")]
61    Rows {
62        /// 上限。
63        limit: usize,
64    },
65    /// 分块基址非法:必须是 64 的倍数,且 `base + 63` 不溢出。
66    #[error("分块基址 {base} 非法:必须为 64 的倍数且不溢出")]
67    ChunkBase {
68        /// 实际基址。
69        base: u64,
70    },
71}
72
73/// 计算 `3^n`;溢出返回 [`LimitError::CountOverflow`]。
74pub fn checked_pow3(n: usize) -> Result<u64, LimitError> {
75    let exp = u32::try_from(n).unwrap_or(u32::MAX);
76    3u64.checked_pow(exp)
77        .ok_or(LimitError::CountOverflow { vars: n })
78}
79
80/// 迭代遍历 AST,检查深度与节点数(不递归,避免自身爆栈)。
81pub fn check_expr(expr: &Expr, limits: Limits) -> Result<(), LimitError> {
82    let mut stack: Vec<(&Expr, usize)> = vec![(expr, 1)];
83    let mut nodes = 0usize;
84    while let Some((node, depth)) = stack.pop() {
85        if depth > limits.max_depth {
86            return Err(LimitError::Depth {
87                limit: limits.max_depth,
88            });
89        }
90        nodes += 1;
91        if nodes > limits.max_nodes {
92            return Err(LimitError::Nodes {
93                limit: limits.max_nodes,
94            });
95        }
96        match node {
97            Expr::Const(_) | Expr::Var(_) => {}
98            Expr::Not(inner) => stack.push((inner, depth + 1)),
99            Expr::And(a, b)
100            | Expr::Or(a, b)
101            | Expr::Xor(a, b)
102            | Expr::Implies(a, b)
103            | Expr::Equiv(a, b) => {
104                stack.push((a, depth + 1));
105                stack.push((b, depth + 1));
106            }
107        }
108    }
109    Ok(())
110}
111
112/// 检查变量数是否在 `3^n` 枚举预算内(应先调用 [`check_expr`] 保证深度安全)。
113pub fn check_vars(expr: &Expr, limits: Limits) -> Result<(), LimitError> {
114    let count = expr.variables().len();
115    if count > limits.max_vars {
116        return Err(LimitError::Vars {
117            limit: limits.max_vars,
118        });
119    }
120    Ok(())
121}
122
123#[cfg(test)]
124mod tests {
125    use super::*;
126    use crate::parser::Parser;
127
128    #[test]
129    fn default_limits_accept_ordinary_expressions() {
130        let e = Parser::parse("(a & b) | (!c => d)").unwrap();
131        assert!(check_expr(&e, Limits::default()).is_ok());
132    }
133
134    #[test]
135    fn depth_limit_is_enforced() {
136        let e = Parser::parse("!!!!a").unwrap();
137        let tight = Limits {
138            max_depth: 3,
139            ..Limits::default()
140        };
141        assert!(matches!(
142            check_expr(&e, tight),
143            Err(LimitError::Depth { .. })
144        ));
145    }
146
147    #[test]
148    fn node_limit_is_enforced() {
149        let e = Parser::parse("a & b & c & d").unwrap();
150        let tight = Limits {
151            max_nodes: 4,
152            ..Limits::default()
153        };
154        assert!(matches!(
155            check_expr(&e, tight),
156            Err(LimitError::Nodes { .. })
157        ));
158    }
159
160    #[test]
161    fn var_limit_is_enforced() {
162        let e = Parser::parse("a & b & c").unwrap();
163        let tight = Limits {
164            max_vars: 2,
165            ..Limits::default()
166        };
167        assert!(matches!(
168            check_vars(&e, tight),
169            Err(LimitError::Vars { .. })
170        ));
171    }
172}