本文介紹了Z3&；的Java綁定的JavaExample.Java測(cè)試的編譯錯(cuò)誤的處理方法，對(duì)大家解決問(wèn)題具有一定的參考價(jià)值，需要的朋友們下面隨著小編來(lái)一起學(xué)習(xí)吧！
問(wèn)題描述
我正在嘗試使用Z3的Java綁定，特別是嘗試運(yùn)行Z3的4.4.2版本中分發(fā)的Java示例JavaExample.java。
JavaExample.java在我使用4.4.2 com.microsoft.z3.jar文件時(shí)編譯得很好。但是，它不會(huì)運(yùn)行，因?yàn)槟J(rèn)的libz3java.dll是32位，而我的環(huán)境是64位。我嘗試為其生成文件生成器scripts/mk_make.py構(gòu)建一個(gè)帶有-x標(biāo)志的64位Z3，但在運(yùn)行nmake(發(fā)布關(guān)于here)時(shí)出錯(cuò)。
不管怎樣，我下載了Z3 4.3.2版本的二進(jìn)制文件，它包含一個(gè)64位的libz3java.dll。但是，現(xiàn)在JavaExample.java無(wú)法編譯，從而生成大量錯(cuò)誤，如：
FiniteDomainNum cannot be resolved to a type Z3Example.java line 2222
行
FiniteDomainNum s1 = (FiniteDomainNum)ctx.mkNumeral(1, s);
有數(shù)百個(gè)這樣的錯(cuò)誤。
JAR文件正確地包含在Eclipse項(xiàng)目中，就像編譯JavaExample.java時(shí)的4.4.2版一樣。
有什么幫助讓這件事繼續(xù)下去嗎？謝謝。
推薦答案
這些錯(cuò)誤可能是由于com.microsoft.z3.jar缺失或不完整造成的。您需要解決另一篇文章中描述的編譯問(wèn)題，然后Java API才能正常運(yùn)行。
這篇關(guān)于Z3&；的Java綁定的JavaExample.Java測(cè)試的編譯錯(cuò)誤的文章就介紹到這了，希望我們推薦的答案對(duì)大家有所幫助，
