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

JavaExample.java在我使用4.4.2 com.microsoft.z3.jar文件时编译得很好。但是，它不会运行，因为默认的libz3java.dll是32位，而我的环境是64位。我尝试为其生成文件生成器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版一样。

有什么帮助让这件事继续下去吗？谢谢。

推荐答案

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