trit_bdd/
lib.rs

1//! 三值等价的 BDD（canonical）判定。
2//!
3//! 每个 trit 仍然是双导轨 `(t, x)`：`(0,0)=False`、`(1,0)=True`、`(0,1)=Unknown`。
4//! 与 SAT 路径不同，这里把导轨直接建成 BDD：
5//!
6//! - 纯二值变量只建一根 `t` 导轨（`x ≡ false`），不付 unknown 的变量成本；
7//! - 三值变量建 `t` / `x` 两根导轨，并在根上检查 `¬(t ∧ x)`；
8//! - 门按代数真值表逐行构造（把每个输入组合的条件 OR 起来），K3/Ł3/B3 共用；
9//! - 等价 = `valid ∧ ¬(a.t ↔ b.t ∧ a.x ↔ b.x)` 为 false（BDD 是 canonical 的）；
10//! - 不等价时从差集 BDD 取一个满足赋值，还原成反例编号。
11//!
12//! BDD 的规模依赖变量顺序与函数结构；结构化公式通常很小，但某些函数会指数爆炸。
13//! 默认变量顺序是表达式首次出现顺序。
14
15#![forbid(unsafe_code)]
16
17use trit_eval::EquivalenceResult;
18
19mod encode;
20mod equiv;
21mod order;
22mod quantify;
23
24pub use equiv::{
25    PremiseCheck, equivalent_bdd, equivalent_bdd_best, equivalent_bdd_best_with_limits,
26    equivalent_bdd_with, equivalent_bdd_with_limits, equivalent_bdd_with_order,
27    premise_counterexample_bdd, premise_counterexample_bdd_with,
28    premise_counterexample_bdd_with_order, satisfiable_bdd, satisfiable_bdd_with,
29    satisfiable_bdd_with_order,
30};
31pub use order::{VarOrder, order_variables};
32pub use quantify::{
33    Quantified, Quantifier, quantify_bdd, quantify_bdd_best, quantify_bdd_best_with_limits,
34    quantify_bdd_with, quantify_bdd_with_order,
35};
36
37/// BDD 判定错误。
38#[derive(Debug, thiserror::Error)]
39pub enum BddError {
40    /// BDD 变量数超过 `u16` 上限。
41    #[error("BDD 变量数 {0} 超过 u16 上限")]
42    TooManyVariables(usize),
43    /// BDD 说可满足但取不到赋值（不应发生）。
44    #[error("BDD 缺少反例赋值")]
45    MissingWitness,
46    /// 被量化的变量不在表达式里。
47    #[error("表达式里没有变量 {0}")]
48    UnknownVariable(String),
49    /// 表达式超出资源预算。
50    #[error("表达式超出预算: {0}")]
51    Limit(#[from] trit_core::limits::LimitError),
52    /// 单个 BDD 的节点数超出预算。
53    #[error("BDD 节点数超过上限 {limit}")]
54    BudgetExceeded {
55        /// 上限。
56        limit: usize,
57    },
58}
59
60/// BDD 节点预算。
61///
62/// **这是软限额**：每次运算返回后检查 `Bdd::size()`，因此单次 `apply`／量化
63/// 在内部产生的峰值仍可能超过 `max_nodes`。需要硬内存/CPU 上界时，应把求解
64/// 放进有资源限制的进程或 worker，而不是依赖本结构。
65#[derive(Debug, Clone, Copy, PartialEq, Eq)]
66pub struct BddLimits {
67    /// 单个 BDD 允许的最大节点数（`Bdd::size`）。
68    pub max_nodes: usize,
69}
70
71impl Default for BddLimits {
72    fn default() -> Self {
73        Self {
74            max_nodes: 1_000_000,
75        }
76    }
77}
78
79impl BddLimits {
80    /// 不设上限。
81    pub const UNLIMITED: Self = Self {
82        max_nodes: usize::MAX,
83    };
84}
85
86/// 一次 BDD 计算的配置：变量顺序（`None` = 首次出现）与节点预算。
87#[derive(Debug, Clone, Copy, Default)]
88pub struct BddRequest<'a> {
89    /// 变量顺序；`None` 使用首次出现顺序。
90    pub order: Option<&'a [String]>,
91    /// 节点预算。
92    pub limits: BddLimits,
93}
94
95/// BDD 判定结果，附带差集 BDD 的节点数。
96#[derive(Debug, Clone, PartialEq, Eq)]
97pub struct BddVerdict {
98    /// 与其它引擎同形的结论。
99    pub result: EquivalenceResult,
100    /// 差集 BDD 的节点数（等价时为 0 或常量大小）。
101    pub nodes: usize,
102}
trit_bdd/lib.rs

trit_bdd/
lib.rs
