歡迎來到Linux教程網
Linux教程網
Linux教程網
Linux教程網
您现在的位置: Linux教程網 >> UnixLinux >  >> Linux綜合 >> 學習Linux

在redhat6.4上編譯z3求解器,redhat6.4z3

在redhat6.4上編譯z3求解器,redhat6.4z3

在redhat6.4上編譯z3求解器,redhat6.4z3


因為項目需要,我們使用到了微軟的z3求解器求約束,但是z3求解器在紅帽平台上並沒有發布編譯好的二進制版本,而我們的運行環境是紅帽的企業版6.4,因此需要自己編譯相應的二進制。

z3是由微軟公司開發的一個優秀的SMT求解器(也就定理證明器),它能夠檢查邏輯表達式的可滿足性。目前的最新版本是4.4.1,github主頁。

從z3主頁上面下載最新的代碼

git clone [email protected]:Z3Prover/z3.git

切換工作目錄到z3下執行

python ./scripts/mk_make.py

報告如下的錯誤

Traceback (most recent call last):
File "./scripts/mk_make.py", line 16, in <module>
update_version()
File "/home/ace/z3/scripts/mk_util.py", line 2614, in update_version
mk_version_dot_h(major, minor, build, revision)
File "/home/ace/z3/scripts/mk_util.py", line 2641, in mk_version_dot_h
'Z3_FULL_VERSION': get_full_version_string(major, minor, build, revision)
File "/home/ace/z3/scripts/mk_util.py", line 3414, in configure_file
print("Generating {} from {}".format(output_file_path, template_file_path))
ValueError: zero length field name in format

這錯誤實在是不好定位,第一個念頭是不是和python版本有關系,當時還不太確定,上谷歌一通搜索,終於在這裡找到了一個貌似有點相關的bugfix。

Fix build error introduced with commit 1c5a57a "glapi/es3.1: Add support
for GLES versions > 3.0" with Python < 2.7.

File "src/mapi/glapi/gen/gl_genexec.py", line 230, in <module>
printer.Print(api)
File "src/mapi/glapi/gen/gl_XML.py", line 120, in Print
self.printBody(api)
File "src/mapi/glapi/gen/gl_genexec.py", line 187, in printBody
condition_parts.append('(ctx->API == API_OPENGLES2 && ctx->Version >= {})'.format(int(f.api_map['es2'] * 10)))
ValueError: zero length field name in format

如此確定應該是和python版本相關,所以著手升級紅帽的python版本,紅帽6.4默認帶的python版本是2.6.6,升級過程參考了linux公社上的一篇文章。

將python升級到2.7.6之後再次運行

python ./scripts/mk_make.py

還是報錯

UnicodeEncodeError: 'ascii' codec can't encode character u'\xa9' in position

不過這次的錯誤比較容易理解,解決方案也比較簡單,在 scripts/mk_util.py文件頭添加

import sys

reload(sys)

sys.setdefaultencoding('utf-8')

指定文件字符集為utf-8。

之後再運行

python scripts/mk_make.py

順利通過編譯配置,然後按照官網上面的指導

cd build

make

sudo make install

順利編譯成功,輸入測試文件得到了預期的結果。

 

 

參考:

https://github.com/Z3Prover/z3

http://code.metager.de/source/history/freedesktop/mesa/mesa/src/mapi/

http://www.linuxidc.com/Linux/2014-03/98608.htm

http://xxx/Linuxjc/1157352.html TechArticle

Copyright © Linux教程網 All Rights Reserved