1

我想在我的 C++ 程序中使用 z3 API。我想知道要包含哪些头文件以及如何运行包含 z3 函数等的程序。

我看到了example.cppz3 源代码附带的文件，为了运行这个文件，我必须make examples在内部执行命令的 build 目录中运行

g++ -o cpp_example  -I../src/api -I../src/api/c++ 
    ../examples/c++/example.cpp libz3.so -lpthread -fopenmp -lrt

现在，如果我创建任何程序，是否../src/api每次需要编译程序时都需要像这样编译它（包含并链接 lib 文件）？

请帮助我，我以前从未使用过z3。任何帮助是极大的赞赏。:)

4

1 回答 1

6

您问题中的命令行用于 Z3 示例应用程序之一。此命令行在build目录中执行。build 目录包含 Z3 编译库：libz3.so. 该命令可能看起来很复杂，因为它使用单个命令编译和链接应用程序。该指令-I<path-name>指示 g++ 在给定目录中查找包含文件。最后，即使我们没有在系统中安装 Z3 包含文件和库，也可以执行该命令。

要在我们的系统中安装 Z3 包含文件和库，我们应该执行sudo make install. 然后，假设我们创建一个tst.cpp包含

#include<iostream>
#include<z3++.h>
using namespace z3;

int main() {
    context c;
    expr x = c.int_const("x");
    std::cout << x + 1 << "\n";
    return 0;
}

要编译它，我们可以使用：

g++ -c tst.cpp

要链接并生成可执行文件，我们可以使用：

g++ -o tst tst.o -lz3

最后，我们可以执行它

./tst
于 2013-07-08T16:34:03.113 回答