Импорт Z3 в Visual Studio 2010
Z3 Prover от Microsoft Research может быть построен с использованием компиляторов Visual Studio и nmake
, Это сделало бы его естественным подходом для разработки с использованием Visual Studio, и я предполагаю, что это то, что делают разработчики (или они на самом деле используют Eclipse или что-то еще?).
Однако я не смог найти никаких инструкций о том, как импортировать исходный код Z3 в Visual Studio. У меня есть VS2010 Ultimate. Любые подсказки на что нажать?
РЕДАКТИРОВАТЬ: я получил код git clone https://git01.codeplex.com/z3
,
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)