2013-06-22 103 views
1

Microsoft Research的Z3 Prover可以使用Visual Studio編譯器和nmake構建。這使得使用Visual Studio進行開發非常合適,我認爲這就是開發人員所做的事情(或者他們實際上是在使用Eclipse還是其他什麼?)。將Z3導入到Visual Studio 2010中

但是,我找不到有關如何將Z3源代碼導入Visual Studio的任何說明。我有VS2010 Ultimate。任何提示點擊什麼?

編輯:我得到了git clone https://git01.codeplex.com/z3的代碼。

回答

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) 
+0

如果你很熟悉代碼,編輯是不錯的,比IDE更不討厭。如果你是新手,並且開始尋找函數聲明,你會很慢。 – Hinton

相關問題