Expand description
三生（Sansheng）：三值推理工具箱的伞包。
内部实现分布在 trit-* crate；这里提供统一入口：
use sansheng::{equivalent_symbolic, Algebra, Parser};
let a = Parser::parse("a & (b | c)").unwrap();
let b = Parser::parse("(a & b) | (a & c)").unwrap();
assert!(equivalent_symbolic(&a, &b, Algebra::Kleene).unwrap().equivalent);量化按 trit 取值（{0,1,X}）解释，而不是按两根布尔导轨：
use std::collections::HashSet;
use sansheng::{Algebra, Parser, Quantifier, quantify_bdd};
let e = Parser::parse("a | !a").unwrap();
let vars = e.variables();
let q = quantify_bdd(&e, &vars, Quantifier::Forall, Algebra::Kleene, &HashSet::new()).unwrap();
assert!(!q.is_valid(), "三值域下 a=X 时 a|!a 不为真");Modules§
Structs§
- Assertion
- 一条断言。
- Assertion
Result - 单条断言的结果。
- Assignment
- 变量赋值：一组
变量名 → 取值。 - Atpg
Report - ATPG 结果。
- BddLimits
- BDD 节点预算。
- BddVerdict
- BDD 判定结果，附带差集 BDD 的节点数。
- Belnap
Row - 一行真值表：按
vars顺序的赋值与结果。 - Belnap
Table - 4^n 真值表。
- BitPlane
- 一个位平面的真值向量。
- Bus
- 向量声明。
- Circuit
- 一个电路。
- Circuit
Report - 电路分析报告。
- Coverage
Stat - 按门类型统计的覆盖率。
- Encoding
Size - 编码规模（变量数 / 子句数），用于验证二值快速路径的收益。
- Equivalence
Result - 两个表达式在给定语义下是否等价（真值表完全相同）。
- Fault
- 一个门引脚上的 stuck-at 故障。
- Gate
- 一条电路连接：门 → 输出信号，输入为信号列表。
- Parser
- 递归下降解析器。
- Policy
- 策略文件。
- Propagation
- 一条输入向量下的三值传播结果。
- Quantified
- 量化后的 BDD 与自由变量。
- Signal
- 电路中的一个信号（节点）。
- Simulation
Row - 一次输入组合下的信号取值表。
- Test
Pattern - 一个测试向量，以及它覆盖的故障下标。
- TriBit
- 三值的位并行表示：一对位平面。
- TriVec
- 位切片的三值向量。
- Truth
Table - 一个表达式的完整真值表结果。
Enums§
- Algebra
- 三值逻辑的语义体系。
- B4
- Belnap 四值。
- BddError
- BDD 判定错误。
- Circuit
Error - 电路分析错误。
- Engine
- 验证引擎。
- Expr
- 表达式节点。
- Gate
Kind - 门类型。
- Policy
Error - 策略错误。
- Quantifier
- 量化方向。
- Symbolic
Error - 符号化判定错误。
- Ternary
- 三值逻辑中的单个取值。
- Untestable
Reason - 不可测故障的原因。
- VarOrder
- BDD 的静态变量排序策略。
Functions§
- analyze
- 对电路做一次完整分析。
- assignment_
index - 把赋值编码成编号；无效域返回
None。 - decode_
assignment - 把三进制赋值编号解码为各变量的取值。
- encoding_
size - 只构建编码并返回规模，不求解；用于验证二值快速路径的收益。
- equivalent
- 判断两个表达式在给定语义下是否逻辑等价（默认预算）。
- equivalent_
bdd - 用 BDD 判定两个表达式在给定语义下是否等价。
- equivalent_
bdd_ best - 试四种静态排序，取差集 BDD 节点数最少者；平局保留先出现者。
- equivalent_
bdd_ with_ limits - 同
equivalent_bdd，但可指定 BDD 节点预算。 - equivalent_
bdd_ with_ order - 用指定变量顺序判定；顺序里缺失的变量按首次出现顺序补在末尾。
- equivalent_
belnap - 在全部
4^n赋值上判定两个表达式是否逐点相等（默认预算）。 - equivalent_
symbolic - 用 SAT 判定等价（所有变量都按三值处理）。
- equivalent_
symbolic_ with - 用 SAT 判定等价；
binary_vars里的变量被固定为已知二值，其子图走经典 CNF。 - eval
- 单点求值：按赋值计算表达式值。
- eval_
belnap - 在给定赋值下求值；未出现的变量按
N处理。 - eval_
bitwise - 位并行求值：把表达式编译成对位平面的操作。
- generate_
tests - 压缩时允许的最多 X 位（填充搜索是启发式的，超过就放弃合并）。 生成 stuck-at 测试向量。
- minimal_
counterexample - 最小反例：只保留区分两边所必需的变量。
- order_
variables - 按给定策略排列两个表达式的并集变量。
- propagate
- 给定一条主输入赋值，做一遍三值传播。
- quantify_
bdd - 对表达式做三值量化。
- satisfiable
- 是否存在合法赋值使表达式为
True；返回一个见证。 - satisfiable_
bdd - 是否存在合法赋值使表达式为
True；返回一个见证。 - table_
belnap - 生成 4^n 真值表（默认预算）。
- truth_
table - 全真值表求值（默认预算）。
Type Aliases§
- VarMap
- 变量名 → 位平面下标的映射。