trit-core 0.8.1

//! 库级资源预算：AST 深度/节点数/枚举变量数。
//!
//! CLI 与各引擎入口共用同一套 `Limits`；默认值对交互式使用足够宽，
//! 调用方可以按场景收紧（例如 WASM 页面只允许 10 个变量）。

use crate::ast::Expr;

/// 资源预算。
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct Limits {
    /// AST 最大深度（根为 1）。
    pub max_depth: usize,
    /// AST 最大节点数。
    pub max_nodes: usize,
    /// 允许做 `3^n` 枚举的变量数上限。
    pub max_vars: usize,
    /// 一次枚举允许生成的最大行数。
    pub max_rows: usize,
}

impl Default for Limits {
    fn default() -> Self {
        Self {
            max_depth: 256,
            max_nodes: 100_000,
            max_vars: 12,
            max_rows: 1_000_000,
        }
    }
}

/// 预算超限。
#[derive(Debug, Clone, PartialEq, Eq, thiserror::Error)]
pub enum LimitError {
    /// 深度超限。
    #[error("表达式深度超过 {limit} 层")]
    Depth {
        /// 上限。
        limit: usize,
    },
    /// 节点数超限。
    #[error("表达式节点数超过 {limit}")]
    Nodes {
        /// 上限。
        limit: usize,
    },
    /// 变量数超出枚举预算。
    #[error("表达式变量数超过 {limit}（3^n 枚举不可行）")]
    Vars {
        /// 上限。
        limit: usize,
    },
    /// 赋值空间 `3^n` 超出 `u64` 可表示范围。
    #[error("赋值空间 3^{vars} 超出 u64 容量")]
    CountOverflow {
        /// 变量数。
        vars: usize,
    },
    /// 枚举行数超出预算。
    #[error("枚举行数超过 {limit}")]
    Rows {
        /// 上限。
        limit: usize,
    },
    /// 分块基址非法：必须是 64 的倍数，且 `base + 63` 不溢出。
    #[error("分块基址 {base} 非法：必须为 64 的倍数且不溢出")]
    ChunkBase {
        /// 实际基址。
        base: u64,
    },
}

/// 计算 `3^n`；溢出返回 [`LimitError::CountOverflow`]。
pub fn checked_pow3(n: usize) -> Result<u64, LimitError> {
    let exp = u32::try_from(n).unwrap_or(u32::MAX);
    3u64.checked_pow(exp)
        .ok_or(LimitError::CountOverflow { vars: n })
}

/// 迭代遍历 AST，检查深度与节点数（不递归，避免自身爆栈）。
pub fn check_expr(expr: &Expr, limits: Limits) -> Result<(), LimitError> {
    let mut stack: Vec<(&Expr, usize)> = vec![(expr, 1)];
    let mut nodes = 0usize;
    while let Some((node, depth)) = stack.pop() {
        if depth > limits.max_depth {
            return Err(LimitError::Depth {
                limit: limits.max_depth,
            });
        }
        nodes += 1;
        if nodes > limits.max_nodes {
            return Err(LimitError::Nodes {
                limit: limits.max_nodes,
            });
        }
        match node {
            Expr::Const(_) | Expr::Var(_) => {}
            Expr::Not(inner) => stack.push((inner, depth + 1)),
            Expr::And(a, b)
            | Expr::Or(a, b)
            | Expr::Xor(a, b)
            | Expr::Implies(a, b)
            | Expr::Equiv(a, b) => {
                stack.push((a, depth + 1));
                stack.push((b, depth + 1));
            }
        }
    }
    Ok(())
}

/// 检查变量数是否在 `3^n` 枚举预算内（应先调用 [`check_expr`] 保证深度安全）。
pub fn check_vars(expr: &Expr, limits: Limits) -> Result<(), LimitError> {
    let count = expr.variables().len();
    if count > limits.max_vars {
        return Err(LimitError::Vars {
            limit: limits.max_vars,
        });
    }
    Ok(())
}

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

    #[test]
    fn default_limits_accept_ordinary_expressions() {
        let e = Parser::parse("(a & b) | (!c => d)").unwrap();
        assert!(check_expr(&e, Limits::default()).is_ok());
    }

    #[test]
    fn depth_limit_is_enforced() {
        let e = Parser::parse("!!!!a").unwrap();
        let tight = Limits {
            max_depth: 3,
            ..Limits::default()
        };
        assert!(matches!(
            check_expr(&e, tight),
            Err(LimitError::Depth { .. })
        ));
    }

    #[test]
    fn node_limit_is_enforced() {
        let e = Parser::parse("a & b & c & d").unwrap();
        let tight = Limits {
            max_nodes: 4,
            ..Limits::default()
        };
        assert!(matches!(
            check_expr(&e, tight),
            Err(LimitError::Nodes { .. })
        ));
    }

    #[test]
    fn var_limit_is_enforced() {
        let e = Parser::parse("a & b & c").unwrap();
        let tight = Limits {
            max_vars: 2,
            ..Limits::default()
        };
        assert!(matches!(
            check_vars(&e, tight),
            Err(LimitError::Vars { .. })
        ));
    }
}