我需要为我的硕士论文研究Z3 SMT求解器。我已经检查了基于 SMT-Lib 输入的 Z3-SMT 教程。但我只能安装需要Python知识的z3-Py。我想知道是否有可能在Mac OSX上使用SMT前端安装z3。如果是，你能帮忙吗？
运行 SMT-LIB 脚本的最简单方法是使用 rise4fun 接口： http://rise4fun.com/Z3
也就是说，您可能需要离线运行Z3来解决大问题或其他程序。 听起来你已经安装了 Z3，因为你有 z3py 工作。 如果你已经成功地安装了 z3py，那么你也可以运行 Z3，因为 z3py 依赖于 Z3（技术上是一个 z3 库，但如果你从 codeplex 获取源代码并编译它，你可能同时安装了库和可执行文件）。 有关所有平台的编译和安装说明，请参阅：https://z3.codeplex.com/SourceControl/latest#README
安装后，您可以使用./z3 -smt2 test.smt在名为test.smt的SMT-LIB2文件上执行z3可执行文件（或者如果您将其放在路径上，则只需z3 -smt2 test.smt）。