visual studio 20172019 调用Z3实现SMT求解问题

visual studio 2017/2019 调用Z3实现SMT求解问题 visual studio 2017/2019 调用Z3实现SMT求解问题

1. vs2017的安装
   首先是对visual studio2017/2019的安装，点击此处下载相应版本；
   安装形式如下：
   

2. Z3求解器的下载
   其次对Z3进行安装，到此处下载z3_master,如图：
   

3. python3.7的安装及测试，此处不是重点，请参考其他博客

4. Z3的安装
   VS2017版本：
   （1）打开适用于VS2017的x86_x64兼容工具命令提示
   （2）cd打开你z3-master所在目录，输入 python scripts/mk_make.py -x，如果提示有错误，那就是需要复制全部文件路径
   结果如下：
   
   （3）正常情况下，此时会出现包含"build && nmake"的语句，然后输入 cd build，再输入 namke，之后静静的盯着屏幕等一段时间，直到最后屏幕上出现 Z3 was successfully built 就说明你的Z3已经安装成功了：
   
   
   VS2019版本：相比于2017版本：主要差距为VS2019没有适用于VS2019的x86_x64兼容工具命令提示符，这样的话，我们这里要用到适用于VS2019的x86_x64交叉工具命令提示符
   5. VS2017/19配置问题（重点问题）
   (1)安装完后的Z3文件夹中会出现build文件夹，这里面会包含libz3.lib以及libz3.dll文件，也是我们后续会用到的文件。
   (2) 接下来就是用VS2017或者2019新建一个工程，建立完成之后，在该工程中建立 三个文件夹，分别为include、lib、bin。如图：
   
   (3)然后将Z3中src/api、src/api/C++中的相关头文件拷贝到项目文件的include文件夹中，从Z3编译后的文件夹build中，分别将libz3.lib，libz3.dll拷贝到项目文件的lib、bin文件夹中。到这里，准备工作就完成了。
   (4)接下来就是对VS2017中新建的项目属性进行配置，为了避免犯错，请配置所有配置以及所有平台；
   A.首先在项目属性—>VC++目录---->包含目录 中载入项目中include文件夹路径；
   B.在项目属性—>VC++目录—>库目录 中载入项目中lib文件夹路径;
   C.在项目属性—>调试 —>环境 设置 PATH= 项目下bin文件夹路径;
   如图：
   
   

D.将libz3.dll添加到链接器—>输入—>附加依赖项中

E.将项目中的lib路径添加到链接器—>常规—>附加库目录中

全部配置完成后就可以编写程序运行了。