Z3&的Java绑定的JavaExample.Java测试的编译错误

2022-08-22 00:00:00 z3 java

我正在尝试使用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才能正常运行。

相关文章