boolector

Boolector SMT求解器的高级安全绑定，版本 3.2.2。

安装

该crate位于 crates.io，因此您可以在您的 Cargo.toml 中将其作为依赖项添加

[dependencies]
boolector = "0.4.3"

此crate依赖于 boolector-sys crate，因此您还需要按照其说明进行安装。具体来说，您可以

• 在您的系统上编译和安装Boolector 3.2.2作为共享库；或
• 在此crate上激活 vendor-lgl 功能，这将自动构建一个静态Boolector并将其链接。例如：

  [dependencies]
  boolector = { version = "0.4.3", features = ["vendor-lgl"] }
  

有关更多详细信息，请参阅 boolector-sys README。

文档

完整文档（包括示例）可在 https://docs.rs/boolector 找到。

注意事项

这些绑定可能并不完整；boolector-sys 中可能存在一些功能在这里没有直接暴露，例如无解释函数（boolector_uf()）。欢迎贡献。

此crate目前需要Rust 1.41+。