libsmt.rs

SMTLIB2 的 Rust 绑定

libsmt.rs 允许开发者编写并交互符合 SMTLIB2 标准的 SMT 求解器。

当前实现支持 Z3 作为默认求解器，但也可以很容易地与接受 SMTLIB2 格式输入的其他求解器一起使用。

文档

一些文档在此处 http://sushant94.me/libsmt.rs/

文档将逐步编写。这将是最低优先级的任务，直到库稳定和健壮。如果您想使用此库并且需要一些文档，请随时提出问题，我将非常乐意帮助您。

使用示例

使用示例可在 examples/ 中找到

待办事项

当前实现没有暴露 SMT 求解器的全部功能。以下是我们的路线图上的一些项目来完成此库

• 实现以下求解器功能

• 声明-const

• 定义-fun

• 定义-sort

• 声明-sort

• 允许用户向 SMT 求解器传递选项

• 改进类型检查

然而，API 没有暴露的功能还可以通过 raw_read() 和 raw_write() 使用，这两个函数直接暴露了底层求解器。

贡献

最欢迎以建议、问题（尤其是）拉取请求形式的贡献！请遵循 Rust 编码风格，并在提交拉取请求时确保编写测试。

许可证

根据以下之一授权

• Apache 许可证版本 2.0，（LICENSE-APACHE 或 https://apache.ac.cn/licenses/LICENSE-2.0）
• 麻省理工学院许可证（《LICENSE-MIT》或http://opensource.org/licenses/MIT）

由您选择。

贡献说明

除非您明确说明，否则您根据Apache-2.0许可证定义的任何有意提交以包含在作品中的贡献，应按上述方式双重许可，不附加任何额外的条款或条件。