1

我想使用 Z3Py，我正在尝试按照http://z3.codeplex.com/SourceControl/changeset/view/89c1785b7322#README中的说明安装 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

当我做 make 我得到错误，例如：

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); }

所以我不知道这是与代码相关的问题还是我仍然遗漏了一些东西。或者，也许，我使用的是非常旧的版本。

谢谢您的回答。

4

1 回答 1

2

我这里没有类似的系统来测试，但我相信这是因为你的系统库使用了类似的东西

#define assert(x) (__builtin_expect...

来定义assert函数。碰巧我们的一个类中的一个函数也被调用assert了，预处理器用#define 的其余部分替换了它。似乎这个问题已经在 Z3 的不稳定分支中得到修复，您可以从Codeplex上的源代码下载中获得，方法是将分支选择器从“master”切换为“unstable”，然后单击下载。

于 2012-12-06T21:35:52.400 回答