IPASIR 对 Rust 的接口

文档	Crates.io

是什么

IPASIR 是一个简单的 C 接口，用于增量 SAT 求解器。（它代表可重入增量 SAT 求解器 API，反向书写。）这个接口由几个不同的求解器支持，因为它用于 SAT 竞赛的增量赛道。包含接口和一些示例求解器的 IPASIR 发行版可以在这个 GitHub 仓库中找到。这个 IPASIR 库是尝试半合理地允许 Rust 程序与这样的 SAT 求解器库进行接口的尝试。

FFI 结构

对于此 FFI 的用户，有两种不同的使用方式。用户可以在提供直接但不安全的 C-API 调用的 raw 模块之上构建他们的应用程序。推荐使用 Solver 类型来使用此 FFI，该类型作为 C-API 的安全包装器。

使用 ipasir::Solver::init() 分配一个新的求解器实例

许可证

根据您选择，许可方式如下：

• Apache 许可证，版本 2.0，(LICENSE-APACHE 或 https://apache.ac.cn/licenses/LICENSE-2.0)
• MIT 许可证 (LICENSE-MIT 或 http://opensource.org/licenses/MIT)

任选其一。

双许可：

贡献

除非您明确说明，否则任何有意提交以包含在您的工作中的贡献，根据 Apache-2.0 许可证的定义，应如上所述双许可，不附加任何其他条款或条件。

发布说明

0.3.1 - 2020 年 4 月 12 日

• 实现 crate 的错误类型 Error 和 Display。

0.3.0 - 2019年4月10日

• 主要的 API 重构
• ipasir::ffi::Solver 现在是 Rust 的 FFI C 目标求解器包装器。
• IpasirSolver 是 Rust IPASIR 兼容求解器需要实现的特质。

0.2.0 - 2018年4月25日

• 将 raw 模块重命名为 sys，以更好地与其他生态系统兼容。
• Lit::to_raw 现在不再公开可见。
• 移除了 LitOrEnd 和 EndOfClause。
• 将 Solver::add API 分割为 Solver::add_lit 和 Solver::finalize_clause。
• 添加了 Clause::len 和 Clause::get 方法。
• 添加了 Lit::new_unchecked 构造函数。
• 添加了 Lit::sign 和 Sign 枚举。
• 添加了 Lit::var 方法。
• 将 SolveControl 现在设置为公开可见。（之前意外设置为私有。）

0.1.0 - 2018年4月24日

• 初始发布