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

Question

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

当我使用 4.4.2 com.microsoft.z3.jar 文件时，

JavaExample.java 编译正常。但是，它不会运行因为默认的 libz3java.dll 是 32 位的，而我的环境是 64 位的。我尝试构建一个带有 -x 标志的 64 位 Z3，它的 Makefile 生成器 scripts/mk_make.py 但是当我运行 nmake （发布关于 ).

无论如何，我随后下载了 Z3 4.3.2 版本的二进制文件，其中包含一个 64 位 libz3java.dll。但是，now 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 正常运行之前，您需要解决其他 post 中描述的编译问题。

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

Compile errors for Z3's JavaExample.java test of java bindings

java

z3