0

我第一次使用z3定理证明器，我安装了z3，然后在我的c++程序中包含了z3++.h，但是当我编译时出现以下错误：

/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 回答