z3(github链接点这里)是由微软公司开发的一个SMT求解器(定理证明器),能够检查逻辑表达式的可满足性。
环境: Visual Studio 2015 Command Prompt
安装准备:
配置Visual Studio Command Prompt:在Visual Studio的菜单栏中选择 工具-外部工具-添加
参数为
标题:mycmd
命令:C:\Windows\System32\cmd.exe
参数:/k “D:\VS2015\Common7\Tools\VsDevCmd.bat”
初始目录:$(ProjectDir)打开Visual Studio Command Prompt:电脑的开始-Visual Studio 2015-目录下有各种环境下的命令窗口,这里选择64位的。
安装过程:- 打开github上下载的Z3目录:cd F:\z3-master\z3-master
- 若Visual Studio为32-bit builds:
1
python scripts/mk_make.py
如果是64-bit build:1
python scripts/mk_make.py -x
cd build
nmake
若提示“Z3 was successfully built.”就成功了
5.然后按照提示,新建 PYTHONPATH环境变量,将build/python目录添加到其中;并将build添加到path环境变量中。