使用鐺 - 2.9與OS X 10.5.8編譯Z3

我想用Z3Py，我試圖安裝Z3按照http://z3.codeplex.com/SourceControl/changeset/view/89c1785b7322#README 我獲得以下的說明：使用鐺 - 2.9與OS X 10.5.8編譯Z3

dhcp-154:z3-89c1785b7322 mgarcia$ ./configure CXX=clang++ 
checking whether we are using the GNU C++ compiler... no 
checking whether clang++ accepts -g... no 
checking for gcc... gcc 
checking whether we are using the GNU C compiler... no 
checking whether gcc accepts -g... no 
checking for gcc option to accept ISO C89... unsupported 
checking whether make sets $(MAKE)... yes 
checking for grep that handles long lines and -e... /usr/bin/grep 
checking for a sed that does not truncate output... /usr/bin/sed 
checking for int *... no 
checking size of int *... 4 
configure: creating ./config.status 
config.status: creating scripts/config-debug.mk 
config.status: creating scripts/config-release.mk 
Z3 was configured with success. 
Host platform: osx 
Compiler:  clang++ 
Arithmetic:  internal 
Python:   python 
Prefix:   /usr 
64-bit:   no

當我做的化妝，我得到錯誤，例如：

In file included from ../src/muz_qe/dl_smt_relation.cpp:32: 
../src/smt/expr_context_simplifier.h:78:10: error: expected parameter declarator 
    void assert(expr* e) { m_solver.assert_expr(e); } 

/usr/include/assert.h:85:23: note: instantiated from: 
    (__builtin_expect(!(e), 0) ? __assert_rtn(__func__, __FILE__, __LINE__, #e) : (void)0) 

In file included from ../src/muz_qe/dl_smt_relation.cpp:32: 
../src/smt/expr_context_simplifier.h:78:10: error: expected ')' 
../src/smt/expr_context_simplifier.h:78:10: note: to match this '(' 
    void assert(expr* e) { m_solver.assert_expr(e); }

所以我不知道這是不是與代碼相關的問題，或者我還是失去了一些東西。或者，也許，我正在使用真正的舊版本。

謝謝你的回答。

來源

2012-12-05 Mairim

我沒有一個類似的系統在這裏進行測試，但我相信這是因爲你的系統庫使用類似

#define assert(x) (__builtin_expect...

定義assert功能。發生在我們其中一個類中的函數之一也被稱爲assert，並且預處理器將其替換爲#define的其餘部分。看來這個問題已經在Z3的不穩定分支中解決了，你可以從Codeplex上的源代碼下載得到，在點擊下載之前將分支選擇器從「主」切換到「不穩定」。

來源

2012-12-06 21:35:52

謝謝，我終於意識到我的C編譯器並沒有創建可執行文件，現在我遇到了一些新問題'dhcp-154：build mgarcia $ make src/shell/datalog_frontend.cpp cc1plus：error：無法識別的命令行選項「-fopenmp」 make：*** [shell/datalog_frontend.o] Error 1'所以我想我需要安裝別的東西。 – Mairim

-fopenmp指許多現代編譯器支持的OpenMP編譯器擴展和庫。據我所知，clang ++不支持它，而Z3配置腳本應該禁用它。腳本（python scripts/mk_make.py）有可能無法識別clang ++，或者傳遞了不正確的選項。您可以通過檢查腳本的輸出來驗證。 –

另外，我剛剛發現mac上的舊版本gcc可能不支持OpenMP。如果你從clang切換到gcc，你能告訴我們'gcc --version'說什麼嗎？ –

使用鐺 - 2.9與OS X 10.5.8編譯Z3

回答

相關問題