如何在 C++ 中使用 Z3答案

【问题标题】：How to use Z3 with C++如何在 C++ 中使用 Z3
【发布时间】：2018-08-23 19:52:27
【问题描述】：

我想将 Z3 与 C++ 一起使用，并按照安装指南 - Building Z3 on Windows using Visual Studio Command Prompt。

我构建成功了，然后我还将构建路径添加到系统路径中。但是，当我尝试运行 example.cpp 文件时，仍然出现错误。错误显示[Error] z3++.h: No such file or directory。谁能告诉我，在使用 Visual Studio 命令提示符成功构建 Z3 后，我需要做任何其他配置才能使用 c++ 运行 Z3？

【问题讨论】：

标签： c++ visual-studio z3

【解决方案1】：

您在编译时是否将z3\src\api\c++ 和z3\src\api 路径添加到您的包含目录？

如果您使用的是 Visual Studio 项目，则需要将其添加到“C++”->“其他包含目录”下的项目属性中。

使用cl手动编译时，可以使用/I[path]命令行参数（https://msdn.microsoft.com/en-us/library/73f9s62w.aspx）。

一旦您真正开始在代码中使用z3 API，您还必须将z3.lib 添加到您的编译中，以免收到undefined reference 错误。在 Visual Studio 中，如果您使用库的相对路径，则为“链接器”->“附加依赖项”和可选的“附加库目录”。

在我的环境中，以下命令行会编译您的示例程序：cl example.cpp /I C:\tools\z3\z3-master\src\api\c++ /I C:\tools\z3\z3-master\src\api C:\tools\z3\z3-master\build\libz3.lib

【讨论】：

谢谢，我解决了 z3++.h 的“没有这样的文件或目录”问题。但是我在添加libz3.lib后仍然有很多LIN2019错误。你知道是什么问题吗？
我首先将“C:\z3-master\build”添加到“附加库目录”，然后将“libz3.lib”添加到“附加依赖项”。但它仍然有很多 LNK2019 错误。
如果 Visual Studio 没有抱怨找不到您指定的库文件而是显示unresolved external symbol 错误，这可能意味着该 DLL 是使用与配置不同的平台设置编译的在你的项目中。您是否使用“x64 Native Tools”Visual Studio 命令提示符编译了 Z3？如果是这样，您需要确保您的项目构建在配置管理器中配置为“x64”：msdn.microsoft.com/en-us/library/9yb4317s.aspx