你好,游客 登录 注册 搜索
背景:
阅读新闻

在RedHat6.4上编译z3求解器

[日期:2016-09-10] 来源:cnblogs.com/xiahouye  作者:夏侯爷 [字体: ]

因为项目需要,我们使用到了微软的z3求解器求约束,但是z3求解器在红帽平台上并没有发布编译好的二进制版本,而我们的运行环境是红帽的RedHat企业版6.4,因此需要自己编译相应的二进制。

z3是由微软公司开发的一个优秀的SMT求解器(也就定理证明器),它能够检查逻辑表达式的可满足性。目前的最新版本是4.4.1github主页

z3主页上面下载最新的代码

git clone git@github.com: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公社上的一篇文章http://www.linuxidc.com/Linux/2014-03/98608.htm

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

顺利编译成功,输入测试文件得到了预期的结果。

更多RedHat相关信息见RedHat 专题页面 http://www.linuxidc.com/topicnews.aspx?tid=10

本文永久更新链接地址http://www.linuxidc.com/Linux/2016-09/135081.htm

linux
相关资讯       RedHat6.4编译z3求解器  z3求解器  z3 
本文评论   查看全部评论 (0)
表情: 表情 姓名: 字数

       

评论声明
  • ��重网上道德,遵守中华人民共和国的各项有关法律法规
  • 承担一切因您的行为而直接或间接导致的民事或刑事法律责任
  • 本站管理人员有权保留或删除其管辖留言中的任意内容
  • 本站有权在网站内转载或引用您的评论
  • 参与本评论即表明您已经阅读并接受上述条款