将Z3导入Visual Studio2010

Question

微软研究院的Z3验证程序可以使用Visual Studio编译器和nmake构建。这使得它很适合使用Visual Studio进行开发，我认为这就是开发人员所做的(或者他们实际上是在使用Eclipse还是其他什么？)。

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

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

Answer 1

我几乎总是使用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)