在 Windows 中安装 Z3

Question

我确实下载了现场的文件 Z3 4.3.0 for Windows（64 位）：http://z3.codeplex.com/releases。

当我尝试运行 bin 文件夹中的 z3.exe 文件时。提示出现并立即消失。我需要知道如何通过 z3.exe 文件运行用 z3 编写的文件。

我该怎么做？或者通过 Java 运行 z3 的最佳选择是什么？

Answer 1

z3.exe 是一个命令行工具。要执行名为 file.smt2 的 SMT-LIB 2.0 文件，您应该在命令提示符中执行以下命令。

 z3 file.smt2

如果包含z3.exe 的目录不在您的PATH 环境变量中，则必须在上述命令中包含该目录。

顺便说一句，Z3 没有图形用户界面或环境。它本质上是一个用于自动推理的库。 z3.exe 是一个使用这个库构建的简单可执行文件，它允许我们执行存储在文件中的命令。

您还可以使用rise4fun 提供的网络界面玩 Z3。 在rise4fun，我们有一个SMT-LIB 前端和一个基于Python 的前端。 他们都有互动教程。

以下是一些了解 SMT 的有用资源：

• Z3 tutorial
• Tutorial on SMT-LIB
• Article describing SMT applications
• SMT-Lib benchmarks
• Stackoverflow：您可以通过在搜索框中包含[z3] 来搜索Z3 相关问题。

Z3 具有适用于多种编程语言的 API：C、C++、.Net、Python 和 OCaml。 在下一个版本中，我们还将提供对 Java 的支持。 您已经可以通过使用其中一个夜间构建来使用 Java。 转至here 以获取有关 Z3 夜间构建的更多信息。 每晚构建包含一个使用 Z3 API 的 Java 示例应用程序。