服务器评测
因为项目需要，我们使用到了微软的z3求解器求约束，但是z3求解器在红帽平台上并没有发布编译好的二进制版本，而我们的运行环境是红帽的RedHat企业版6.4，因此需要自己编译相应的二进制。
z3是由微软公司开发的一个优秀的SMT求解器（也就定理证明器），它能够检查逻辑表达式的可满足性。目前的最新版本是4.4.1，github主页。
从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
