1

Microsoft Research 的 Z3 Prover 可以使用 Visual Studio 编译器和nmake. 这将使它很自然地适合使用 Visual Studio 进行开发，我认为这就是开发人员所做的（或者他们实际上是在使用 Eclipse 还是其他什么？）。

但是，我找不到任何有关如何将 Z3 源代码导入 Visual Studio 的说明。我有VS2010 Ultimate。关于点击什么的任何提示？

编辑：我得到了代码git clone https://git01.codeplex.com/z3。

4

1 回答 1

3

我几乎总是使用 nmake 来构建 Z3，因为我在工作中使用老式的编辑器。

您也可以将 Z3 导入 VS。尽管您仍然可以将 VS 的 VS 调试器和性能工具与来自 nmake 的可执行文件一起使用，但它使修复构建错误变得更加容易，并且与调试的集成更加顺畅。

在命令行帮助之后，用于构建 vs 项目的选项称为 -v 或 --vsproj。

C:\z3>scripts\mk_make.py --help
mk_make.py: Z3 Makefile generator

This script generates the Makefile for the Z3 theorem prover.
It must be executed from the Z3 root directory.

Options:
  -h, --help                    display this message.
  -s, --silent                  do not print verbose messages.
  --parallel=num                use cl option /MP with 'num' parallel processes
  -b <sudir>, --build=<subdir>  subdirectory where Z3 will be built 
                                (default: build).
   --githash=hash                include the given hash in the binaries.
  -d, --debug                   compile Z3 in debug mode.
  -t, --trace                   enable tracing in release mode.
  -x, --x64                     create 64 binary when using Visual Studio.
  -m, --makefiles               generate only makefiles.
  -v, --vsproj                  generate Visual Studio Project Files.
  -n, --nodotnet                do not generate Microsoft.Z3.dll make rules.
  -j, --java                    generate Java bindinds.
  --staticlib                   build Z3 static library.

Some influential environment variables:
   JDK_HOME   JDK installation directory (only relevant if -j or --java option is provided)
   JNI_HOME   JNI bindings directory (only relevant if -j or --java option is provided)
于 2013-06-22T16:46:19.270 回答