編譯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才能像它應該那樣運行。