Rust-SMT-LIB-API

此crate提供与SMT求解器交互的通用高级API。该接口的目标是无解器无关（即用户可以通过修改一行代码来在后端SMT求解器之间切换）并尽可能模仿SMT-LIB标准命令。目前支持Z3作为后端。有关SMT-LIB和Z3的更多信息，请参阅下面的链接。有关如何使用该接口的示例，请参阅tests/test.rs。

安装z3

• Rust-SMT-LIB-API需要Z3的最新夜间构建版本
• 按照Z3网站上的安装说明进行操作（见下文）

构建

• 下载或克隆Rust-SMT-LIB-API
• 切换到Rust-SMT-LIB-API的根目录并运行：cargo test

其他链接

• SMT-LIB标准和文档.
• Z3 SMT求解器.

许可证

Rust-SMT-LIB-API遵循MIT许可证，如LICENSE文件所示。