我无法使用 Visual C++ 和 gcc 编译 Z3

Question

我是 Z3 新手，所以我的问题可能太基础了。 但是如果你让我知道我的问题的一些信息，我很高兴。 我在这个网站上搜索过历史。 但我无法获得详细信息。 （因为也许..我的问题太基本了..）

1. [使用 Visual C++] 1）首先，我在codePlex网站下载了“z3 4.3.0 for window”。 但是这个文件没有示例文件（test_capi.c）。 所以我得到了“z3-89c1785b73225a1b363c0e485f854613121b70a7.zip”例如文件。 （我不记得我能得到什么......：（）

   我成功地将 python 文件编译为 codeplex site quide。 但我无法使用 Visual C++ 编译 test_capi.c。 我还在“z3 4.3.0 for window”文件夹中添加了“test_capi.c”，但我也无法编译。

   最后，我刚刚尝试使用“z3-src-4.1.1”的“test_capi.vcxproj”，并且成功了。 看不懂。

   如果我想测试“我的文件”，“z3 4.3.0 for window”需要什么文件？ 或者 我是否必须仅对 Visual c++ 使用“z3 4.1.1”并在“z3 4.1.1”的某个位置添加“我的文件”？ （需要 Z3 4.1.1 的所有文件？？以及 Some 位置是什么？）

   我阅读了其他一些评论 - “Z3 4.3.0”被简化了。 我理解这条评论我只能使用“z3 4.3.0”并成功测试。 但正如我告诉你的，我无法编译。 请给我一些信息..

2. [在 ubuntu 中使用 gcc] 首先，我从 codeplex 站点下载了“z3-4.3.2.07d56bdc705c-x86-ubuntu-12.04.zip”。 因为我尝试了 git 命令来获取源代码，但我找不到源代码。 （我也不知道原因..） 无论如何...“z3-4.3.2.07d56bdc705c-x86-ubuntu-12.04.zip”没有任何示例文件，只有 bin & include 文件夹存在。 所以我也使用了“z3 4.1.1”，但我无法使用下面的命令进行编译。 gcc -fopenmp -o test_capi -I ../../Include -L ../../lib test_capi.c -lz3-gmp

   错误是“找不到 -lz3-gmp。”

   在一些评论中，我发现“使用“sudo install””，但我不知道如何安装 lz3。 （当然只有“sudo install”不起作用，“sudo apt-get install z3”也不起作用......）

   对于使用gcc编译“test_capi.c”，你能详细解释一下吗..？

   我对多种指南感到困惑，但我无法获得基本信息。

   提前谢谢你，我希望能得到信息……即使我的问题太基本了……

Answer 1

首先，您应该只使用一个版本的源代码。 4.1.1 版本非常旧，新版本不再附带 test_capi.vcxproj，而是通过 Makefile 完成所有操作。对于最新版本，请使用unstable 分支（例如，选择unstable here 然后点击下载。）

可以通过调用build 目录中的nmake examples（在Windows 上）或make examples（在Linux 上）来编译示例。 makefile 有一个名为 _ex_c_example 的目标，它显示了如何为 C 示例调用编译器。该目标使用的各种变量在 build/config.mk 中定义。请注意，这些变量在 Windows 和 Linux 上设置为不同的值（此文件由 python scripts/mk_make.py 生成）。

许多 Linux 发行版上的 git 命令与 codeplex git 服务器不兼容（修复请参阅 here），但如果您直接从网页下载源代码，则当然没有必要。