Z3 对 java 绑定的 JavaExample.java 测试的编译错误

Question

我正在尝试使用 Z3 的 java 绑定，特别是尝试运行在 Z3 的 4.4.2 版本中分发的 Java 示例 JavaExample.java。

JavaExample.java 在我使用 4.4.2 com.microsoft.z3.jar 文件时编译良好。但是，它不会运行，因为默认的 libz3java.dll 是 32 位的，而我的环境是 64 位的。我尝试为它的 Makefile 制造商scripts/mk_make.py 构建一个带有-x 标志的 64 位 Z3，但是当我运行 nmake 时产生了一个错误（关于 here 的发布）。

无论如何，我随后下载了 Z3 4.3.2 版本的二进制文件，其中包含一个 64 位 libz3java.dll。但是，现在 JavaExample.java 无法编译，会产生大量错误，例如：

FiniteDomainNum cannot be resolved to a type    Z3Example.java  line 2222

换行

FiniteDomainNum s1 = (FiniteDomainNum)ctx.mkNumeral(1, s);

有数百个这样的错误。

jar 文件正确包含在 Eclipse 项目中，就像 JavaExample.java 编译时的 4.4.2 一样。

有什么帮助吗？谢谢。

Answer 1

这些错误可能是由于 com.microsoft.z3.jar 缺失或不完整造成的。您需要理清另一篇文章中描述的编译问题，Java API 才能正常运行。