z3 - z3求解器：Mac平台上的z3-SMT

Question

我需要为我的硕士论文研究 Z3 SMT 求解器。我已经查看了基于 SMT-Lib 输入的 Z3-SMT 教程。但我只能安装需要 Python 知识的 z3-Py。我想知道是否有可能在 Mac OSX 上使用 SMT 前端安装 z3。如果是，你能帮忙吗？

Answer 1

运行 SMT-LIB 脚本最简单的方法是使用rise4fun 接口：http ://rise4fun.com/Z3

也就是说，您可能需要离线运行 Z3 以解决大问题或在其他程序中。听起来你已经安装了 Z3，因为你有 z3py 工作。如果您已成功安装 z3py，那么您也可以运行 Z3，因为 z3py 依赖于 Z3（技术上是一个 z3 库，但如果您从 codeplex 获取源代码并编译它，您可能已经安装了库和可执行文件）。有关所有平台的编译和安装说明，请参见：https ://z3.codeplex.com/SourceControl/latest#README

安装后，您可以在名为 test.smt 的 SMT-LIB2 文件上执行 z3 可执行文件，使用./z3 -smt2 test.smt（或者只是z3 -smt2 test.smt将其放在路径上）。