tptp

一个针对 TPTP 格式的解析器 crate。

功能

• nom 解析器提供最大灵活性
• 高性能、流式、零拷贝解析
• 便捷抽象：访问者模式、输入迭代器
• 遵循 TPTP BNF
• 完全支持 CNF/FOF 方言
• 不断增长的 TFX 支持

文档和示例

文档在 docs.rs。 examples/ 目录包含一些简单的程序。《code>tptp2json/ 包含一个稍微复杂一些的程序，用于通过 serde 将 TPTP 输入转换为 JSON Lines。

性能

“足够快”。

非科学的基准测试

$ cargo bench
100000 iterations, 970 bytes of SYN000-1.p
0.74 seconds total (130.54 MB/s).
100000 iterations, 1281 bytes of SYN000+1.p
1.51 seconds total (84.75 MB/s).
100000 iterations, 2420 bytes of SYN000_1.p
2.94 seconds total (82.37 MB/s).
100000 iterations, 5209 bytes of SYN000=2.p
6.38 seconds total (81.68 MB/s).
$

examples/validate 目前在不到4秒内检查了 458MB 的 CSR002+5.ax。

限制

由于这是递归下降解析，极深嵌套的结构可能导致栈溢出：这在实践中并没有成为问题。解析器仅在工作内存中的字节上工作：这是设计上的选择。如果你想从某处读取数据，请使用 mmap(2)（适用于大文件）或分块读取数据，直到可以解析输入。请参阅 nom 的 流式文档。