需要帮助在c ++程序中使用z3 API

Question

我想在我的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.任何帮助是极大的赞赏.:)

Answer 1

您的问题中的命令行用于其中一个Z3示例应用程序.此命令行在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