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ます。私たちのクラスの 1 つの関数の 1 つが呼び出さassertれ、プリプロセッサがそれを #define の残りの部分に置き換えます。この問題は、 Codeplexのソース コード ダウンロードから入手できる Z3 の不安定版ブランチでは、[ダウンロード] をクリックする前にブランチ セレクタを「マスター」から「不安定版」に切り替えることで、既に修正されているようです。

于 2012-12-06T21:35:52.400 に答える