编译Z3的JavaExample.java测试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); 

有数百个这样的错误的。

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

任何帮助，让这个去？谢谢。

Answer 1

这些错误可能是由于com.microsoft.z3.jar丢失或不完整的缘故。您需要先解决在其他帖子中描述的编译问题，然后Java API才能像它应该那样运行。