| 名称 | smt-solver-interface |
| 描述 | 用于验证和综合的SMT求解器接口 allowed-tools: - Bash - Read - Write - Edit - Glob - Grep metadata: specialization: 计算机科学 domain: 科学 category: 形式化验证 phase: 6 |
SMT求解器接口
目的
为使用SMT求解器进行自动推理、验证和程序综合提供专家指导。
能力
- Z3查询生成
- CVC5接口
- 理论选择指导
- 模型提取
- 不可满足核心分析
- 增量求解
使用指南
- 编码: 以SMT-LIB格式编码问题
- 理论选择: 选择合适的理论
- 求解: 运行SMT求解器
- 模型提取: 提取满足赋值
- 调试: 分析不可满足核心进行调试
工具/库
- Z3
- CVC5
- Boolector
- Yices