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

【问题标题】：z3 solver: z3-SMT on Mac platformz3求解器：Mac平台上的z3-SMT
【发布时间】：2013-11-01 16:29:01
【问题描述】：

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

【问题讨论】：

来自 z3.codeplex.com：“支持的平台：Windows、OSX、Linux 和 FreeBSD”上面说它将在 OSX 上运行。
@Okuma.Scott，我按照网站上的说明进行操作，但得到以下结果：Z3Py 构建成功。因此，据我了解，安装了使用 python 的 z3。我对python一无所知，我想知道是否有任何方法可以使用SMT Lib安装z3。
根据维基百科，SMT-LIB 可以与C/C++, .NET, OCaml, Python, and Java 一起使用。但是http://www.smtlib.org/ 提供的信息非常少。如果维基百科是对的，它看起来很有希望。
Wikipedia 似乎从here 获取信息“也可以通过使用 ANSI C API、.NET 托管公共语言运行时的 API 或 OCaml API 在程序上调用 Z3。”
谢谢你们。我应用了@Taylor 的建议，现在它正在工作。

标签： z3 z3py

【解决方案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）。

【讨论】：