我确实下载了现场的适用于 Windows(64 位)的文件 Z3 4.3.0:http: //z3.codeplex.com/releases。
当我尝试运行 bin 文件夹中的文件 z3.exe 时。提示出现并立即消失。我需要知道如何通过 z3.exe 文件运行用 z3 编写的文件。
我怎样才能做到这一点?或者通过 Java 运行 z3 的最佳选择是什么?
我确实下载了现场的适用于 Windows(64 位)的文件 Z3 4.3.0:http: //z3.codeplex.com/releases。
当我尝试运行 bin 文件夹中的文件 z3.exe 时。提示出现并立即消失。我需要知道如何通过 z3.exe 文件运行用 z3 编写的文件。
我怎样才能做到这一点?或者通过 Java 运行 z3 的最佳选择是什么?
z3.exe
是一个命令行工具。要执行名为 的 SMT-LIB 2.0 文件file.smt2
,您应该在命令提示符中执行以下命令。
z3 file.smt2
如果包含的目录z3.exe
不在您的PATH
环境变量中,则必须在上面的命令中包含该目录。
顺便说一句,Z3 没有图形用户界面或环境。它本质上是一个用于自动推理的库。z3.exe
是一个使用这个库构建的简单可执行文件,它允许我们执行存储在文件中的命令。
您还可以使用rise4fun提供的Web 界面来玩Z3 。在rise4fun,我们有一个SMT-LIB前端和一个基于Python的前端。他们都有互动教程。
以下是一些了解 SMT 的有用资源:
[z3]
在搜索框中搜索 Z3 相关问题。Z3 has APIs for several programming languages: C, C++, .Net, Python and OCaml. In the next release, we will also provide support for Java. You can already play with the Java by using one of the nightly builds. Go here for more information about Z3 nightly builds. The nightly builds contain a Java example application using the Z3 API.