0

初めて z3 定理証明器を使用しています。z3 をインストールしてから、z3++.h を C++ プログラムに含めましたが、コンパイルすると次のエラーが発生します。

/tmp/ccVlHDDf.o: In function `z3::context::check_error() const':
engine.cpp:(.text._ZNK2z37context11check_errorEv[z3::context::check_error() const]+0x11): undefined reference to `Z3_get_error_code'
engine.cpp:(.text._ZNK2z37context11check_errorEv[z3::context::check_error() const]+0x3c): undefined reference to `Z3_get_error_msg_ex'
/tmp/ccVlHDDf.o: In function `z3::ast::ast(z3::context&, _Z3_ast*)':
engine.cpp:(.text._ZN2z33astC2ERNS_7contextEP7_Z3_ast[_ZN2z33astC5ERNS_7contextEP7_Z3_ast]+0x43): undefined reference to `Z3_inc_ref'
/tmp/ccVlHDDf.o: In function `z3::cast_ast<z3::expr>::operator()(z3::context&, _Z3_ast*)':

含まれている他のファイルをチェックして、これらが定義され、見つかったかどうかを確認しました

Z3_error_code Z3_API Z3_get_error_code(__in Z3_context c);

z3_api.h で。しかし、それが呼び出されたのか、関数が宣言されたのかはわかりません。誰か助けてくれませんか。

4

1 に答える 1

2

これはリンク エラーです。使用しているコマンドラインは何ですか? システムに Z3 インクルード ファイルとライブラリをインストールした場合は、-lz3アプリケーションをリンクするときにオプションを含める必要があります。Z3 ライブラリが標準のディレクトリにない場合は、-L<path-to-Z3-library>.

于 2013-07-08T17:10:20.000 に答える