rsmt2

一个通用的库，用于与运行在独立系统进程中的SMT-LIB 2兼容的求解器交互，例如 z3 和 CVC4。

如果您使用此库，请通过 仓库 与我们联系，以便我们将您的项目添加到readme中。

查看 changes.md 了解变更列表。

特性

• 支持主要求解器（z3、CVC4、Yices 2）
• 所有基本声明/定义/断言/模型/值命令
• check-sat-assuming，具有专门的 actlit API
• 可以通过环境变量传递运行每个求解器的命令，请参阅 conf 模块
• alt-ergo
• get-proof 命令

已知使用 rsmt2 的项目

• kinō，一个转换系统的模型检查器（已废弃）
• hoice，基于机器学习的Horn子句谓词合成器

许可证

MIT/Apache-2.0