Z3求解器在Windows下的安装

发表于 | 分类于

z3（github链接点这里）是由微软公司开发的一个SMT求解器（定理证明器），能够检查逻辑表达式的可满足性。

环境： Visual Studio 2015 Command Prompt

安装准备：

  1. 配置Visual Studio Command Prompt：在Visual Studio的菜单栏中选择 工具-外部工具-添加
    external
    参数为
    标题：mycmd
    命令：C:\Windows\System32\cmd.exe
    参数：/k “D:\VS2015\Common7\Tools\VsDevCmd.bat”
    初始目录：$(ProjectDir)
    mycmd

  2. 打开Visual Studio Command Prompt:电脑的开始-Visual Studio 2015-目录下有各种环境下的命令窗口，这里选择64位的。
    VS
    安装过程：

  3. 打开github上下载的Z3目录：cd F:\z3-master\z3-master
  4. 若Visual Studio为32-bit builds：
    1
    python scripts/mk_make.py

如果是64-bit build:

1
python scripts/mk_make.py -x

  1. cd build

  2. nmake
    若提示“Z3 was successfully built.”就成功了
    success

5.然后按照提示，新建 PYTHONPATH环境变量，将build/python目录添加到其中；并将build添加到path环境变量中。