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

我想在我的C++程序中使用z3 API。我想知道它的头文件，包括如何运行包含Z3的功能等在C++程序中使用z3 API需要帮助

只见example.cpp文件附带了Z3的源代码，为了运行这个文件的程序，我不得不运行在make examples建立在内部执行的命令

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

现在，如果我创建任何程序目录，做我需要编译它像这样（包括../src/api和链接以lib文件）每次我需要编译我的程序的时间？

请帮助我，我从来没有使用z3之前。任何帮助是极大的赞赏。 :)

来源

2013-07-07 user2347029

是的，您每次都需要相同的编译器标志。通常，人们将这些构建规则封装在Makefiles中。 – crowder

@crowder：ohh :(为了使用z3命令，我是否需要拥有所有的子目录和文件z3目录，或者我可以保留其中一些编译文件所需的文件（以及哪些是必需的）？ – user2347029

My猜测是你会发现那些包含相互依赖关系的东西，你将难以辨别或解开。我不知道z3的许可证是什么样的（你应该在分发源代码之前理解这个问题），但是你可能需要整个事情或大部分，建立你的项目，假设你真的使用它彻底。 – crowder

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

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

#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; 
}

要编译文件tst.cpp，我们可以只使用：

g++ -c tst.cpp

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

g++ -o tst tst.o -lz3

最后，我们可以执行它

./tst

来源

2013-07-08 16:34:03

谢谢吨。 :) :)这正是我想要的。再次感谢。 :) :) – user2347029

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

回答

相关问题